ObservableCore.lean

1 import KomorebiLSM.BehaviorMinimality
2 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
3 
4 /-! P28: an invertible population core plus a global behavior-rank bound
5 constructs an isomorphism, not merely interpolation of the observed columns. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Behavior
8 open scoped BigOperators
9 open FiniteInstruments
10 variable {S I : Type*} [Fintype I] [DecidableEq I]
11 
12 noncomputable def evaluate (f : List S → ℝ) (tests : I → List S) :
13     space f →ₗ[ℝ] (I → ℝ) :=
14   LinearMap.pi (fun i => (LinearMap.proj (tests i)).comp (space f).subtype)
15 
16 omit [Fintype I] [DecidableEq I] in
17 @[simp] theorem evaluate_apply (f : List S → ℝ) (tests : I → List S)
18     (v : space f) (i : I) : evaluate f tests v i = (v : List S → ℝ) (tests i) := rfl
19 
20 noncomputable def core (f : List S → ℝ) (tests histories : I → List S) : Matrix I I ℝ :=
21   fun i j => f (histories j ++ tests i)
22 
23 noncomputable def shiftedCore (f : List S → ℝ) (tests histories : I → List S)
24     (s : S) : Matrix I I ℝ :=
25   fun i j => f (histories j ++ s :: tests i)
26 
27 noncomputable def synthesize (f : List S → ℝ) (histories : I → List S) :
28     (I → ℝ) →ₗ[ℝ] space f :=
29   ∑ j, (LinearMap.proj j).smulRight (history f (histories j))
30 
31 omit [DecidableEq I] in
32 @[simp] theorem synthesize_apply (f : List S → ℝ) (histories : I → List S) (c : I → ℝ) :
33     synthesize f histories c = ∑ j, c j • history f (histories j) := by
34   simp [synthesize,LinearMap.sum_apply]
35 
36 omit [DecidableEq I] in
37 /-- The actual test map composed with column synthesis is exactly the core. -/
38 theorem evaluate_synthesize (f : List S → ℝ) (tests histories : I → List S) (c : I → ℝ) :
39     evaluate f tests (synthesize f histories c) = (core f tests histories).mulVec c := by
40   funext i
41   simp [synthesize_apply,core,Matrix.mulVec,dotProduct,mul_comm]
42 
43 omit [DecidableEq I] in
44 theorem evaluate_shift_synthesize (f : List S → ℝ) (tests histories : I → List S)
45     (s : S) (c : I → ℝ) :
46     evaluate f tests (branch f s (synthesize f histories c)) =
47       (shiftedCore f tests histories s).mulVec c := by
48   funext i
49   simp [synthesize_apply,map_sum,map_smul,shiftedCore,Matrix.mulVec,dotProduct,
50     List.append_assoc,mul_comm]
51 
52 /-- Invertibility yields surjectivity of the test evaluations without a rank bound. -/
53 theorem evaluate_surjective (f : List S → ℝ) (tests histories : I → List S)
54     (hH : IsUnit (core f tests histories).det) : Function.Surjective (evaluate f tests) := by
55   intro z
56   have hs := Matrix.mulVec_surjective_iff_isUnit.mpr
57     ((core f tests histories).isUnit_iff_isUnit_det.mpr hH)
58   obtain ⟨c,hc⟩ := hs z
59   exact ⟨synthesize f histories c,(evaluate_synthesize f tests histories c).trans hc⟩
60 
61 /-- Invertibility gives a lower rank bound; the upper bound is a separate hypothesis. -/
62 theorem core_rank_exact (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
63     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
64     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) :
65     Module.finrank ℝ (space f) = Fintype.card I := by
66   apply le_antisymm hr
67   simpa only [Module.finrank_fintype_fun_eq_card] using
68     LinearMap.finrank_le_finrank_of_surjective (evaluate_surjective f tests histories hH)
69 
70 theorem evaluate_bijective (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
71     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
72     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) :
73     Function.Bijective (evaluate f tests) := by
74   have hd : Module.finrank ℝ (space f) = Module.finrank ℝ (I → ℝ) := by
75     simpa only [Module.finrank_fintype_fun_eq_card] using core_rank_exact f tests histories hH hr
76   have hs := evaluate_surjective f tests histories hH
77   exact ⟨(LinearMap.injective_iff_surjective_of_finrank_eq_finrank hd).mpr hs,hs⟩
78 
79 /-- The chosen history columns span the full behavior space only after using coverage. -/
80 theorem synthesize_surjective (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
81     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
82     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) :
83     Function.Surjective (synthesize f histories) := by
84   intro v
85   have hs := Matrix.mulVec_surjective_iff_isUnit.mpr
86     ((core f tests histories).isUnit_iff_isUnit_det.mpr hH)
87   obtain ⟨c,hc⟩ := hs (evaluate f tests v)
88   exact ⟨c,(evaluate_bijective f tests histories hH hr).1
89     ((evaluate_synthesize f tests histories c).trans hc)⟩
90 
91 noncomputable def coreEquiv (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
92     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
93     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) :
94     space f ≃ₗ[ℝ] (I → ℝ) := LinearEquiv.ofBijective _ (evaluate_bijective f tests histories hH hr)
95 
96 /-- Only population table entries occur in this formula. -/
97 noncomputable def reconstructed (f : List S → ℝ) (tests histories : I → List S)
98     (s : S) : Matrix I I ℝ := shiftedCore f tests histories s * (core f tests histories)⁻¹
99 
100 /-- The formula G H^{-1} acts correctly on every behavior state. -/
101 theorem reconstructed_intertwines (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
102     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
103     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (s : S) (v : space f) :
104     (reconstructed f tests histories s).mulVec (evaluate f tests v) =
105       evaluate f tests (branch f s v) := by
106   obtain ⟨c,rfl⟩ := synthesize_surjective f tests histories hH hr v
107   rw [evaluate_synthesize,evaluate_shift_synthesize]
108   rw [Matrix.mulVec_mulVec,reconstructed,
109     Matrix.nonsing_inv_mul_cancel_right _ _ hH]
110 
111 theorem reconstructed_core_equation (f : List S → ℝ) (tests histories : I → List S)
112     (hH : IsUnit (core f tests histories).det) (s : S) :
113     reconstructed f tests histories s * core f tests histories = shiftedCore f tests histories s := by
114   exact Matrix.nonsing_inv_mul_cancel_right _ _ hH
115 
116 /-- The same full-rank core makes the reconstructed matrix unique. -/
117 theorem reconstructed_unique (f : List S → ℝ) (tests histories : I → List S)
118     (hH : IsUnit (core f tests histories).det) (s : S) (D : Matrix I I ℝ)
119     (hD : D * core f tests histories = shiftedCore f tests histories s) :
120     D = reconstructed f tests histories s := by
121   rw [reconstructed,← hD,Matrix.mul_nonsing_inv_cancel_right _ _ hH]
122 
123 noncomputable def tableState (f : List S → ℝ) (tests : I → List S) (h : List S) : I → ℝ :=
124   fun i => f (h ++ tests i)
125 
126 omit [Fintype I] [DecidableEq I] in
127 theorem tableState_eq_evaluate (f : List S → ℝ) (tests : I → List S) (h : List S) :
128     tableState f tests h = evaluate f tests (history f h) := rfl
129 
130 /-- Every history, not only the columns used in the inverse, is recovered. -/
131 theorem reconstructed_state (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
132     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
133     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (w : List S) :
134     wordAction (fun s => (reconstructed f tests histories s).mulVecLin) w
135       (tableState f tests []) = tableState f tests w := by
136   have hi : ∀ s,
137       ((reconstructed f tests histories s).mulVecLin).comp (evaluate f tests) =
138         (evaluate f tests).comp (branch f s) := by
139     intro s
140     ext v i
141     exact congrFun (reconstructed_intertwines f tests histories hH hr s v) i
142   have hw := word_intertwining (branch f)
143     (fun s => (reconstructed f tests histories s).mulVecLin) (evaluate f tests) hi w
144   have he := congrArg (fun L : space f →ₗ[ℝ] (I → ℝ) => L (history f [])) hw
145   simpa only [LinearMap.comp_apply,word_history,List.nil_append,tableState_eq_evaluate] using he
146 
147 omit [Fintype I] [DecidableEq I] in
148 /-- A designated empty test is the literal mass coordinate. -/
149 theorem tableState_mass (f : List S → ℝ) (tests : I → List S) (i0 : I)
150     (hi : tests i0 = []) (h : List S) : tableState f tests h i0 = f h := by
151   simp [tableState,hi]
152 
153 theorem reconstructed_probability (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
154     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
155     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = [])
156     (w : List S) :
157     (wordAction (fun s => (reconstructed f tests histories s).mulVecLin) w
158       (tableState f tests [])) i0 = f w := by
159   rw [reconstructed_state f tests histories hH hr]
160   exact tableState_mass f tests i0 hi w
161 
162 /-- The inferred state is updated after a positive-probability history. -/
163 theorem reconstructed_conditional_update (f : List S → ℝ) [FiniteDimensional ℝ (space f)]
164     (tests histories : I → List S) (hH : IsUnit (core f tests histories).det)
165     (hr : Module.finrank ℝ (space f) ≤ Fintype.card I) (i0 : I) (hi : tests i0 = [])
166     (h : List S) (s : S) (hh : f h ≠ 0) :
167     normalize (LinearMap.proj i0)
168       ((reconstructed f tests histories s).mulVecLin ((f h)⁻¹ • tableState f tests h)) =
169       (f (h ++ [s]))⁻¹ • tableState f tests (h ++ [s]) := by
170   have hb : (reconstructed f tests histories s).mulVecLin (tableState f tests h) =
171       tableState f tests (h ++ [s]) := by
172     simpa only [Matrix.mulVecLin_apply,tableState_eq_evaluate,branch_history] using
173       reconstructed_intertwines f tests histories hH hr s (history f h)
174   rw [map_smul,hb]
175   simp only [FiniteInstruments.normalize,map_smul,LinearMap.proj_apply,tableState_mass f tests i0 hi,
176     smul_eq_mul,mul_inv_rev,inv_inv,smul_smul]
177   rw [mul_assoc, mul_inv_cancel₀ hh, mul_one]
178 
179 end Komorebi.LSM.Behavior

Back to source controls