Block5Examples.lean

1 import KomorebiLSM.BehaviorProbability
2 import KomorebiLSM.PositivePackets
3 import KomorebiLSM.Block4Examples
4 import Mathlib.LinearAlgebra.Matrix.Notation
5 
6 /-! Exact population-table reconstruction and coverage counterexamples.
7 The table formula contains no hidden-state matrix; the declared generator is
8 used separately to prove this example's rank and probability hypotheses. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.Block5Examples
11 open scoped BigOperators
12 open FiniteInstruments Behavior
13 open Block4Examples
14 
15 noncomputable def process (w : List (Unit × Bool)) : ℝ :=
16   summaryMass (wordAction reducedBranch w (summary initialPrior))
17 
18 noncomputable def declaredModel : Behavior.Realization process (Fin 2 → ℝ) where
19   initial := summary initialPrior
20   operator := reducedBranch
21   readout := summaryMass
22   correct _ := rfl
23 
24 instance process_finite : FiniteDimensional ℝ (Behavior.space process) :=
25   declaredModel.behavior_finite
26 
27 theorem process_rank_upper : Module.finrank ℝ (Behavior.space process) ≤ 2 := by
28   simpa only [Module.finrank_fintype_fun_eq_card,Fintype.card_fin] using
29     declaredModel.behavior_dimension_le
30 
31 theorem process_equals_hidden (w : List (Unit × Bool)) :
32     process w = FiniteInstruments.mass (wordAction tinyInstrument.branch w initialPrior) :=
33   all_word_readouts w initialPrior
34 
35 theorem process_causal : Behavior.CausalLaw process := by
36   have he : process = fun w => FiniteInstruments.mass (wordAction tinyInstrument.branch w initialPrior) :=
37     funext process_equals_hidden
38   rw [he]
39   exact instrument_causal tinyInstrument initialPrior initial_prior_valid
40 
41 theorem every_process_word_valid (w : List (Unit × Bool)) : 0 ≤ process w ∧ process w ≤ 1 :=
42   process_causal.word_bounds w
43 
44 noncomputable def selected (i : Fin 2) : List (Unit × Bool) :=
45   if i.val=0 then [] else [((),true)]
46 
47 theorem first_test_empty : selected 0 = [] := rfl
48 
49 theorem initial_vector : summary initialPrior = ![(1 : ℝ),1/2] := by
50   funext i
51   fin_cases i
52   · exact initial_predictive_state.1
53   · exact initial_predictive_state.2
54 
55 theorem population_core : Behavior.core process selected selected =
56     !![(1 : ℝ),5/8;5/8,15/32] := by
57   ext i j
58   fin_cases i <;> fin_cases j <;>
59     norm_num [Behavior.core,selected,process,wordAction,initial_vector,summaryMass,
60       reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
61 
62 theorem core_determinant : (Behavior.core process selected selected).det = 5/64 := by
63   rw [population_core]
64   norm_num [Matrix.det_fin_two]
65 
66 theorem core_invertible : IsUnit (Behavior.core process selected selected).det := by
67   rw [core_determinant]
68   norm_num
69 
70 theorem full_behavior_rank_two : Module.finrank ℝ (Behavior.space process) = 2 := by
71   simpa only [Fintype.card_fin] using
72     core_rank_exact process selected selected core_invertible process_rank_upper
73 
74 theorem no_scalar_full_rank_bound : ¬ Module.finrank ℝ (Behavior.space process) ≤ 1 := by
75   rw [full_behavior_rank_two]
76   norm_num
77 
78 theorem shifted_false : shiftedCore process selected selected ((),false) =
79     !![(3/8 : ℝ),5/32;3/16,5/64] := by
80   ext i j
81   fin_cases i <;> fin_cases j <;>
82     norm_num [shiftedCore,selected,process,wordAction,initial_vector,summaryMass,
83       reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
84 
85 theorem shifted_true : shiftedCore process selected selected ((),true) =
86     !![(5/8 : ℝ),15/32;15/32,45/128] := by
87   ext i j
88   fin_cases i <;> fin_cases j <;>
89     norm_num [shiftedCore,selected,process,wordAction,initial_vector,summaryMass,
90       reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
91 
92 theorem learned_false : reconstructed process selected selected ((),false) =
93     !![(1 : ℝ),-1;1/2,-1/2] := by
94   symm
95   apply reconstructed_unique process selected selected core_invertible
96   rw [population_core,shifted_false]
97   ext i j
98   fin_cases i <;> fin_cases j <;> norm_num [Matrix.mul_apply,Fin.sum_univ_succ]
99 
100 theorem learned_true : reconstructed process selected selected ((),true) =
101     !![(0 : ℝ),1;0,3/4] := by
102   symm
103   apply reconstructed_unique process selected selected core_invertible
104   rw [population_core,shifted_true]
105   ext i j
106   fin_cases i <;> fin_cases j <;> norm_num [Matrix.mul_apply,Fin.sum_univ_succ]
107 
108 theorem learned_initial : tableState process selected [] = ![(1 : ℝ),5/8] := by
109   funext i
110   fin_cases i <;>
111     norm_num [tableState,selected,process,wordAction,initial_vector,summaryMass,
112       reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
113 
114 /-- This is the general all-word theorem applied to the exact population core. -/
115 theorem learned_all_words (w : List (Unit × Bool)) :
116     (wordAction (fun s => (reconstructed process selected selected s).mulVecLin) w
117       (tableState process selected [])) 0 = process w :=
118   reconstructed_probability process selected selected core_invertible
119     process_rank_upper 0 first_test_empty w
120 
121 theorem learned_reachable_and_observable :
122     (tableModel process selected selected core_invertible process_rank_upper 0 first_test_empty).IsReachable ∧
123     (tableModel process selected selected core_invertible process_rank_upper 0 first_test_empty).IsObservable :=
124   ⟨tableModel_reachable process selected selected core_invertible process_rank_upper 0 first_test_empty,
125    tableModel_observable process selected selected core_invertible process_rank_upper 0 first_test_empty⟩
126 
127 theorem learned_two_symbols_in_time_order :
128     process [((),true),((),false)] = 5/32 ∧ process [((),false),((),true)] = 3/16 := by
129   rw [process_equals_hidden,process_equals_hidden]
130   exact ⟨true_then_false_probability,false_then_true_probability⟩
131 
132 theorem learned_negative_entry : reconstructed process selected selected ((),false) 0 1 = -1 := by
133   rw [learned_false]
134   rfl
135 
136 theorem true_history_state : tableState process selected [((),true)] = ![(5/8 : ℝ),15/32] := by
137   funext i
138   fin_cases i <;>
139     norm_num [tableState,selected,process,wordAction,initial_vector,summaryMass,
140       reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
141 
142 theorem double_true_history_state : tableState process selected [((),true),((),true)] =
143     ![(15/32 : ℝ),45/128] := by
144   funext i
145   fin_cases i <;>
146     norm_num [tableState,selected,process,wordAction,initial_vector,summaryMass,
147       reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
148 
149 theorem normalized_true_state :
150     (process [((),true)])⁻¹ • tableState process selected [((),true)] = ![(1 : ℝ),3/4] := by
151   have hmass := tableState_mass process selected 0 first_test_empty [((),true)]
152   rw [true_history_state] at hmass
153   rw [← hmass,true_history_state]
154   ext i
155   fin_cases i <;> norm_num
156 
157 theorem normalized_double_true_state :
158     (process [((),true),((),true)])⁻¹ • tableState process selected [((),true),((),true)] =
159       ![(1 : ℝ),3/4] := by
160   have hmass := tableState_mass process selected 0 first_test_empty [((),true),((),true)]
161   rw [double_true_history_state] at hmass
162   rw [← hmass,double_true_history_state]
163   ext i
164   fin_cases i <;> norm_num
165 
166 theorem different_histories_same_conditional_behavior :
167     (process [((),true)])⁻¹ • history process [((),true)] =
168       (process [((),true),((),true)])⁻¹ • history process [((),true),((),true)] := by
169   apply (evaluate_bijective process selected selected core_invertible process_rank_upper).1
170   simpa only [map_smul,← tableState_eq_evaluate] using
171     normalized_true_state.trans normalized_double_true_state.symm
172 
173 theorem different_histories_equal_every_conditional_test (t : List (Unit × Bool)) :
174     process ([((),true)] ++ t) / process [((),true)] =
175       process ([((),true),((),true)] ++ t) / process [((),true),((),true)] :=
176   (conditional_equivalence process _ _).mp different_histories_same_conditional_behavior t
177 
178 /-- A one-entry core is invertible, but does not cover this rank-two process. -/
179 noncomputable def undersized : Fin 1 → List (Unit × Bool) := fun _ => []
180 
181 theorem small_core_invertible : IsUnit (Behavior.core process undersized undersized).det := by
182   have he : Behavior.core process undersized undersized = (1 : Matrix (Fin 1) (Fin 1) ℝ) := by
183     ext i j
184     fin_cases i; fin_cases j
185     norm_num [Behavior.core,undersized,process,wordAction,initial_vector,summaryMass]
186   rw [he,Matrix.det_one]
187   exact isUnit_one
188 
189 theorem undersized_true_matrix : reconstructed process undersized undersized ((),true) =
190     (5/8 : ℝ) • (1 : Matrix (Fin 1) (Fin 1) ℝ) := by
191   symm
192   apply reconstructed_unique process undersized undersized small_core_invertible
193   ext i j
194   fin_cases i; fin_cases j
195   norm_num [Behavior.core,undersized,shiftedCore,process,wordAction,initial_vector,summaryMass,
196     reducedBranch,reducedMatrix,Matrix.mul_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
197 
198 theorem undersized_initial : tableState process undersized [] = fun _ => (1 : ℝ) := by
199   funext i
200   norm_num [tableState,undersized,process,wordAction,initial_vector,summaryMass]
201 
202 /-- An invertible finite table by itself does not identify every future word. -/
203 theorem finite_table_without_coverage_fails :
204     (wordAction (fun s => (reconstructed process undersized undersized s).mulVecLin)
205       [((),true),((),true)] (tableState process undersized [])) 0 ≠
206         process [((),true),((),true)] := by
207   have hmass := tableState_mass process selected 0 first_test_empty [((),true),((),true)]
208   rw [double_true_history_state] at hmass
209   rw [← hmass]
210   norm_num [wordAction,undersized_true_matrix,undersized_initial,Matrix.mulVec,dotProduct,
211     Fin.sum_univ_succ]
212 
213 /-- The redundant three-state hidden model is not observable, despite reproducing f. -/
214 noncomputable def hiddenModel : Behavior.Realization process (Fin 3 → ℝ) where
215   initial := initialPrior
216   operator := tinyInstrument.branch
217   readout := FiniteInstruments.mass
218   correct w := (process_equals_hidden w).symm
219 
220 theorem hidden_model_not_observable : ¬ hiddenModel.IsObservable := by
221   intro ho
222   apply distinct_hidden_priors
223   apply ho
224   funext w
225   exact same_every_future_word w
226 
227 
228 noncomputable def haarDetail : Matrix (Fin 2) (Fin 2) ℝ :=
229   !![1/2,-1/2;-1/2,1/2]
230 
231 noncomputable def haarAverage : Matrix (Fin 2) (Fin 2) ℝ :=
232   !![1/2,1/2;1/2,1/2]
233 
234 theorem haar_complete : haarAverage + haarDetail = 1 := by
235   ext i j
236   fin_cases i <;> fin_cases j <;> norm_num [haarAverage,haarDetail]
237 
238 theorem haar_idempotent : haarDetail * haarDetail = haarDetail ∧
239     haarAverage * haarAverage = haarAverage := by
240   constructor <;> ext i j <;> fin_cases i <;> fin_cases j <;>
241     norm_num [haarAverage,haarDetail,Matrix.mul_apply,Fin.sum_univ_succ]
242 
243 theorem haar_detail_signed : haarDetail.mulVec ![(3/4 : ℝ),1/4] = ![(1/4 : ℝ),-1/4] := by
244   ext i
245   fin_cases i <;> norm_num [haarDetail,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
246 
247 theorem haar_detail_not_probability :
248     ¬ (∀ i, 0 ≤ haarDetail.mulVec ![(3/4 : ℝ),1/4] i) := by
249   intro h
250   have he := h 1
251   rw [haar_detail_signed] at he
252   norm_num at he
253 
254 theorem signed_packet_can_have_zero_mass :
255     FiniteInstruments.mass (haarDetail.mulVec ![(3/4 : ℝ),1/4]) = 0 ∧
256       haarDetail.mulVec ![(3/4 : ℝ),1/4] ≠ 0 := by
257   rw [haar_detail_signed]
258   constructor
259   · norm_num [FiniteInstruments.mass_apply,Fin.sum_univ_succ]
260   · intro h
261     have he := congrFun h 0
262     norm_num at he
263 
264 noncomputable def selector (j : Fin 2) : Matrix (Fin 2) (Fin 2) ℝ :=
265   Matrix.diagonal (fun i => if i=j then 1 else 0)
266 
267 theorem selector_positive (j : Fin 2) (x : Fin 2 → ℝ) (hx : ∀ i, 0 ≤ x i) :
268     ∀ i, 0 ≤ (selector j).mulVec x i := by
269   apply (PositivePackets.orthant_preserving_iff (selector j)).mpr
270   · intro i k
271     fin_cases j <;> fin_cases i <;> fin_cases k <;> norm_num [selector]
272   · exact hx
273 
274 theorem selector_complete : ∑ j : Fin 2, (selector j).mulVecLin = LinearMap.id := by
275   apply LinearMap.ext
276   intro x
277   funext i
278   fin_cases i <;> simp [selector,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
279 
280 /-- A true positive packet family instantiates the general mixture theorem. -/
281 theorem coordinate_packet_mixture (z : Fin 2 → ℝ) (hz : ∀ i, 0 ≤ z i) :
282     ∑ j ∈ Finset.univ.filter
283       (fun j : Fin 2 => 0 < FiniteInstruments.mass ((selector j).mulVecLin z)),
284       FiniteInstruments.mass ((selector j).mulVecLin z) •
285       ((FiniteInstruments.mass ((selector j).mulVecLin z))⁻¹ • (selector j).mulVecLin z) = z := by
286   exact PositivePackets.positive_packet_mixture {x : Fin 2 → ℝ | ∀ i, 0 ≤ x i}
287     FiniteInstruments.mass PositivePackets.orthant_strict_mass
288     (fun j => (selector j).mulVecLin) selector_positive selector_complete z hz
289 
290 theorem coordinate_weights :
291     FiniteInstruments.mass ((selector 0).mulVec ![(3/4 : ℝ),1/4]) = 3/4 ∧
292     FiniteInstruments.mass ((selector 1).mulVec ![(3/4 : ℝ),1/4]) = 1/4 := by
293   norm_num [selector,FiniteInstruments.mass_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
294 
295 
296 theorem inverse_core_explicit : (Behavior.core process selected selected)⁻¹ =
297     !![(6 : ℝ),-8;-8,64/5] := by
298   apply Matrix.inv_eq_left_inv
299   rw [population_core]
300   ext i j
301   fin_cases i <;> fin_cases j <;> norm_num [Matrix.mul_apply,Fin.sum_univ_succ]
302 
303 theorem inverse_side_matters :
304     (Behavior.core process selected selected)⁻¹ * shiftedCore process selected selected ((),false) ≠
305       reconstructed process selected selected ((),false) := by
306   intro he
307   have hh := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℝ => M 0 0) he
308   rw [inverse_core_explicit,shifted_false,learned_false] at hh
309   norm_num [Matrix.mul_apply,Fin.sum_univ_succ] at hh
310 
311 
312 noncomputable def signedProcess (w : List Unit) : ℝ := (-1) ^ w.length
313 
314 theorem negative_word_action (w : List Unit) (x : ℝ) :
315     wordAction (fun _ : Unit => -(LinearMap.id : ℝ →ₗ[ℝ] ℝ)) w x = (-1 : ℝ)^w.length * x := by
316   induction w generalizing x with
317   | nil => simp
318   | cons s w ih =>
319     simp only [wordAction_cons,LinearMap.comp_apply,LinearMap.neg_apply,LinearMap.id_apply,
320       ih,List.length_cons,pow_succ]
321     ring
322 
323 noncomputable def signedModel : Behavior.Realization signedProcess ℝ where
324   initial := 1
325   operator _ := -LinearMap.id
326   readout := LinearMap.id
327   correct w := by simp [negative_word_action,signedProcess]
328 
329 instance signed_process_finite : FiniteDimensional ℝ (Behavior.space signedProcess) :=
330   signedModel.behavior_finite
331 
332 theorem signed_process_rank_at_most_one : Module.finrank ℝ (Behavior.space signedProcess) ≤ 1 := by
333   simpa only [Module.finrank_self] using signedModel.behavior_dimension_le
334 
335 theorem finite_rank_is_not_probability : signedProcess [()] = -1 := by
336   norm_num [signedProcess]
337 
338 end Komorebi.LSM.Block5Examples

Back to source controls