ConditionalStochasticCompletion.lean

1 import KomorebiLSM.CanonicalCone
2 import KomorebiLSM.PositivePackets
3 import KomorebiLSM.CoreStability
4 import KomorebiLSM.FilteringStability
5 import KomorebiLSM.FiniteTableP32
6 import KomorebiLSM.ResetCertificate
7 
8 /-! P37: population-table reconstruction, its actual probability cone,
9 coordinate transport, full packet synthesis and conditional perturbation bounds.
10 Causality and global rank coverage are explicit population assumptions. -/
11 set_option autoImplicit false
12 namespace Komorebi.LSM.ConditionalStochasticCompletion
13 open scoped BigOperators
14 open FiniteInstruments Behavior
15 
16 section Exact
17 variable {A O I : Type*} [Fintype O] [Fintype I] [DecidableEq I]
18 variable (f : List (A × O) → ℝ) [FiniteDimensional ℝ (space f)]
19 variable (tests histories : I → List (A × O))
20 variable (hH : IsUnit (core f tests histories).det)
21 variable (hr : Module.finrank ℝ (space f) ≤ Fintype.card I)
22 
23 /-- The canonical cone transported by the constructed population-core isomorphism. -/
24 noncomputable def coreCone : Set (I → ℝ) :=
25   (coreEquiv f tests histories hH hr).symm ⁻¹' probabilityCone f
26 
27 omit [Fintype O] in
28 theorem coreCone_image : coreCone f tests histories hH hr =
29     (coreEquiv f tests histories hH hr) '' probabilityCone f := by
30   ext z
31   constructor
32   · intro hz
33     exact ⟨(coreEquiv f tests histories hH hr).symm z, hz,
34       (coreEquiv f tests histories hH hr).apply_symm_apply z⟩
35   · rintro ⟨v, hv, rfl⟩
36     simpa [coreCone] using hv
37 
38 omit [Fintype O] in
39 theorem coreCone_closed : IsClosed (coreCone f tests histories hH hr) :=
40   probabilityCone_closed.preimage
41     (coreEquiv f tests histories hH hr).symm.toContinuousLinearEquiv.continuous
42 
43 omit [Fintype O] in
44 theorem coreCone_convex : Convex ℝ (coreCone f tests histories hH hr) :=
45   probabilityCone_convex.linear_preimage
46     (coreEquiv f tests histories hH hr).symm.toLinearMap
47 
48 omit [Fintype O] in
49 theorem coreCone_pointed {z : I → ℝ}
50     (hz : z ∈ coreCone f tests histories hH hr)
51     (hn : -z ∈ coreCone f tests histories hH hr) : z = 0 := by
52   apply (coreEquiv f tests histories hH hr).symm.injective
53   rw [map_zero]
54   exact probabilityCone_pointed hz (by simpa [coreCone] using hn)
55 
56 theorem coreCone_spans (hf : CausalLaw f) :
57     Submodule.span ℝ (coreCone f tests histories hH hr) = ⊤ := by
58   rw [coreCone_image, Submodule.span_image_linearEquiv, probabilityCone_spans hf]
59   rw [Submodule.map_top]
60   exact LinearMap.range_eq_top.mpr (coreEquiv f tests histories hH hr).surjective
61 
62 omit [Fintype O] in
63 /-- The actual inferred symbol operator, not a supplied candidate, preserves the cone. -/
64 theorem coreCone_invariant (s : A × O) {z : I → ℝ}
65     (hz : z ∈ coreCone f tests histories hH hr) :
66     (reconstructed f tests histories s).mulVecLin z ∈ coreCone f tests histories hH hr := by
67   let e := coreEquiv f tests histories hH hr
68   have he : (reconstructed f tests histories s).mulVecLin z =
69       e (branch f s (e.symm z)) := by
70     have h := reconstructed_intertwines f tests histories hH hr s (e.symm z)
71     simpa only [show evaluate f tests = e.toLinearMap from rfl,
72       LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, Matrix.mulVecLin_apply] using h
73   rw [he]
74   change e.symm (e (branch f s (e.symm z))) ∈ probabilityCone f
75   rw [e.symm_apply_apply]
76   exact probabilityCone_invariant s hz
77 
78 omit [Fintype O] in
79 theorem core_mass (i₀ : I) (hi : tests i₀ = []) (z : I → ℝ) :
80     mass f ((coreEquiv f tests histories hH hr).symm z) = z i₀ := by
81   let e := coreEquiv f tests histories hH hr
82   have he := congrFun (e.apply_symm_apply z) i₀
83   change (e.symm z : List (A × O) → ℝ) (tests i₀) = z i₀ at he
84   simpa only [hi, Behavior.mass_apply] using he
85 
86 theorem coreCone_strict_mass (hf : CausalLaw f) (i₀ : I) (hi : tests i₀ = [])
87     {z : I → ℝ} (hz : z ∈ coreCone f tests histories hH hr) (hne : z ≠ 0) :
88     0 < z i₀ := by
89   rw [← core_mass f tests histories hH hr i₀ hi z]
90   apply probabilityCone_strict_mass hf hz
91   intro he
92   apply hne
93   exact (coreEquiv f tests histories hH hr).symm.injective (by simpa using he)
94 
95 theorem initial_coreCone (hf : CausalLaw f) :
96     tableState f tests [] ∈ coreCone f tests histories hH hr := by
97   change (coreEquiv f tests histories hH hr).symm
98     ((coreEquiv f tests histories hH hr) (history f [])) ∈ probabilityCone f
99   rw [LinearEquiv.symm_apply_apply]
100   exact history_mem_probabilityCone hf []
101 
102 include hH hr in
103 theorem core_instrument_mass (hf : CausalLaw f) (i₀ : I) (hi : tests i₀ = [])
104     (a : A) (z : I → ℝ) :
105     ∑ o, ((reconstructed f tests histories (a,o)).mulVecLin z) i₀ = z i₀ := by
106   let e := coreEquiv f tests histories hH hr
107   have he (s : A × O) :
108       (reconstructed f tests histories s).mulVecLin z =
109         e (branch f s (e.symm z)) := by
110     simpa only [show evaluate f tests = e.toLinearMap from rfl,
111       LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, Matrix.mulVecLin_apply] using
112       reconstructed_intertwines f tests histories hH hr s (e.symm z)
113   simp only [he]
114   change (∑ o, (branch f (a,o) (e.symm z) : List (A × O) → ℝ) (tests i₀)) = z i₀
115   rw [hi]
116   exact (hf.behavior_mass (e.symm z) a).trans (core_mass f tests histories hH hr i₀ hi z)
117 
118 /-- Every positive history is a normalized point of the transported cone,
119 with all future experiment probabilities given by the chronological ratio. -/
120 theorem conditional_core_history (hf : CausalLaw f) (i₀ : I) (hi : tests i₀ = [])
121     (h : List (A × O)) (hh : 0 < f h) :
122     ((f h)⁻¹ • tableState f tests h) ∈ coreCone f tests histories hH hr ∧
123     (((f h)⁻¹ • tableState f tests h) i₀ = 1) ∧
124     ∀ t, (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) t
125       ((f h)⁻¹ • tableState f tests h)) i₀ = f (h ++ t) / f h ∧
126       0 ≤ f (h ++ t) / f h ∧ f (h ++ t) / f h ≤ 1 := by
127   refine ⟨?_, ?_, ?_⟩
128   · change (coreEquiv f tests histories hH hr).symm
129       ((f h)⁻¹ • (coreEquiv f tests histories hH hr) (history f h)) ∈ probabilityCone f
130     rw [map_smul, LinearEquiv.symm_apply_apply]
131     exact probabilityCone_smul (inv_nonneg.mpr hh.le) (history_mem_probabilityCone hf h)
132   · simp [Pi.smul_apply, tableState_mass f tests i₀ hi h, ne_of_gt hh]
133   · intro t
134     refine ⟨?_, hf.conditional_bounds h t hh⟩
135     rw [map_smul]
136     have he := core_test_readout f tests histories hH hr i₀ hi t (history f h)
137     change (f h)⁻¹ * (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) t
138       (evaluate f tests (history f h))) i₀ = _
139     rw [he]
140     simp only [history_apply, div_eq_mul_inv, mul_comm]
141 
142 /-- P37's exact learned realization is minimal and correct on all finite words;
143 its normalized state and likelihood are recursively obtained from table matrices. -/
144 theorem exact_stochastic_completion (hf : CausalLaw f) (i₀ : I) (hi : tests i₀ = []) :
145     Module.finrank ℝ (space f) = Fintype.card I ∧
146     (tableModel f tests histories hH hr i₀ hi).IsReachable ∧
147     (tableModel f tests histories hH hr i₀ hi).IsObservable ∧
148     (∀ w, (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) w
149       (tableState f tests [])) i₀ = f w) ∧
150     (∀ h s, 0 < f h → 0 < f (h ++ [s]) →
151       0 < ((reconstructed f tests histories s).mulVecLin
152         ((f h)⁻¹ • tableState f tests h)) i₀ ∧
153       normalize (LinearMap.proj i₀)
154         ((reconstructed f tests histories s).mulVecLin
155           ((f h)⁻¹ • tableState f tests h)) =
156           (f (h ++ [s]))⁻¹ • tableState f tests (h ++ [s])) ∧
157     tableState f tests [] ∈ coreCone f tests histories hH hr ∧
158     (∀ s z, z ∈ coreCone f tests histories hH hr →
159       (reconstructed f tests histories s).mulVecLin z ∈ coreCone f tests histories hH hr) ∧
160     (∀ a z, ∑ o, ((reconstructed f tests histories (a,o)).mulVecLin z) i₀ = z i₀) := by
161   refine ⟨core_rank_exact f tests histories hH hr,
162     tableModel_reachable f tests histories hH hr i₀ hi,
163     tableModel_observable f tests histories hH hr i₀ hi,
164     reconstructed_probability f tests histories hH hr i₀ hi, ?_,
165     initial_coreCone f tests histories hH hr hf,
166     fun s _ => coreCone_invariant f tests histories hH hr s,
167     core_instrument_mass f tests histories hH hr hf i₀ hi⟩
168   intro h s hh hs
169   exact ⟨reconstructed_likelihood_pos f tests histories hH hr i₀ hi h s hh hs,
170     reconstructed_conditional_update f tests histories hH hr i₀ hi h s (ne_of_gt hh)⟩
171 
172 end Exact
173 
174 section Atlas
175 variable {S E F : Type*} [AddCommGroup E] [Module ℝ E]
176 variable [AddCommGroup F] [Module ℝ F]
177 
178 /-- All symbol maps are conjugated using the same invertible atlas. -/
179 def atlasOperator (T : E ≃ₗ[ℝ] F) (B : S → E →ₗ[ℝ] E) (s : S) : F →ₗ[ℝ] F :=
180   T.toLinearMap.comp ((B s).comp T.symm.toLinearMap)
181 
182 def atlasMass (T : E ≃ₗ[ℝ] F) (lam : E →ₗ[ℝ] ℝ) : F →ₗ[ℝ] ℝ :=
183   lam.comp T.symm.toLinearMap
184 
185 theorem atlas_word (T : E ≃ₗ[ℝ] F) (B : S → E →ₗ[ℝ] E)
186     (w : List S) (z : E) :
187     wordAction (atlasOperator T B) w (T z) = T (wordAction B w z) := by
188   induction w generalizing z with
189   | nil => rfl
190   | cons s w ih =>
191     simpa only [wordAction_cons, LinearMap.comp_apply, atlasOperator,
192       LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] using ih (B s z)
193 
194 theorem atlas_likelihood (T : E ≃ₗ[ℝ] F) (B : S → E →ₗ[ℝ] E)
195     (lam : E →ₗ[ℝ] ℝ) (w : List S) (z : E) :
196     atlasMass T lam (wordAction (atlasOperator T B) w (T z)) =
197       lam (wordAction B w z) := by
198   rw [atlas_word]
199   simp [atlasMass]
200 
201 theorem atlas_posterior (T : E ≃ₗ[ℝ] F) (lam : E →ₗ[ℝ] ℝ) (z : E) :
202     normalize (atlasMass T lam) (T z) = T (normalize lam z) := by
203   simp [FiniteInstruments.normalize, atlasMass]
204 
205 theorem atlas_cone_invariant (T : E ≃ₗ[ℝ] F) (B : S → E →ₗ[ℝ] E)
206     (C : Set E) (hc : ∀ s z, z ∈ C → B s z ∈ C) (s : S) {z : F}
207     (hz : z ∈ T '' C) : atlasOperator T B s z ∈ T '' C := by
208   obtain ⟨x, hx, rfl⟩ := hz
209   exact ⟨B s x, hc s x hx, by simp [atlasOperator]⟩
210 
211 /-- Completeness preserves the synthesized state before any probability readout. -/
212 theorem full_packet_prediction {J : Type*} [Fintype J]
213     (P : J → E →ₗ[ℝ] E) (hP : ∑ j, P j = LinearMap.id)
214     (B : S → E →ₗ[ℝ] E) (lam : E →ₗ[ℝ] ℝ) (w : List S) (z : E) :
215     lam (wordAction B w (∑ j, P j z)) = lam (wordAction B w z) := by
216   have he := congrArg (fun F : E →ₗ[ℝ] E => F z) hP
217   have hs : ∑ j, P j z = z := by
218     simpa only [LinearMap.sum_apply, LinearMap.id_apply] using he
219   rw [hs]
220 
221 end Atlas
222 section Perturbation
223 variable {r : ℕ}
224 
225 /-- Matrices act on the declared Euclidean core coordinates. -/
226 noncomputable def matrixOperator (M : Matrix (Fin r) (Fin r) ℝ) :
227     EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r) :=
228   M.toEuclideanLin.toContinuousLinearMap
229 
230 theorem matrixOperator_add (M N : Matrix (Fin r) (Fin r) ℝ) :
231     matrixOperator (M+N) = matrixOperator M + matrixOperator N := by
232   change LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin (M+N)) = _
233   rw [map_add, map_add]
234   rfl
235 
236 theorem matrixOperator_mul (M N : Matrix (Fin r) (Fin r) ℝ) :
237     matrixOperator (M*N) = (matrixOperator M).comp (matrixOperator N) := by
238   ext x i
239   change ((M*N).mulVec x) i = (M.mulVec (N.mulVec x)) i
240   rw [Matrix.mulVec_mulVec]
241 
242 variable {A O : Type*} (f : List (A × O) → ℝ)
243 variable (tests histories : Fin r → List (A × O))
244 
245 /-- The fit uses the observed shifted block and observed core, without a hidden operator. -/
246 noncomputable def tableFit (s : A × O) (E F : Matrix (Fin r) (Fin r) ℝ) :
247     EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r) :=
248   (matrixOperator (shiftedCore f tests histories s + F)).comp
249     (Identification.pinvL (matrixOperator (core f tests histories + E)))
250 
251 theorem tableFit_eq_coreFit (hH : IsUnit (core f tests histories).det)
252     (s : A × O) (E F : Matrix (Fin r) (Fin r) ℝ) :
253     tableFit f tests histories s E F =
254       Identification.coreFit (matrixOperator (core f tests histories))
255         (matrixOperator E) (matrixOperator F)
256         (matrixOperator (reconstructed f tests histories s)) := by
257   unfold tableFit Identification.coreFit
258   rw [matrixOperator_add, matrixOperator_add, ← matrixOperator_mul,
259     reconstructed_core_equation f tests histories hH s]
260 
261 theorem tableFit_error (hH : IsUnit (core f tests histories).det)
262     (s : A × O) (E F : Matrix (Fin r) (Fin r) ℝ)
263     (hE : ‖matrixOperator E‖ < Identification.rowGain (matrixOperator (core f tests histories))) :
264     ‖tableFit f tests histories s E F - matrixOperator (reconstructed f tests histories s)‖ ≤
265       (‖matrixOperator F‖ + ‖matrixOperator (reconstructed f tests histories s)‖ * ‖matrixOperator E‖) /
266         (Identification.rowGain (matrixOperator (core f tests histories)) - ‖matrixOperator E‖) := by
267   rw [tableFit_eq_coreFit f tests histories hH s E F]
268   exact Identification.core_error_bound _ _ _ _ hE
269 
270 /-- The actual table fit supplies the operator defects in the normalized
271 recursion. State bounds and branch likelihood margins remain explicit. -/
272 theorem tableFit_filtering_path (hH : IsUnit (core f tests histories).det)
273     (s : ℕ → A × O) (E F : ℕ → Matrix (Fin r) (Fin r) ℝ)
274     (z zhat : ℕ → EuclideanSpace ℝ (Fin r)) (i₀ : Fin r)
275     (R : ℝ) (ηhat : ℕ → ℝ)
276     (hE : ∀ t, ‖matrixOperator (E t)‖ <
277       Identification.rowGain (matrixOperator (core f tests histories)))
278     (true_step : ∀ t, z (t+1) = Filtering.normalize (EuclideanSpace.proj i₀)
279       (matrixOperator (reconstructed f tests histories (s t)) (z t)))
280     (fit_step : ∀ t, zhat (t+1) = Filtering.normalize (EuclideanSpace.proj i₀)
281       (tableFit f tests histories (s t) (E t) (F t) (zhat t)))
282     (hz : ∀ t, ‖z t‖ ≤ R)
283     (hp : ∀ t, (matrixOperator (reconstructed f tests histories (s t)) (z t)) i₀ ≠ 0)
284     (hq : ∀ t, ηhat t ≤ (tableFit f tests histories (s t) (E t) (F t) (zhat t)) i₀)
285     (hη : ∀ t, 0 < ηhat t) (T : ℕ) :
286     ‖zhat T-z T‖ ≤ Stability.errorEnvelope
287       (fun t => (1+R*‖(EuclideanSpace.proj i₀ : EuclideanSpace ℝ (Fin r) →L[ℝ] ℝ)‖) *
288         ‖tableFit f tests histories (s t) (E t) (F t)‖ / ηhat t)
289       (fun t => (1+R*‖(EuclideanSpace.proj i₀ : EuclideanSpace ℝ (Fin r) →L[ℝ] ℝ)‖) *
290         ((‖matrixOperator (F t)‖ + ‖matrixOperator (reconstructed f tests histories (s t))‖ *
291             ‖matrixOperator (E t)‖) /
292           (Identification.rowGain (matrixOperator (core f tests histories)) - ‖matrixOperator (E t)‖)) *
293           R / ηhat t) ‖zhat 0-z 0‖ T := by
294   exact Filtering.filtering_path (EuclideanSpace.proj i₀)
295     (fun t => matrixOperator (reconstructed f tests histories (s t)))
296     (fun t => tableFit f tests histories (s t) (E t) (F t)) z zhat R
297     (fun t => ‖tableFit f tests histories (s t) (E t) (F t)‖)
298     (fun t => (‖matrixOperator (F t)‖ + ‖matrixOperator (reconstructed f tests histories (s t))‖ *
299         ‖matrixOperator (E t)‖) /
300       (Identification.rowGain (matrixOperator (core f tests histories)) - ‖matrixOperator (E t)‖))
301     ηhat true_step fit_step (fun _ => le_rfl)
302     (fun t => tableFit_error f tests histories hH (s t) (E t) (F t) (hE t))
303     hz hp hq hη T
304 
305 end Perturbation
306 section ResetData
307 open MeasureTheory ProbabilityTheory
308 variable {A O Ω : Type*} [Fintype A] [Fintype O] [MeasurableSpace Ω]
309 variable {μ : Measure Ω} [IsProbabilityMeasure μ] {r N : ℕ}
310 
311 /-- One prospectively declared experiment set includes the core, all shifted
312 blocks and the initial vector. Repeated words may appear under different indices. -/
313 abbrev DataIndex (A O : Type*) (r : ℕ) :=
314   Sum (Fin r × Fin r) (Sum ((A × O) × Fin r × Fin r) (Fin r))
315 
316 def experimentWord (tests histories : Fin r → List (A × O)) :
317     DataIndex A O r → List (A × O)
318   | .inl (i,j) => histories j ++ tests i
319   | .inr (.inl (s,i,j)) => histories j ++ s :: tests i
320   | .inr (.inr i) => tests i
321 
322 noncomputable def estimatedCore
323     (X : DataIndex A O r → Fin N → Ω → ℝ) (ω : Ω) : Matrix (Fin r) (Fin r) ℝ :=
324   fun i j => ResetCertificate.sampleMean (X (.inl (i,j))) ω
325 
326 noncomputable def estimatedShift
327     (X : DataIndex A O r → Fin N → Ω → ℝ) (s : A × O) (ω : Ω) :
328     Matrix (Fin r) (Fin r) ℝ :=
329   fun i j => ResetCertificate.sampleMean (X (.inr (.inl (s,i,j)))) ω
330 
331 noncomputable def estimatedInitial
332     (X : DataIndex A O r → Fin N → Ω → ℝ) (ω : Ω) : EuclideanSpace ℝ (Fin r) :=
333   WithLp.toLp 2 (fun i => ResetCertificate.sampleMean (X (.inr (.inr i))) ω)
334 
335 /-- The sample event controls every matrix entry, hence actual operator norms,
336 and also the initial Euclidean state. It does not infer population rank. -/
337 theorem reset_table_event
338     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O)) (i₀ : Fin r)
339     (hN : 0 < N) (X : DataIndex A O r → Fin N → Ω → ℝ) {δ : ℝ}
340     (hδ : 0 < δ) (hδ1 : δ < 1)
341     (hind : ∀ w, iIndepFun (X w) μ) (hm : ∀ w i, Measurable (X w i))
342     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
343     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = f (experimentWord tests histories w)) :
344     1-δ ≤ μ.real {ω |
345       (∀ w, |ResetCertificate.sampleMean (X w) ω - f (experimentWord tests histories w)| ≤
346         ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ) ∧
347       ‖matrixOperator (estimatedCore X ω - core f tests histories)‖ ≤
348         r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ ∧
349       (∀ s, ‖matrixOperator (estimatedShift X s ω - shiftedCore f tests histories s)‖ ≤
350         r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ) ∧
351       ‖estimatedInitial X ω - WithLp.toLp 2 (fun i => f (tests i))‖ ≤
352         Real.sqrt r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ} := by
353   let : Nonempty (DataIndex A O r) := ⟨.inr (.inr i₀)⟩
354   have he := ResetCertificate.reset_probability_certificate hN X
355     (fun w => f (experimentWord tests histories w)) hδ hδ1 hind hm hb hp
356   apply he.trans (measureReal_mono ?_)
357   intro ω hω
358   refine ⟨hω, ?_, ?_, ?_⟩
359   · apply ResetCertificate.matrix_opNorm_le _ _ (Real.sqrt_nonneg _)
360     intro i j
361     exact hω (.inl (i,j))
362   · intro s
363     apply ResetCertificate.matrix_opNorm_le _ _ (Real.sqrt_nonneg _)
364     intro i j
365     exact hω (.inr (.inl (s,i,j)))
366   · apply ResetCertificate.vector_norm_le _ _ (Real.sqrt_nonneg _)
367     intro i
368     exact hω (.inr (.inr i))
369 
370 omit [Fintype A] [Fintype O] [MeasurableSpace Ω] in
371 /-- Substitution shows the inferred matrices use the sampled blocks themselves. -/
372 theorem sampled_tableFit
373     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O))
374     (X : DataIndex A O r → Fin N → Ω → ℝ) (s : A × O) (ω : Ω) :
375     tableFit f tests histories s (estimatedCore X ω - core f tests histories)
376       (estimatedShift X s ω - shiftedCore f tests histories s) =
377       (matrixOperator (estimatedShift X s ω)).comp
378         (Identification.pinvL (matrixOperator (estimatedCore X ω))) := by
379   simp [tableFit]
380 
381 /-- The same reset event also bounds every reconstructed symbol operator.
382 The positive core gap is separate from statistical coverage. -/
383 theorem reset_operator_event
384     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O)) (i₀ : Fin r)
385     (hH : IsUnit (core f tests histories).det)
386     (hN : 0 < N) (X : DataIndex A O r → Fin N → Ω → ℝ) {δ : ℝ}
387     (hδ : 0 < δ) (hδ1 : δ < 1)
388     (hind : ∀ w, iIndepFun (X w) μ) (hm : ∀ w i, Measurable (X w i))
389     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
390     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = f (experimentWord tests histories w))
391     (hgap : r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ <
392       Identification.rowGain (matrixOperator (core f tests histories))) :
393     1-δ ≤ μ.real {ω | ∀ s,
394       ‖(matrixOperator (estimatedShift X s ω)).comp
395           (Identification.pinvL (matrixOperator (estimatedCore X ω))) -
396           matrixOperator (reconstructed f tests histories s)‖ ≤
397         ((r:ℝ) * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ +
398           ‖matrixOperator (reconstructed f tests histories s)‖ *
399           ((r:ℝ) * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ)) /
400           (Identification.rowGain (matrixOperator (core f tests histories)) -
401             (r:ℝ) * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ)} := by
402   have he := reset_table_event f tests histories i₀ hN X hδ hδ1 hind hm hb hp
403   apply he.trans (measureReal_mono ?_)
404   intro ω hω s
405   rw [← sampled_tableFit f tests histories X s ω]
406   have hE := hω.2.1.trans_lt hgap
407   apply (tableFit_error f tests histories hH s _ _ hE).trans
408   have hnum := add_le_add (hω.2.2.1 s)
409     (mul_le_mul_of_nonneg_left hω.2.1
410       (norm_nonneg (matrixOperator (reconstructed f tests histories s))))
411   have hε : 0 ≤ (r:ℝ) * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ :=
412     (norm_nonneg _).trans hω.2.1
413   apply (div_le_div_of_nonneg_right hnum (sub_pos.mpr hE).le).trans
414   apply div_le_div_of_nonneg_left (by positivity) (sub_pos.mpr hgap)
415   exact sub_le_sub_left hω.2.1 _
416 
417 /-- On the very same simultaneous reset event, a separated population table
418 has the data-selected singular-subspace certificate. -/
419 theorem reset_spectral_event
420     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O)) (i₀ : Fin r)
421     (hN : 0 < N) (X : DataIndex A O r → Fin N → Ω → ℝ) {δ : ℝ}
422     (hδ : 0 < δ) (hδ1 : δ < 1)
423     (hind : ∀ w, iIndepFun (X w) μ) (hm : ∀ w i, Measurable (X w i))
424     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
425     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = f (experimentWord tests histories w))
426     (hrank : 0 < Module.finrank ℝ (matrixOperator (core f tests histories)).toLinearMap.range)
427     (hsmall : r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ <
428       Spectral.leastPositive (matrixOperator (core f tests histories)).toLinearMap / 2) :
429     1-δ ≤ μ.real {ω |
430       let M := matrixOperator (core f tests histories)
431       let E := matrixOperator (estimatedCore X ω - core f tests histories)
432       let ε := (r:ℝ) * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ
433       Spectral.leastPositive M.toLinearMap - ε ≤
434         (M+E).toLinearMap.singularValues (Module.finrank ℝ M.toLinearMap.range-1) ∧
435       (M+E).toLinearMap.singularValues (Module.finrank ℝ M.toLinearMap.range) ≤ ε ∧
436       ‖M.toLinearMap.range.starProjection - (Spectral.learnedLeft M E).starProjection‖ ≤
437         2*ε/Spectral.leastPositive M.toLinearMap ∧
438       2*ε/Spectral.leastPositive M.toLinearMap < 1} := by
439   have he := reset_table_event f tests histories i₀ hN X hδ hδ1 hind hm hb hp
440   apply he.trans (measureReal_mono ?_)
441   intro ω hω
442   exact Spectral.finite_table_stability _ _ hrank _ hω.2.1 hsmall
443 
444 /-- The four quantitative conclusions of the constructed finite-table subspace theorem. -/
445 def SpectralCertificate (M E : EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))
446     (ε : ℝ) : Prop :=
447   Spectral.leastPositive M.toLinearMap - ε ≤
448       (M+E).toLinearMap.singularValues (Module.finrank ℝ M.toLinearMap.range-1) ∧
449   (M+E).toLinearMap.singularValues (Module.finrank ℝ M.toLinearMap.range) ≤ ε ∧
450   ‖M.toLinearMap.range.starProjection - (Spectral.learnedLeft M E).starProjection‖ ≤
451     2*ε/Spectral.leastPositive M.toLinearMap ∧
452   2*ε/Spectral.leastPositive M.toLinearMap < 1
453 
454 /-- Joint conclusions indexed by one sample outcome, with one common entry budget. -/
455 def JointCertificate
456     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O))
457     (X : DataIndex A O r → Fin N → Ω → ℝ) (ω : Ω) (ε : ℝ) : Prop :=
458   ‖estimatedInitial X ω - WithLp.toLp 2 (fun i => f (tests i))‖ ≤ Real.sqrt r*ε ∧
459   ‖matrixOperator (estimatedCore X ω-core f tests histories)‖ ≤ r*ε ∧
460   (∀ s, ‖(matrixOperator (estimatedShift X s ω)).comp
461       (Identification.pinvL (matrixOperator (estimatedCore X ω))) -
462       matrixOperator (reconstructed f tests histories s)‖ ≤
463     ((r:ℝ)*ε + ‖matrixOperator (reconstructed f tests histories s)‖*((r:ℝ)*ε)) /
464       (Identification.rowGain (matrixOperator (core f tests histories))-(r:ℝ)*ε)) ∧
465   SpectralCertificate (matrixOperator (core f tests histories))
466     (matrixOperator (estimatedCore X ω-core f tests histories)) ((r:ℝ)*ε)
467 
468 omit [Fintype A] [Fintype O] [MeasurableSpace Ω] in
469 /-- One entry event implies all certificates together. No probability budgets
470 are added when the operator and spectral conclusions use the same data. -/
471 theorem simultaneous_certificates_of_entries
472     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O))
473     (hH : IsUnit (core f tests histories).det)
474     (X : DataIndex A O r → Fin N → Ω → ℝ) (ω : Ω) (ε : ℝ) (hε : 0 ≤ ε)
475     (hω : ∀ w, |ResetCertificate.sampleMean (X w) ω - f (experimentWord tests histories w)| ≤ ε)
476     (hgap : (r:ℝ)*ε < Identification.rowGain (matrixOperator (core f tests histories)))
477     (hrank : 0 < Module.finrank ℝ (matrixOperator (core f tests histories)).toLinearMap.range)
478     (hsmall : (r:ℝ)*ε < Spectral.leastPositive (matrixOperator (core f tests histories)).toLinearMap / 2) :
479     JointCertificate f tests histories X ω ε := by
480   have hcore : ‖matrixOperator (estimatedCore X ω-core f tests histories)‖ ≤ (r:ℝ)*ε := by
481     apply ResetCertificate.matrix_opNorm_le _ ε hε
482     intro i j
483     exact hω (.inl (i,j))
484   have hshift : ∀ s, ‖matrixOperator (estimatedShift X s ω-shiftedCore f tests histories s)‖ ≤ (r:ℝ)*ε := by
485     intro s
486     apply ResetCertificate.matrix_opNorm_le _ ε hε
487     intro i j
488     exact hω (.inr (.inl (s,i,j)))
489   refine ⟨?_, hcore, ?_, ?_⟩
490   · apply ResetCertificate.vector_norm_le _ ε hε
491     intro i
492     exact hω (.inr (.inr i))
493   · intro s
494     rw [← sampled_tableFit f tests histories X s ω]
495     have hE := hcore.trans_lt hgap
496     apply (tableFit_error f tests histories hH s _ _ hE).trans
497     have hnum := add_le_add (hshift s)
498       (mul_le_mul_of_nonneg_left hcore (norm_nonneg (matrixOperator (reconstructed f tests histories s))))
499     apply (div_le_div_of_nonneg_right hnum (sub_pos.mpr hE).le).trans
500     apply div_le_div_of_nonneg_left (by positivity) (sub_pos.mpr hgap)
501     exact sub_le_sub_left hcore _
502   · exact Spectral.finite_table_stability _ _ hrank _ hcore hsmall
503 
504 /-- P37's joint statistical event retains P35's original failure budget. -/
505 theorem reset_joint_event
506     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O)) (i₀ : Fin r)
507     (hH : IsUnit (core f tests histories).det)
508     (hN : 0 < N) (X : DataIndex A O r → Fin N → Ω → ℝ) {δ : ℝ}
509     (hδ : 0 < δ) (hδ1 : δ < 1)
510     (hind : ∀ w, iIndepFun (X w) μ) (hm : ∀ w i, Measurable (X w i))
511     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
512     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = f (experimentWord tests histories w))
513     (hgap : r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ <
514       Identification.rowGain (matrixOperator (core f tests histories)))
515     (hrank : 0 < Module.finrank ℝ (matrixOperator (core f tests histories)).toLinearMap.range)
516     (hsmall : r * ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ <
517       Spectral.leastPositive (matrixOperator (core f tests histories)).toLinearMap / 2) :
518     1-δ ≤ μ.real {ω | JointCertificate f tests histories X ω
519       (ResetCertificate.radius (Fintype.card (DataIndex A O r)) N δ)} := by
520   let : Nonempty (DataIndex A O r) := ⟨.inr (.inr i₀)⟩
521   have he := ResetCertificate.reset_probability_certificate hN X
522     (fun w => f (experimentWord tests histories w)) hδ hδ1 hind hm hb hp
523   apply he.trans (measureReal_mono ?_)
524   intro ω hω
525   exact simultaneous_certificates_of_entries f tests histories hH X ω _
526     (Real.sqrt_nonneg _) hω hgap hrank hsmall
527 
528 omit [Fintype A] [Fintype O] [MeasurableSpace Ω] in
529 /-- Filtering is conditional on branch margins and state bounds on the very
530 same joint event. It spends no new statistical error budget. -/
531 theorem filtering_on_joint_event
532     (f : List (A × O) → ℝ) (tests histories : Fin r → List (A × O))
533     (X : DataIndex A O r → Fin N → Ω → ℝ) (ω : Ω) (ε : ℝ)
534     (hc : JointCertificate f tests histories X ω ε)
535     (s : ℕ → A × O) (z zhat : ℕ → EuclideanSpace ℝ (Fin r)) (i₀ : Fin r)
536     (R : ℝ) (ηhat : ℕ → ℝ)
537     (true_step : ∀ t, z (t+1) = Filtering.normalize (EuclideanSpace.proj i₀)
538       (matrixOperator (reconstructed f tests histories (s t)) (z t)))
539     (fit_step : ∀ t, zhat (t+1) = Filtering.normalize (EuclideanSpace.proj i₀)
540       ((matrixOperator (estimatedShift X (s t) ω)).comp
541         (Identification.pinvL (matrixOperator (estimatedCore X ω))) (zhat t)))
542     (hz : ∀ t, ‖z t‖ ≤ R)
543     (hp : ∀ t, (matrixOperator (reconstructed f tests histories (s t)) (z t)) i₀ ≠ 0)
544     (hq : ∀ t, ηhat t ≤ ((matrixOperator (estimatedShift X (s t) ω)).comp
545       (Identification.pinvL (matrixOperator (estimatedCore X ω))) (zhat t)) i₀)
546     (hη : ∀ t, 0 < ηhat t) (T : ℕ) :
547     ‖zhat T-z T‖ ≤ Stability.errorEnvelope
548       (fun t => (1+R*‖(EuclideanSpace.proj i₀ : EuclideanSpace ℝ (Fin r) →L[ℝ] ℝ)‖) *
549         ‖(matrixOperator (estimatedShift X (s t) ω)).comp
550           (Identification.pinvL (matrixOperator (estimatedCore X ω)))‖ / ηhat t)
551       (fun t => (1+R*‖(EuclideanSpace.proj i₀ : EuclideanSpace ℝ (Fin r) →L[ℝ] ℝ)‖) *
552         (((r:ℝ)*ε + ‖matrixOperator (reconstructed f tests histories (s t))‖*((r:ℝ)*ε)) /
553           (Identification.rowGain (matrixOperator (core f tests histories))-(r:ℝ)*ε)) *
554           R / ηhat t) ‖zhat 0-z 0‖ T := by
555   exact Filtering.filtering_path (EuclideanSpace.proj i₀)
556     (fun t => matrixOperator (reconstructed f tests histories (s t)))
557     (fun t => (matrixOperator (estimatedShift X (s t) ω)).comp
558       (Identification.pinvL (matrixOperator (estimatedCore X ω)))) z zhat R
559     (fun t => ‖(matrixOperator (estimatedShift X (s t) ω)).comp
560       (Identification.pinvL (matrixOperator (estimatedCore X ω)))‖)
561     (fun t => ((r:ℝ)*ε + ‖matrixOperator (reconstructed f tests histories (s t))‖*((r:ℝ)*ε)) /
562       (Identification.rowGain (matrixOperator (core f tests histories))-(r:ℝ)*ε))
563     ηhat true_step fit_step (fun _ => le_rfl) (fun t => hc.2.2.1 (s t)) hz hp hq hη T
564 
565 end ResetData
566 end Komorebi.LSM.ConditionalStochasticCompletion

Back to source controls