← All the evidencesentinel-proofs
Every file in sentinel-proofs.zip, with its SHA-256.
Audit.lean
SHA-256 38284392194bdbe1dd5093e781fa4a515f8971e9e39c142a5ff385450a31904b
import SentinelProofs
import SentinelTheory
#print axioms SentinelProofs.clip_bounds
#print axioms SentinelProofs.blend_bounds
#print axioms SentinelProofs.coefficient_bounds
#print axioms SentinelProofs.step_bounds
#print axioms SentinelProofs.trajectory_bounds
#print axioms SentinelProofs.weight_nonnegative
#print axioms SentinelProofs.weight_sum_bound
#print axioms SentinelProofs.weight_sum_below_one
#print axioms SentinelTheory.event_dependent_rates_bounded
#print axioms SentinelTheory.trace_matches_clipped_update
#print axioms SentinelTheory.trace_zero_time
#print axioms SentinelTheory.trace_time_subdivision
#print axioms SentinelTheory.future_change_telescopes
#print axioms SentinelTheory.future_probability_difference_bounds
#print axioms SentinelTheory.exponential_width_monotone
#print axioms SentinelTheory.normalized_square_monotone
#print axioms SentinelTheory.ellipse_expansion_contains_old
#print axioms SentinelTheory.branch_union_preserves_old
#print axioms SentinelTheory.path_product_bounds
#print axioms SentinelTheory.strongest_route_can_lose_mass
#print axioms SentinelTheory.path_mass_geometric_bound
#print axioms SentinelTheory.dominated_path_series_summable
#print axioms SentinelTheory.geometric_tail_exact
#print axioms SentinelTheory.dominated_path_tail_bound
#print axioms SentinelTheory.euler_phase_identity
#print axioms SentinelTheory.phase_has_unit_norm
#print axioms SentinelTheory.phase_composition
#print axioms SentinelTheory.evidence_xor_explanations_ambiguous
#print axioms SentinelTheory.evidence_common_flip_invariant
#print axioms SentinelTheory.evidence_observations_cannot_decode_h
#print axioms SentinelTheory.evidence_correction_recovers
#print axioms SentinelTheory.evidence_same_group_disagreement_cancels
#print axioms SentinelTheory.evidence_cross_group_disagreement
#print axioms SentinelTheory.evidence_majority_flip_equivariant
#print axioms SentinelTheory.evidence_majority_ignores_one_fault
#print axioms SentinelTheory.evidence_majority_follows_common_fault
#print axioms SentinelTheory.evidence_bias_shift_unidentifiable
#print axioms SentinelTheory.evidence_posterior_odds
#print axioms SentinelTheory.evidence_log_ratios_add
#print axioms SentinelTheory.evidence_duplicate_overcounts
#print axioms SentinelTheory.evidence_cusum_nonneg
#print axioms SentinelTheory.evidence_cusum_dominates
#print axioms SentinelTheory.evidence_cusum_monotone
#print axioms SentinelTheory.evidence_cusum_resets
#print axioms SentinelTheory.evidence_cusum_growth_bound
#print axioms SentinelTheory.evidence_value_of_information_nonneg
#print axioms SentinelTheory.evidence_no_value_when_decision_fixed
#print axioms SentinelTheory.evidence_smoothed_table_normalized
#print axioms SentinelTheory.evidence_smoothed_table_positive
#print axioms SentinelTheory.evidence_chain_rule
#print axioms SentinelTheory.evidence_disagreement_bounds
#print axioms SentinelTheory.evidence_disagreement_symm
#print axioms SentinelTheory.evidence_disagreement_self
#print axioms SentinelTheory.evidence_disagreement_triangle
#print axioms SentinelTheory.xor_conditional_entropy_exact
#print axioms SentinelTheory.xor_joint_information_exact
#print axioms SentinelTheory.xor_single_information_zero
#print axioms SentinelTheory.xor_joint_information_positive
#print axioms SentinelTheory.noiseless_xor_one_bit
#print axioms SentinelTheory.independent_noise_zero_information
#print axioms SentinelTheory.language_silence_is_an_option
#print axioms SentinelTheory.language_adding_option_never_lowers
#print axioms SentinelTheory.language_silence_wins_when_all_negative
#print axioms SentinelTheory.language_budgeted_selection_silence
#print axioms SentinelTheory.language_value_of_information_nonneg
#print axioms SentinelTheory.language_value_of_information_nonneg_joint
#print axioms SentinelTheory.language_value_of_information_zero_of_constant_best
#print axioms SentinelTheory.language_mismatch_complement
#print axioms SentinelTheory.language_independent_mismatch_bounds
#print axioms SentinelTheory.language_brier_bounds
#print axioms SentinelTheory.language_mean_brier_bounds
#print axioms SentinelTheory.language_constant_forecast_decomposition
#print axioms SentinelTheory.language_base_rate_brier_at_most_quarter
#print axioms SentinelTheory.language_half_forecast_brier
#print axioms SentinelTheory.language_identical_inputs_brier_floor
#print axioms SentinelTheory.language_expression_count
#print axioms SentinelTheory.language_novel_combination_count
#print axioms SentinelTheory.language_novel_combination_exists
#print axioms SentinelTheory.language_codebook_flip_invariant
#print axioms SentinelTheory.language_flip_sequence_same_observations
#print axioms SentinelTheory.language_no_detector_separates_flip
#print axioms SentinelTheory.language_same_history_one_world_wrong
#print axioms SentinelTheory.language_fusion_nonzero
#print axioms SentinelTheory.interest_ceiling
#print axioms SentinelTheory.interest_zero_relevance
#print axioms SentinelTheory.interest_increases_with_exposure
#print axioms SentinelTheory.hard_constraint_zero_activation
#print axioms SentinelTheory.unresolved_keeps_allowance
#print axioms SentinelTheory.positive_exploration_can_activate
#print axioms SentinelTheory.uniform_second_moment
#print axioms SentinelTheory.uniform_fourth_moment
#print axioms SentinelTheory.orthogonal_cubic_zero_linear_moment
#print axioms SentinelTheory.cubic_from_intermediate_multiplication
#print axioms SentinelTheory.corroboration_false_positive_bound
#print axioms SentinelTheory.confirming_alerts_are_subset
#print axioms SentinelTheory.noisy_xor_single_feature_blind
#print axioms SentinelTheory.noisy_xor_other_feature_blind
#print axioms SentinelTheory.noisy_xor_output_fair
#print axioms SentinelTheory.noisy_xor_joint_is_informative
#print axioms SentinelTheory.noisy_xor_mass_nonnegative
#print axioms SentinelTheory.noisy_xor_mass_normalized
#print axioms SentinelTheory.xor_is_linear_over_two
#print axioms SentinelTheory.independent_clean_sample_mass
#print axioms SentinelTheory.two_step_path_composition
#print axioms SentinelTheory.inverse_certifies_unique_linear_solution
#print axioms SentinelTheory.disjunction_from_and_not
#print axioms SentinelTheory.expression_renaming_preserves_meaning
#print axioms SentinelTheory.finite_boolean_function_expressible
#print axioms SentinelTheory.boolean_function_count
#print axioms SentinelTheory.three_bit_function_count
#print axioms SentinelTheory.macro_substitution_preserves_meaning
#print axioms SentinelTheory.language_growth_preserves_known
#print axioms SentinelTheory.finite_expression_in_limit
#print axioms SentinelTheory.pathway_operator_norm_bound
#print axioms SentinelTheory.pathway_matrix_series_inverse
#print axioms SentinelTheory.pathway_matrix_series_summable
#print axioms SentinelTheory.pathway_matrix_tail_bound
#print axioms SentinelTheory.empirical_update_identity
#print axioms SentinelTheory.empirical_update_bounds
#print axioms SentinelTheory.beta_mean_strict_bounds
#print axioms SentinelTheory.beta_variance_expression_nonnegative
#print axioms SentinelTheory.uniform_beta_unknown
#print axioms SentinelTheory.missing_evidence_unchanged
#print axioms SentinelTheory.posterior_nonnegative
#print axioms SentinelTheory.posterior_normalized
#print axioms SentinelTheory.zero_prior_stays_zero
#print axioms SentinelTheory.posterior_uninformative
#print axioms SentinelTheory.mixture_bounds
#print axioms SentinelTheory.markov_mixture_normalized
#print axioms SentinelTheory.charger_example
#print axioms SentinelTheory.propagated_battery_example
#print axioms SentinelTheory.propagated_task_example
#print axioms SentinelTheory.fourier_delay_phase
#print axioms SentinelTheory.fourier_gain_and_delay
#print axioms SentinelTheory.cross_spectrum_factorization
#print axioms SentinelTheory.forced_trace_initial_value
#print axioms SentinelTheory.forced_trace_convolution
#print axioms SentinelTheory.forced_trace_solves_relaxation
#print axioms SentinelTheory.feasibility_monotone
#print axioms SentinelTheory.adding_resources_preserves_feasibility
#print axioms SentinelTheory.indicator_bounds
#print axioms SentinelTheory.indicator_monotone
#print axioms SentinelTheory.feasibility_gain_bounds
#print axioms SentinelTheory.product_unit_bounds
#print axioms SentinelTheory.opportunity_relevance_bounds
#print axioms SentinelTheory.alternative_routes_monotone
#print axioms SentinelTheory.new_route_preserves_possibilities
#print axioms SentinelTheory.missing_requirements_shrink
#print axioms SentinelTheory.failure_of_one_route_allows_another
#print axioms SentinelTheory.action_does_not_identify_preference
#print axioms SentinelTheory.identical_observations_cannot_decode_distinct_targets
#print axioms SentinelTheory.refinement_preserves_old_representation
#print axioms SentinelTheory.refinement_separates_distinctions
#print axioms SentinelTheory.fixed_representation_cannot_predict_different_futures
#print axioms SentinelTheory.unknown_zero_gate_blocks_activity
#print axioms SentinelTheory.net_gain_positive_iff
#print axioms SentinelTheory.uniform_coverage_budget
#print axioms SentinelTheory.information_can_be_ignored
#print axioms SentinelTheory.timing_clock_compose
#print axioms SentinelTheory.timing_clock_inverse
#print axioms SentinelTheory.timing_offset_latency_not_identifiable
#print axioms SentinelTheory.timing_clock_error_bound
#print axioms SentinelTheory.timing_periodic_shift_indistinguishable
#print axioms SentinelTheory.timing_decay_semigroup
#print axioms SentinelTheory.timing_decay_bounded_between_updates
#print axioms SentinelTheory.timing_wake_time_hits_threshold
#print axioms SentinelTheory.timing_wake_time_nonneg
#print axioms SentinelTheory.timing_value_of_computation_nonneg
#print axioms SentinelTheory.timing_compute_only_if_gain_exceeds_cost
#print axioms SentinelTheory.timing_budget_active_count_bound
#print axioms SentinelTheory.timing_budget_subset_feasible
#print axioms SentinelTheory.timing_budget_shrink_drops_member
#print axioms SentinelTheory.timing_beta_estimate_open_unit
#print axioms SentinelTheory.timing_beta_estimate_monotone_in_successes
#print axioms SentinelTheory.timing_suspend_discount_le
#print axioms SentinelTheory.timing_compression_pigeonhole
#print axioms SentinelTheory.timing_compression_not_injective
#print axioms SentinelTheory.timing_inspect_budget_success_bound
#print axioms SentinelTheory.timing_effective_sample_size_bounds
#print axioms SentinelTheory.timing_effective_sample_size_independent
#print axioms SentinelTheory.timing_effective_sample_size_decreasing
#print axioms SentinelTheory.value_tentative_threshold
#print axioms SentinelTheory.value_tentative_monotone
#print axioms SentinelTheory.value_interrupt_rule_monotone
#print axioms SentinelTheory.value_optimal_with_silence_nonneg
#print axioms SentinelTheory.value_unconstrained_threshold_optimal
#print axioms SentinelTheory.value_gated_budget_value_bound
#print axioms SentinelTheory.value_silent_history_hides_sign
#print axioms SentinelTheory.value_selective_feedback_bias
#print axioms SentinelTheory.value_joint_survival_factorization
#print axioms SentinelTheory.value_exponential_survival_bounds
#print axioms SentinelTheory.value_survival_decreases_with_delay
#print axioms SentinelTheory.value_waiting_cannot_raise_utility
#print axioms SentinelTheory.value_verification_posterior_bounds
#print axioms SentinelTheory.value_verification_posterior_vs_prior
#print axioms SentinelTheory.value_verification_posterior_mean
#print axioms SentinelTheory.value_two_outcome_option_value
#print axioms SentinelTheory.value_verification_never_worse_before_cost
#print axioms SentinelTheory.value_filter_step_normalized
#print axioms SentinelTheory.value_rotation_nonidentifiable
#print axioms SentinelTheory.value_flip_nonidentifiable
#print axioms SentinelTheory.value_alignment_candidate_count
#print axioms SentinelTheory.value_blocked_action_value_survives
#print axioms SentinelTheory.value_equal_likelihood_posterior_is_prior
#print axioms SentinelTheory.value_pursuit_switch_deviation
#print axioms SentinelTheory.value_pursuit_switch_contracts
#print axioms SentinelTheory.value_pursuit_switch_iterate
#print axioms SentinelTheory.value_pursuit_drifts_to_uncertainty
#print axioms SentinelTheory.value_shrinkage_between
#print axioms SentinelTheory.value_policy_permission_gate
#print axioms SentinelTheory.value_policy_normalized
SentinelProofs.lean
SHA-256 0f90ff71963af569905fb41e64838b8d05d104306f3241de8ecf07bd8a0dbb52
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Algebra.BigOperators.Field
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
/- Real-arithmetic specification; see ../docs/lean-result.md for verification. -/
noncomputable section
open scoped BigOperators
namespace SentinelProofs
def clip (drive : ℝ) : ℝ := max 0 (min 1 drive)
theorem clip_bounds (drive : ℝ) : 0 ≤ clip drive ∧ clip drive ≤ 1 := by
constructor
· exact le_max_left _ _
· exact max_le zero_le_one (min_le_left _ _)
def blend (u target eta : ℝ) : ℝ := (1 - eta) * u + eta * target
theorem blend_bounds {u target eta : ℝ}
(hu : 0 ≤ u ∧ u ≤ 1) (ht : 0 ≤ target ∧ target ≤ 1)
(he : 0 ≤ eta ∧ eta ≤ 1) :
0 ≤ blend u target eta ∧ blend u target eta ≤ 1 := by
have hremain : 0 ≤ 1 - eta := sub_nonneg.mpr he.2
constructor
· exact add_nonneg (mul_nonneg hremain hu.1) (mul_nonneg he.1 ht.1)
· have hleft := mul_le_mul_of_nonneg_left hu.2 hremain
have hright := mul_le_mul_of_nonneg_left ht.2 he.1
dsimp [blend]
nlinarith
def coefficient (dt tau : ℝ) : ℝ := 1 - Real.exp (-dt / tau)
theorem coefficient_bounds {dt tau : ℝ} (hdt : 0 ≤ dt) (htau : 0 < tau) :
0 ≤ coefficient dt tau ∧ coefficient dt tau ≤ 1 := by
have hratio : -dt / tau ≤ 0 := div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr hdt) htau.le
have hexp : Real.exp (-dt / tau) ≤ 1 := by
simpa using Real.exp_le_exp.mpr hratio
have hpos := Real.exp_pos (-dt / tau)
dsimp [coefficient]
constructor <;> linarith
def step (u drive dt tau : ℝ) : ℝ := blend u (clip drive) (coefficient dt tau)
theorem step_bounds {u drive dt tau : ℝ}
(hu : 0 ≤ u ∧ u ≤ 1) (hdt : 0 ≤ dt) (htau : 0 < tau) :
0 ≤ step u drive dt tau ∧ step u drive dt tau ≤ 1 := by
exact blend_bounds hu (clip_bounds drive) (coefficient_bounds hdt htau)
def trajectory (initial : ℝ) (drive dt tau : ℕ → ℝ) : ℕ → ℝ
| 0 => initial
| n + 1 => step (trajectory initial drive dt tau n) (drive n) (dt n) (tau n)
theorem trajectory_bounds (initial : ℝ) (drive dt tau : ℕ → ℝ)
(hu : 0 ≤ initial ∧ initial ≤ 1)
(hdt : ∀ n, 0 ≤ dt n) (htau : ∀ n, 0 < tau n) (n : ℕ) :
0 ≤ trajectory initial drive dt tau n ∧ trajectory initial drive dt tau n ≤ 1 := by
induction n with
| zero => exact hu
| succ n ih => exact step_bounds ih (hdt n) (htau n)
def weight {ι : Type*} (s : Finset ι) (g : ι → ℝ) (rho : ℝ) (j : ι) : ℝ :=
rho * g j / max 1 (∑ k ∈ s, g k)
theorem weight_nonnegative {ι : Type*} (s : Finset ι) (g : ι → ℝ) (rho : ℝ)
(hrho : 0 ≤ rho) (hg : ∀ j ∈ s, 0 ≤ g j) {j : ι} (hj : j ∈ s) :
0 ≤ weight s g rho j := by
exact div_nonneg (mul_nonneg hrho (hg j hj))
(le_trans zero_le_one (le_max_left _ _))
theorem weight_sum_bound {ι : Type*} (s : Finset ι) (g : ι → ℝ) (rho : ℝ)
(hrho : 0 ≤ rho) : (∑ j ∈ s, weight s g rho j) ≤ rho := by
have hd : 0 < max (1 : ℝ) (∑ k ∈ s, g k) :=
lt_of_lt_of_le zero_lt_one (le_max_left _ _)
unfold weight
rw [← Finset.sum_div, ← Finset.mul_sum]
apply (div_le_iff₀ hd).2
exact mul_le_mul_of_nonneg_left (le_max_right _ _) hrho
theorem weight_sum_below_one {ι : Type*} (s : Finset ι) (g : ι → ℝ) (rho : ℝ)
(hrho : 0 ≤ rho) (hrho_one : rho < 1) :
(∑ j ∈ s, weight s g rho j) < 1 := by
exact lt_of_le_of_lt (weight_sum_bound s g rho hrho) hrho_one
#print axioms clip_bounds
#print axioms blend_bounds
#print axioms coefficient_bounds
#print axioms step_bounds
#print axioms trajectory_bounds
#print axioms weight_nonnegative
#print axioms weight_sum_bound
#print axioms weight_sum_below_one
end SentinelProofs
SentinelTheory/Dynamics.lean
SHA-256 17d7fc8b700f4609d12f12daf9e97b0da670a9945a8db9c4e65f5fca62523b8c
import SentinelTheory.Structure
import Mathlib.Analysis.Complex.Trigonometric
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def eventTrajectory (initial : ℝ) (drive eta : ℕ → ℝ) : ℕ → ℝ
| 0 => initial
| n + 1 => SentinelProofs.blend (eventTrajectory initial drive eta n)
(SentinelProofs.clip (drive n)) (eta n)
theorem event_dependent_rates_bounded (initial : ℝ) (drive eta : ℕ → ℝ)
(hi : 0 ≤ initial ∧ initial ≤ 1) (he : ∀ n, 0 ≤ eta n ∧ eta n ≤ 1) (n : ℕ) :
0 ≤ eventTrajectory initial drive eta n ∧ eventTrajectory initial drive eta n ≤ 1 := by
induction n with
| zero => exact hi
| succ n ih => exact SentinelProofs.blend_bounds ih (SentinelProofs.clip_bounds _) (he n)
def constantDriveTrace (initial target dt tau : ℝ) : ℝ :=
target + (initial - target) * Real.exp (-dt / tau)
theorem trace_matches_clipped_update (u drive dt tau : ℝ) :
SentinelProofs.step u drive dt tau =
constantDriveTrace u (SentinelProofs.clip drive) dt tau := by
dsimp [SentinelProofs.step, SentinelProofs.blend, SentinelProofs.coefficient, constantDriveTrace]
ring
theorem trace_zero_time (u target tau : ℝ) : constantDriveTrace u target 0 tau = u := by
simp [constantDriveTrace]
theorem trace_time_subdivision (u target a b tau : ℝ) :
constantDriveTrace (constantDriveTrace u target a tau) target b tau =
constantDriveTrace u target (a + b) tau := by
have h : -(a + b) / tau = -a / tau + -b / tau := by ring
simp only [constantDriveTrace, h, Real.exp_add]
ring
theorem future_change_telescopes (past present future : ℝ) :
(future - present) + (present - past) = future - past := by ring
theorem future_probability_difference_bounds (p q : ℝ)
(hp : 0 ≤ p ∧ p ≤ 1) (hq : 0 ≤ q ∧ q ≤ 1) : -1 ≤ p - q ∧ p - q ≤ 1 := by
constructor <;> linarith
theorem exponential_width_monotone (a rate t u : ℝ)
(ha : 0 ≤ a) (hr : 0 ≤ rate) (htu : t ≤ u) :
a * Real.exp (rate * t) ≤ a * Real.exp (rate * u) := by
apply mul_le_mul_of_nonneg_left _ ha
exact Real.exp_le_exp.mpr (mul_le_mul_of_nonneg_left htu hr)
theorem normalized_square_monotone (x a b : ℝ) (ha : 0 < a) (hab : a ≤ b) :
(x / b)^2 ≤ (x / a)^2 := by
have hb : 0 < b := ha.trans_le hab
have hab2 : a^2 ≤ b^2 := by nlinarith
have ha2 : 0 < a^2 := by positivity
rw [div_pow, div_pow]
exact div_le_div_of_nonneg_left (sq_nonneg x) ha2 hab2
theorem ellipse_expansion_contains_old (x y a b c d : ℝ)
(ha : 0 < a) (hb : 0 < b) (hac : a ≤ c) (hbd : b ≤ d)
(hold : (x / a)^2 + (y / b)^2 ≤ 1) :
(x / c)^2 + (y / d)^2 ≤ 1 := by
have hx := normalized_square_monotone x a c ha hac
have hy := normalized_square_monotone y b d hb hbd
linarith
theorem branch_union_preserves_old {Path State : Type*} (old new : Set Path)
(regions : Path → Set State) (h : old ⊆ new) :
(⋃ p ∈ old, regions p) ⊆ ⋃ p ∈ new, regions p := by
intro x hx
simp only [Set.mem_iUnion] at hx ⊢
obtain ⟨p, hp, hxp⟩ := hx
exact ⟨p, h hp, hxp⟩
theorem path_product_bounds {ι : Type*} (s : Finset ι) (b : ι → ℝ)
(hb : ∀ i ∈ s, 0 ≤ b i ∧ b i ≤ 1) :
0 ≤ ∏ i ∈ s, b i ∧ (∏ i ∈ s, b i) ≤ 1 := by
exact ⟨Finset.prod_nonneg (fun i hi => (hb i hi).1),
Finset.prod_le_one (fun i hi => (hb i hi).1) (fun i hi => (hb i hi).2)⟩
theorem strongest_route_can_lose_mass : max (3 / 10 : ℝ) (1 / 10) < 3 / 10 + 1 / 10 := by
norm_num
def pathMass {ι : Type*} (s : Finset ι) (w : ι → ι → ℝ) : ℕ → ι → ℝ
| 0, _ => 1
| n + 1, i => ∑ j ∈ s, w i j * pathMass s w n j
theorem path_mass_geometric_bound {ι : Type*} (s : Finset ι) (w : ι → ι → ℝ)
(rho : ℝ) (hr : 0 ≤ rho) (hw : ∀ i j, j ∈ s → 0 ≤ w i j)
(hrow : ∀ i, (∑ j ∈ s, w i j) ≤ rho) (n : ℕ) (i : ι) :
0 ≤ pathMass s w n i ∧ pathMass s w n i ≤ rho^n := by
induction n generalizing i with
| zero => simp [pathMass]
| succ n ih =>
constructor
· exact Finset.sum_nonneg fun j hj => mul_nonneg (hw i j hj) (ih j).1
· calc
pathMass s w (n + 1) i ≤ ∑ j ∈ s, w i j * rho^n := by
apply Finset.sum_le_sum
intro j hj
exact mul_le_mul_of_nonneg_left (ih j).2 (hw i j hj)
_ = (∑ j ∈ s, w i j) * rho^n := (Finset.sum_mul _ _ _).symm
_ ≤ rho * rho^n := mul_le_mul_of_nonneg_right (hrow i) (pow_nonneg hr n)
_ = rho^(n + 1) := (pow_succ' rho n).symm
theorem dominated_path_series_summable (a : ℕ → ℝ) (rho : ℝ)
(hr : 0 ≤ rho) (hr1 : rho < 1) (ha : ∀ n, 0 ≤ a n)
(hbound : ∀ n, a n ≤ rho^n) : Summable a := by
exact Summable.of_nonneg_of_le ha hbound (summable_geometric_of_lt_one hr hr1)
theorem geometric_tail_exact (rho : ℝ) (hr : 0 ≤ rho) (hr1 : rho < 1) (m : ℕ) :
(∑' n : ℕ, rho^(m + 1 + n)) = rho^(m + 1) / (1 - rho) := by
simp_rw [pow_add]
rw [tsum_mul_left, tsum_geometric_of_lt_one hr hr1]
rfl
theorem dominated_path_tail_bound (a : ℕ → ℝ) (rho : ℝ)
(hr : 0 ≤ rho) (hr1 : rho < 1) (ha : ∀ n, 0 ≤ a n)
(hbound : ∀ n, a n ≤ rho^n) (m : ℕ) :
(∑' n : ℕ, a (m + 1 + n)) ≤ rho^(m + 1) / (1 - rho) := by
have hg : Summable (fun n : ℕ => rho^(m + 1 + n)) := by
simp_rw [pow_add]
exact (summable_geometric_of_lt_one hr hr1).mul_left _
have ha' : Summable (fun n : ℕ => a (m + 1 + n)) :=
Summable.of_nonneg_of_le (fun n => ha _) (fun n => hbound _) hg
calc
(∑' n : ℕ, a (m + 1 + n)) ≤ ∑' n : ℕ, rho^(m + 1 + n) :=
ha'.tsum_le_tsum (fun n => hbound _) hg
_ = rho^(m + 1) / (1 - rho) := geometric_tail_exact rho hr hr1 m
theorem euler_phase_identity (theta : ℂ) :
Complex.exp (theta * Complex.I) = Complex.cos theta + Complex.sin theta * Complex.I :=
Complex.exp_mul_I theta
theorem phase_has_unit_norm (theta : ℝ) : ‖Complex.exp (theta * Complex.I)‖ = 1 :=
Complex.norm_exp_ofReal_mul_I theta
theorem phase_composition (a b : ℂ) :
Complex.exp ((a + b) * Complex.I) =
Complex.exp (a * Complex.I) * Complex.exp (b * Complex.I) := by
rw [add_mul, Complex.exp_add]
end SentinelTheory
SentinelTheory/Evidence.lean
SHA-256 533e49412b47bb0b2fb21e1b3e943b1b267e08f4f81bc9b809c23c37c795c7ff
import SentinelProofs
import SentinelTheory.Probability
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Positivity
import Mathlib.Analysis.SpecialFunctions.Log.Basic
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def evidenceObs {ι : Type*} (h : Bool) (F : ι → Bool) (e : ι → Bool) (j : ι) : Bool :=
xor (xor h (F j)) (e j)
theorem evidence_xor_explanations_ambiguous (h f : Bool) :
∃ h' f' : Bool, (h', f') ≠ (h, f) ∧ xor h' f' = xor h f :=
⟨!h, !f, by cases h <;> cases f <;> decide, by cases h <;> cases f <;> rfl⟩
theorem evidence_common_flip_invariant {ι : Type*} (h : Bool) (F e : ι → Bool) (j : ι) :
evidenceObs (!h) (fun i => !F i) e j = evidenceObs h F e j := by
cases h <;> cases hf : F j <;> cases he : e j <;> simp [evidenceObs, hf, he]
theorem evidence_observations_cannot_decode_h {ι : Type*} (h : Bool) (F e : ι → Bool) :
∃ F' : ι → Bool, (∀ j, evidenceObs (!h) F' e j = evidenceObs h F e j) ∧ (!h) ≠ h :=
⟨fun i => !F i, fun j => evidence_common_flip_invariant h F e j, by cases h <;> decide⟩
theorem evidence_correction_recovers (h a b : Bool) :
xor (xor h (xor a b)) (xor a b) = h := by
cases h <;> cases a <;> cases b <;> rfl
theorem evidence_same_group_disagreement_cancels (h f e1 e2 : Bool) :
xor (xor (xor h f) e1) (xor (xor h f) e2) = xor e1 e2 := by
cases h <;> cases f <;> cases e1 <;> cases e2 <;> rfl
theorem evidence_cross_group_disagreement (h f1 f2 e1 e2 : Bool) :
xor (xor (xor h f1) e1) (xor (xor h f2) e2) = xor (xor f1 f2) (xor e1 e2) := by
cases h <;> cases f1 <;> cases f2 <;> cases e1 <;> cases e2 <;> rfl
def evidenceMajority (a b c : Bool) : Bool := (a && b) || (a && c) || (b && c)
theorem evidence_majority_flip_equivariant (a b c : Bool) :
evidenceMajority (!a) (!b) (!c) = !evidenceMajority a b c := by
cases a <;> cases b <;> cases c <;> rfl
theorem evidence_majority_ignores_one_fault (h c : Bool) :
evidenceMajority h h c = h ∧ evidenceMajority h c h = h ∧ evidenceMajority c h h = h := by
cases h <;> cases c <;> decide
theorem evidence_majority_follows_common_fault (h f : Bool) :
evidenceMajority (xor h f) (xor h f) (xor h f) = xor h f := by
cases h <;> cases f <;> rfl
theorem evidence_bias_shift_unidentifiable (x b δ : ℝ) :
(x + δ) + (b - δ) = x + b := by ring
theorem evidence_posterior_odds (mass lik : Bool → ℝ)
(h0 : 0 < mass false * lik false) (h1 : 0 < mass true * lik true) :
posterior Finset.univ mass lik true / posterior Finset.univ mass lik false =
(mass true / mass false) * (lik true / lik false) := by
have hs : 0 < mass true * lik true + mass false * lik false := by linarith
have a : mass false ≠ 0 := fun h => by simp [h] at h0
have b : lik false ≠ 0 := fun h => by simp [h] at h0
have c : mass true ≠ 0 := fun h => by simp [h] at h1
simp only [posterior, Fintype.sum_bool]
field_simp
theorem evidence_log_ratios_add (l0 l1 m0 m1 : ℝ)
(a : 0 < l0) (b : 0 < l1) (c : 0 < m0) (d : 0 < m1) :
Real.log ((l1 * m1) / (l0 * m0)) = Real.log (l1 / l0) + Real.log (m1 / m0) := by
rw [show (l1 * m1) / (l0 * m0) = (l1 / l0) * (m1 / m0) by field_simp]
exact Real.log_mul (by positivity) (by positivity)
theorem evidence_duplicate_overcounts (r : ℝ) (hr : 0 < r) :
(1 < r → r < r * r) ∧ (r < 1 → r * r < r) := by
constructor <;> intro h <;> nlinarith
def evidenceCusumStep (c llr : ℝ) : ℝ := max 0 (c + llr)
theorem evidence_cusum_nonneg (c llr : ℝ) : 0 ≤ evidenceCusumStep c llr :=
le_max_left _ _
theorem evidence_cusum_dominates (c llr : ℝ) : c + llr ≤ evidenceCusumStep c llr :=
le_max_right _ _
theorem evidence_cusum_monotone {c c' : ℝ} (llr : ℝ) (h : c ≤ c') :
evidenceCusumStep c llr ≤ evidenceCusumStep c' llr :=
max_le_max le_rfl (by linarith)
theorem evidence_cusum_resets (c llr : ℝ) (h : c + llr ≤ 0) : evidenceCusumStep c llr = 0 :=
max_eq_left h
theorem evidence_cusum_growth_bound (c llr : ℝ) (hc : 0 ≤ c) :
evidenceCusumStep c llr ≤ c + |llr| :=
max_le (by linarith [abs_nonneg llr]) (by linarith [le_abs_self llr])
theorem evidence_value_of_information_nonneg {Z D : Type*} (zs : Finset Z) (ds : Finset D)
(hne : ds.Nonempty) (f : Z → D → ℝ) :
∀ d ∈ ds, ∑ z ∈ zs, f z d ≤ ∑ z ∈ zs, ds.sup' hne (f z) :=
fun _ hd => Finset.sum_le_sum fun z _ => Finset.le_sup' (f z) hd
theorem evidence_no_value_when_decision_fixed {Z D : Type*} (zs : Finset Z) (ds : Finset D)
(hne : ds.Nonempty) (f : Z → D → ℝ) (d0 : D) (hd0 : d0 ∈ ds)
(hbest : ∀ z ∈ zs, ∀ d ∈ ds, f z d ≤ f z d0) :
∑ z ∈ zs, ds.sup' hne (f z) = ∑ z ∈ zs, f z d0 :=
Finset.sum_congr rfl fun z hz =>
le_antisymm (Finset.sup'_le hne _ (hbest z hz)) (Finset.le_sup' (f z) hd0)
theorem evidence_smoothed_table_normalized {ι : Type*} (s : Finset ι) (c : ι → ℝ) (n α : ℝ)
(hc : ∑ i ∈ s, c i = n) (hpos : 0 < n + s.card * α) :
∑ i ∈ s, (c i + α) / (n + s.card * α) = 1 := by
rw [← Finset.sum_div, Finset.sum_add_distrib, hc, Finset.sum_const, nsmul_eq_mul]
exact div_self (ne_of_gt hpos)
theorem evidence_smoothed_table_positive (c α n : ℝ) (k : ℕ)
(hc : 0 ≤ c) (hα : 0 < α) (hd : 0 < n + k * α) :
0 < (c + α) / (n + k * α) := div_pos (by linarith) hd
theorem evidence_chain_rule (pM pMT pMTV pMTVA : ℝ)
(h1 : 0 < pM) (h2 : 0 < pMT) (h3 : 0 < pMTV) :
pM * (pMT / pM) * (pMTV / pMT) * (pMTVA / pMTV) = pMTVA := by
field_simp
def evidenceDisagreement {N : ℕ} (a b : Fin N → Bool) : ℝ :=
((Finset.univ.filter fun t => a t ≠ b t).card : ℝ) / N
theorem evidence_disagreement_bounds {N : ℕ} (hN : 0 < N) (a b : Fin N → Bool) :
0 ≤ evidenceDisagreement a b ∧ evidenceDisagreement a b ≤ 1 := by
have hp : (0 : ℝ) < N := by exact_mod_cast hN
refine ⟨by unfold evidenceDisagreement; positivity, ?_⟩
unfold evidenceDisagreement
rw [div_le_one hp]
exact_mod_cast (Finset.card_filter_le _ _).trans (by simp)
theorem evidence_disagreement_symm {N : ℕ} (a b : Fin N → Bool) :
evidenceDisagreement a b = evidenceDisagreement b a := by
unfold evidenceDisagreement
congr 3
ext t
simp [ne_comm]
theorem evidence_disagreement_self {N : ℕ} (a : Fin N → Bool) : evidenceDisagreement a a = 0 := by
simp [evidenceDisagreement]
theorem evidence_disagreement_triangle {N : ℕ} (a b c : Fin N → Bool) :
evidenceDisagreement a c ≤ evidenceDisagreement a b + evidenceDisagreement b c := by
unfold evidenceDisagreement
rw [← add_div]
rcases Nat.eq_zero_or_pos N with h | h
· subst h; simp
have hp : (0 : ℝ) < N := by exact_mod_cast h
apply div_le_div_of_nonneg_right _ hp.le
have hsub : (Finset.univ.filter fun t => a t ≠ c t) ⊆
(Finset.univ.filter fun t => a t ≠ b t) ∪ (Finset.univ.filter fun t => b t ≠ c t) := by
intro t ht
simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_union] at ht ⊢
by_cases hab : a t = b t
· right; rw [← hab]; exact ht
· left; exact hab
exact_mod_cast (Finset.card_le_card hsub).trans (Finset.card_union_le _ _)
end SentinelTheory
SentinelTheory/Information.lean
SHA-256 a20dad0d1b8ff42d93671ac22089ba3db7e231b01c7afb6dc104c52e4e624e53
import SentinelTheory.Learning
import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def binaryEntropyBits (p : ℝ) : ℝ := Real.binEntropy p / Real.log 2
def xorConditionalEntropy (delta : ℝ) : ℝ :=
∑ a : Bool, ∑ b : Bool, (1 / 4 : ℝ) *
Real.binEntropy (4 * xorJoint delta a b true)
def xorJointInformation (delta : ℝ) : ℝ :=
(Real.binEntropy (1 / 2) - xorConditionalEntropy delta) / Real.log 2
def xorSingleInformation (delta : ℝ) : ℝ :=
(Real.binEntropy (1 / 2) - ∑ a : Bool, (1 / 2 : ℝ) *
Real.binEntropy (2 * ∑ b : Bool, xorJoint delta a b true)) / Real.log 2
theorem xor_conditional_entropy_exact (delta : ℝ) :
xorConditionalEntropy delta = Real.binEntropy delta := by
simp only [xorConditionalEntropy, Fintype.sum_bool, xorJoint]
norm_num
rw [show (4 : ℝ) * (delta / 4) = delta by ring,
show (4 : ℝ) * ((1 - delta) / 4) = 1 - delta by ring]
rw [Real.binEntropy_one_sub]
ring
theorem xor_joint_information_exact (delta : ℝ) :
xorJointInformation delta = 1 - binaryEntropyBits delta := by
have hlog : Real.log (2 : ℝ) ≠ 0 := ne_of_gt (Real.log_pos (by norm_num))
unfold xorJointInformation binaryEntropyBits
rw [xor_conditional_entropy_exact]
have hh : Real.binEntropy (1 / 2 : ℝ) = Real.log 2 := by
simp
rw [hh]
field_simp
theorem xor_single_information_zero (delta : ℝ) : xorSingleInformation delta = 0 := by
unfold xorSingleInformation
simp_rw [noisy_xor_single_feature_blind]
norm_num [Fintype.sum_bool]
ring
theorem xor_joint_information_positive (delta : ℝ) (hd : delta < 1 / 2) :
0 < xorJointInformation delta := by
have hne : delta ≠ (2 : ℝ)⁻¹ := by norm_num at *; linarith
have hh : Real.binEntropy delta < Real.log 2 := Real.binEntropy_lt_log_two.mpr hne
have hlog : 0 < Real.log (2 : ℝ) := Real.log_pos (by norm_num)
rw [xor_joint_information_exact]
exact sub_pos.mpr ((div_lt_one hlog).mpr hh)
theorem noiseless_xor_one_bit : xorJointInformation 0 = 1 := by
rw [xor_joint_information_exact]
simp [binaryEntropyBits]
theorem independent_noise_zero_information : xorJointInformation (1 / 2) = 0 := by
rw [xor_joint_information_exact]
have hh : Real.binEntropy (1 / 2 : ℝ) = Real.log 2 := by
simp
have hlog : Real.log (2 : ℝ) ≠ 0 := ne_of_gt (Real.log_pos (by norm_num))
unfold binaryEntropyBits
rw [hh]
simp [hlog]
end SentinelTheory
SentinelTheory/Language.lean
SHA-256 b2785ef80e6f5826e68e9ffddd6ded59eb1dbfb7ad8a3f6fa08a38a2bbc94916
import SentinelTheory.Probability
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def bestValue {α : Type*} (s : Finset α) (v : α → ℝ) (σ : ℝ) : ℝ :=
(insert σ (s.image v)).max' (Finset.insert_nonempty _ _)
theorem language_silence_is_an_option {α : Type*} (s : Finset α) (v : α → ℝ) (σ : ℝ) :
σ ≤ bestValue s v σ ∧ ∀ u ∈ s, v u ≤ bestValue s v σ := by
refine ⟨Finset.le_max' _ _ (Finset.mem_insert_self _ _), fun u hu => ?_⟩
exact Finset.le_max' _ _ (Finset.mem_insert_of_mem (Finset.mem_image_of_mem v hu))
theorem language_adding_option_never_lowers {α : Type*} {s t : Finset α} (v : α → ℝ) (σ : ℝ)
(h : s ⊆ t) : bestValue s v σ ≤ bestValue t v σ := by
apply Finset.max'_le
intro y hy
rcases Finset.mem_insert.mp hy with rfl | hy
· exact (language_silence_is_an_option t v y).1
· obtain ⟨u, hu, rfl⟩ := Finset.mem_image.mp hy
exact (language_silence_is_an_option t v σ).2 u (h hu)
theorem language_silence_wins_when_all_negative {α : Type*} (s : Finset α) (v : α → ℝ) (σ : ℝ)
(h : ∀ u ∈ s, v u < σ) : bestValue s v σ = σ ∧ ∀ u ∈ s, v u < bestValue s v σ := by
have heq : bestValue s v σ = σ := by
apply le_antisymm
· apply Finset.max'_le
intro y hy
rcases Finset.mem_insert.mp hy with rfl | hy
· exact le_rfl
· obtain ⟨u, hu, rfl⟩ := Finset.mem_image.mp hy
exact (h u hu).le
· exact (language_silence_is_an_option s v σ).1
exact ⟨heq, fun u hu => lt_of_lt_of_eq (h u hu) heq.symm⟩
theorem language_budgeted_selection_silence {α : Type*} (net : α → ℝ)
(h : ∀ u, net u ≤ 0) (S : Finset α) : ∑ u ∈ S, net u ≤ 0 :=
Finset.sum_nonpos fun u _ => h u
theorem language_value_of_information_nonneg {A Y : Type*} [Fintype Y] (As : Finset A)
(hA : As.Nonempty) (f : A → Y → ℝ) :
As.sup' hA (fun a => ∑ y, f a y) ≤ ∑ y, As.sup' hA (fun a => f a y) := by
apply Finset.sup'_le
intro a ha
exact Finset.sum_le_sum fun y _ => Finset.le_sup' (fun a => f a y) ha
theorem language_value_of_information_nonneg_joint {A Y G : Type*} [Fintype Y] [Fintype G]
(As : Finset A) (hA : As.Nonempty) (w : Y → G → ℝ) (U : A → G → ℝ) :
As.sup' hA (fun a => ∑ g, (∑ y, w y g) * U a g) ≤
∑ y, As.sup' hA (fun a => ∑ g, w y g * U a g) := by
have key : ∀ a, ∑ g, (∑ y, w y g) * U a g = ∑ y, ∑ g, w y g * U a g := by
intro a
rw [Finset.sum_comm]
simp [Finset.sum_mul]
simpa only [key] using
language_value_of_information_nonneg As hA (fun a y => ∑ g, w y g * U a g)
theorem language_value_of_information_zero_of_constant_best {A Y : Type*} [Fintype Y]
(As : Finset A) (hA : As.Nonempty) (f : A → Y → ℝ) (a0 : A) (h0 : a0 ∈ As)
(hbest : ∀ y, ∀ a ∈ As, f a y ≤ f a0 y) :
As.sup' hA (fun a => ∑ y, f a y) = ∑ y, As.sup' hA (fun a => f a y) := by
apply le_antisymm (language_value_of_information_nonneg As hA f)
calc ∑ y, As.sup' hA (fun a => f a y) ≤ ∑ y, f a0 y :=
Finset.sum_le_sum fun y _ => Finset.sup'_le _ _ fun a ha => hbest y a ha
_ ≤ As.sup' hA (fun a => ∑ y, f a y) :=
Finset.le_sup' (fun a => ∑ y, f a y) h0
theorem language_mismatch_complement {ι : Type*} [Fintype ι] [DecidableEq ι]
(P : ι → ι → ℝ) (hP : ∑ k, ∑ l, P k l = 1) :
∑ k, ∑ l, (if k = l then 0 else P k l) = 1 - ∑ k, P k k := by
have h : ∀ k, ∑ l, (if k = l then 0 else P k l) = ∑ l, P k l - P k k := by
intro k
have h1 : ∀ l, (if k = l then 0 else P k l) = P k l - (if k = l then P k l else 0) := by
intro l
split_ifs <;> simp
simp [h1, Finset.sum_sub_distrib]
simp [h, Finset.sum_sub_distrib, hP]
theorem language_independent_mismatch_bounds {ι : Type*} [Fintype ι] (a b : ι → ℝ)
(ha : ∀ k, 0 ≤ a k) (hb : ∀ k, 0 ≤ b k) (sa : ∑ k, a k = 1) (sb : ∑ k, b k = 1) :
0 ≤ 1 - ∑ k, a k * b k ∧ 1 - ∑ k, a k * b k ≤ 1 := by
have hb1 : ∀ k, b k ≤ 1 := fun k =>
sb ▸ Finset.single_le_sum (fun j _ => hb j) (Finset.mem_univ k)
constructor
· have : ∑ k, a k * b k ≤ ∑ k, a k :=
Finset.sum_le_sum fun k _ => by nlinarith [ha k, hb1 k]
linarith
· have : 0 ≤ ∑ k, a k * b k := Finset.sum_nonneg fun k _ => mul_nonneg (ha k) (hb k)
linarith
def brier (p y : ℝ) : ℝ := (p - y) ^ 2
theorem language_brier_bounds (p y : ℝ) (hp : 0 ≤ p ∧ p ≤ 1) (hy : y = 0 ∨ y = 1) :
0 ≤ brier p y ∧ brier p y ≤ 1 := by
unfold brier
refine ⟨sq_nonneg _, ?_⟩
rcases hy with rfl | rfl <;> nlinarith [hp.1, hp.2]
theorem language_mean_brier_bounds {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (p y : ι → ℝ)
(hp : ∀ i ∈ s, 0 ≤ p i ∧ p i ≤ 1) (hy : ∀ i ∈ s, y i = 0 ∨ y i = 1) :
0 ≤ (∑ i ∈ s, brier (p i) (y i)) / s.card ∧
(∑ i ∈ s, brier (p i) (y i)) / s.card ≤ 1 := by
have hc : (0 : ℝ) < s.card := by exact_mod_cast hs.card_pos
constructor
· exact div_nonneg (Finset.sum_nonneg fun i hi => (language_brier_bounds _ _ (hp i hi) (hy i hi)).1) hc.le
· rw [div_le_one hc]
calc ∑ i ∈ s, brier (p i) (y i) ≤ ∑ _i ∈ s, (1 : ℝ) :=
Finset.sum_le_sum fun i hi => (language_brier_bounds _ _ (hp i hi) (hy i hi)).2
_ = s.card := by simp
theorem language_constant_forecast_decomposition (r p : ℝ) :
r * brier p 1 + (1 - r) * brier p 0 = r * (1 - r) + (p - r) ^ 2 := by
unfold brier
ring
theorem language_base_rate_brier_at_most_quarter (r : ℝ) : r * (1 - r) ≤ 1 / 4 := by
nlinarith [sq_nonneg (r - 1 / 2)]
theorem language_half_forecast_brier (y : ℝ) (hy : y = 0 ∨ y = 1) : brier (1 / 2) y = 1 / 4 := by
unfold brier
rcases hy with rfl | rfl <;> norm_num
theorem language_identical_inputs_brier_floor (p : ℝ) :
1 / 2 ≤ brier p 0 + brier p 1 := by
unfold brier
nlinarith [sq_nonneg (2 * p - 1)]
theorem language_expression_count (n k : ℕ) : Fintype.card (Fin k → Fin n) = n ^ k := by
simp
theorem language_novel_combination_count (n k : ℕ) (H : Finset (Fin k → Fin n)) :
(Finset.univ \ H).card = n ^ k - H.card := by
rw [Finset.card_univ_diff]
simp
theorem language_novel_combination_exists (n k : ℕ) (H : Finset (Fin k → Fin n))
(h : H.card < n ^ k) : ∃ c : Fin k → Fin n, c ∉ H := by
by_contra hc
push_neg at hc
have : (Finset.univ : Finset (Fin k → Fin n)) ⊆ H := fun c _ => hc c
have := Finset.card_le_card this
simp at this
omega
def pairMeaning {ι : Type*} (b : ι → Bool) (i j : ι) (c : Bool) : Bool :=
xor (xor (b i) (b j)) c
theorem language_codebook_flip_invariant {ι : Type*} (b : ι → Bool) (i j : ι) (c : Bool) :
pairMeaning (fun w => !b w) i j c = pairMeaning b i j c := by
unfold pairMeaning
show xor (xor (!b i) (!b j)) c = xor (xor (b i) (b j)) c
generalize b i = x
generalize b j = y
cases x <;> cases y <;> cases c <;> rfl
theorem language_flip_sequence_same_observations {ι : Type*} (Z E : ι → Bool) :
(fun i => xor (Z i) (E i)) = (fun i => xor (!Z i) (!E i)) := by
funext i
cases Z i <;> cases E i <;> rfl
theorem language_no_detector_separates_flip {ι : Type*} (Z E : ι → Bool) (i : ι)
(D : (ι → Bool) → (ι → Bool)) :
D (fun j => xor (Z j) (E j)) ≠ Z ∨
D (fun j => xor (!Z j) (!E j)) ≠ fun j => !Z j := by
by_contra h
push_neg at h
rw [← language_flip_sequence_same_observations, h.1] at h
have := congrFun h.2 i
cases hz : Z i <;> simp [hz] at this
theorem language_same_history_one_world_wrong {H D : Type*} (f : H → D) (h : H) (c1 c2 : D)
(hc : c1 ≠ c2) : f h ≠ c1 ∨ f h ≠ c2 := by
by_contra hh
push_neg at hh
exact hc (hh.1.symm.trans hh.2)
theorem language_fusion_nonzero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
(u v : E) (hu : u ≠ 0) (huv : (2 : ℝ) / 5 ≤ inner ℝ u v) :
u + (17 / 20 : ℝ) • v ≠ 0 := by
intro h
have h2 := norm_add_sq_real u ((17 / 20 : ℝ) • v)
rw [h, norm_zero, real_inner_smul_right] at h2
have h3 : 0 < ‖u‖ := norm_pos_iff.mpr hu
nlinarith [sq_nonneg ‖(17 / 20 : ℝ) • v‖, sq_pos_of_pos h3]
end SentinelTheory
SentinelTheory/Latest.lean
SHA-256 1016eef2165c88340bd323c0b2db14c19a900e0db1ec0c9f0554c6c64afa2153
import SentinelTheory.Signals
import SentinelTheory.Learning
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
noncomputable section
namespace SentinelTheory
def saturatingInterest (relevance exposure tau : ℝ) : ℝ :=
relevance * SentinelProofs.coefficient exposure tau
theorem interest_ceiling (r exposure tau : ℝ) (hr : 0 ≤ r)
(he : 0 ≤ exposure) (ht : 0 < tau) :
0 ≤ saturatingInterest r exposure tau ∧ saturatingInterest r exposure tau ≤ r := by
have hc := SentinelProofs.coefficient_bounds he ht
constructor
· exact mul_nonneg hr hc.1
· simpa [saturatingInterest] using mul_le_mul_of_nonneg_left hc.2 hr
theorem interest_zero_relevance (exposure tau : ℝ) : saturatingInterest 0 exposure tau = 0 := by
simp [saturatingInterest]
theorem interest_increases_with_exposure (r a b tau : ℝ) (hr : 0 ≤ r)
(hab : a ≤ b) (ht : 0 < tau) : saturatingInterest r a tau ≤ saturatingInterest r b tau := by
have hh : -b / tau ≤ -a / tau := div_le_div_of_nonneg_right (by linarith) ht.le
have he := Real.exp_le_exp.mpr hh
unfold saturatingInterest SentinelProofs.coefficient
exact mul_le_mul_of_nonneg_left (by linarith) hr
def effectiveRelevance (r allowance : ℝ) (hardExcluded unresolved : Bool) : ℝ :=
if hardExcluded then 0 else if unresolved then max r allowance else r
theorem hard_constraint_zero_activation (r allowance : ℝ) (unresolved : Bool) :
effectiveRelevance r allowance true unresolved = 0 := by simp [effectiveRelevance]
theorem unresolved_keeps_allowance (r allowance : ℝ) :
allowance ≤ effectiveRelevance r allowance false true := by
simp only [effectiveRelevance, Bool.false_eq_true, if_false, if_true]
exact le_max_right _ _
theorem positive_exploration_can_activate (r allowance exposure tau : ℝ)
(ha : 0 < allowance) (he : 0 < exposure) (ht : 0 < tau) :
0 < saturatingInterest (effectiveRelevance r allowance false true) exposure tau := by
have hr : 0 < effectiveRelevance r allowance false true :=
ha.trans_le (unresolved_keeps_allowance r allowance)
have hneg : -exposure / tau < 0 := div_neg_of_neg_of_pos (by linarith) ht
have hx : Real.exp (-exposure / tau) < 1 := by
simpa using Real.exp_lt_exp.mpr hneg
exact mul_pos hr (sub_pos.mpr hx)
def uniformMoment (n : ℕ) : ℝ := (1 / 4) * ∫ x in (-2 : ℝ)..2, x^n
theorem uniform_second_moment : uniformMoment 2 = 4 / 3 := by
norm_num [uniformMoment, integral_pow]
theorem uniform_fourth_moment : uniformMoment 4 = 16 / 5 := by
norm_num [uniformMoment, integral_pow]
theorem orthogonal_cubic_zero_linear_moment :
uniformMoment 4 - (12 / 5) * uniformMoment 2 = 0 := by
rw [uniform_fourth_moment, uniform_second_moment]
norm_num
theorem cubic_from_intermediate_multiplication (x : ℝ) : (x * x) * x = x^3 := by ring
theorem corroboration_false_positive_bound (p q : ℝ)
(hp : 0 ≤ p) (hq : 0 ≤ q ∧ q ≤ 1) : 0 ≤ p * q ∧ p * q ≤ p := by
exact ⟨mul_nonneg hp hq.1, by simpa using mul_le_mul_of_nonneg_left hq.2 hp⟩
theorem confirming_alerts_are_subset {α : Type*} (initial confirmed : Set α) :
initial ∩ confirmed ⊆ initial := Set.inter_subset_left
end SentinelTheory
SentinelTheory/Learning.lean
SHA-256 de9c2c01a48e27f352f1576184b67131790b39345e9ba3eaeef221c0a0cfbbb2
import SentinelTheory.Dynamics
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Matrix.Mul
import Mathlib.Data.Fintype.Pi
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def xorJoint (delta : ℝ) (a b y : Bool) : ℝ :=
if (Bool.xor a b) = y then (1 - delta) / 4 else delta / 4
theorem noisy_xor_single_feature_blind (delta : ℝ) (a y : Bool) :
(∑ b : Bool, xorJoint delta a b y) = 1 / 4 := by
cases a <;> cases y <;> simp [xorJoint] <;> ring
theorem noisy_xor_other_feature_blind (delta : ℝ) (b y : Bool) :
(∑ a : Bool, xorJoint delta a b y) = 1 / 4 := by
cases b <;> cases y <;> simp [xorJoint] <;> ring
theorem noisy_xor_output_fair (delta : ℝ) (y : Bool) :
(∑ a : Bool, ∑ b : Bool, xorJoint delta a b y) = 1 / 2 := by
simp_rw [noisy_xor_single_feature_blind]
norm_num [Fintype.sum_bool]
theorem noisy_xor_joint_is_informative (delta : ℝ) (hd : delta < 1 / 2) :
1 / 2 < 1 - delta := by linarith
theorem noisy_xor_mass_nonnegative (delta : ℝ) (hd : 0 ≤ delta ∧ delta ≤ 1)
(a b y : Bool) : 0 ≤ xorJoint delta a b y := by
unfold xorJoint
split_ifs
· exact div_nonneg (sub_nonneg.mpr hd.2) (by norm_num)
· exact div_nonneg hd.1 (by norm_num)
theorem noisy_xor_mass_normalized (delta : ℝ) :
(∑ y : Bool, ∑ a : Bool, ∑ b : Bool, xorJoint delta a b y) = 1 := by
simp_rw [noisy_xor_output_fair]
norm_num [Fintype.sum_bool]
theorem xor_is_linear_over_two (a b : Bool) :
(if Bool.xor a b then (1 : ZMod 2) else 0) =
(if a then (1 : ZMod 2) else 0) + (if b then (1 : ZMod 2) else 0) := by
cases a <;> cases b <;> decide
theorem independent_clean_sample_mass (delta : ℝ) (n : ℕ) :
(∏ _i : Fin n, (1 - delta)) = (1 - delta)^n := by simp
theorem two_step_path_composition {ι : Type*} [Fintype ι]
(w : Matrix ι ι ℝ) (a c : ι) :
(w * w) a c = ∑ b, w a b * w b c := by rfl
theorem inverse_certifies_unique_linear_solution {ι : Type*} [Fintype ι] [DecidableEq ι]
(a b : Matrix ι ι (ZMod 2)) (hba : b * a = 1)
(x z y : ι → ZMod 2) (hx : a.mulVec x = y) (hz : a.mulVec z = y) : x = z := by
have h : b.mulVec (a.mulVec x) = b.mulVec (a.mulVec z) := by rw [hx, hz]
simpa [Matrix.mulVec_mulVec, hba] using h
inductive BoolExpr (ι : Type*) where
| constant : Bool → BoolExpr ι
| atom : ι → BoolExpr ι
| negate : BoolExpr ι → BoolExpr ι
| conjunction : BoolExpr ι → BoolExpr ι → BoolExpr ι
def BoolExpr.eval {ι : Type*} : BoolExpr ι → (ι → Bool) → Bool
| .constant b, _ => b
| .atom i, x => x i
| .negate e, x => !(e.eval x)
| .conjunction e f, x => e.eval x && f.eval x
def BoolExpr.disjunction {ι : Type*} (e f : BoolExpr ι) : BoolExpr ι :=
.negate (.conjunction (.negate e) (.negate f))
theorem disjunction_from_and_not {ι : Type*} (e f : BoolExpr ι) (x : ι → Bool) :
(e.disjunction f).eval x = (e.eval x || f.eval x) := by
simp only [BoolExpr.disjunction, BoolExpr.eval]
cases e.eval x <;> cases f.eval x <;> rfl
def BoolExpr.rename {ι κ : Type*} (f : ι → κ) : BoolExpr ι → BoolExpr κ
| .constant b => .constant b
| .atom i => .atom (f i)
| .negate e => .negate (e.rename f)
| .conjunction e g => .conjunction (e.rename f) (g.rename f)
theorem expression_renaming_preserves_meaning {ι κ : Type*} (f : ι → κ)
(e : BoolExpr ι) (x : κ → Bool) : (e.rename f).eval x = e.eval (x ∘ f) := by
induction e with
| constant b => rfl
| atom i => rfl
| negate e ih => simp [BoolExpr.rename, BoolExpr.eval, ih]
| conjunction e g ihe ihg => simp [BoolExpr.rename, BoolExpr.eval, ihe, ihg]
theorem finite_boolean_function_expressible (n : ℕ) :
∀ f : (Fin n → Bool) → Bool, ∃ e : BoolExpr (Fin n), ∀ x, e.eval x = f x := by
induction n with
| zero =>
intro f
refine ⟨.constant (f Fin.elim0), ?_⟩
intro x
have hx : x = Fin.elim0 := by funext i; exact Fin.elim0 i
simp [BoolExpr.eval, hx]
| succ n ih =>
intro f
obtain ⟨low, hl⟩ := ih (fun x => f (Fin.cases false x))
obtain ⟨high, hh⟩ := ih (fun x => f (Fin.cases true x))
let bit : BoolExpr (Fin (n + 1)) := .atom 0
let result := (BoolExpr.conjunction bit (high.rename Fin.succ)).disjunction
(.conjunction (.negate bit) (low.rename Fin.succ))
refine ⟨result, ?_⟩
intro x
have hx : Fin.cases (x 0) (x ∘ Fin.succ) = x := by
funext i
refine Fin.cases ?_ (fun _ => ?_) i <;> rfl
simp only [result, disjunction_from_and_not, BoolExpr.eval,
expression_renaming_preserves_meaning, hl, hh, bit]
cases h : x 0
· simpa [h] using congrArg f hx
· simpa [h] using congrArg f hx
theorem boolean_function_count (n : ℕ) :
Fintype.card ((Fin n → Bool) → Bool) = 2^(2^n) := by simp
theorem three_bit_function_count : Fintype.card ((Fin 3 → Bool) → Bool) = 256 := by
rw [boolean_function_count]
norm_num
def BoolExpr.substitute {ι κ : Type*} (replacement : ι → BoolExpr κ) : BoolExpr ι → BoolExpr κ
| .constant b => .constant b
| .atom i => replacement i
| .negate e => .negate (e.substitute replacement)
| .conjunction e f => .conjunction (e.substitute replacement) (f.substitute replacement)
theorem macro_substitution_preserves_meaning {ι κ : Type*} (e : BoolExpr ι)
(r : ι → BoolExpr κ) (x : κ → Bool) :
(e.substitute r).eval x = e.eval (fun i => (r i).eval x) := by
induction e with
| constant b => rfl
| atom i => rfl
| negate e ih => simp [BoolExpr.substitute, BoolExpr.eval, ih]
| conjunction e f ihe ihf => simp [BoolExpr.substitute, BoolExpr.eval, ihe, ihf]
theorem language_growth_preserves_known {α : Type*} (language additions : Set α) :
language ⊆ language ∪ additions := Set.subset_union_left
theorem finite_expression_in_limit {α : Type*} (language : ℕ → Set α) (n : ℕ) :
language n ⊆ ⋃ k, language k := by
intro e he
exact Set.mem_iUnion.mpr ⟨n, he⟩
end SentinelTheory
SentinelTheory/Pathways.lean
SHA-256 abeb643ef1a39dd7182593110dd00b83ffa4b7ae60f41e65dfaf7db97e2ea476
import SentinelTheory.Dynamics
import Mathlib.Analysis.Matrix
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
noncomputable section
open scoped BigOperators Matrix.Norms.Operator
namespace SentinelTheory
theorem pathway_operator_norm_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
(w : Matrix ι ι ℝ) (rho : ℝ) (hr : 0 ≤ rho)
(hw : ∀ i j, 0 ≤ w i j) (hrow : ∀ i, (∑ j, w i j) ≤ rho) : ‖w‖ ≤ rho := by
let r : NNReal := ⟨rho, hr⟩
rw [Matrix.linfty_opNorm_def]
change ((Finset.univ.sup fun i => ∑ j, ‖w i j‖₊ : NNReal) : ℝ) ≤ (r : ℝ)
apply_mod_cast (show (Finset.univ.sup fun i => ∑ j, ‖w i j‖₊) ≤ r from ?_)
apply Finset.sup_le
intro i _
have h : (∑ j, ‖w i j‖) ≤ rho := by
have he : (∑ j, ‖w i j‖) = ∑ j, w i j :=
Finset.sum_congr rfl (fun j _ => Real.norm_of_nonneg (hw i j))
rw [he]
exact hrow i
apply NNReal.coe_le_coe.mp
simpa [r] using h
theorem pathway_matrix_series_inverse {ι : Type*} [Fintype ι] [DecidableEq ι]
(w : Matrix ι ι ℝ) (rho : ℝ) (hr : 0 ≤ rho) (hr1 : rho < 1)
(hw : ∀ i j, 0 ≤ w i j) (hrow : ∀ i, (∑ j, w i j) ≤ rho) :
(∑' n : ℕ, w^n) = (1 - w)⁻¹ := by
have hn : ‖w‖ < 1 := (pathway_operator_norm_bound w rho hr hw hrow).trans_lt hr1
rw [Matrix.nonsing_inv_eq_ringInverse]
exact geom_series_eq_inverse w hn
theorem pathway_matrix_series_summable {ι : Type*} [Fintype ι] [DecidableEq ι]
(w : Matrix ι ι ℝ) (rho : ℝ) (hr : 0 ≤ rho) (hr1 : rho < 1)
(hw : ∀ i j, 0 ≤ w i j) (hrow : ∀ i, (∑ j, w i j) ≤ rho) :
Summable (fun n : ℕ => w^n) := by
exact summable_geometric_of_norm_lt_one
((pathway_operator_norm_bound w rho hr hw hrow).trans_lt hr1)
theorem pathway_matrix_tail_bound {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι]
(w : Matrix ι ι ℝ) (rho : ℝ) (hr : 0 ≤ rho) (hr1 : rho < 1)
(hw : ∀ i j, 0 ≤ w i j) (hrow : ∀ i, (∑ j, w i j) ≤ rho) (m : ℕ) :
‖∑' n : ℕ, w^(m + 1 + n)‖ ≤ rho^(m + 1) / (1 - rho) := by
have hg : HasSum (fun n : ℕ => rho^(m + 1 + n)) (rho^(m + 1) / (1 - rho)) := by
simp only [pow_add, div_eq_mul_inv]
exact (hasSum_geometric_of_lt_one hr hr1).mul_left _
apply tsum_of_norm_bounded hg
intro n
exact (norm_pow_le w _).trans
(pow_le_pow_left₀ (norm_nonneg w) (pathway_operator_norm_bound w rho hr hw hrow) _)
end SentinelTheory
SentinelTheory/Probability.lean
SHA-256 922df5b1afd29122860b23bf61da5d020579a5d0375fdb7069cadc469eab877b
import SentinelProofs
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
noncomputable section
open scoped BigOperators
namespace SentinelTheory
theorem empirical_update_identity (successes n outcome : ℝ) (hn : 0 < n) :
successes / n + (outcome - successes / n) / (n + 1) =
(successes + outcome) / (n + 1) := by
have h0 : n ≠ 0 := ne_of_gt hn
have h1 : n + 1 ≠ 0 := by linarith
field_simp
ring
theorem empirical_update_bounds (p y n : ℝ) (hp : 0 ≤ p ∧ p ≤ 1)
(hy : 0 ≤ y ∧ y ≤ 1) (hn : 0 ≤ n) :
0 ≤ (n * p + y) / (n + 1) ∧ (n * p + y) / (n + 1) ≤ 1 := by
have hd : 0 < n + 1 := by linarith
constructor
· exact div_nonneg (add_nonneg (mul_nonneg hn hp.1) hy.1) hd.le
· apply (div_le_iff₀ hd).2
nlinarith [mul_le_mul_of_nonneg_left hp.2 hn]
theorem beta_mean_strict_bounds (s f a b : ℝ)
(hs : 0 ≤ s) (hf : 0 ≤ f) (ha : 0 < a) (hb : 0 < b) :
0 < (s + a) / (s + f + a + b) ∧ (s + a) / (s + f + a + b) < 1 := by
have hd : 0 < s + f + a + b := by linarith
constructor
· exact div_pos (by linarith) hd
· apply (div_lt_one hd).2
linarith
theorem beta_variance_expression_nonnegative (s f a b : ℝ)
(hs : 0 ≤ s) (hf : 0 ≤ f) (ha : 0 < a) (hb : 0 < b) :
0 ≤ ((s + a) * (f + b)) /
((s + f + a + b)^2 * (s + f + a + b + 1)) := by
positivity
theorem uniform_beta_unknown : (0 + (1 : ℝ)) / (0 + 0 + 1 + 1) = 1 / 2 := by
norm_num
def evidenceCounts (s f : ℕ) (observed : Option Bool) : ℕ × ℕ :=
match observed with
| none => (s, f)
| some true => (s + 1, f)
| some false => (s, f + 1)
theorem missing_evidence_unchanged (s f : ℕ) : evidenceCounts s f none = (s, f) := rfl
def posterior {ι : Type*} (s : Finset ι) (mass likelihood : ι → ℝ) (i : ι) : ℝ :=
mass i * likelihood i / ∑ j ∈ s, mass j * likelihood j
theorem posterior_nonnegative {ι : Type*} (s : Finset ι) (p l : ι → ℝ)
(hp : ∀ i ∈ s, 0 ≤ p i) (hl : ∀ i ∈ s, 0 ≤ l i)
{i : ι} (hi : i ∈ s) : 0 ≤ posterior s p l i := by
apply div_nonneg (mul_nonneg (hp i hi) (hl i hi))
exact Finset.sum_nonneg fun j hj => mul_nonneg (hp j hj) (hl j hj)
theorem posterior_normalized {ι : Type*} (s : Finset ι) (p l : ι → ℝ)
(hz : 0 < ∑ j ∈ s, p j * l j) : ∑ i ∈ s, posterior s p l i = 1 := by
simp only [posterior, ← Finset.sum_div]
exact div_self (ne_of_gt hz)
theorem zero_prior_stays_zero {ι : Type*} (s : Finset ι) (p l : ι → ℝ)
(i : ι) (hi : p i = 0) : posterior s p l i = 0 := by
simp [posterior, hi]
theorem posterior_uninformative {ι : Type*} (s : Finset ι) (p : ι → ℝ)
(hp : ∑ j ∈ s, p j = 1) (i : ι) : posterior s p (fun _ => 1) i = p i := by
simp [posterior, hp]
theorem mixture_bounds {ι : Type*} (s : Finset ι) (p v : ι → ℝ)
(hp : ∀ i ∈ s, 0 ≤ p i) (hs : ∑ i ∈ s, p i = 1)
(hv : ∀ i ∈ s, 0 ≤ v i ∧ v i ≤ 1) :
0 ≤ ∑ i ∈ s, p i * v i ∧ (∑ i ∈ s, p i * v i) ≤ 1 := by
constructor
· exact Finset.sum_nonneg fun i hi => mul_nonneg (hp i hi) (hv i hi).1
· calc
(∑ i ∈ s, p i * v i) ≤ ∑ i ∈ s, p i := by
apply Finset.sum_le_sum
intro i hi
simpa using mul_le_mul_of_nonneg_left (hv i hi).2 (hp i hi)
_ = 1 := hs
theorem markov_mixture_normalized {ι κ : Type*} (s : Finset ι) (t : Finset κ)
(p : ι → ℝ) (kernel : ι → κ → ℝ) (hp : ∑ i ∈ s, p i = 1)
(hk : ∀ i ∈ s, ∑ j ∈ t, kernel i j = 1) :
(∑ j ∈ t, ∑ i ∈ s, p i * kernel i j) = 1 := by
rw [Finset.sum_comm]
calc
(∑ i ∈ s, ∑ j ∈ t, p i * kernel i j) = ∑ i ∈ s, p i := by
apply Finset.sum_congr rfl
intro i hi
rw [← Finset.mul_sum, hk i hi, mul_one]
_ = 1 := hp
theorem charger_example :
((9 / 10 : ℝ) * (4 / 10)) /
((9 / 10) * (4 / 10) + (2 / 10) * (6 / 10)) = 3 / 4 := by norm_num
theorem propagated_battery_example :
(3 / 4 : ℝ) * (95 / 100) + (1 / 4) * (25 / 100) = 775 / 1000 := by norm_num
theorem propagated_task_example :
(775 / 1000 : ℝ) * (8 / 10) + (225 / 1000) * (1 / 10) = 6425 / 10000 := by norm_num
end SentinelTheory
SentinelTheory/Signals.lean
SHA-256 3f86943920e0bcb30e1fd4510f721b4fcb5cb3934c51117ea365bbe48c16db3d
import SentinelTheory.Dynamics
import Mathlib.Analysis.Fourier.FourierTransform
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
noncomputable section
open MeasureTheory
namespace SentinelTheory
theorem fourier_delay_phase (f : ℝ → ℂ) (delta w : ℝ) :
Fourier.fourierIntegral Real.fourierChar volume (fun t => f (t - delta)) w =
(Real.fourierChar (-delta * w) : ℂ) *
Fourier.fourierIntegral Real.fourierChar volume f w := by
have h := congrFun
(Fourier.fourierIntegral_comp_add_right Real.fourierChar volume f (-delta)) w
simpa [Function.comp_apply, sub_eq_add_neg, Circle.smul_def, smul_eq_mul] using h
theorem fourier_gain_and_delay (f : ℝ → ℂ) (c : ℂ) (delta w : ℝ) :
Fourier.fourierIntegral Real.fourierChar volume (fun t => c * f (t - delta)) w =
c * (Real.fourierChar (-delta * w) : ℂ) *
Fourier.fourierIntegral Real.fourierChar volume f w := by
have h := congrFun (Fourier.fourierIntegral_const_smul Real.fourierChar volume
(fun t => f (t - delta)) c) w
change Fourier.fourierIntegral Real.fourierChar volume (fun t => c * f (t - delta)) w =
c * Fourier.fourierIntegral Real.fourierChar volume (fun t => f (t - delta)) w at h
rw [h, fourier_delay_phase]
ring
theorem cross_spectrum_factorization (x gain phase : ℂ) :
(starRingEnd ℂ) x * (gain * phase * x) = gain * (Complex.normSq x : ℂ) * phase := by
rw [Complex.normSq_eq_conj_mul_self]
ring
def forcedTrace (initial t0 tau : ℝ) (u : ℝ → ℝ) (t : ℝ) : ℝ :=
Real.exp (-t / tau) * (Real.exp (t0 / tau) * initial +
(1 / tau) * ∫ s in t0..t, Real.exp (s / tau) * u s)
theorem forced_trace_initial_value (initial t0 tau : ℝ) (u : ℝ → ℝ) :
forcedTrace initial t0 tau u t0 = initial := by
have he : Real.exp (-t0 / tau) * Real.exp (t0 / tau) = 1 := by
rw [← Real.exp_add]
have h : -t0 / tau + t0 / tau = 0 := by ring
rw [h, Real.exp_zero]
simp only [forcedTrace, intervalIntegral.integral_same, mul_zero, add_zero]
rw [← mul_assoc, he, one_mul]
theorem forced_trace_convolution (initial t0 tau : ℝ) (u : ℝ → ℝ) (t : ℝ) :
forcedTrace initial t0 tau u t =
Real.exp (-(t - t0) / tau) * initial +
(1 / tau) * ∫ s in t0..t, Real.exp (-(t - s) / tau) * u s := by
have he (s : ℝ) : Real.exp (-(t - s) / tau) =
Real.exp (-t / tau) * Real.exp (s / tau) := by
rw [← Real.exp_add]
congr 1
ring
simp only [he, mul_assoc, intervalIntegral.integral_const_mul, forcedTrace]
ring
theorem forced_trace_solves_relaxation (initial t0 tau : ℝ) (u : ℝ → ℝ)
(hu : Continuous u) (htau : tau ≠ 0) (t : ℝ) :
HasDerivAt (forcedTrace initial t0 tau u)
((u t - forcedTrace initial t0 tau u t) / tau) t := by
have hc : Continuous (fun s : ℝ => Real.exp (s / tau) * u s) :=
((continuous_id.div_const tau).rexp).mul hu
have hi := intervalIntegral.integral_hasDerivAt_right (a := t0) (b := t)
(hc.intervalIntegrable _ _) hc.aestronglyMeasurable.stronglyMeasurableAtFilter hc.continuousAt
have he := (((hasDerivAt_id t).neg).div_const tau).exp
have hp := he.mul ((hasDerivAt_const t (Real.exp (t0 / tau) * initial)).add
(hi.const_mul (1 / tau)))
have hcancel : Real.exp (-t / tau) * Real.exp (t / tau) = 1 := by
rw [← Real.exp_add]
have h : -t / tau + t / tau = 0 := by ring
rw [h, Real.exp_zero]
convert hp using 1
dsimp [forcedTrace]
have hscaled := congrArg (fun z : ℝ => z * u t * tau) hcancel
simp only [neg_div] at hscaled
field_simp
nlinarith [hscaled]
end SentinelTheory
SentinelTheory/Structure.lean
SHA-256 63a131c02a40ec2000f946e162a62951015912159ef1b1d173267b6ca2e47dd8
import SentinelTheory.Probability
import Mathlib.Data.Finset.Lattice.Fold
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def Feasible {ι : Type*} (required supply : ι → ℝ) : Prop := ∀ i, required i ≤ supply i
theorem feasibility_monotone {ι : Type*} (r s t : ι → ℝ)
(hs : Feasible r s) (hst : ∀ i, s i ≤ t i) : Feasible r t := by
intro i
exact (hs i).trans (hst i)
theorem adding_resources_preserves_feasibility {ι : Type*} (r s extra : ι → ℝ)
(hs : Feasible r s) (he : ∀ i, 0 ≤ extra i) :
Feasible r (fun i => s i + extra i) := by
apply feasibility_monotone r s _ hs
intro i
linarith [he i]
def truthIndicator (p : Prop) : ℝ := by
classical
exact if p then 1 else 0
theorem indicator_bounds (p : Prop) : 0 ≤ truthIndicator p ∧ truthIndicator p ≤ 1 := by
classical
by_cases h : p <;> simp [truthIndicator, h]
theorem indicator_monotone {p q : Prop} (h : p → q) : truthIndicator p ≤ truthIndicator q := by
classical
by_cases hp : p
· simp [truthIndicator, hp, h hp]
· simp [truthIndicator, hp]
exact (indicator_bounds q).1
theorem feasibility_gain_bounds {ι : Type*} (r s extra : ι → ℝ)
(he : ∀ i, 0 ≤ extra i) :
0 ≤ truthIndicator (Feasible r (fun i => s i + extra i)) - truthIndicator (Feasible r s) ∧
truthIndicator (Feasible r (fun i => s i + extra i)) - truthIndicator (Feasible r s) ≤ 1 := by
have hm := indicator_monotone (adding_resources_preserves_feasibility r s extra · he)
have ha := indicator_bounds (Feasible r (fun i => s i + extra i))
have hb := indicator_bounds (Feasible r s)
constructor <;> linarith
theorem product_unit_bounds {a b : ℝ} (ha : 0 ≤ a ∧ a ≤ 1) (hb : 0 ≤ b ∧ b ≤ 1) :
0 ≤ a * b ∧ a * b ≤ 1 := by
constructor
· exact mul_nonneg ha.1 hb.1
· calc
a * b ≤ a * 1 := mul_le_mul_of_nonneg_left hb.2 ha.1
_ ≤ 1 := by simpa using ha.2
theorem opportunity_relevance_bounds {q v gain : ℝ}
(hq : 0 ≤ q ∧ q ≤ 1) (hv : 0 ≤ v ∧ v ≤ 1) (hg : 0 ≤ gain ∧ gain ≤ 1) :
0 ≤ q * v * gain ∧ q * v * gain ≤ 1 :=
product_unit_bounds (product_unit_bounds hq hv) hg
def RouteFeasible {ι : Type*} (routes : Set (Set ι)) (available : Set ι) : Prop :=
∃ route ∈ routes, route ⊆ available
theorem alternative_routes_monotone {ι : Type*} (routes : Set (Set ι))
(a b : Set ι) (hab : a ⊆ b) (ha : RouteFeasible routes a) : RouteFeasible routes b := by
obtain ⟨r, hr, hra⟩ := ha
exact ⟨r, hr, hra.trans hab⟩
theorem new_route_preserves_possibilities {ι : Type*} (old new : Set (Set ι))
(a : Set ι) (h : old ⊆ new) (ha : RouteFeasible old a) : RouteFeasible new a := by
obtain ⟨r, hr, hra⟩ := ha
exact ⟨r, h hr, hra⟩
theorem missing_requirements_shrink {ι : Type*} (r a b : Set ι) (h : a ⊆ b) :
r \ b ⊆ r \ a := by
intro i hi
exact ⟨hi.1, fun ha => hi.2 (h ha)⟩
theorem failure_of_one_route_allows_another (a b c d : Prop) (h : c ∧ d) :
(a ∧ b) ∨ (c ∧ d) := Or.inr h
theorem action_does_not_identify_preference :
¬ Function.Injective (fun p : Bool × Bool => p.1 && p.2) := by
intro h
have he : (true, false) = (false, true) := h (by decide)
have impossible : true = false := congrArg Prod.fst he
cases impossible
theorem identical_observations_cannot_decode_distinct_targets
{World Obs Target : Type*} (observe : World → Obs) (target : World → Target)
(x y : World) (ho : observe x = observe y) (ht : target x ≠ target y) :
¬ ∃ decoder : Obs → Target, decoder (observe x) = target x ∧ decoder (observe y) = target y := by
rintro ⟨decoder, hx, hy⟩
apply ht
calc
target x = decoder (observe x) := hx.symm
_ = decoder (observe y) := congrArg decoder ho
_ = target y := hy
theorem refinement_preserves_old_representation {H A B : Type*}
(phi : H → A) (g : H → B) (h : H) : (phi h, g h).1 = phi h := rfl
theorem refinement_separates_distinctions {H A B : Type*}
(phi : H → A) (g : H → B) (x y : H) (hg : g x ≠ g y) :
(phi x, g x) ≠ (phi y, g y) := by
intro h
exact hg (congrArg Prod.snd h)
theorem fixed_representation_cannot_predict_different_futures {H A B : Type*}
(phi : H → A) (future : H → B) (x y : H)
(hphi : phi x = phi y) (hf : future x ≠ future y) :
¬ ∃ predictor : A → B, predictor (phi x) = future x ∧ predictor (phi y) = future y :=
identical_observations_cannot_decode_distinct_targets phi future x y hphi hf
theorem unknown_zero_gate_blocks_activity (river interest : ℝ) : river * 0 * interest = 0 := by ring
theorem net_gain_positive_iff (benefit complexity compute : ℝ) :
0 < benefit - complexity - compute ↔ complexity + compute < benefit := by
constructor <;> intro h <;> linarith
theorem uniform_coverage_budget {ι : Type*} (all selected : Finset ι) (k : ℕ)
(hk : selected.card ≤ k) (hall : 0 < all.card) :
(selected.card : ℝ) / all.card ≤ (k : ℝ) / all.card := by
apply div_le_div_of_nonneg_right
· exact_mod_cast hk
· positivity
theorem information_can_be_ignored {Obs Decision : Type*}
(observations : Finset Obs) (decisions : Finset Decision) (hd : decisions.Nonempty)
(p : Obs → ℝ) (u : Obs → Decision → ℝ) (hp : ∀ o ∈ observations, 0 ≤ p o) :
decisions.sup' hd (fun d => ∑ o ∈ observations, p o * u o d) ≤
∑ o ∈ observations, p o * decisions.sup' hd (u o) := by
apply Finset.sup'_le
intro d hdmem
apply Finset.sum_le_sum
intro o hom
apply mul_le_mul_of_nonneg_left _ (hp o hom)
exact Finset.le_sup' (u o) hdmem
end SentinelTheory
SentinelTheory/Timing.lean
SHA-256 bf2f02c6529ac6e65694e3763d7232d645252607719ae67e261117f18a52d82c
import SentinelTheory.Latest
import Mathlib.Data.Fintype.Pi
import Mathlib.Data.Fintype.Card
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Algebra.Ring.Periodic
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def clockMap (a b t : ℝ) : ℝ := a * t + b
theorem timing_clock_compose (a1 b1 a2 b2 t : ℝ) :
clockMap a2 b2 (clockMap a1 b1 t) = clockMap (a2 * a1) (a2 * b1 + b2) t := by
unfold clockMap; ring
theorem timing_clock_inverse (a b t : ℝ) (ha : a ≠ 0) :
clockMap (1 / a) (-b / a) (clockMap a b t) = t ∧
clockMap a b (clockMap (1 / a) (-b / a) t) = t := by
unfold clockMap
constructor <;> field_simp <;> ring
theorem timing_offset_latency_not_identifiable (a beta ell d t : ℝ) :
a * t + beta + ell = a * t + (beta + d) + (ell - d) := by ring
theorem timing_clock_error_bound (a a' b b' ea eb T t : ℝ)
(hA : |a - a'| ≤ ea) (hB : |b - b'| ≤ eb) (ht0 : 0 ≤ t) (htT : t ≤ T) :
|clockMap a b t - clockMap a' b' t| ≤ ea * T + eb := by
unfold clockMap
have h1 : a * t + b - (a' * t + b') = (a - a') * t + (b - b') := by ring
rw [h1]
have h2 : |(a - a') * t| ≤ ea * T := by
rw [abs_mul, abs_of_nonneg ht0]
exact mul_le_mul hA htT ht0 ((abs_nonneg _).trans hA)
exact (abs_add_le _ _).trans (add_le_add h2 hB)
theorem timing_periodic_shift_indistinguishable (f : ℝ → ℝ) (P : ℝ) (hf : Function.Periodic f P)
(k : ℤ) (t : ℝ) : f (t + k * P) = f t :=
hf.int_mul k t
theorem timing_decay_semigroup (lam h a b : ℝ) :
Real.exp (-lam * (a + b)) * h = Real.exp (-lam * b) * (Real.exp (-lam * a) * h) := by
rw [mul_add, Real.exp_add]; ring
theorem timing_decay_bounded_between_updates (lam h0 s t : ℝ) (hl : 0 ≤ lam) (hh : 0 ≤ h0)
(hst : s ≤ t) :
0 ≤ Real.exp (-lam * t) * h0 ∧ Real.exp (-lam * t) * h0 ≤ Real.exp (-lam * s) * h0 := by
refine ⟨mul_nonneg (Real.exp_pos _).le hh, ?_⟩
apply mul_le_mul_of_nonneg_right _ hh
exact Real.exp_le_exp.mpr (by nlinarith)
theorem timing_wake_time_hits_threshold (R tc theta : ℝ) (htc : 0 < tc) (h0 : 0 < theta)
(hR : theta < R) :
R * (1 - Real.exp (-(-tc * Real.log (1 - theta / R)) / tc)) = theta := by
have hR0 : 0 < R := h0.trans hR
have hp : 0 < 1 - theta / R := by
have : theta / R < 1 := (div_lt_one hR0).mpr hR
linarith
have : -(-tc * Real.log (1 - theta / R)) / tc = Real.log (1 - theta / R) := by
field_simp
rw [this, Real.exp_log hp]
field_simp
ring
theorem timing_wake_time_nonneg (R tc theta : ℝ) (htc : 0 < tc) (h0 : 0 < theta) (hR : theta < R) :
0 ≤ -tc * Real.log (1 - theta / R) := by
have hR0 : 0 < R := h0.trans hR
have hp : 0 < 1 - theta / R := by
have : theta / R < 1 := (div_lt_one hR0).mpr hR
linarith
have hq : 1 - theta / R ≤ 1 := by
have : 0 ≤ theta / R := div_nonneg h0.le hR0.le
linarith
have := Real.log_nonpos hp.le hq
nlinarith
theorem timing_value_of_computation_nonneg {Z D : Type*} [Fintype Z] [Fintype D] [Nonempty D]
(p : Z → ℝ) (u : Z → D → ℝ) (hp : ∀ z, 0 ≤ p z) :
Finset.univ.sup' Finset.univ_nonempty (fun d => ∑ z, p z * u z d) ≤
∑ z, p z * Finset.univ.sup' Finset.univ_nonempty (u z) := by
apply Finset.sup'_le
intro d _
apply Finset.sum_le_sum
intro z _
exact mul_le_mul_of_nonneg_left (Finset.le_sup' (u z) (Finset.mem_univ d)) (hp z)
theorem timing_compute_only_if_gain_exceeds_cost (p v c : ℝ) :
0 < p * v - c ↔ c < p * v := sub_pos
theorem timing_budget_active_count_bound {ι : Type*} (S : Finset ι) (c : ι → ℝ) (c0 B : ℝ)
(hc : ∀ i ∈ S, c0 ≤ c i) (hc0 : 0 < c0) (hB : ∑ i ∈ S, c i ≤ B) :
(S.card : ℝ) ≤ B / c0 := by
rw [le_div_iff₀ hc0]
calc (S.card : ℝ) * c0 = ∑ _i ∈ S, c0 := by simp
_ ≤ ∑ i ∈ S, c i := Finset.sum_le_sum hc
_ ≤ B := hB
theorem timing_budget_subset_feasible {ι : Type*} (S T : Finset ι) (c : ι → ℝ) (B : ℝ)
(hc : ∀ i, 0 ≤ c i) (hST : S ⊆ T) (hT : ∑ i ∈ T, c i ≤ B) : ∑ i ∈ S, c i ≤ B :=
(Finset.sum_le_sum_of_subset_of_nonneg hST (fun i _ _ => hc i)).trans hT
theorem timing_budget_shrink_drops_member {ι : Type*} [DecidableEq ι] (S : Finset ι) (c : ι → ℝ) (B : ℝ)
(j : ι) (hj : j ∈ S) (hB : ∑ i ∈ S, c i ≤ B) :
∑ i ∈ S.erase j, c i ≤ B - c j := by
have := Finset.add_sum_erase S c hj
linarith
theorem timing_beta_estimate_open_unit (s f : ℝ) (hs : 0 ≤ s) (hf : 0 ≤ f) :
0 < (1 + s) / (3 + s + f) ∧ (1 + s) / (3 + s + f) < 1 := by
constructor
· positivity
· rw [div_lt_one (by positivity)]; linarith
theorem timing_beta_estimate_monotone_in_successes (s s' f : ℝ) (hs : 0 ≤ s) (hss : s ≤ s')
(hf : 0 ≤ f) : (1 + s) / (3 + s + f) ≤ (1 + s') / (3 + s' + f) := by
have hs' : 0 ≤ s' := hs.trans hss
rw [div_le_div_iff₀ (by positivity) (by positivity)]
nlinarith
theorem timing_suspend_discount_le (g V : ℝ) (n m : ℕ) (hg0 : 0 ≤ g) (hg1 : g ≤ 1) (hV : 0 ≤ V)
(hnm : n ≤ m) : g ^ m * V ≤ g ^ n * V ∧ g ^ n * V ≤ V := by
constructor
· exact mul_le_mul_of_nonneg_right (pow_le_pow_of_le_one hg0 hg1 hnm) hV
· have := pow_le_one₀ hg0 hg1 (n := n)
nlinarith
theorem timing_compression_pigeonhole (N B : ℕ)
(enc : (Fin N → Bool) → (Fin B → Bool)) (hinj : Function.Injective enc) : N ≤ B := by
have h := Fintype.card_le_of_injective enc hinj
simp only [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin] at h
exact (Nat.pow_le_pow_iff_right (by norm_num)).mp h
theorem timing_compression_not_injective (N B : ℕ) (hBN : B < N) :
¬ ∃ enc : (Fin N → Bool) → (Fin B → Bool), Function.Injective enc := by
rintro ⟨enc, hinj⟩
exact absurd (timing_compression_pigeonhole N B enc hinj) (by omega)
theorem timing_inspect_budget_success_bound (N B : ℕ) (S : Finset (Fin N)) (hS : S.card ≤ B)
(hN : 0 < N) : (S.card : ℝ) / N ≤ (B : ℝ) / N := by
apply div_le_div_of_nonneg_right _ (by exact_mod_cast hN.le)
exact_mod_cast hS
theorem timing_effective_sample_size_bounds (n rho : ℝ) (hn : 1 ≤ n) (h0 : 0 ≤ rho)
(h1 : rho ≤ 1) : 1 ≤ n / (1 + (n - 1) * rho) ∧ n / (1 + (n - 1) * rho) ≤ n := by
have hd : 0 < 1 + (n - 1) * rho := by nlinarith
constructor
· rw [le_div_iff₀ hd]; nlinarith
· rw [div_le_iff₀ hd]; nlinarith [mul_nonneg (mul_nonneg (by linarith : (0:ℝ) ≤ n) (by linarith : (0:ℝ) ≤ n - 1)) h0]
theorem timing_effective_sample_size_independent (n : ℝ) :
n / (1 + (n - 1) * 0) = n := by simp
theorem timing_effective_sample_size_decreasing (n r r' : ℝ) (hn : 1 ≤ n) (h0 : 0 ≤ r)
(hr : r ≤ r') : n / (1 + (n - 1) * r') ≤ n / (1 + (n - 1) * r) := by
have h1 : 0 < 1 + (n - 1) * r := by nlinarith
apply div_le_div_of_nonneg_left (by linarith) h1
nlinarith
end SentinelTheory
SentinelTheory/Values.lean
SHA-256 8f8d0f6e5e69b8b7b7fdc7eb8642fec1200b4671d27464eabec2b882737999bb
import SentinelTheory.Probability
import SentinelTheory.Structure
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.Data.Fintype.Perm
import Mathlib.Analysis.SpecificLimits.Basic
noncomputable section
open scoped BigOperators
namespace SentinelTheory
def valueTentativeUtility (B CF CI p : ℝ) : ℝ := p * B - (1 - p) * CF - CI
theorem value_tentative_threshold (B CF CI p : ℝ) :
0 < valueTentativeUtility B CF CI p ↔ CF + CI < p * (B + CF) := by
unfold valueTentativeUtility
constructor <;> intro h <;> linarith
theorem value_tentative_monotone (B B' CF CF' CI CI' p p' : ℝ)
(hp : 0 ≤ p) (hpp : p ≤ p') (hp1 : p' ≤ 1) (hB : 0 ≤ B) (hBB : B ≤ B')
(hCF : 0 ≤ CF') (hCC : CF' ≤ CF) (hCI : CI' ≤ CI) :
valueTentativeUtility B CF CI p ≤ valueTentativeUtility B' CF' CI' p' := by
unfold valueTentativeUtility
nlinarith [mul_le_mul hpp hBB hB (hp.trans hpp),
mul_le_mul (sub_le_sub_left hpp 1) hCC hCF (sub_nonneg.mpr (hpp.trans hp1))]
theorem value_interrupt_rule_monotone (v v' c c' : ℝ) (hv : v ≤ v') (hc : c' ≤ c)
(h : c < v) : c' < v' := lt_of_le_of_lt hc (lt_of_lt_of_le h hv)
theorem value_optimal_with_silence_nonneg {ι : Type*} [Finite ι] (u : Option ι → ℝ)
(hsilent : u none = 0) : ∃ a, (∀ b, u b ≤ u a) ∧ 0 ≤ u a := by
haveI : Nonempty (Option ι) := ⟨none⟩
obtain ⟨a, ha⟩ := Finite.exists_max u
exact ⟨a, ha, hsilent ▸ ha none⟩
theorem value_unconstrained_threshold_optimal {ι : Type*} (s : Finset ι) (A Y : ι → ℝ)
(h0 : ∀ i ∈ s, 0 ≤ A i) (h1 : ∀ i ∈ s, A i ≤ 1) :
∑ i ∈ s, A i * Y i ≤ ∑ i ∈ s, max (Y i) 0 := by
apply Finset.sum_le_sum
intro i hi
rcases le_total (Y i) 0 with hy | hy
· rw [max_eq_right hy]
nlinarith [h0 i hi]
· rw [max_eq_left hy]
nlinarith [h1 i hi]
theorem value_gated_budget_value_bound {ι : Type*} (s : Finset ι) (A Y P : ι → ℝ)
(M B : ℝ) (hM : 0 ≤ M) (h0 : ∀ i ∈ s, 0 ≤ A i)
(hP : ∀ i ∈ s, A i ≤ P i) (hY : ∀ i ∈ s, Y i ≤ M)
(hB : ∑ i ∈ s, A i ≤ B) : ∑ i ∈ s, A i * Y i ≤ B * M ∧ ∀ i ∈ s, P i = 0 → A i = 0 := by
constructor
· calc
∑ i ∈ s, A i * Y i ≤ ∑ i ∈ s, A i * M :=
Finset.sum_le_sum fun i hi => mul_le_mul_of_nonneg_left (hY i hi) (h0 i hi)
_ = (∑ i ∈ s, A i) * M := by rw [Finset.sum_mul]
_ ≤ B * M := mul_le_mul_of_nonneg_right hB hM
· intro i hi hp
exact le_antisymm (hp ▸ hP i hi) (h0 i hi)
def valueObservedHistory (y : ℤ) (act : ℕ → Bool) : ℕ → Option ℤ :=
fun t => if act t then some y else none
theorem value_silent_history_hides_sign (act : ℕ → Bool) (hs : ∀ t, act t = false) :
valueObservedHistory 7 act = valueObservedHistory (-7) act ∧
¬ ∃ decoder : (ℕ → Option ℤ) → ℤ,
decoder (valueObservedHistory 7 act) = 7 ∧ decoder (valueObservedHistory (-7) act) = -7 := by
have he : valueObservedHistory 7 act = valueObservedHistory (-7) act := by
funext t
simp [valueObservedHistory, hs t]
refine ⟨he, ?_⟩
exact identical_observations_cannot_decode_distinct_targets
(fun y : ℤ => valueObservedHistory y act) (fun y => y) 7 (-7) he (by norm_num)
theorem value_selective_feedback_bias (P f1 f0 : ℝ) (hP0 : 0 < P) (hP1 : P < 1)
(h1 : 0 < f1) (h0 : 0 < f0) :
P * f1 / (P * f1 + (1 - P) * f0) = P ↔ f1 = f0 := by
have hd : 0 < P * f1 + (1 - P) * f0 := by nlinarith [mul_pos hP0 h1, mul_pos (sub_pos.mpr hP1) h0]
rw [div_eq_iff hd.ne']
constructor
· intro h
have : (1 - P) * (f1 - f0) = 0 := by nlinarith [h]
rcases mul_eq_zero.mp this with h' | h'
· exact absurd h' (sub_pos.mpr hP1).ne'
· linarith
· intro h
subst h
ring
theorem value_joint_survival_factorization (nE nYE nYD : ℝ) (h : nYE ≠ 0) :
nYD / nE = (nYE / nE) * (nYD / nYE) := by
by_cases hE : nE = 0
· simp [hE]
· field_simp
theorem value_exponential_survival_bounds (Λ : ℝ) (h : 0 ≤ Λ) :
0 < Real.exp (-Λ) ∧ Real.exp (-Λ) ≤ 1 :=
⟨Real.exp_pos _, Real.exp_le_one_iff.mpr (by linarith)⟩
theorem value_survival_decreases_with_delay (lam : ℝ → ℝ) (t d1 d2 : ℝ)
(hc : Continuous lam) (hn : ∀ u, 0 ≤ lam u) (h1 : 0 ≤ d1) (h12 : d1 ≤ d2) :
Real.exp (-∫ u in t..t + d2, lam u) ≤ Real.exp (-∫ u in t..t + d1, lam u) := by
apply Real.exp_le_exp.mpr
have := intervalIntegral.integral_mono_interval (μ := MeasureTheory.volume)
(f := lam) (a := t) (b := t + d1) (c := t) (d := t + d2) le_rfl
(by linarith) (by linarith) (Filter.Eventually.of_forall hn)
(hc.intervalIntegrable _ _)
linarith
theorem value_waiting_cannot_raise_utility (B CF CI p S : ℝ) (hB : 0 ≤ B + CF)
(hS1 : S ≤ 1) (hp : 0 ≤ p) :
valueTentativeUtility B CF CI (p * S) ≤ valueTentativeUtility B CF CI p ∧ p * S ≤ p := by
have hps : p * S ≤ p := by nlinarith
refine ⟨?_, hps⟩
unfold valueTentativeUtility
nlinarith [mul_nonneg (sub_nonneg.mpr hps) hB]
theorem value_verification_posterior_bounds (r q f : ℝ) (hr : 0 ≤ r ∧ r ≤ 1)
(hq : 0 ≤ q ∧ q ≤ 1) (hf : 0 ≤ f ∧ f ≤ 1) (hd : 0 < r * q + (1 - r) * f) :
0 ≤ r * q / (r * q + (1 - r) * f) ∧ r * q / (r * q + (1 - r) * f) ≤ 1 := by
have h1 : 0 ≤ (1 - r) * f := mul_nonneg (sub_nonneg.mpr hr.2) hf.1
exact ⟨div_nonneg (mul_nonneg hr.1 hq.1) hd.le, (div_le_one hd).mpr (by linarith)⟩
theorem value_verification_posterior_vs_prior (r q f : ℝ) (hr : 0 ≤ r ∧ r ≤ 1)
(hqf : f ≤ q) (hd : 0 < r * q + (1 - r) * f) :
r ≤ r * q / (r * q + (1 - r) * f) := by
rw [le_div_iff₀ hd]
nlinarith [mul_nonneg (mul_nonneg hr.1 (sub_nonneg.mpr hr.2)) (sub_nonneg.mpr hqf)]
theorem value_verification_posterior_mean (r q f : ℝ)
(hp : 0 < r * q + (1 - r) * f) (hm : 0 < r * (1 - q) + (1 - r) * (1 - f)) :
(r * q + (1 - r) * f) * (r * q / (r * q + (1 - r) * f)) +
(r * (1 - q) + (1 - r) * (1 - f)) *
(r * (1 - q) / (r * (1 - q) + (1 - r) * (1 - f))) = r ∧
(r * q + (1 - r) * f) + (r * (1 - q) + (1 - r) * (1 - f)) = 1 := by
constructor
· rw [mul_div_cancel₀ _ hp.ne', mul_div_cancel₀ _ hm.ne']
ring
· ring
theorem value_two_outcome_option_value (w1 w2 a b : ℝ) (h1 : 0 ≤ w1) (h2 : 0 ≤ w2) : max 0 (w1 * a + w2 * b) ≤ w1 * max 0 a + w2 * max 0 b := by
apply max_le
· exact add_nonneg (mul_nonneg h1 (le_max_left _ _)) (mul_nonneg h2 (le_max_left _ _))
· exact add_le_add (mul_le_mul_of_nonneg_left (le_max_right _ _) h1)
(mul_le_mul_of_nonneg_left (le_max_right _ _) h2)
theorem value_verification_never_worse_before_cost (B CF CI r q f : ℝ)
(hp : 0 < r * q + (1 - r) * f) (hm : 0 < r * (1 - q) + (1 - r) * (1 - f))
(hP : 0 ≤ r * q + (1 - r) * f) (hM : 0 ≤ r * (1 - q) + (1 - r) * (1 - f)) :
max 0 (valueTentativeUtility B CF CI r) ≤
(r * q + (1 - r) * f) *
max 0 (valueTentativeUtility B CF CI (r * q / (r * q + (1 - r) * f))) +
(r * (1 - q) + (1 - r) * (1 - f)) *
max 0 (valueTentativeUtility B CF CI
(r * (1 - q) / (r * (1 - q) + (1 - r) * (1 - f)))) := by
obtain ⟨hmean, hsum⟩ := value_verification_posterior_mean r q f hp hm
have key : valueTentativeUtility B CF CI r =
(r * q + (1 - r) * f) *
valueTentativeUtility B CF CI (r * q / (r * q + (1 - r) * f)) +
(r * (1 - q) + (1 - r) * (1 - f)) *
valueTentativeUtility B CF CI
(r * (1 - q) / (r * (1 - q) + (1 - r) * (1 - f))) := by
unfold valueTentativeUtility
set x := r * q / (r * q + (1 - r) * f)
set y := r * (1 - q) / (r * (1 - q) + (1 - r) * (1 - f))
set u := r * q + (1 - r) * f
set v := r * (1 - q) + (1 - r) * (1 - f)
have : (u * x + v * y) = r := hmean
linear_combination (-(B + CF)) * this + (CF + CI) * hsum
rw [key]
exact value_two_outcome_option_value _ _ _ _ hP hM
theorem value_filter_step_normalized {ι : Type*} (s : Finset ι) (p L : ι → ℝ)
(T : ι → ι → ℝ) (hp : ∑ i ∈ s, p i = 1) (hT0 : ∀ i ∈ s, ∀ j ∈ s, 0 ≤ T i j)
(hT : ∀ i ∈ s, ∑ j ∈ s, T i j = 1) (hp0 : ∀ i ∈ s, 0 ≤ p i)
(hL : ∀ i ∈ s, 0 ≤ L i)
(hz : 0 < ∑ j ∈ s, (∑ i ∈ s, p i * T i j) * L j) :
∑ j ∈ s, ∑ i ∈ s, p i * T i j = 1 ∧
∑ j ∈ s, posterior s (fun j => ∑ i ∈ s, p i * T i j) L j = 1 ∧
∀ j ∈ s, 0 ≤ posterior s (fun j => ∑ i ∈ s, p i * T i j) L j ∧
posterior s (fun j => ∑ i ∈ s, p i * T i j) L j ≤ 1 := by
have hpred : ∀ j ∈ s, 0 ≤ ∑ i ∈ s, p i * T i j := fun j hj =>
Finset.sum_nonneg fun i hi => mul_nonneg (hp0 i hi) (hT0 i hi j hj)
refine ⟨markov_mixture_normalized s s p T hp hT, posterior_normalized s _ L hz, fun j hj => ⟨posterior_nonnegative s _ L hpred hL hj, ?_⟩⟩
have hn := posterior_normalized s (fun j => ∑ i ∈ s, p i * T i j) L hz
have hnn : ∀ k ∈ s, 0 ≤ posterior s (fun j => ∑ i ∈ s, p i * T i j) L k :=
fun k hk => posterior_nonnegative s _ L hpred hL hk
calc posterior s (fun j => ∑ i ∈ s, p i * T i j) L j
≤ ∑ k ∈ s, posterior s (fun j => ∑ i ∈ s, p i * T i j) L k :=
Finset.single_le_sum hnn hj
_ = 1 := hn
theorem value_rotation_nonidentifiable :
(fun z : ZMod 4 => z + 1) (0 : ZMod 4) = (fun z : ZMod 4 => z) ((0 : ZMod 4) + 1) ∧
((0 : ZMod 4) ≠ (0 : ZMod 4) + 1) := by
decide
theorem value_flip_nonidentifiable (f : Bool → ℝ) (v : Bool) :
(fun w => f (!w)) (!v) = f v := by
simp
theorem value_alignment_candidate_count : Fintype.card (Equiv.Perm (Fin 4)) = 24 := by
rw [Fintype.card_perm, Fintype.card_fin]
rfl
theorem value_blocked_action_value_survives (v a : ℝ) (hv : 0 < v) (ha : a < 1) (hv1 : v ≤ 1) :
0 < v * (1 - a) / (1 - v * a) ∧
v * (1 - a) / (1 - v * a) + (1 - v) * a / (1 - v * a) + (1 - v) * (1 - a) / (1 - v * a) = 1 := by
have hva : v * a < 1 := by nlinarith
have hd : 0 < 1 - v * a := by linarith
refine ⟨div_pos (mul_pos hv (by linarith)) hd, ?_⟩
rw [← add_div, ← add_div, div_eq_one_iff_eq hd.ne']
ring
theorem value_equal_likelihood_posterior_is_prior (π l : ℝ) (hl : 0 < l) :
π * l / (π * l + (1 - π) * l) = π := by
have : π * l + (1 - π) * l = l := by ring
rw [this]
field_simp
theorem value_pursuit_switch_deviation (q h : ℝ) :
((1 - h) * q + h * (1 - q)) - 1 / 2 = (1 - 2 * h) * (q - 1 / 2) := by ring
theorem value_pursuit_switch_contracts (q h : ℝ) (hh : 0 ≤ h ∧ h ≤ 1) :
|((1 - h) * q + h * (1 - q)) - 1 / 2| ≤ |q - 1 / 2| := by
rw [value_pursuit_switch_deviation, abs_mul]
have : |1 - 2 * h| ≤ 1 := abs_le.mpr ⟨by linarith, by linarith⟩
nlinarith [abs_nonneg (q - 1 / 2), abs_nonneg (1 - 2 * h)]
def valueSwitchIter (h : ℝ) (q0 : ℝ) : ℕ → ℝ
| 0 => q0
| n + 1 => (1 - h) * valueSwitchIter h q0 n + h * (1 - valueSwitchIter h q0 n)
theorem value_pursuit_switch_iterate (h q0 : ℝ) (n : ℕ) :
valueSwitchIter h q0 n - 1 / 2 = (1 - 2 * h) ^ n * (q0 - 1 / 2) := by
induction n with
| zero => simp [valueSwitchIter]
| succ n ih =>
simp only [valueSwitchIter, pow_succ]
linear_combination (1 - 2 * h) * ih
theorem value_pursuit_drifts_to_uncertainty (h q0 : ℝ) (hh : 0 < h) (hh1 : h < 1) :
Filter.Tendsto (valueSwitchIter h q0) Filter.atTop (nhds (1 / 2)) := by
have hab : |1 - 2 * h| < 1 := abs_lt.mpr ⟨by linarith, by linarith⟩
have h1 := (tendsto_pow_atTop_nhds_zero_of_abs_lt_one hab).mul_const (q0 - 1 / 2)
have h2 := h1.add_const (1 / 2)
simp only [zero_mul, zero_add] at h2
refine h2.congr fun n => ?_
have := value_pursuit_switch_iterate h q0 n
linarith
theorem value_shrinkage_between (n k x m : ℝ) (hn : 0 ≤ n) (hk : 0 < k) :
min x m ≤ (n * x + k * m) / (n + k) ∧ (n * x + k * m) / (n + k) ≤ max x m := by
have hd : 0 < n + k := by linarith
constructor
· rw [le_div_iff₀ hd]
nlinarith [min_le_left x m, min_le_right x m]
· rw [div_le_iff₀ hd]
nlinarith [le_max_left x m, le_max_right x m]
def valuePermittedPolicy {α : Type*} (s : Finset α) (permitted : α → Prop) [DecidablePred permitted]
(base : α → ℝ) (tilt : α → ℝ) (a : α) : ℝ :=
posterior s (fun b => if permitted b then base b else 0) (fun b => Real.exp (tilt b)) a
theorem value_policy_permission_gate {α : Type*} (s : Finset α) (permitted : α → Prop)
[DecidablePred permitted] (base tilt : α → ℝ) (a : α) (ha : ¬ permitted a) :
valuePermittedPolicy s permitted base tilt a = 0 := by
apply zero_prior_stays_zero
simp [ha]
theorem value_policy_normalized {α : Type*} (s : Finset α) (permitted : α → Prop)
[DecidablePred permitted] (base tilt : α → ℝ) (b : α) (hb : b ∈ s) (hperm : permitted b)
(hbase : ∀ a ∈ s, 0 ≤ base a) (hpos : 0 < base b) :
∑ a ∈ s, valuePermittedPolicy s permitted base tilt a = 1 := by
apply posterior_normalized
have hnn : ∀ j ∈ s, 0 ≤ (if permitted j then base j else 0) * Real.exp (tilt j) := by
intro j hj
split_ifs
· exact mul_nonneg (hbase j hj) (Real.exp_pos _).le
· simp
calc (0 : ℝ) < (if permitted b then base b else 0) * Real.exp (tilt b) := by
simp [hperm]
exact mul_pos hpos (Real.exp_pos _)
_ ≤ _ := Finset.single_le_sum hnn hb
end SentinelTheory
SentinelTheory.lean
SHA-256 4005ce1b068194b0a141b583c861688c34cc7dfe4550bdd9d9d135dcbabcfc1b
import SentinelTheory.Probability
import SentinelTheory.Structure
import SentinelTheory.Dynamics
import SentinelTheory.Learning
import SentinelTheory.Signals
import SentinelTheory.Information
import SentinelTheory.Pathways
import SentinelTheory.Latest
import SentinelTheory.Evidence
import SentinelTheory.Timing
import SentinelTheory.Values
import SentinelTheory.Language
audit-axioms.py
SHA-256 9e3e6ca1fb839d65b20ff5e0b9366f3bd56b357d5e672d27c8e6fb227ef9b35d
from pathlib import Path
import re
import runpy
expected = runpy.run_path('proof-inventory.py')['inventory']()
audit = Path('Audit.lean').read_text()
reported = re.findall(r'^#print axioms ([\w.]+)$', audit, re.M)
if expected != reported:
raise SystemExit('Every project theorem must have exactly one matching axiom report')
report = Path('.verification/axioms.txt').read_text()
allowed = {'propext', 'Classical.choice', 'Quot.sound'}
for name in expected:
match = re.search(r"'" + re.escape(name) +
r"' depends on axioms:\s*\[(.*?)\]", report, re.S)
empty = re.search(r"'" + re.escape(name) +
r"' does not depend on any axioms", report)
if not match and not empty:
raise SystemExit(f'Missing axiom report for {name}; inspect .verification/axioms.txt')
used = set(re.findall(r'[A-Za-z_][A-Za-z_0-9.]*', match[1])) if match else set()
if used - allowed:
raise SystemExit(f'Unexpected axioms for {name}: {used - allowed}')
print(f'Lean checked {len(expected)} theorem declarations; axiom audit passed.')
check-proofs.sh
SHA-256 011615d80e4d30f3374f9b9e1a1603d73a7452d7e69ca1433c889def00caea01
#!/bin/sh
set -eu
project_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)
cd "$project_dir"
PATH="$HOME/.elan/bin:$PATH"
export PATH
mkdir -p .verification
python3 proof-inventory.py
if ! lake build > .verification/build.txt 2>&1; then
cat .verification/build.txt
exit 1
fi
cat .verification/build.txt
if ! lake env lean -DwarningAsError=true Audit.lean > .verification/axioms.txt 2>&1; then
cat .verification/axioms.txt
exit 1
fi
python3 audit-axioms.py
lean --version > .verification/toolchain.txt
printf '%s\n' 'Proof checking completed. See .verification/axioms.txt and toolchain.txt.'
lake-manifest.json
SHA-256 3ac00c566bbfca931e7e4785dd9012e378c8219711bb5796e603869acc387b58
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.24.0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
"name": "plausible",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/LeanSearchClient",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
"name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "d768126816be17600904726ca7976b185786e6b9",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "556caed0eadb7901e068131d1be208dd907d07a2",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.74",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "sentinel_proofs",
"lakeDir": ".lake"}
lakefile.toml
SHA-256 358c8a23c3d9631b615074876fb9dee5c6800789faa606f52436e4f41b338f54
name = "sentinel_proofs"
version = "0.1.0"
defaultTargets = ["SentinelProofs", "SentinelTheory", "Audit"]
[leanOptions]
warningAsError = true
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.24.0"
[[lean_lib]]
name = "SentinelProofs"
[[lean_lib]]
name = "SentinelTheory"
[[lean_lib]]
name = "Audit"
lean-toolchain
SHA-256 42779d67b81608af8a12aa4328d2ab47ca201925b3b2bd68369587b5340bb434
leanprover/lean4:v4.24.0
proof-inventory.py
SHA-256 5cc6012997aea270327145f2e1335473884e5bdee3be483412dd386f8b080254
from pathlib import Path
import re
def inventory():
files = sorted(path for path in Path('.').rglob('*.lean')
if path.name != 'Audit.lean'
and not any(part in ('.lake', '.verification') for part in path.parts))
declarations = []
for path in files:
source = path.read_text()
if re.search(r'\b(sorry|admit|axiom|native_decide|unsafe)\b', source):
raise SystemExit(f'Rejected proof escape in {path}')
names = re.findall(r'^(?:theorem|lemma) (\w+)', source, re.M)
if not names:
continue
namespaces = re.findall(r'^namespace (\w+)$', source, re.M)
if len(namespaces) != 1:
raise SystemExit(f'Expected one explicit namespace in {path}')
for name in names:
declarations.append(f'{namespaces[0]}.{name}')
if not declarations or len(set(declarations)) != len(declarations):
raise SystemExit('Empty or duplicate theorem inventory')
return declarations
if __name__ == '__main__':
declarations = inventory()
text = 'import SentinelProofs\nimport SentinelTheory\n\n'
text += ''.join(f'#print axioms {name}\n' for name in declarations)
Path('Audit.lean').write_text(text)
print(f'Generated audit for {len(declarations)} theorem declarations.')
setup-and-check.sh
SHA-256 eb63e4a80167f7f603f726dbea62331a8166299709ba6eb4303aea493845a788
#!/bin/sh
set -eu
project_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)
cd "$project_dir"
mkdir -p .verification
if [ ! -x "$HOME/.elan/bin/elan" ]; then
curl --fail --location --proto '=https' --tlsv1.2 \
https://elan.lean-lang.org/elan-init.sh -o .verification/elan-init.sh
sh .verification/elan-init.sh -y --no-modify-path --default-toolchain none
fi
PATH="$HOME/.elan/bin:$PATH"
export PATH
elan toolchain install leanprover/lean4:v4.24.0
lake update
python3 - <<'PY'
from pathlib import Path
import re
import subprocess
sources = sorted(path for path in Path('.').rglob('*.lean')
if not any(part in ('.lake', '.verification') for part in path.parts))
modules = sorted({module for path in sources for module in
re.findall(r'^import (Mathlib[\w.]*)$', path.read_text(), re.M)})
subprocess.run(['lake', 'exe', 'cache', 'get',
*(module.replace('.', '/') + '.lean' for module in modules)], check=True)
PY
sh "$project_dir/check-proofs.sh"