LineageExamples.lean

1 import MachineTheory.Variation
2 
3 /-! # Exact finite boundary examples for adaptive-lineage error control
4 
5 These examples use the inherited finite real-valued distribution interface.
6 They illustrate the hypotheses and limits of Core 7.4. They are not a proof
7 of its countably infinite probability-space theorem. Every probability is an
8 exact sum over a declared finite world space, not an empirical estimate.
9 -/
10 namespace Komorebi.MachineTheory.LineageExamples
11 open Instrument Variation Finset
12 open scoped BigOperators
13 noncomputable section
14 
15 /-- Probability of a finite event under the supplied finite distribution. -/
16 def prob {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
17     (p : Ω → ℝ) (E : Finset Ω) : ℝ := mass (Variation.restrict E p)
18 
19 theorem prob_mono {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
20     (p : Ω → ℝ) (hp : ∀ w, 0 ≤ p w) {E F : Finset Ω} (h : E ⊆ F) :
21     prob p E ≤ prob p F := by
22   apply Finset.sum_le_sum
23   intro w _
24   by_cases he : w ∈ E
25   · simp only [Variation.restrict, he, h he, ↓reduceIte, le_refl]
26   · by_cases hf : w ∈ F
27     · simpa only [Variation.restrict, he, hf, ↓reduceIte] using hp w
28     · simp only [Variation.restrict, he, hf, ↓reduceIte, le_refl]
29 
30 def fair (_w : Bool) : ℝ := 1/2
31 
32 theorem fair_dist : IsDist fair := by
33   constructor
34   · intro w; norm_num [fair]
35   · norm_num [mass, fair, Fintype.sum_bool]
36 
37 /-- Both candidates make false claims; each accepts on its own labeled world. -/
38 def claimTrue (_candidate : Bool) : Prop := False
39 
40 def accepts (candidate world : Bool) : Prop := world = candidate
41 
42 def fixedBad (candidate : Bool) : Finset Bool := by
43   classical
44   exact univ.filter fun world => accepts candidate world ∧ ¬ claimTrue candidate
45 
46 /-- Selection observes the world, then chooses the candidate that accepts there. -/
47 def selectedCandidate (world : Bool) : Bool := world
48 
49 def selectedBad : Finset Bool := by
50   classical
51   exact univ.filter fun world =>
52     accepts (selectedCandidate world) world ∧ ¬ claimTrue (selectedCandidate world)
53 
54 theorem fixed_candidate_half (candidate : Bool) : prob fair (fixedBad candidate) = 1/2 := by
55   cases candidate <;>
56     norm_num [prob, mass, Variation.restrict, fair, fixedBad, accepts, claimTrue, Fintype.sum_bool]
57 
58 theorem selected_candidate_certain : prob fair selectedBad = 1 := by
59   norm_num [prob, mass, Variation.restrict, fair, selectedBad, selectedCandidate,
60     accepts, claimTrue, Fintype.sum_bool]
61 
62 /-- Pointwise nominal validity before selection does not imply validity afterward. -/
63 theorem selection_invalidates_nominal_bound :
64     (∀ candidate, prob fair (fixedBad candidate) ≤ 1/2) ∧
65     ¬ prob fair selectedBad ≤ 1/2 := by
66   constructor
67   · intro candidate; rw [fixed_candidate_half]
68   · rw [selected_candidate_certain]; norm_num
69 
70 /-- Conditional on the revealed world, its selected false acceptance has probability one. -/
71 theorem revealed_history_error (world : Bool) :
72     prob fair (selectedBad ∩ {world}) / prob fair {world} = 1 := by
73   cases world <;>
74     norm_num [prob, mass, Variation.restrict, fair, selectedBad, selectedCandidate,
75       accepts, claimTrue, Fintype.sum_bool]
76 
77 /-- Disjoint false-acceptance events attain the union bound exactly. -/
78 theorem disjoint_union_sharp :
79     Disjoint (fixedBad false) (fixedBad true) ∧
80     prob fair (fixedBad false ∪ fixedBad true) =
81       prob fair (fixedBad false) + prob fair (fixedBad true) ∧
82     prob fair (fixedBad false ∪ fixedBad true) = 1 := by
83   constructor
84   · apply Finset.disjoint_left.mpr
85     intro world hf ht
86     simp only [fixedBad, mem_filter, mem_univ, true_and, accepts, claimTrue,
87       not_false_eq_true, and_true] at hf ht
88     exact Bool.false_ne_true (hf.symm.trans ht)
89   · norm_num [prob, mass, Variation.restrict, fair, fixedBad, accepts,
90       claimTrue, Fintype.sum_bool]
91 
92 /-- Repeating one event is perfectly dependent: the union bound is strict,
93 and the product formula for independence is false. This concerns the union
94 step alone, not conditional validity after observing an earlier outcome. -/
95 theorem dependent_repetition :
96     prob fair (fixedBad true ∪ fixedBad true) = 1/2 ∧
97     prob fair (fixedBad true ∪ fixedBad true) <
98       prob fair (fixedBad true) + prob fair (fixedBad true) ∧
99     prob fair (fixedBad true ∩ fixedBad true) ≠
100       prob fair (fixedBad true) * prob fair (fixedBad true) := by
101   simp only [union_self, inter_self, fixed_candidate_half]
102   norm_num
103 
104 /-- A gate can depend arbitrarily on the same world. Retained bad events
105 are still contained in the ungated lineage's bad events. -/
106 theorem gated_union_containment {Ω : Type*} [DecidableEq Ω]
107     (stages : Finset ℕ) (bad gate : ℕ → Finset Ω) :
108     stages.biUnion (fun i => bad i ∩ gate i) ⊆ stages.biUnion bad := by
109   intro w hw
110   obtain ⟨i, hi, hwi⟩ := mem_biUnion.mp hw
111   exact mem_biUnion.mpr ⟨i, hi, (mem_inter.mp hwi).1⟩
112 
113 theorem gated_union_probability {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
114     (p : Ω → ℝ) (hp : IsDist p) (stages : Finset ℕ) (bad gate : ℕ → Finset Ω) :
115     prob p (stages.biUnion (fun i => bad i ∩ gate i)) ≤
116       prob p (stages.biUnion bad) :=
117   prob_mono p hp.1 (gated_union_containment stages bad gate)
118 
119 /-- Gating preserves an unconditional bound; it does not bound error
120 conditional on the decision to retain. The retained mass here is positive. -/
121 theorem retention_can_condition_to_certain_error :
122     0 < prob fair (fixedBad true) ∧
123     prob fair (fixedBad true ∩ fixedBad true) ≤ 1/2 ∧
124     prob fair (fixedBad true ∩ fixedBad true) / prob fair (fixedBad true) = 1 := by
125   simp only [inter_self, fixed_candidate_half]
126   norm_num
127 
128 /-- Zero probability is weaker than event emptiness under a law with zero-mass worlds. -/
129 theorem null_event_is_nonempty :
130     IsDist (basis false : Bool → ℝ) ∧
131     ({true} : Finset Bool).Nonempty ∧ prob (basis false) {true} = 0 := by
132   refine ⟨basis_dist false, by simp, ?_⟩
133   norm_num [prob, mass, Variation.restrict, basis, Fintype.sum_bool]
134 
135 /-- An arbitrary finite prefix can be error-free while a later stage is certain to fail. -/
136 def lateBad (cutoff stage : ℕ) : Finset Bool := if stage = cutoff then univ else ∅
137 
138 theorem late_failure (cutoff : ℕ) :
139     (∀ stage < cutoff, prob fair (lateBad cutoff stage) = 0) ∧
140     prob fair (lateBad cutoff cutoff) = 1 := by
141   constructor
142   · intro stage hstage
143     have hne : stage ≠ cutoff := Nat.ne_of_lt hstage
144     simp [prob, mass, Variation.restrict, lateBad, hne]
145   · norm_num [prob, mass, Variation.restrict, lateBad, fair, Fintype.sum_bool]
146 
147 /-- A sum of declared numbers alone has no connection to the event probabilities. -/
148 theorem numeric_budget_without_validity :
149     (∑ _stage : Bool, (0 : ℝ)) ≤ 1/10 ∧ ¬ prob fair selectedBad ≤ 1/10 := by
150   rw [selected_candidate_certain]
151   norm_num
152 
153 end
154 end Komorebi.MachineTheory.LineageExamples

Back to source controls