ObservableRealization.lean

1 import KomorebiLSM.ObservableCore
2 
3 /-! P28 packaged as a population-table model, with full-law reconstruction,
4 minimal dimension and normalized history updates. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.Behavior
7 open scoped BigOperators
8 open FiniteInstruments
9 variable {S I : Type*} [Fintype I] [DecidableEq I]
10 
11 noncomputable def tableModel (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
12     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
13     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = []) :
14     Realization f (I → ℝ) where
15   initial := tableState f tests []
16   operator s := (reconstructed f tests histories s).mulVecLin
17   readout := LinearMap.proj i0
18   correct := reconstructed_probability f tests histories hH hr i0 hi
19 
20 /-- State-space dimension is minimal among all finite linear realizations. -/
21 theorem tableModel_minimal (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
22     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
23     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I)
24     {E : Type*} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E]
25     (r : Realization f E) : Fintype.card I ≤ Module.finrank ℝ E := by
26   rw [← core_rank_exact f tests histories hH hr]
27   exact r.behavior_dimension_le
28 
29 /-- In core coordinates the initial state really is the vector f(t_i). -/
30 theorem tableModel_initial (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
31     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
32     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = []) :
33     (tableModel f tests histories hH hr i0 hi).initial = fun i => f (tests i) := by
34   funext i
35   simp [tableModel,tableState]
36 
37 /-- All history columns are reachable in the inferred coordinate space. -/
38 theorem tableModel_reachable (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
39     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
40     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = []) :
41     (tableModel f tests histories hH hr i0 hi).IsReachable := by
42   let r := tableModel f tests histories hH hr i0 hi
43   apply top_unique
44   intro z _
45   obtain ⟨v,hv⟩ := evaluate_surjective f tests histories hH z
46   obtain ⟨c,rfl⟩ := synthesize_surjective f tests histories hH hr v
47   rw [← hv,synthesize_apply,map_sum]
48   apply Submodule.sum_mem
49   intro j _
50   rw [map_smul]
51   apply Submodule.smul_mem
52   have hstate : evaluate f tests (history f (histories j)) = r.state (histories j) :=
53     (reconstructed_state f tests histories hH hr (histories j)).symm
54   rw [hstate]
55   exact Submodule.subset_span ⟨histories j,rfl⟩
56 
57 /-- Core evaluation is the same change of coordinates for every future test. -/
58 theorem core_test_readout (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
59     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
60     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = [])
61     (w : List S) (v : space f) :
62     (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) w
63       (evaluate f tests v)) i0 = (v : List S → ℝ) w := by
64   have hcomm : ∀ s,
65       ((reconstructed f tests histories s).mulVecLin).comp (evaluate f tests) =
66         (evaluate f tests).comp (branch f s) := by
67     intro s
68     ext v i
69     exact congrFun (reconstructed_intertwines f tests histories hH hr s v) i
70   have hw := word_intertwining (branch f)
71     (fun s => (reconstructed f tests histories s).mulVecLin) (evaluate f tests) hcomm w
72   have he := congrArg (fun L : space f →ₗ[ℝ] (I → ℝ) => L v i0) hw
73   simpa only [LinearMap.comp_apply,evaluate_apply,hi,← mass_apply,test_evaluation] using he
74 
75 theorem tableModel_observable (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
76     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
77     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = []) :
78     (tableModel f tests histories hH hr i0 hi).IsObservable := by
79   intro x y h
80   obtain ⟨v,rfl⟩ := evaluate_surjective f tests histories hH x
81   obtain ⟨w,rfl⟩ := evaluate_surjective f tests histories hH y
82   apply congrArg (evaluate f tests)
83   apply Subtype.ext
84   funext t
85   have ht := congrFun h t
86   change (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) t
87     (evaluate f tests v)) i0 =
88     (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) t
89     (evaluate f tests w)) i0 at ht
90   simpa only [core_test_readout f tests histories hH hr i0 hi] using ht
91 
92 /-- Branch probability is the chronological joint/history ratio. -/
93 theorem reconstructed_likelihood (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
94     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
95     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = [])
96     (h : List S) (s : S) :
97     ((reconstructed f tests histories s).mulVecLin ((f h)⁻¹ • tableState f tests h)) i0 =
98       f (h ++ [s]) / f h := by
99   have hb : (reconstructed f tests histories s).mulVecLin (tableState f tests h) =
100       tableState f tests (h ++ [s]) := by
101     simpa only [Matrix.mulVecLin_apply,tableState_eq_evaluate,branch_history] using
102       reconstructed_intertwines f tests histories hH hr s (history f h)
103   rw [map_smul,hb]
104   simp only [Pi.smul_apply,smul_eq_mul,tableState_mass f tests i0 hi,div_eq_mul_inv,mul_comm]
105 
106 /-- Positive history and joint evidence give a positive conditioning denominator. -/
107 theorem reconstructed_likelihood_pos (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
108     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
109     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = [])
110     (h : List S) (s : S) (hh : 0 < f h) (hs : 0 < f (h ++ [s])) :
111     0 < ((reconstructed f tests histories s).mulVecLin
112       ((f h)⁻¹ • tableState f tests h)) i0 := by
113   rw [reconstructed_likelihood f tests histories hH hr i0 hi]
114   exact div_pos hs hh
115 
116 /-- P28: the matrices are explicitly G_s H^{-1}, with minimality, mass,
117 reachability, observability and correctness for every future word. -/
118 theorem observable_table_reconstruction (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
119     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
120     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = []) :
121     Module.finrank ℝ (space f) = Fintype.card I ∧
122     (tableModel f tests histories hH hr i0 hi).IsReachable ∧
123     (tableModel f tests histories hH hr i0 hi).IsObservable ∧
124     (∀ s, (tableModel f tests histories hH hr i0 hi).operator s =
125       (shiftedCore f tests histories s * (core f tests histories)⁻¹).mulVecLin) ∧
126     (∀ w, (tableModel f tests histories hH hr i0 hi).state w = tableState f tests w) := by
127   exact ⟨core_rank_exact f tests histories hH hr,
128     tableModel_reachable f tests histories hH hr i0 hi,
129     tableModel_observable f tests histories hH hr i0 hi,
130     fun _ => rfl,reconstructed_state f tests histories hH hr⟩
131 
132 end Komorebi.LSM.Behavior

Back to source controls