Block02Examples.lean

1 import MachineTheory.Refinement
2 import Mathlib.Tactic.FinCases
3 import Mathlib.Data.Fintype.BigOperators
4 import Mathlib.Algebra.BigOperators.Fin
5 
6 /-! Kernel-checked finite witnesses for Block 02. All numerical probabilities are
7 exact rationals interpreted in the reals. There is no sampling or external evaluator. -/
8 namespace Komorebi.MachineTheory.Block02Examples
9 open scoped BigOperators
10 open Instrument Bayes Bayes.ReportingModel BayesianLumping Refinement
11 noncomputable section
12 
13 /-- The sensor reveals the model bit, then the channel deletes the entire reading. -/
14 def erased : ReportingModel Bool Bool Unit where
15   likelihood m o := if o = m then 1 else 0
16   likelihood_nonneg m o := by split_ifs <;> norm_num
17   likelihood_sum m := by cases m <;> norm_num
18   channel _ _ := 1
19   channel_nonneg _ _ := by norm_num
20   channel_sum _ := by simp
21 
22 def fair : Bool → ℝ := fun _ => 1/2
23 
24 theorem fair_is_dist : IsDist fair := by norm_num [IsDist, fair, mass]
25 
26 /-- A prior concentrated on one model cannot reveal the lost distinction. -/
27 theorem supported_prior_misses_loss : erased.PreservesAt (basis false) := by
28   intro o z h
29   cases z
30   cases o
31   · funext m; cases m <;>
32       norm_num [update, normalize, mass, weights, raw, report, joint, erased, basis]
33   · norm_num [evidence, mass, weights, joint, erased, basis] at h
34 
35 /-- The same channel fails for a full-support prior, so it fails the all-prior contract. -/
36 theorem erased_not_preserves_all : ¬ erased.PreservesAll := by
37   intro h
38   have he := h fair fair_is_dist false () (by
39     norm_num [evidence, mass, weights, joint, erased, fair])
40   have h0 := congrFun he false
41   norm_num [update, normalize, mass, weights, raw, report, joint, erased, fair] at h0
42 
43 theorem erased_has_no_actual_reconstruction : ¬ ∃ ρ, erased.Reconstructs ρ := by
44   intro h
45   exact erased_not_preserves_all (erased.all_iff_reconstruction.mpr h)
46 
47 /-- A noisy bit accompanied by an independent fair flag. -/
48 def flagged : ReportingModel Bool (Bool × Bool) Bool where
49   likelihood m o := if o.1 = m then 3/8 else 1/8
50   likelihood_nonneg m o := by split_ifs <;> norm_num
51   likelihood_sum m := by cases m <;> norm_num [Fintype.sum_prod_type]
52   channel o z := if o.1 = z then 1 else 0
53   channel_nonneg o z := by split_ifs <;> norm_num
54   channel_sum o := by rcases o with ⟨b,f⟩; cases b <;> norm_num
55 
56 def flagReconstruction (z : Bool) (o : Bool × Bool) : ℝ :=
57   if o.1 = z then 1/2 else 0
58 
59 theorem flagged_reconstructs : flagged.Reconstructs flagReconstruction := by
60   refine ⟨?_, ?_, ?_⟩
61   · intro z o; unfold flagReconstruction; split_ifs <;> norm_num
62   · intro z; cases z <;> norm_num [flagReconstruction, Fintype.sum_prod_type]
63   · intro m o z; rcases o with ⟨b,f⟩
64     cases m <;> cases b <;> cases f <;> cases z <;>
65       norm_num [joint, report, flagged, flagReconstruction, Fintype.sum_prod_type]
66 
67 theorem flag_can_be_discarded_for_every_prior : flagged.PreservesAll :=
68   flagged.preservesAll_of_reconstructs flagged_reconstructs
69 
70 /-- A retained report that is impossible under every model still gets a normalized
71 reconstruction row. It does not get an invented posterior. -/
72 def unusedReport : ReportingModel Bool Unit Bool where
73   likelihood _ _ := 1
74   likelihood_nonneg _ _ := by norm_num
75   likelihood_sum _ := by simp
76   channel _ z := if z then 0 else 1
77   channel_nonneg _ z := by cases z <;> norm_num
78   channel_sum _ := by norm_num
79 
80 theorem impossible_report_reconstruction_row :
81     unusedReport.Reconstructs (fun _ _ => 1) := by
82   refine ⟨by intros; norm_num, by intros; simp, ?_⟩
83   intro m o z; cases o; cases z <;> norm_num [joint, report, unusedReport]
84 
85 theorem impossible_report_has_no_posterior :
86     posterior? (weights fair (unusedReport.report true)) = none := by
87   norm_num [posterior?, mass, weights, report, joint, unusedReport, fair]
88 
89 /-- Nonconstant likelihoods can commute with a one-block probability record.
90 This is why Core 3.5 protects at least two blocks. -/
91 def nonconstantLikelihood (b : Bool) : ℝ := if b then 3 else 1
92 
93 theorem one_block_still_corrects (p : Bool → ℝ) (hp : IsDist p) :
94     push (fun _ : Bool => ()) (update p nonconstantLikelihood) =
95       update (push (fun _ : Bool => ()) p) (fun _ : Unit => 1) := by
96   have he : p false + p true = 1 := by simpa [mass, add_comm] using hp.2
97   have hn0 := hp.1 false
98   have hn1 := hp.1 true
99   have hz : p false + 3 * p true ≠ 0 := by nlinarith
100   funext z; cases z
101   have hz' : 3 * p true + p false ≠ 0 := by nlinarith
102   have hs : p true + p false = 1 := by linarith
103   simp [update, normalize, weights, push, mass, nonconstantLikelihood, ← add_div, hz', hs]
104 
105 theorem one_block_likelihood_not_constant : nonconstantLikelihood false ≠ nonconstantLikelihood true := by
106   norm_num [nonconstantLikelihood]
107 
108 /-- Four states encoded 00,01,10,11, with successors 00,10,11,11.
109 A future distinction propagates backwards through two refinement rounds. -/
110 abbrev Four := Bool × Bool
111 
112 def successor : Four → Four
113   | (false,false) => (false,false)
114   | (false,true) => (true,false)
115   | (true,_) => (true,true)
116 
117 def fourKernel (_ : Unit) (y x : Four) : ℝ := if y = successor x then 1 else 0
118 
119 def mandatory : Setoid Four := Setoid.ker (fun x => x.1 && x.2)
120 
121 def afterOne : Setoid Four := Setoid.ker (fun x : Four => if x.1 then x else (false,false))
122 
123 @[simp] theorem mandatory_rel (x y : Four) :
124     mandatory x y ↔ (x.1 && x.2) = (y.1 && y.2) := Iff.rfl
125 
126 @[simp] theorem afterOne_rel (x y : Four) :
127     afterOne x y ↔ (if x.1 then x else (false,false)) =
128       (if y.1 then y else (false,false)) := Iff.rfl
129 
130 theorem refinement_first_round : step fourKernel mandatory = afterOne := by
131   apply Setoid.ext
132   rintro ⟨x₁,x₂⟩ ⟨y₁,y₂⟩
133   rw [step_rel_iff]
134   cases x₁ <;> cases x₂ <;> cases y₁ <;> cases y₂ <;>
135     norm_num [fourKernel, successor, Fintype.sum_prod_type, Prod.forall]
136 
137 theorem refinement_second_round : step fourKernel afterOne = ⊥ := by
138   apply Setoid.ext
139   rintro ⟨x₁,x₂⟩ ⟨y₁,y₂⟩
140   rw [step_rel_iff]
141   cases x₁ <;> cases x₂ <;> cases y₁ <;> cases y₂ <;>
142     norm_num [fourKernel, successor, Fintype.sum_prod_type, Prod.forall]
143 
144 theorem discrete_is_stable : Stable fourKernel (⊥ : Setoid Four) := by
145   apply (stable_iff fourKernel ⊥).mpr
146   intro x y h
147   have he : x = y := h
148   subst y; rfl
149 
150 theorem two_strict_rounds :
151     Refinement.sequence fourKernel mandatory 1 ≠ mandatory ∧
152     Refinement.sequence fourKernel mandatory 2 ≠ Refinement.sequence fourKernel mandatory 1 ∧
153     Stable fourKernel (Refinement.sequence fourKernel mandatory 2) := by
154   have hfirst : afterOne ≠ mandatory := by
155     intro he
156     have h : mandatory (false,false) (true,false) := by change false = false; rfl
157     rw [← he] at h
158     norm_num at h
159   have hsecond : (⊥ : Setoid Four) ≠ afterOne := by
160     intro he
161     have h : afterOne (false,false) (false,true) := by
162       change (false,false) = (false,false); rfl
163     rw [← he] at h
164     exact (by decide : ((false,false) : Four) ≠ (false,true)) h
165   simpa only [Refinement.sequence, refinement_first_round, refinement_second_round] using
166     And.intro hfirst (And.intro hsecond discrete_is_stable)
167 
168 /-- Stable dynamics alone do not establish Bayesian closure for a nontrivial partition. -/
169 theorem likelihood_split_cannot_be_omitted :
170     ¬ ∃ g : Bool → ℝ, (∀ b, 0 < g b) ∧
171       ∀ p : Four → ℝ, IsDist p →
172         push Prod.fst (update p (fun x => nonconstantLikelihood x.2)) =
173           update (push Prod.fst p) g := by
174   intro h
175   have hs : Function.Surjective (Prod.fst : Four → Bool) := fun b => ⟨(b,false),rfl⟩
176   have hl : ∀ x : Four, 0 < nonconstantLikelihood x.2 := by
177     rintro ⟨b,c⟩; cases c <;> norm_num [nonconstantLikelihood]
178   have hn : ∃ u v : Four, u.1 ≠ v.1 := ⟨(false,false),(true,false),by decide⟩
179   have he := (fixed_positive_coarse_iff Prod.fst hs
180     (fun x : Four => nonconstantLikelihood x.2) hl hn).mp h
181       (false,false) (false,true) rfl
182   norm_num [nonconstantLikelihood] at he
183 
184 def fourLaw : Law Four Unit Unit where
185   kernel a _ := fourKernel a
186   nonnegative a o y x := by unfold fourKernel; split_ifs <;> norm_num
187   normalized a x := by
188     rcases x with ⟨b,c⟩
189     cases b <;> cases c <;> norm_num [fourKernel, successor, Fintype.sum_prod_type] <;> decide
190 
191 theorem mandatory_nontrivial : ∃ x y : Four, ¬ mandatory x y :=
192   ⟨(false,false),(true,true),by simp⟩
193 
194 /-- The concrete two-round chain has the same operational contract as Core 3.5. -/
195 theorem discrete_is_only_admissible (P : Setoid Four)
196     (hp : Admissible fourLaw (fun _ : Unit => fun _ : Four => (1 : ℝ)) mandatory P) :
197     P = ⊥ := by
198   have he := (admissible_iff fourLaw (fun _ : Unit => fun _ : Four => (1 : ℝ))
199     mandatory P (by intros; norm_num) mandatory_nontrivial).mp hp
200   have hI : initial mandatory (fun _ : Unit => fun _ : Four => (1 : ℝ)) = mandatory := by
201     apply Setoid.ext; intro x y
202     change (mandatory x y ∧ (fun _ : Unit => (1 : ℝ)) = fun _ : Unit => (1 : ℝ)) ↔ _
203     simp
204   rw [hI] at he
205   have h2 := stable_refines_sequence (transition fourLaw) he.1 he.2 2
206   have hK : transition fourLaw = fourKernel := rfl
207   rw [hK] at h2
208   simp only [Refinement.sequence, refinement_first_round, refinement_second_round] at h2
209   exact le_antisymm h2 bot_le
210 
211 end
212 end Komorebi.MachineTheory.Block02Examples

Back to source controls