theory-theorem-index.md

SHA-256 1c1acc37f572da7293c006ca0cadade99e9eb738471d7cba33a3662be3e86997 · download the original

# Theorem index

These are the exact checked declaration locations. Read each signature for assumptions.

## SentinelProofs.lean

- [clip_bounds](../lean/SentinelProofs.lean#L17)
- [blend_bounds](../lean/SentinelProofs.lean#L24)
- [coefficient_bounds](../lean/SentinelProofs.lean#L38)
- [step_bounds](../lean/SentinelProofs.lean#L49)
- [trajectory_bounds](../lean/SentinelProofs.lean#L58)
- [weight_nonnegative](../lean/SentinelProofs.lean#L69)
- [weight_sum_bound](../lean/SentinelProofs.lean#L75)
- [weight_sum_below_one](../lean/SentinelProofs.lean#L84)

## Dynamics.lean

- [event_dependent_rates_bounded](../lean/SentinelTheory/Dynamics.lean#L15)
- [trace_matches_clipped_update](../lean/SentinelTheory/Dynamics.lean#L25)
- [trace_zero_time](../lean/SentinelTheory/Dynamics.lean#L31)
- [trace_time_subdivision](../lean/SentinelTheory/Dynamics.lean#L34)
- [future_change_telescopes](../lean/SentinelTheory/Dynamics.lean#L41)
- [future_probability_difference_bounds](../lean/SentinelTheory/Dynamics.lean#L44)
- [exponential_width_monotone](../lean/SentinelTheory/Dynamics.lean#L48)
- [normalized_square_monotone](../lean/SentinelTheory/Dynamics.lean#L54)
- [ellipse_expansion_contains_old](../lean/SentinelTheory/Dynamics.lean#L62)
- [branch_union_preserves_old](../lean/SentinelTheory/Dynamics.lean#L70)
- [path_product_bounds](../lean/SentinelTheory/Dynamics.lean#L78)
- [strongest_route_can_lose_mass](../lean/SentinelTheory/Dynamics.lean#L84)
- [path_mass_geometric_bound](../lean/SentinelTheory/Dynamics.lean#L91)
- [dominated_path_series_summable](../lean/SentinelTheory/Dynamics.lean#L109)
- [geometric_tail_exact](../lean/SentinelTheory/Dynamics.lean#L114)
- [dominated_path_tail_bound](../lean/SentinelTheory/Dynamics.lean#L120)
- [euler_phase_identity](../lean/SentinelTheory/Dynamics.lean#L134)
- [phase_has_unit_norm](../lean/SentinelTheory/Dynamics.lean#L138)
- [phase_composition](../lean/SentinelTheory/Dynamics.lean#L141)

## Information.lean

- [xor_conditional_entropy_exact](../lean/SentinelTheory/Information.lean#L21)
- [xor_joint_information_exact](../lean/SentinelTheory/Information.lean#L30)
- [xor_single_information_zero](../lean/SentinelTheory/Information.lean#L40)
- [xor_joint_information_positive](../lean/SentinelTheory/Information.lean#L46)
- [noiseless_xor_one_bit](../lean/SentinelTheory/Information.lean#L54)
- [independent_noise_zero_information](../lean/SentinelTheory/Information.lean#L58)

## Latest.lean

- [interest_ceiling](../lean/SentinelTheory/Latest.lean#L11)
- [interest_zero_relevance](../lean/SentinelTheory/Latest.lean#L19)
- [interest_increases_with_exposure](../lean/SentinelTheory/Latest.lean#L22)
- [hard_constraint_zero_activation](../lean/SentinelTheory/Latest.lean#L32)
- [unresolved_keeps_allowance](../lean/SentinelTheory/Latest.lean#L35)
- [positive_exploration_can_activate](../lean/SentinelTheory/Latest.lean#L40)
- [uniform_second_moment](../lean/SentinelTheory/Latest.lean#L52)
- [uniform_fourth_moment](../lean/SentinelTheory/Latest.lean#L55)
- [orthogonal_cubic_zero_linear_moment](../lean/SentinelTheory/Latest.lean#L58)
- [cubic_from_intermediate_multiplication](../lean/SentinelTheory/Latest.lean#L63)
- [corroboration_false_positive_bound](../lean/SentinelTheory/Latest.lean#L65)
- [confirming_alerts_are_subset](../lean/SentinelTheory/Latest.lean#L69)

## Learning.lean

- [noisy_xor_single_feature_blind](../lean/SentinelTheory/Learning.lean#L13)
- [noisy_xor_other_feature_blind](../lean/SentinelTheory/Learning.lean#L17)
- [noisy_xor_output_fair](../lean/SentinelTheory/Learning.lean#L21)
- [noisy_xor_joint_is_informative](../lean/SentinelTheory/Learning.lean#L26)
- [noisy_xor_mass_nonnegative](../lean/SentinelTheory/Learning.lean#L29)
- [noisy_xor_mass_normalized](../lean/SentinelTheory/Learning.lean#L36)
- [xor_is_linear_over_two](../lean/SentinelTheory/Learning.lean#L41)
- [independent_clean_sample_mass](../lean/SentinelTheory/Learning.lean#L46)
- [two_step_path_composition](../lean/SentinelTheory/Learning.lean#L49)
- [inverse_certifies_unique_linear_solution](../lean/SentinelTheory/Learning.lean#L53)
- [disjunction_from_and_not](../lean/SentinelTheory/Learning.lean#L74)
- [expression_renaming_preserves_meaning](../lean/SentinelTheory/Learning.lean#L85)
- [finite_boolean_function_expressible](../lean/SentinelTheory/Learning.lean#L93)
- [boolean_function_count](../lean/SentinelTheory/Learning.lean#L120)
- [three_bit_function_count](../lean/SentinelTheory/Learning.lean#L123)
- [macro_substitution_preserves_meaning](../lean/SentinelTheory/Learning.lean#L133)
- [language_growth_preserves_known](../lean/SentinelTheory/Learning.lean#L142)
- [finite_expression_in_limit](../lean/SentinelTheory/Learning.lean#L145)

## Pathways.lean

- [pathway_operator_norm_bound](../lean/SentinelTheory/Pathways.lean#L10)
- [pathway_matrix_series_inverse](../lean/SentinelTheory/Pathways.lean#L27)
- [pathway_matrix_series_summable](../lean/SentinelTheory/Pathways.lean#L35)
- [pathway_matrix_tail_bound](../lean/SentinelTheory/Pathways.lean#L42)

## Probability.lean

- [empirical_update_identity](../lean/SentinelTheory/Probability.lean#L9)
- [empirical_update_bounds](../lean/SentinelTheory/Probability.lean#L17)
- [beta_mean_strict_bounds](../lean/SentinelTheory/Probability.lean#L26)
- [beta_variance_expression_nonnegative](../lean/SentinelTheory/Probability.lean#L35)
- [uniform_beta_unknown](../lean/SentinelTheory/Probability.lean#L41)
- [missing_evidence_unchanged](../lean/SentinelTheory/Probability.lean#L50)
- [posterior_nonnegative](../lean/SentinelTheory/Probability.lean#L55)
- [posterior_normalized](../lean/SentinelTheory/Probability.lean#L61)
- [zero_prior_stays_zero](../lean/SentinelTheory/Probability.lean#L66)
- [posterior_uninformative](../lean/SentinelTheory/Probability.lean#L70)
- [mixture_bounds](../lean/SentinelTheory/Probability.lean#L74)
- [markov_mixture_normalized](../lean/SentinelTheory/Probability.lean#L87)
- [charger_example](../lean/SentinelTheory/Probability.lean#L99)
- [propagated_battery_example](../lean/SentinelTheory/Probability.lean#L103)
- [propagated_task_example](../lean/SentinelTheory/Probability.lean#L106)

## Signals.lean

- [fourier_delay_phase](../lean/SentinelTheory/Signals.lean#L10)
- [fourier_gain_and_delay](../lean/SentinelTheory/Signals.lean#L18)
- [cross_spectrum_factorization](../lean/SentinelTheory/Signals.lean#L29)
- [forced_trace_initial_value](../lean/SentinelTheory/Signals.lean#L38)
- [forced_trace_convolution](../lean/SentinelTheory/Signals.lean#L47)
- [forced_trace_solves_relaxation](../lean/SentinelTheory/Signals.lean#L59)

## Structure.lean

- [feasibility_monotone](../lean/SentinelTheory/Structure.lean#L10)
- [adding_resources_preserves_feasibility](../lean/SentinelTheory/Structure.lean#L15)
- [indicator_bounds](../lean/SentinelTheory/Structure.lean#L26)
- [indicator_monotone](../lean/SentinelTheory/Structure.lean#L30)
- [feasibility_gain_bounds](../lean/SentinelTheory/Structure.lean#L37)
- [product_unit_bounds](../lean/SentinelTheory/Structure.lean#L46)
- [opportunity_relevance_bounds](../lean/SentinelTheory/Structure.lean#L54)
- [alternative_routes_monotone](../lean/SentinelTheory/Structure.lean#L62)
- [new_route_preserves_possibilities](../lean/SentinelTheory/Structure.lean#L67)
- [missing_requirements_shrink](../lean/SentinelTheory/Structure.lean#L72)
- [failure_of_one_route_allows_another](../lean/SentinelTheory/Structure.lean#L77)
- [action_does_not_identify_preference](../lean/SentinelTheory/Structure.lean#L80)
- [identical_observations_cannot_decode_distinct_targets](../lean/SentinelTheory/Structure.lean#L87)
- [refinement_preserves_old_representation](../lean/SentinelTheory/Structure.lean#L98)
- [refinement_separates_distinctions](../lean/SentinelTheory/Structure.lean#L101)
- [fixed_representation_cannot_predict_different_futures](../lean/SentinelTheory/Structure.lean#L107)
- [unknown_zero_gate_blocks_activity](../lean/SentinelTheory/Structure.lean#L113)
- [net_gain_positive_iff](../lean/SentinelTheory/Structure.lean#L115)
- [uniform_coverage_budget](../lean/SentinelTheory/Structure.lean#L119)
- [information_can_be_ignored](../lean/SentinelTheory/Structure.lean#L126)

## Evidence.lean

- [evidence_xor_explanations_ambiguous](../lean/SentinelTheory/Evidence.lean#L15)
- [evidence_common_flip_invariant](../lean/SentinelTheory/Evidence.lean#L19)
- [evidence_observations_cannot_decode_h](../lean/SentinelTheory/Evidence.lean#L23)
- [evidence_correction_recovers](../lean/SentinelTheory/Evidence.lean#L27)
- [evidence_same_group_disagreement_cancels](../lean/SentinelTheory/Evidence.lean#L31)
- [evidence_cross_group_disagreement](../lean/SentinelTheory/Evidence.lean#L35)
- [evidence_majority_flip_equivariant](../lean/SentinelTheory/Evidence.lean#L41)
- [evidence_majority_ignores_one_fault](../lean/SentinelTheory/Evidence.lean#L45)
- [evidence_majority_follows_common_fault](../lean/SentinelTheory/Evidence.lean#L49)
- [evidence_bias_shift_unidentifiable](../lean/SentinelTheory/Evidence.lean#L53)
- [evidence_posterior_odds](../lean/SentinelTheory/Evidence.lean#L56)
- [evidence_log_ratios_add](../lean/SentinelTheory/Evidence.lean#L67)
- [evidence_duplicate_overcounts](../lean/SentinelTheory/Evidence.lean#L73)
- [evidence_cusum_nonneg](../lean/SentinelTheory/Evidence.lean#L79)
- [evidence_cusum_dominates](../lean/SentinelTheory/Evidence.lean#L82)
- [evidence_cusum_monotone](../lean/SentinelTheory/Evidence.lean#L85)
- [evidence_cusum_resets](../lean/SentinelTheory/Evidence.lean#L89)
- [evidence_cusum_growth_bound](../lean/SentinelTheory/Evidence.lean#L92)
- [evidence_value_of_information_nonneg](../lean/SentinelTheory/Evidence.lean#L96)
- [evidence_no_value_when_decision_fixed](../lean/SentinelTheory/Evidence.lean#L101)
- [evidence_smoothed_table_normalized](../lean/SentinelTheory/Evidence.lean#L108)
- [evidence_smoothed_table_positive](../lean/SentinelTheory/Evidence.lean#L114)
- [evidence_chain_rule](../lean/SentinelTheory/Evidence.lean#L118)
- [evidence_disagreement_bounds](../lean/SentinelTheory/Evidence.lean#L126)
- [evidence_disagreement_symm](../lean/SentinelTheory/Evidence.lean#L134)
- [evidence_disagreement_self](../lean/SentinelTheory/Evidence.lean#L141)
- [evidence_disagreement_triangle](../lean/SentinelTheory/Evidence.lean#L144)

## Timing.lean

- [timing_clock_compose](../lean/SentinelTheory/Timing.lean#L13)
- [timing_clock_inverse](../lean/SentinelTheory/Timing.lean#L17)
- [timing_offset_latency_not_identifiable](../lean/SentinelTheory/Timing.lean#L23)
- [timing_clock_error_bound](../lean/SentinelTheory/Timing.lean#L26)
- [timing_periodic_shift_indistinguishable](../lean/SentinelTheory/Timing.lean#L37)
- [timing_decay_semigroup](../lean/SentinelTheory/Timing.lean#L41)
- [timing_decay_bounded_between_updates](../lean/SentinelTheory/Timing.lean#L45)
- [timing_wake_time_hits_threshold](../lean/SentinelTheory/Timing.lean#L52)
- [timing_wake_time_nonneg](../lean/SentinelTheory/Timing.lean#L65)
- [timing_value_of_computation_nonneg](../lean/SentinelTheory/Timing.lean#L77)
- [timing_compute_only_if_gain_exceeds_cost](../lean/SentinelTheory/Timing.lean#L87)
- [timing_budget_active_count_bound](../lean/SentinelTheory/Timing.lean#L90)
- [timing_budget_subset_feasible](../lean/SentinelTheory/Timing.lean#L98)
- [timing_budget_shrink_drops_member](../lean/SentinelTheory/Timing.lean#L102)
- [timing_beta_estimate_open_unit](../lean/SentinelTheory/Timing.lean#L108)
- [timing_beta_estimate_monotone_in_successes](../lean/SentinelTheory/Timing.lean#L114)
- [timing_suspend_discount_le](../lean/SentinelTheory/Timing.lean#L120)
- [timing_compression_pigeonhole](../lean/SentinelTheory/Timing.lean#L127)
- [timing_compression_not_injective](../lean/SentinelTheory/Timing.lean#L133)
- [timing_inspect_budget_success_bound](../lean/SentinelTheory/Timing.lean#L138)
- [timing_effective_sample_size_bounds](../lean/SentinelTheory/Timing.lean#L143)
- [timing_effective_sample_size_independent](../lean/SentinelTheory/Timing.lean#L150)
- [timing_effective_sample_size_decreasing](../lean/SentinelTheory/Timing.lean#L153)

## Values.lean

- [value_tentative_threshold](../lean/SentinelTheory/Values.lean#L14)
- [value_tentative_monotone](../lean/SentinelTheory/Values.lean#L19)
- [value_interrupt_rule_monotone](../lean/SentinelTheory/Values.lean#L27)
- [value_optimal_with_silence_nonneg](../lean/SentinelTheory/Values.lean#L30)
- [value_unconstrained_threshold_optimal](../lean/SentinelTheory/Values.lean#L36)
- [value_gated_budget_value_bound](../lean/SentinelTheory/Values.lean#L47)
- [value_silent_history_hides_sign](../lean/SentinelTheory/Values.lean#L63)
- [value_selective_feedback_bias](../lean/SentinelTheory/Values.lean#L74)
- [value_joint_survival_factorization](../lean/SentinelTheory/Values.lean#L89)
- [value_exponential_survival_bounds](../lean/SentinelTheory/Values.lean#L95)
- [value_survival_decreases_with_delay](../lean/SentinelTheory/Values.lean#L99)
- [value_waiting_cannot_raise_utility](../lean/SentinelTheory/Values.lean#L109)
- [value_verification_posterior_bounds](../lean/SentinelTheory/Values.lean#L117)
- [value_verification_posterior_vs_prior](../lean/SentinelTheory/Values.lean#L123)
- [value_verification_posterior_mean](../lean/SentinelTheory/Values.lean#L129)
- [value_two_outcome_option_value](../lean/SentinelTheory/Values.lean#L140)
- [value_verification_never_worse_before_cost](../lean/SentinelTheory/Values.lean#L146)
- [value_filter_step_normalized](../lean/SentinelTheory/Values.lean#L172)
- [value_rotation_nonidentifiable](../lean/SentinelTheory/Values.lean#L192)
- [value_flip_nonidentifiable](../lean/SentinelTheory/Values.lean#L197)
- [value_alignment_candidate_count](../lean/SentinelTheory/Values.lean#L201)
- [value_blocked_action_value_survives](../lean/SentinelTheory/Values.lean#L205)
- [value_equal_likelihood_posterior_is_prior](../lean/SentinelTheory/Values.lean#L214)
- [value_pursuit_switch_deviation](../lean/SentinelTheory/Values.lean#L220)
- [value_pursuit_switch_contracts](../lean/SentinelTheory/Values.lean#L223)
- [value_pursuit_switch_iterate](../lean/SentinelTheory/Values.lean#L233)
- [value_pursuit_drifts_to_uncertainty](../lean/SentinelTheory/Values.lean#L241)
- [value_shrinkage_between](../lean/SentinelTheory/Values.lean#L251)
- [value_policy_permission_gate](../lean/SentinelTheory/Values.lean#L264)
- [value_policy_normalized](../lean/SentinelTheory/Values.lean#L270)

## Language.lean

- [language_silence_is_an_option](../lean/SentinelTheory/Language.lean#L13)
- [language_adding_option_never_lowers](../lean/SentinelTheory/Language.lean#L18)
- [language_silence_wins_when_all_negative](../lean/SentinelTheory/Language.lean#L27)
- [language_budgeted_selection_silence](../lean/SentinelTheory/Language.lean#L40)
- [language_value_of_information_nonneg](../lean/SentinelTheory/Language.lean#L44)
- [language_value_of_information_nonneg_joint](../lean/SentinelTheory/Language.lean#L51)
- [language_value_of_information_zero_of_constant_best](../lean/SentinelTheory/Language.lean#L62)
- [language_mismatch_complement](../lean/SentinelTheory/Language.lean#L72)
- [language_independent_mismatch_bounds](../lean/SentinelTheory/Language.lean#L83)
- [language_brier_bounds](../lean/SentinelTheory/Language.lean#L97)
- [language_mean_brier_bounds](../lean/SentinelTheory/Language.lean#L103)
- [language_constant_forecast_decomposition](../lean/SentinelTheory/Language.lean#L115)
- [language_base_rate_brier_at_most_quarter](../lean/SentinelTheory/Language.lean#L120)
- [language_half_forecast_brier](../lean/SentinelTheory/Language.lean#L123)
- [language_identical_inputs_brier_floor](../lean/SentinelTheory/Language.lean#L127)
- [language_expression_count](../lean/SentinelTheory/Language.lean#L132)
- [language_novel_combination_count](../lean/SentinelTheory/Language.lean#L135)
- [language_novel_combination_exists](../lean/SentinelTheory/Language.lean#L140)
- [language_codebook_flip_invariant](../lean/SentinelTheory/Language.lean#L152)
- [language_flip_sequence_same_observations](../lean/SentinelTheory/Language.lean#L160)
- [language_no_detector_separates_flip](../lean/SentinelTheory/Language.lean#L165)
- [language_same_history_one_world_wrong](../lean/SentinelTheory/Language.lean#L175)
- [language_fusion_nonzero](../lean/SentinelTheory/Language.lean#L181)