Refinement.lean

1 import MachineTheory.BayesianLumping
2 import Mathlib.SetTheory.Cardinal.Finite
3 
4 /-! Core 3.5. The refinement is defined by actual block-probability sums.
5 The stopping bound is the number of states minus the initial number of blocks,
6 not the number of pairs and not a supplied termination assumption. -/
7 namespace Komorebi.MachineTheory
8 namespace Refinement
9 open scoped BigOperators
10 open Instrument Bayes BayesianLumping
11 noncomputable section
12 variable {X A O : Type*} [Fintype X]
13 
14 def project (P : Setoid X) : X → Quotient P := Quotient.mk P
15 
16 def coarsen {P Q : Setoid X} (h : P ≤ Q) : Quotient P → Quotient Q :=
17   Quotient.map id (fun _ _ hp => h hp)
18 
19 omit [Fintype X] in
20 @[simp] theorem coarsen_project {P Q : Setoid X} (h : P ≤ Q) (x : X) :
21     coarsen h (project P x) = project Q x := rfl
22 
23 omit [Fintype X] in
24 theorem project_surjective (P : Setoid X) : Function.Surjective (project P) := by
25   intro q; induction q using Quotient.inductionOn with | _ x => exact ⟨x,rfl⟩
26 
27 omit [Fintype X] in
28 theorem coarsen_surjective {P Q : Setoid X} (h : P ≤ Q) :
29     Function.Surjective (coarsen h) := by
30   intro q; induction q using Quotient.inductionOn with | _ x => exact ⟨project P x,rfl⟩
31 
32 def blockCount (P : Setoid X) : ℕ := Nat.card (Quotient P)
33 
34 theorem blockCount_le (P : Setoid X) : blockCount P ≤ Fintype.card X := by
35   classical
36   simpa [blockCount, Nat.card_eq_fintype_card] using
37     Fintype.card_le_of_surjective (project P) (project_surjective P)
38 
39 theorem blockCount_strict {P Q : Setoid X} (h : P ≤ Q) (hne : P ≠ Q) :
40     blockCount Q < blockCount P := by
41   classical
42   have hni : ¬ Function.Injective (coarsen h) := by
43     intro hi
44     apply hne
45     apply le_antisymm h
46     intro x y hxy
47     apply Quotient.exact
48     exact hi (show coarsen h (project P x) = coarsen h (project P y) from Quotient.sound hxy)
49   simpa [blockCount, Nat.card_eq_fintype_card] using
50     Fintype.card_lt_of_surjective_not_injective (coarsen h) (coarsen_surjective h) hni
51 
52 /-- Successor-block masses are the next refinement signature. -/
53 def signature (K : A → X → X → ℝ) (P : Setoid X) (x : X) : A → Quotient P → ℝ := by
54   classical
55   exact fun a => push (project P) (fun y => K a y x)
56 
57 def step (K : A → X → X → ℝ) (P : Setoid X) : Setoid X :=
58   P ⊓ Setoid.ker (signature K P)
59 
60 def Stable (K : A → X → X → ℝ) (P : Setoid X) : Prop := step K P = P
61 
62 theorem step_le (K : A → X → X → ℝ) (P : Setoid X) : step K P ≤ P :=
63   fun _ _ h => h.1
64 
65 theorem stable_iff (K : A → X → X → ℝ) (P : Setoid X) :
66     Stable K P ↔ ∀ x y, P x y → signature K P x = signature K P y := by
67   constructor
68   · intro h x y hxy
69     have hh : step K P x y := by rw [h]; exact hxy
70     exact hh.2
71   · intro h
72     exact le_antisymm (step_le K P) (fun x y hxy => ⟨hxy,h x y hxy⟩)
73 
74 /-- Aggregation along two finite quotients is literal aggregation along their composite. -/
75 theorem push_comp {Y Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
76     (π : X → Y) (ψ : Y → Z) (p : X → ℝ) :
77     push ψ (push π p) = push (ψ ∘ π) p := by
78   funext z
79   unfold push
80   have hi (y : Y) :
81       (if ψ y = z then ∑ x, if π x = y then p x else 0 else 0) =
82       ∑ x, if π x = y then (if ψ y = z then p x else 0) else 0 := by
83     by_cases hy : ψ y = z <;> simp [hy]
84   simp_rw [hi]
85   rw [Finset.sum_comm]
86   apply Finset.sum_congr rfl
87   intro x _
88   simp
89 
90 /-- A stable finer partition stays finer after each actual block-sum split. -/
91 theorem stable_refines_step (K : A → X → X → ℝ) {P Q : Setoid X}
92     (h : Q ≤ P) (hQ : Stable K Q) : Q ≤ step K P := by
93   classical
94   intro x y hxy
95   refine ⟨h hxy, ?_⟩
96   have hs := (stable_iff K Q).mp hQ x y hxy
97   funext a
98   have he := congrArg (push (coarsen h)) (congrFun hs a)
99   simp only [signature, push_comp] at he
100   exact he
101 
102 attribute [local instance] Classical.propDecidable
103 
104 /-- A finite state representative suffices to name each current block.
105 This connects the quotient implementation to the manuscript's literal block sums. -/
106 theorem step_rel_iff (K : A → X → X → ℝ) (P : Setoid X) (x y : X) :
107     step K P x y ↔ P x y ∧ ∀ a z,
108       (∑ u, if P u z then K a u x else 0) =
109       (∑ u, if P u z then K a u y else 0) := by
110   constructor
111   · rintro ⟨hxy,hs⟩
112     refine ⟨hxy, ?_⟩
113     intro a z
114     have hh := congrFun (congrFun hs a) (project P z)
115     simpa only [signature, push, project, Quotient.eq] using hh
116   · rintro ⟨hxy,hs⟩
117     refine ⟨hxy, ?_⟩
118     funext a q
119     induction q using Quotient.inductionOn with
120     | _ z => simpa only [signature, push, project, Quotient.eq] using hs a z
121 
122 /-- The first split retains both the mandatory target and every likelihood value. -/
123 def initial (P₀ : Setoid X) (l : O → X → ℝ) : Setoid X :=
124   P₀ ⊓ Setoid.ker (fun x => fun o => l o x)
125 
126 def sequence (K : A → X → X → ℝ) (I : Setoid X) : ℕ → Setoid X
127   | 0 => I
128   | n+1 => step K (sequence K I n)
129 
130 theorem sequence_le_initial (K : A → X → X → ℝ) (I : Setoid X) (n : ℕ) :
131     sequence K I n ≤ I := by
132   induction n with
133   | zero => exact le_rfl
134   | succ n ih => exact le_trans (step_le K _) ih
135 
136 theorem stable_refines_sequence (K : A → X → X → ℝ) {I Q : Setoid X}
137     (h : Q ≤ I) (hq : Stable K Q) (n : ℕ) : Q ≤ sequence K I n := by
138   induction n with
139   | zero => exact h
140   | succ n ih => exact stable_refines_step K ih hq
141 
142 /-- Every strict refinement adds a block, so a fixed point is reached within
143 the manuscript's linear-in-state-count number of strict rounds. -/
144 theorem bounded_stabilization (K : A → X → X → ℝ) (I : Setoid X) :
145     ∃ n ≤ Fintype.card X - blockCount I, Stable K (sequence K I n) := by
146   by_contra hn
147   push Not at hn
148   let b := Fintype.card X - blockCount I
149   have hg : ∀ n, n ≤ b+1 → blockCount I + n ≤ blockCount (sequence K I n) := by
150     intro n
151     induction n with
152     | zero => intro _; simp [sequence]
153     | succ n ih =>
154       intro hnb
155       have hnb' : n ≤ b := by omega
156       have hs := hn n hnb'
157       have hc := blockCount_strict (step_le K (sequence K I n)) hs
158       have hi := ih (by omega)
159       change blockCount I + (n+1) ≤ blockCount (step K (sequence K I n))
160       omega
161   have hb := hg (b+1) le_rfl
162   have hmax := blockCount_le (sequence K I (b+1))
163   have hi := blockCount_le I
164   dsimp [b] at hb hmax
165   omega
166 
167 def stopIndex (K : A → X → X → ℝ) (I : Setoid X) : ℕ := by
168   classical
169   exact Nat.find (bounded_stabilization K I)
170 
171 def terminal (K : A → X → X → ℝ) (I : Setoid X) : Setoid X :=
172   sequence K I (stopIndex K I)
173 
174 theorem stopIndex_bound (K : A → X → X → ℝ) (I : Setoid X) :
175     stopIndex K I ≤ Fintype.card X - blockCount I := by
176   classical
177   exact (Nat.find_spec (bounded_stabilization K I)).1
178 
179 theorem terminal_stable (K : A → X → X → ℝ) (I : Setoid X) :
180     Stable K (terminal K I) := by
181   classical
182   exact (Nat.find_spec (bounded_stabilization K I)).2
183 
184 theorem terminal_le (K : A → X → X → ℝ) (I : Setoid X) : terminal K I ≤ I :=
185   sequence_le_initial K I _
186 
187 theorem terminal_coarsest (K : A → X → X → ℝ) (I : Setoid X) {Q : Setoid X}
188     (h : Q ≤ I) (hs : Stable K Q) : Q ≤ terminal K I :=
189   stable_refines_sequence K h hs _
190 
191 theorem terminal_unique (K : A → X → X → ℝ) (I : Setoid X) (Q : Setoid X)
192     (hle : Q ≤ I) (hs : Stable K Q)
193     (hgreatest : ∀ R, R ≤ I → Stable K R → R ≤ Q) : Q = terminal K I :=
194   le_antisymm (terminal_coarsest K I hle hs)
195     (hgreatest _ (terminal_le K I) (terminal_stable K I))
196 
197 /-- A stochastic transition is represented by an instrument with one trivial report.
198 The successor law is still column-oriented, as in Block 01. -/
199 def transition (K : Law X A Unit) : A → X → X → ℝ := fun a => K.kernel a ()
200 
201 def PredictionExists (K : Law X A Unit) (P : Setoid X) : Prop := by
202   classical
203   exact ∃ L : Law (Quotient P) A Unit,
204     ∀ a o, Intertwines (project P) (K.kernel a o) (L.kernel a o)
205 
206 theorem stable_iff_prediction (K : Law X A Unit) (P : Setoid X) :
207     Stable (transition K) P ↔ PredictionExists K P := by
208   classical
209   change Stable (transition K) P ↔
210     ∃ L : Law (Quotient P) A Unit,
211       ∀ a o, Intertwines (project P) (K.kernel a o) (L.kernel a o)
212   rw [quotient_exists_iff (project P) (project_surjective P) K]
213   constructor
214   · intro h a o z x y hxy
215     cases o
216     exact congrFun (congrFun ((stable_iff (transition K) P).mp h x y
217       (Quotient.exact hxy)) a) z
218   · intro h
219     apply (stable_iff (transition K) P).mpr
220     intro x y hxy
221     funext a z
222     exact h a () z x y (Quotient.sound hxy)
223 
224 /-- A separate correction uses one fixed positive coarse likelihood for every prior. -/
225 def CorrectionsExist (l : O → X → ℝ) (P : Setoid X) : Prop := by
226   classical
227   exact ∀ o, ∃ g : Quotient P → ℝ, (∀ z, 0 < g z) ∧
228     ∀ p, IsDist p → push (project P) (update p (l o)) =
229       update (push (project P) p) g
230 
231 def Admissible (K : Law X A Unit) (l : O → X → ℝ) (P₀ P : Setoid X) : Prop :=
232   P ≤ P₀ ∧ PredictionExists K P ∧ CorrectionsExist l P
233 
234 /-- The Bayesian necessity is proved from two-point priors, not assumed as a field
235 of the target partition. The likelihood split is exactly the necessary initial split. -/
236 theorem admissible_iff (K : Law X A Unit) (l : O → X → ℝ) (P₀ P : Setoid X)
237     (hl : ∀ o x, 0 < l o x) (hnt : ∃ x y, ¬ P₀ x y) :
238     Admissible K l P₀ P ↔ P ≤ initial P₀ l ∧ Stable (transition K) P := by
239   classical
240   constructor
241   · rintro ⟨hle,hpred,hcorr⟩
242     refine ⟨?_, (stable_iff_prediction K P).mpr hpred⟩
243     intro x y hxy
244     refine ⟨hle hxy, ?_⟩
245     funext o
246     have hn : ∃ u v, project P u ≠ project P v := by
247       obtain ⟨u,v,h⟩ := hnt
248       exact ⟨u,v, fun he => h (hle (Quotient.exact he))⟩
249     exact (fixed_positive_coarse_iff (project P) (project_surjective P) (l o)
250       (hl o) hn).mp (hcorr o) x y (Quotient.sound hxy)
251   · rintro ⟨hle,hs⟩
252     refine ⟨fun _ _ hxy => (hle hxy).1, (stable_iff_prediction K P).mp hs, ?_⟩
253     intro o
254     let g : Quotient P → ℝ := fun z => l o z.out
255     have hf : ∀ x, l o x = g (project P x) := by
256       intro x
257       have hp : P x (project P x).out := Quotient.exact (Quotient.out_eq (project P x)).symm
258       exact congrFun (hle hp).2 o
259     exact ⟨g, fun z => hl o z.out,
260       fun p _ => update_commutes_of_factored (project P) (l o) g hf p⟩
261 
262 /-- Core 3.5: the specified splitting process terminates within the exact block-count
263 bound and returns the unique coarsest operationally admissible refinement. -/
264 theorem least_prediction_correction_refinement (K : Law X A Unit)
265     (l : O → X → ℝ) (P₀ : Setoid X) (hl : ∀ o x, 0 < l o x)
266     (hnt : ∃ x y, ¬ P₀ x y) :
267     let I := initial P₀ l
268     let n := stopIndex (transition K) I
269     let P := sequence (transition K) I n
270     n ≤ Fintype.card X - blockCount I ∧
271       Admissible K l P₀ P ∧
272       (∀ Q, Admissible K l P₀ Q → Q ≤ P) ∧
273       (∀ Q, Admissible K l P₀ Q →
274         (∀ R, Admissible K l P₀ R → R ≤ Q) → Q = P) := by
275   dsimp only
276   let I := initial P₀ l
277   let P := terminal (transition K) I
278   have hadm : Admissible K l P₀ P :=
279     (admissible_iff K l P₀ P hl hnt).mpr
280       ⟨terminal_le _ _, terminal_stable _ _⟩
281   have hmin : ∀ Q, Admissible K l P₀ Q → Q ≤ P := by
282     intro Q hq
283     obtain ⟨hqI,hqS⟩ := (admissible_iff K l P₀ Q hl hnt).mp hq
284     exact terminal_coarsest _ _ hqI hqS
285   refine ⟨stopIndex_bound _ _, hadm, hmin, ?_⟩
286   intro Q hq hbest
287   exact le_antisymm (hmin Q hq) (hbest P hadm)
288 
289 end
290 end Refinement
291 end Komorebi.MachineTheory

Back to source controls