Block4Examples.lean

1 import KomorebiLSM.InstrumentRealization
2 import Mathlib.Tactic.FinCases
3 import Mathlib.Tactic.NormNum
4 import Mathlib.Algebra.BigOperators.Fin
5 
6 /-! Exact examples distinguish prediction from reconstruction, word order,
7 likelihood from posterior, and linear uniqueness from admissible-state equality. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.Block4Examples
10 open scoped BigOperators
11 open Module FiniteBayes FiniteInstruments
12 
13 noncomputable def hiddenMatrix (o : Bool) : Matrix (Fin 3) (Fin 3) ℝ := fun j i =>
14   if o then
15     if j.val = 2 then (if i.val = 2 then 3/4 else 1/2) else 0
16   else
17     if j.val = 2 then 0 else (if i.val = 2 then 1/8 else 1/4)
18 
19 noncomputable def tinyInstrument : Instrument (Fin 3) Unit Bool where
20   matrix _ := hiddenMatrix
21   nonneg := by
22     intro a o j i
23     cases o <;> fin_cases j <;> fin_cases i <;> norm_num [hiddenMatrix]
24   mass_one := by
25     intro a i
26     fin_cases i <;> norm_num [hiddenMatrix, Fin.sum_univ_succ]
27 
28 noncomputable def summaryMatrix : Matrix (Fin 2) (Fin 3) ℝ := fun j i =>
29   if j.val = 0 then 1 else if i.val = 2 then 1 else 0
30 
31 noncomputable def summary : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) := summaryMatrix.mulVecLin
32 
33 def summaryMass : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
34 
35 noncomputable def reducedMatrix (o : Bool) : Matrix (Fin 2) (Fin 2) ℝ := fun j i =>
36   if o then (if i.val = 0 then 1/2 else 1/4)
37   else if j.val = 0 then (if i.val = 0 then 1/2 else -1/4) else 0
38 
39 noncomputable def reducedBranch (s : Unit × Bool) :
40     (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) := (reducedMatrix s.2).mulVecLin
41 
42 theorem summary_coordinates (p : Fin 3 → ℝ) :
43     summary p 0 = mass p ∧ summary p 1 = p 2 := by
44   simp [summary, summaryMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_succ]
45 
46 theorem summary_preserves_mass : summaryMass.comp summary = mass := by
47   apply LinearMap.ext
48   intro p
49   exact (summary_coordinates p).1
50 
51 theorem summary_surjective : Function.Surjective summary := by
52   intro z
53   let p : Fin 3 → ℝ := fun i => if i.val=0 then z 0-z 1 else if i.val=2 then z 1 else 0
54   refine ⟨p, ?_⟩
55   funext j
56   fin_cases j <;> simp [summary,summaryMatrix,Matrix.mulVec,dotProduct,Fin.sum_univ_succ,p]
57 
58 theorem reduced_intertwining (s : Unit × Bool) :
59     (reducedBranch s).comp summary = summary.comp (tinyInstrument.branch s) := by
60   apply LinearMap.ext
61   intro p
62   funext j
63   rcases s with ⟨a,o⟩
64   cases o <;> fin_cases j <;>
65     simp [reducedBranch,reducedMatrix,summary,summaryMatrix,tinyInstrument,
66       Instrument.branch,hiddenMatrix,Matrix.mulVec,dotProduct,Fin.sum_univ_succ] <;> ring
67 
68 theorem reduced_maps_unique (s : Unit × Bool)
69     (D : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ))
70     (hD : D.comp summary = summary.comp (tinyInstrument.branch s)) : D = reducedBranch s :=
71   closed_operator_unique summary summary_surjective _ _ D (reduced_intertwining s) hD
72 
73 theorem all_word_readouts (w : List (Unit × Bool)) (p : Fin 3 → ℝ) :
74     summaryMass (wordAction reducedBranch w (summary p)) =
75       mass (wordAction tinyInstrument.branch w p) :=
76   reduced_word_readout tinyInstrument summary reducedBranch summaryMass
77     summary_preserves_mass reduced_intertwining w p
78 
79 theorem same_summary : summary (pointMass (0 : Fin 3)) = summary (pointMass 1) := by
80   funext j
81   fin_cases j <;> norm_num [summary,summaryMatrix,pointMass,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
82 
83 theorem distinct_hidden_priors : pointMass (0 : Fin 3) ≠ pointMass 1 := by
84   exact fun h => (by norm_num : (0 : Fin 3) ≠ 1) (pointMass_injective h)
85 
86 theorem same_every_future_word (w : List (Unit × Bool)) :
87     mass (wordAction tinyInstrument.branch w (pointMass 0)) =
88       mass (wordAction tinyInstrument.branch w (pointMass 1)) := by
89   rw [← all_word_readouts, ← all_word_readouts, same_summary]
90 
91 theorem mass_row_in_completion :
92     (mass : (Fin 3 → ℝ) →ₗ[ℝ] ℝ) ∈ instrumentCompletion tinyInstrument.branch mass :=
93   massRow_mem_completion _ _
94 
95 theorem coordinate_two_from_word :
96     (LinearMap.proj 2 : (Fin 3 → ℝ) →ₗ[ℝ] ℝ) =
97       (4 : ℝ) • wordRow tinyInstrument.branch mass [((),true)] - (2 : ℝ) • mass := by
98   apply LinearMap.ext
99   intro p
100   simp [wordRow,wordAction,tinyInstrument,Instrument.branch,hiddenMatrix,
101     Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
102   ring
103 
104 theorem coordinate_two_in_completion :
105     (LinearMap.proj 2 : (Fin 3 → ℝ) →ₗ[ℝ] ℝ) ∈ instrumentCompletion tinyInstrument.branch mass := by
106   rw [coordinate_two_from_word]
107   exact (instrumentCompletion tinyInstrument.branch mass).sub_mem
108     ((instrumentCompletion tinyInstrument.branch mass).smul_mem _ (wordRow_mem_completion _ _ _))
109     ((instrumentCompletion tinyInstrument.branch mass).smul_mem _ mass_row_in_completion)
110 
111 /-- The actual completed row space is exactly the two-row summary space. -/
112 theorem completion_exactly_two_rows : instrumentCompletion tinyInstrument.branch mass =
113     LinearMap.range summary.dualMap := by
114   apply le_antisymm
115   · exact completion_le_word_reading_summary _ summary
116       (realization_reads_all_words tinyInstrument summary reducedBranch summaryMass
117         summary_preserves_mass reduced_intertwining)
118   · apply summary_rowspace_le
119     intro j
120     fin_cases j
121     · change summaryMass.comp summary ∈ instrumentCompletion tinyInstrument.branch mass
122       rw [summary_preserves_mass]
123       exact mass_row_in_completion
124     · have he : (LinearMap.proj (1 : Fin 2)).comp summary =
125           (LinearMap.proj (2 : Fin 3) : (Fin 3 → ℝ) →ₗ[ℝ] ℝ) := by
126         apply LinearMap.ext
127         intro p
128         exact (summary_coordinates p).2
129       change (LinearMap.proj (1 : Fin 2)).comp summary ∈ instrumentCompletion tinyInstrument.branch mass
130       rw [he]
131       exact coordinate_two_in_completion
132 
133 theorem first_hidden_coordinate_is_omitted :
134     (LinearMap.proj 0 : (Fin 3 → ℝ) →ₗ[ℝ] ℝ) ∉ instrumentCompletion tinyInstrument.branch mass := by
135   rw [completion_exactly_two_rows]
136   rintro ⟨f,hf⟩
137   have h0 := congrArg (fun g : (Fin 3 → ℝ) →ₗ[ℝ] ℝ => g (pointMass 0)) hf
138   have h1 := congrArg (fun g : (Fin 3 → ℝ) →ₗ[ℝ] ℝ => g (pointMass 1)) hf
139   change f (summary (pointMass 0)) = pointMass (0 : Fin 3) 0 at h0
140   change f (summary (pointMass 1)) = pointMass (1 : Fin 3) 0 at h1
141   rw [same_summary] at h0
142   norm_num [pointMass] at h0 h1
143   linarith
144 
145 noncomputable def initialPrior (i : Fin 3) : ℝ := if i.val=2 then 1/2 else 1/4
146 
147 theorem initial_prior_valid : IsPrior initialPrior := by
148   constructor
149   · intro i; fin_cases i <;> norm_num [initialPrior]
150   · norm_num [initialPrior,Fin.sum_univ_succ]
151 
152 theorem initial_predictive_state : summary initialPrior 0 = 1 ∧ summary initialPrior 1 = 1/2 := by
153   norm_num [summary,summaryMatrix,initialPrior,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
154 
155 theorem initial_likelihoods :
156     mass (tinyInstrument.branch ((),false) initialPrior) = 3/8 ∧
157     mass (tinyInstrument.branch ((),true) initialPrior) = 5/8 := by
158   norm_num [tinyInstrument,Instrument.branch,hiddenMatrix,initialPrior,
159     Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
160 
161 theorem true_then_false_probability :
162     mass (wordAction tinyInstrument.branch [((),true),((),false)] initialPrior) = 5/32 := by
163   norm_num [wordAction,tinyInstrument,Instrument.branch,hiddenMatrix,initialPrior,Matrix.mul_apply,
164     Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
165 
166 theorem false_then_true_probability :
167     mass (wordAction tinyInstrument.branch [((),false),((),true)] initialPrior) = 3/16 := by
168   norm_num [wordAction,tinyInstrument,Instrument.branch,hiddenMatrix,initialPrior,Matrix.mul_apply,
169     Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
170 
171 theorem order_matters :
172     mass (wordAction tinyInstrument.branch [((),true),((),false)] initialPrior) ≠
173       mass (wordAction tinyInstrument.branch [((),false),((),true)] initialPrior) := by
174   rw [true_then_false_probability,false_then_true_probability]
175   norm_num
176 
177 theorem complete_tree_mass (as : List Unit) :
178     tinyInstrument.observationTreeMass as initialPrior = 1 := by
179   rw [Instrument.observationTreeMass_eq,mass_prior _ initial_prior_valid]
180 
181 theorem signed_reduced_entry : reducedMatrix false 0 1 = -1/4 := by
182   norm_num [reducedMatrix]
183 
184 theorem reduced_probabilities_valid (w : List (Unit × Bool)) :
185     0 ≤ summaryMass (wordAction reducedBranch w (summary initialPrior)) ∧
186       summaryMass (wordAction reducedBranch w (summary initialPrior)) ≤ 1 := by
187   rw [all_word_readouts]
188   exact tinyInstrument.word_probability w initialPrior initial_prior_valid
189 
190 
191 theorem completion_dimension_two :
192     finrank ℝ (instrumentCompletion tinyInstrument.branch mass) = 2 := by
193   rw [completion_exactly_two_rows,
194     LinearMap.finrank_range_of_inj (LinearMap.dualMap_injective_of_surjective summary_surjective),
195     Subspace.dual_finrank_eq, Module.finrank_fintype_fun_eq_card, Fintype.card_fin]
196 
197 theorem mass_alone_cannot_predict :
198     ¬ ∃ f : ℝ → ℝ, ∀ p, IsPrior p →
199       f (mass p) = mass (tinyInstrument.branch ((),true) p) := by
200   rintro ⟨f,hf⟩
201   have h0 := hf (pointMass 0) (point_prior (0 : Fin 3))
202   have h2 := hf (pointMass 2) (point_prior (2 : Fin 3))
203   rw [mass_pointMass] at h0 h2
204   norm_num [mass_apply, Instrument.branch_apply, tinyInstrument, hiddenMatrix,pointMass,
205     Fin.sum_univ_succ] at h0 h2
206   linarith
207 
208 noncomputable def wrongMatrix : Matrix (Fin 2) (Fin 2) ℝ := fun j i =>
209   if i.val=0 then (if j.val=0 then 1/2 else 1/4) else 0
210 
211 noncomputable def wrongBranch : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) := wrongMatrix.mulVecLin
212 
213 noncomputable def actualDefect : Fin 2 → ℝ :=
214   closureDefect summary (tinyInstrument.branch ((),true)) wrongBranch initialPrior
215 
216 theorem exact_likelihood_pair :
217     mass (tinyInstrument.branch ((),true) initialPrior) = 5/8 ∧
218     summaryMass (wrongBranch (summary initialPrior)) = 1/2 := by
219   norm_num [tinyInstrument,Instrument.branch,hiddenMatrix,initialPrior,summaryMass,
220     wrongBranch,wrongMatrix,summary,summaryMatrix,Matrix.mulVec,Matrix.mul_apply,dotProduct,Fin.sum_univ_succ]
221 
222 theorem exact_defect_coordinates : actualDefect 0 = 1/8 ∧ actualDefect 1 = 3/8 := by
223   norm_num [actualDefect,closureDefect,tinyInstrument,Instrument.branch,hiddenMatrix,initialPrior,
224     wrongBranch,wrongMatrix,summary,summaryMatrix,Matrix.mulVec,Matrix.mul_apply,dotProduct,Fin.sum_univ_succ]
225 
226 theorem likelihood_error_is_mass_defect :
227     mass (tinyInstrument.branch ((),true) initialPrior) -
228       summaryMass (wrongBranch (summary initialPrior)) = summaryMass actualDefect :=
229   likelihood_defect summary _ wrongBranch mass summaryMass summary_preserves_mass initialPrior
230 
231 theorem true_posterior_coordinates :
232     summary (normalize mass (tinyInstrument.branch ((),true) initialPrior)) 0 = 1 ∧
233     summary (normalize mass (tinyInstrument.branch ((),true) initialPrior)) 1 = 1 := by
234   norm_num [FiniteInstruments.normalize,tinyInstrument,Instrument.branch,hiddenMatrix,initialPrior,
235     summary,summaryMatrix,Matrix.mulVec,Matrix.mul_apply,dotProduct,Fin.sum_univ_succ]
236 
237 theorem proposed_posterior_coordinates :
238     normalize summaryMass (wrongBranch (summary initialPrior)) 0 = 1 ∧
239     normalize summaryMass (wrongBranch (summary initialPrior)) 1 = 1/2 := by
240   norm_num [FiniteInstruments.normalize,summaryMass,wrongBranch,wrongMatrix,initialPrior,
241     summary,summaryMatrix,Matrix.mulVec,Matrix.mul_apply,dotProduct,Fin.sum_univ_succ]
242 
243 theorem proposed_posterior_is_realizable :
244     normalize summaryMass (wrongBranch (summary initialPrior)) ∈ realizableBeliefs summary := by
245   refine ⟨initialPrior,initial_prior_valid, ?_⟩
246   funext j
247   fin_cases j
248   · exact initial_predictive_state.1.trans proposed_posterior_coordinates.1.symm
249   · exact initial_predictive_state.2.trans proposed_posterior_coordinates.2.symm
250 
251 theorem oblique_defect_coordinates :
252     oblique summaryMass (normalize summaryMass (wrongBranch (summary initialPrior))) actualDefect 0 = 0 ∧
253     oblique summaryMass (normalize summaryMass (wrongBranch (summary initialPrior))) actualDefect 1 = 5/16 := by
254   have hm : summaryMass actualDefect = 1/8 := exact_defect_coordinates.1
255   simp only [oblique_apply,Pi.sub_apply,Pi.smul_apply,smul_eq_mul,hm,
256     exact_defect_coordinates.1,exact_defect_coordinates.2,
257     proposed_posterior_coordinates.1,proposed_posterior_coordinates.2]
258   norm_num
259 
260 theorem normalized_defect_coordinates :
261     summary (normalize mass (tinyInstrument.branch ((),true) initialPrior)) 0 -
262       normalize summaryMass (wrongBranch (summary initialPrior)) 0 = 0 ∧
263     summary (normalize mass (tinyInstrument.branch ((),true) initialPrior)) 1 -
264       normalize summaryMass (wrongBranch (summary initialPrior)) 1 = 1/2 := by
265   rw [true_posterior_coordinates.1,true_posterior_coordinates.2,
266     proposed_posterior_coordinates.1,proposed_posterior_coordinates.2]
267   norm_num
268 
269 theorem example_satisfies_general_defect :
270     summary (normalize mass (tinyInstrument.branch ((),true) initialPrior)) -
271       normalize summaryMass (wrongBranch (summary initialPrior)) =
272     (mass (tinyInstrument.branch ((),true) initialPrior))⁻¹ •
273       oblique summaryMass (normalize summaryMass (wrongBranch (summary initialPrior))) actualDefect := by
274   exact normalized_closure_defect summary _ wrongBranch summaryMass summary_preserves_mass initialPrior
275     (by rw [exact_likelihood_pair.1]; norm_num) (by rw [exact_likelihood_pair.2]; norm_num)
276 
277 noncomputable def coinInstrument (theta : ℝ) (h0 : 0 ≤ theta) (h1 : theta ≤ 1) :
278     Instrument (Fin 1) Unit Bool where
279   matrix _ o _ _ := if o then theta else 1-theta
280   nonneg := by intro a o j i; cases o <;> simp [h0,sub_nonneg.mpr h1]
281   mass_one := by intro a i; simp
282 
283 noncomputable def coinOne : Instrument (Fin 1) Unit Bool := coinInstrument (1/3) (by norm_num) (by norm_num)
284 noncomputable def coinTwo : Instrument (Fin 1) Unit Bool := coinInstrument (2/3) (by norm_num) (by norm_num)
285 
286 theorem coin_true_on_prior (theta : ℝ) (h0 : 0 ≤ theta) (h1 : theta ≤ 1)
287     (p : Fin 1 → ℝ) (hp : IsPrior p) :
288     (coinInstrument theta h0 h1).branch ((),true) p = fun _ => theta := by
289   have hp0 : p 0 = 1 := by simpa [Fin.sum_univ_succ] using hp.2
290   funext j
291   rw [Instrument.branch_apply]
292   simp [coinInstrument,hp0]
293 
294 theorem coins_posterior_agrees_all_priors (p : Fin 1 → ℝ) (hp : IsPrior p) :
295     normalize mass (coinOne.branch ((),true) p) = normalize mass (coinTwo.branch ((),true) p) := by
296   change normalize mass ((coinInstrument (1/3) _ _).branch ((),true) p) =
297     normalize mass ((coinInstrument (2/3) _ _).branch ((),true) p)
298   rw [coin_true_on_prior _ _ _ p hp,coin_true_on_prior _ _ _ p hp]
299   funext j
300   norm_num [FiniteInstruments.normalize]
301 
302 theorem coins_likelihoods_differ_all_priors (p : Fin 1 → ℝ) (hp : IsPrior p) :
303     mass (coinOne.branch ((),true) p) = 1/3 ∧ mass (coinTwo.branch ((),true) p) = 2/3 := by
304   change mass ((coinInstrument (1/3) _ _).branch ((),true) p) = 1/3 ∧
305     mass ((coinInstrument (2/3) _ _).branch ((),true) p) = 2/3
306   rw [coin_true_on_prior _ _ _ p hp,coin_true_on_prior _ _ _ p hp]
307   norm_num
308 
309 theorem coins_branches_distinct : coinOne.branch ((),true) ≠ coinTwo.branch ((),true) := by
310   intro h
311   have hx := congrArg (fun F : (Fin 1 → ℝ) →ₗ[ℝ] (Fin 1 → ℝ) => mass (F (pointMass 0))) h
312   have hd := coins_likelihoods_differ_all_priors (pointMass 0) (point_prior 0)
313   rw [hd.1,hd.2] at hx
314   norm_num at hx
315 
316 theorem posterior_alone_does_not_imply_closure :
317     (∀ p, IsStrictPrior p →
318       normalize mass (coinOne.branch ((),true) p) = normalize mass (coinTwo.branch ((),true) p)) ∧
319     (LinearMap.id : (Fin 1 → ℝ) →ₗ[ℝ] (Fin 1 → ℝ)).comp (coinOne.branch ((),true)) ≠
320       (coinTwo.branch ((),true)).comp LinearMap.id := by
321   refine ⟨fun p hp => coins_posterior_agrees_all_priors p hp.1, ?_⟩
322   simpa using coins_branches_distinct
323 
324 theorem impossible_branch_not_prior :
325     ¬ IsPrior (normalize mass ((coinInstrument 0 le_rfl (by norm_num)).branch ((),true) (pointMass 0))) := by
326   rw [coin_true_on_prior _ _ _ _ (point_prior 0)]
327   intro h
328   have hh := h.2
329   norm_num [FiniteInstruments.normalize] at hh
330 
331 /-- This is an intentionally non-onto representation. -/
332 def embeddedScalar : ℝ →ₗ[ℝ] (Fin 2 → ℝ) :=
333   LinearMap.pi (fun j => if j.val=0 then LinearMap.id else 0)
334 
335 def invisibleDirection : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) :=
336   LinearMap.pi (fun j => if j.val=1 then LinearMap.proj 1 else 0)
337 
338 theorem invisible_on_representation : invisibleDirection.comp embeddedScalar = 0 := by
339   apply LinearMap.ext
340   intro x
341   funext j
342   fin_cases j <;> simp [invisibleDirection,embeddedScalar]
343 
344 theorem invisible_is_not_zero : invisibleDirection ≠ 0 := by
345   intro h
346   have hh := congrArg (fun F : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) => F (pointMass 1) 1) h
347   norm_num [invisibleDirection,pointMass] at hh
348 
349 theorem onto_required_for_uniqueness :
350     invisibleDirection.comp embeddedScalar = (0 : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ)).comp embeddedScalar ∧
351       invisibleDirection ≠ 0 := by
352   exact ⟨by simpa using invisible_on_representation, invisible_is_not_zero⟩
353 
354 
355 noncomputable def outsideState : Fin 2 → ℝ := fun j => if j.val=0 then 1 else 3
356 
357 theorem outside_probability_negative :
358     summaryMass (reducedBranch ((),false) outsideState) = -1/4 := by
359   norm_num [outsideState,summaryMass,reducedBranch,reducedMatrix,
360     Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
361 
362 theorem mass_one_does_not_imply_realizability :
363     summaryMass outsideState = 1 ∧ outsideState ∉ realizableBeliefs summary := by
364   constructor
365   · norm_num [summaryMass,outsideState]
366   · intro hz
367     have hp := reduced_likelihood_prior tinyInstrument summary reducedBranch summaryMass
368       summary_preserves_mass reduced_intertwining () outsideState hz
369     have hneg := hp.1 false
370     change 0 ≤ summaryMass (reducedBranch ((),false) outsideState) at hneg
371     rw [outside_probability_negative] at hneg
372     norm_num at hneg
373 
374 end Komorebi.LSM.Block4Examples

Back to source controls