CertifiedTemplate.lean

1 import KomorebiLSM.PolynomialGramP53
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 import Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
4 import Mathlib.Tactic
5 
6 /-! Proposition 60: exact recognition of one fixed certified polynomial template.
7 Matching is a finite scalar linear system. Observability proves uniqueness of
8 all matches, while certificate transport requires an invertible match and an
9 independent check of the fitted initial state. -/
10 set_option autoImplicit false
11 namespace Komorebi.LSM.CertifiedTemplate
12 open scoped BigOperators Matrix
13 open FiniteInstruments
14 
15 section Matching
16 variable {E S : Type*} [AddCommGroup E] [Module ℝ E]
17 
18 /-- The exact coefficient and mass equations, with no invertibility assumed. -/
19 def Matches (C Chat : S → E →ₗ[ℝ] E) (l lhat : E →ₗ[ℝ] ℝ) (T : E →ₗ[ℝ] E) : Prop :=
20   (∀ s, (Chat s).comp T=T.comp (C s)) ∧ lhat.comp T=l
21 
22 /-- All unknowns occur linearly; the mass target is the inhomogeneous part. -/
23 def constraintMap (C Chat : S → E →ₗ[ℝ] E) (lhat : E →ₗ[ℝ] ℝ) :
24     (E →ₗ[ℝ] E) →ₗ[ℝ] ((S → E →ₗ[ℝ] E) × (E →ₗ[ℝ] ℝ)) where
25   toFun T := (fun s => (Chat s).comp T-T.comp (C s),lhat.comp T)
26   map_add' T U := by
27     apply Prod.ext
28     · funext s
29       simp [LinearMap.comp_add,LinearMap.add_comp]
30       abel
31     · simp [LinearMap.comp_add]
32   map_smul' a T := by
33     apply Prod.ext
34     · funext s
35       simp [LinearMap.comp_smul,LinearMap.smul_comp,smul_sub]
36     · simp [LinearMap.comp_smul]
37 
38 theorem matches_iff_linear_system (C Chat : S → E →ₗ[ℝ] E)
39     (l lhat : E →ₗ[ℝ] ℝ) (T : E →ₗ[ℝ] E) :
40     Matches C Chat l lhat T ↔ constraintMap C Chat lhat T=(0,l) := by
41   constructor
42   · rintro ⟨hc,hm⟩
43     apply Prod.ext
44     · funext s
45       exact sub_eq_zero.mpr (hc s)
46     · exact hm
47   · intro h
48     refine ⟨?_,congrArg Prod.snd h⟩
49     intro s
50     exact sub_eq_zero.mp (congrFun (congrArg Prod.fst h) s)
51 
52 theorem Matches.coefficient_apply {C Chat : S → E →ₗ[ℝ] E}
53     {l lhat : E →ₗ[ℝ] ℝ} {T : E →ₗ[ℝ] E} (h : Matches C Chat l lhat T)
54     (s : S) (z : E) : Chat s (T z)=T (C s z) :=
55   congrArg (fun L : E →ₗ[ℝ] E => L z) (h.1 s)
56 
57 theorem Matches.word_readout {C Chat : S → E →ₗ[ℝ] E}
58     {l lhat : E →ₗ[ℝ] ℝ} {T : E →ₗ[ℝ] E} (h : Matches C Chat l lhat T)
59     (w : List S) : (lhat.comp (wordAction Chat w)).comp T=l.comp (wordAction C w) := by
60   rw [LinearMap.comp_assoc,word_intertwining C Chat T h.1,← LinearMap.comp_assoc,h.2]
61 
62 /-- The literal coefficient-word rows span the fitted dual space. -/
63 def CoefficientObservable (Chat : S → E →ₗ[ℝ] E) (lhat : E →ₗ[ℝ] ℝ) : Prop :=
64   Submodule.span ℝ (Set.range (fun w : List S => lhat.comp (wordAction Chat w)))=⊤
65 
66 theorem observable_separates {Chat : S → E →ₗ[ℝ] E} {lhat : E →ₗ[ℝ] ℝ}
67     (ho : CoefficientObservable Chat lhat) (x : E)
68     (hx : ∀ w : List S, lhat (wordAction Chat w x)=0) : x=0 := by
69   apply (Module.forall_dual_apply_eq_zero_iff ℝ x).mp
70   intro f
71   have hf : f ∈ Submodule.span ℝ (Set.range (fun w : List S => lhat.comp (wordAction Chat w))) := by
72     rw [ho]
73     trivial
74   induction hf using Submodule.span_induction with
75   | mem f hf =>
76     obtain ⟨w,rfl⟩ := hf
77     exact hx w
78   | zero => simp
79   | add f g hf hg ihf ihg => simp [ihf,ihg]
80   | smul a f hf ih => simp [ih]
81 
82 /-- Uniqueness is derived from fitted word rows and includes singular competitors. -/
83 theorem observable_match_unique {C Chat : S → E →ₗ[ℝ] E}
84     {l lhat : E →ₗ[ℝ] ℝ} (ho : CoefficientObservable Chat lhat)
85     (T U : E →ₗ[ℝ] E) (hT : Matches C Chat l lhat T) (hU : Matches C Chat l lhat U) : T=U := by
86   apply LinearMap.ext
87   intro z
88   apply sub_eq_zero.mp
89   apply observable_separates ho (T z-U z)
90   intro w
91   have ht := congrArg (fun L : E →ₗ[ℝ] ℝ => L z) (hT.word_readout w)
92   have hu := congrArg (fun L : E →ₗ[ℝ] ℝ => L z) (hU.word_readout w)
93   simpa only [map_sub,LinearMap.comp_apply,sub_eq_zero] using ht.trans hu.symm
94 end Matching
95 
96 section ScalarSystem
97 variable {r : ℕ} {S : Type*}
98 abbrev State (r : ℕ) := Fin r → ℝ
99 abbrev ScalarIndex (S : Type*) (r : ℕ) := Sum (S × Fin r × Fin r) (Fin r)
100 
101 /-- The actual finite scalar constraints, indexed by operator entries and mass entries. -/
102 noncomputable def scalarConstraintMap
103     (C Chat : S → State r →ₗ[ℝ] State r) (lhat : State r →ₗ[ℝ] ℝ) :
104     (State r →ₗ[ℝ] State r) →ₗ[ℝ] (ScalarIndex S r → ℝ) where
105   toFun T e := match e with
106     | .inl (s,i,j) => LinearMap.toMatrix' ((Chat s).comp T-T.comp (C s)) i j
107     | .inr j => lhat (T (Pi.single j 1))
108   map_add' T U := by
109     funext e
110     rcases e with ⟨s,i,j⟩ | j
111     · simp [LinearMap.comp_add,LinearMap.add_comp]
112       ring
113     · simp
114   map_smul' a T := by
115     funext e
116     rcases e with ⟨s,i,j⟩ | j
117     · simp [LinearMap.comp_smul,LinearMap.smul_comp]
118       ring
119     · simp
120 
121 noncomputable def scalarTarget (l : State r →ₗ[ℝ] ℝ) : ScalarIndex S r → ℝ
122   | .inl _ => 0
123   | .inr j => l (Pi.single j 1)
124 
125 /-- Equality with the explicit scalar right-hand side is exactly the written match. -/
126 theorem matches_iff_scalar_system (C Chat : S → State r →ₗ[ℝ] State r)
127     (l lhat : State r →ₗ[ℝ] ℝ) (T : State r →ₗ[ℝ] State r) :
128     Matches C Chat l lhat T ↔ scalarConstraintMap C Chat lhat T=scalarTarget l := by
129   constructor
130   · rintro ⟨hc,hm⟩
131     funext e
132     rcases e with ⟨s,i,j⟩ | j
133     · simp only [scalarConstraintMap,LinearMap.coe_mk,AddHom.coe_mk,scalarTarget,
134         hc s,sub_self,map_zero,Matrix.zero_apply]
135     · exact congrArg (fun L : State r →ₗ[ℝ] ℝ => L (Pi.single j 1)) hm
136   · intro h
137     refine ⟨?_,?_⟩
138     · intro s
139       apply sub_eq_zero.mp
140       apply LinearMap.toMatrix'.injective
141       ext i j
142       exact congrFun h (.inl (s,i,j))
143     · apply (Pi.basisFun ℝ (Fin r)).ext
144       intro j
145       simpa only [Pi.basisFun_apply,LinearMap.comp_apply,scalarConstraintMap,
146         LinearMap.coe_mk,AddHom.coe_mk,scalarTarget] using congrFun h (.inr j)
147 
148 /-- The operator rows are the usual entrywise matrix equations in the unknown T. -/
149 theorem scalar_operator_row (C Chat : S → State r →ₗ[ℝ] State r)
150     (lhat : State r →ₗ[ℝ] ℝ) (T : State r →ₗ[ℝ] State r) (s : S) (i j : Fin r) :
151     scalarConstraintMap C Chat lhat T (.inl (s,i,j))=
152       (∑ k, LinearMap.toMatrix' (Chat s) i k*LinearMap.toMatrix' T k j)-
153       ∑ k, LinearMap.toMatrix' T i k*LinearMap.toMatrix' (C s) k j := by
154   change LinearMap.toMatrix' ((Chat s).comp T-T.comp (C s)) i j=_
155   rw [map_sub,LinearMap.toMatrix'_comp,LinearMap.toMatrix'_comp]
156   rfl
157 
158 /-- The mass rows are also literal scalar linear equations in the same entries. -/
159 theorem scalar_mass_row (C Chat : S → State r →ₗ[ℝ] State r)
160     (lhat : State r →ₗ[ℝ] ℝ) (T : State r →ₗ[ℝ] State r) (j : Fin r) :
161     scalarConstraintMap C Chat lhat T (.inr j)=
162       ∑ k, lhat (Pi.single k 1)*LinearMap.toMatrix' T k j := by
163   change lhat (T (Pi.single j 1))=_
164   have he : T (Pi.single j 1)=∑ k : Fin r, (T (Pi.single j 1) k) • Pi.single k 1 := by
165     ext i
166     simp [Pi.single_apply,mul_ite]
167   rw [he,map_sum]
168   apply Finset.sum_congr rfl
169   intro k _
170   simp only [map_smul,smul_eq_mul,LinearMap.toMatrix'_apply]
171   ring
172 end ScalarSystem
173 
174 
175 section PolynomialTransport
176 open PolynomialGram MatrixEmbedding MeasureTheory
177 variable {E D A R : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
178 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
179 variable [Fintype D] [DecidableEq D] [Fintype A] [Fintype R]
180 variable [MeasurableSpace A] [MeasurableSingletonClass A]
181 variable {n q bound : ℕ}
182 
183 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype A]
184   [MeasurableSpace A] [MeasurableSingletonClass A] in
185 /-- Exact coefficient matching implies matching of every finite weighted sum. -/
186 theorem weighted_coefficients_transport (T : E ≃ₗ[ℝ] E)
187     (B Chat : A → Fin n → E →L[ℝ] E)
188     (hc : ∀ a k z, Chat a k (T z)=T (B a k z))
189     (a : A) (weights : Fin n → ℝ) (z : E) :
190     (∑ k, weights k • Chat a k) (T z)=T ((∑ k, weights k • B a k) z) := by
191   simp only [_root_.sum_apply,_root_.smul_apply,hc,map_sum,map_smul]
192 
193 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype A]
194   [MeasurableSpace A] [MeasurableSingletonClass A] in
195 theorem polynomial_density_transport (T : E ≃ₗ[ℝ] E)
196     (B Chat : A → Fin n → E →L[ℝ] E)
197     (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) (a : A) (u : ℝ) (z : E) :
198     operatorPolynomial (Chat a) u (T z)=T (operatorPolynomial (B a) u z) :=
199   weighted_coefficients_transport T B Chat hc a (fun k => u^(k:ℕ)) z
200 
201 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype A]
202   [MeasurableSpace A] [MeasurableSingletonClass A] in
203 /-- The actual fitted density is the conjugate by the same invertible solution. -/
204 theorem polynomial_density_conjugate (T : E ≃ₗ[ℝ] E)
205     (B Chat : A → Fin n → E →L[ℝ] E)
206     (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) (a : A) (u : ℝ) :
207     (operatorPolynomial (Chat a) u).toLinearMap=
208       T.toLinearMap.comp ((operatorPolynomial (B a) u).toLinearMap.comp T.symm.toLinearMap) := by
209   apply LinearMap.ext
210   intro z
211   simpa only [LinearEquiv.apply_symm_apply,LinearMap.comp_apply,LinearEquiv.coe_coe,
212     ContinuousLinearMap.coe_coe] using
213     polynomial_density_transport T B Chat hc a u (T.symm z)
214 
215 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DecidableEq D]
216   [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A] in
217 /-- On the transported state basis the literal embedded polynomials coincide. -/
218 theorem embedded_polynomial_transport (M : Embedding E D) (T : E ≃ₗ[ℝ] E)
219     (B Chat : A → Fin n → E →L[ℝ] E)
220     (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) (a : A) (z : E) :
221     embeddedPolynomial (M.transport T).J (Chat a) (T z)=embeddedPolynomial M.J (B a) z := by
222   funext i j
223   change Polynomial.ofFn n (fun k => M.J (T.symm (Chat a k (T z))) i j)=_
224   simp only [hc,LinearEquiv.symm_apply_apply]
225   rfl
226 
227 /-- Transport retains the actual Gram matrices and every finite coefficient
228 check; no new Gram feasibility or positivity hypothesis is introduced. -/
229 noncomputable def transportedCertificate (M : Embedding E D) (b : Module.Basis R ℝ E)
230     (B Chat : A → Fin n → E →L[ℝ] E)
231     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
232     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) :
233     CoefficientCertificate (b.map T) (M.transport T).coneInstance (M.transport T).J Chat q bound where
234   gram0 := W.gram0
235   gram1 := W.gram1
236   gram0_positive := W.gram0_positive
237   gram1_positive := W.gram1_positive
238   left_degree a r i j := by
239     simpa only [Module.Basis.map_apply,embedded_polynomial_transport M T B Chat hc] using W.left_degree a r i j
240   right_degree a r i j := by
241     simpa only [Module.Basis.map_apply,Embedding.transport_apply] using W.right_degree a r i j
242   coefficients a r i j k := by
243     simpa only [Module.Basis.map_apply,embedded_polynomial_transport M T B Chat hc,
244       Embedding.transport_apply] using W.coefficients a r i j k
245   mass a r := by
246     change (M.transport T).mass ((∑ k : Fin n, UniformIntervalMoments.moment k • Chat a k) (T (b r)))=
247       (M.transport T).mass (T (b r))
248     rw [weighted_coefficients_transport T B Chat hc,Embedding.transport_mass,Embedding.transport_mass]
249     exact W.mass a r
250 
251 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [MeasurableSingletonClass A] in
252 @[simp] theorem transportedCertificate_gram0 (M : Embedding E D) (b : Module.Basis R ℝ E)
253     (B Chat : A → Fin n → E →L[ℝ] E)
254     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
255     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) :
256     (transportedCertificate M b B Chat W T hc).gram0=W.gram0 := rfl
257 
258 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [MeasurableSingletonClass A] in
259 @[simp] theorem transportedCertificate_gram1 (M : Embedding E D) (b : Module.Basis R ℝ E)
260     (B Chat : A → Fin n → E →L[ℝ] E)
261     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
262     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) :
263     (transportedCertificate M b B Chat W T hc).gram1=W.gram1 := rfl
264 
265 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [DecidableEq D] in
266 /-- The separately matched mass row is exactly the transported trace mass. -/
267 theorem matched_mass_transport (M : Embedding E D) (T : E ≃ₗ[ℝ] E)
268     (lhat : E →ₗ[ℝ] ℝ) (hm : lhat.comp T.toLinearMap=M.mass) :
269     lhat=(M.transport T).mass := by
270   apply LinearMap.ext
271   intro z
272   have h := congrArg (fun L : E →ₗ[ℝ] ℝ => L (T.symm z)) hm
273   simpa only [LinearMap.comp_apply,LinearEquiv.coe_coe,LinearEquiv.apply_symm_apply,
274     Embedding.mass_apply,Embedding.transport] using h
275 
276 omit [MeasurableSpace E] [BorelSpace E] [DecidableEq D] in
277 /-- Initial admissibility remains a real, separate transported-cone check. -/
278 theorem fitted_initial_check (M : Embedding E D) (T : E ≃ₗ[ℝ] E)
279     (lhat : E →ₗ[ℝ] ℝ) (hm : lhat.comp T.toLinearMap=M.mass) (zhat : E) :
280     zhat∈(M.transport T).coneInstance.base ↔
281       (M.J (T.symm zhat)).PosSemidef ∧ lhat zhat=1 := by
282   rw [matched_mass_transport M T lhat hm]
283   rfl
284 
285 /-- The transported finite witness builds the literal fitted polynomial instrument. -/
286 noncomputable def fittedInstrument (M : Embedding E D) (b : Module.Basis R ℝ E)
287     (B Chat : A → Fin n → E →L[ℝ] E)
288     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
289     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) :
290     ContinuousInstrument.DensityInstrument (A := A) (M.transport T).coneInstance
291       UniformIntervalMoments.measure :=
292   (transportedCertificate M b B Chat W T hc).instrument (M.transport T).coneInstance_mem
293 
294 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [MeasurableSingletonClass A] in
295 /-- Actual chronological fine-record states use exactly the same coordinate map. -/
296 theorem record_run_transport (M : Embedding E D) (b : Module.Basis R ℝ E)
297     (B Chat : A → Fin n → E →L[ℝ] E)
298     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
299     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z)) (z : E) :
300     (N : ℕ) → ∀ h : ContinuousRecords.History (A × ℝ) N,
301       ContinuousRecords.run (fittedInstrument M b B Chat W T hc) (T z) N h=
302         T (ContinuousRecords.run (PolynomialGramP53.instrument M b B W) z N h)
303   | 0,_ => rfl
304   | N+1,h => by
305     change operatorPolynomial (Chat h.2.1) h.2.2
306       (ContinuousRecords.run (fittedInstrument M b B Chat W T hc) (T z) N h.1)=_
307     rw [record_run_transport M b B Chat W T hc z N h.1]
308     exact polynomial_density_transport T B Chat hc h.2.1 h.2.2 _
309 
310 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSingletonClass A] in
311 /-- Equality of the actual full record measures holds for every shared measurable
312 history-dependent policy and every horizon, hence for every measurable event. -/
313 theorem record_law_transport (M : Embedding E D) (b : Module.Basis R ℝ E)
314     (B Chat : A → Fin n → E →L[ℝ] E)
315     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
316     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z))
317     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (z : E) (N : ℕ) :
318     ContinuousRecords.recordLaw (fittedInstrument M b B Chat W T hc) π (T z) N=
319       ContinuousRecords.recordLaw (PolynomialGramP53.instrument M b B W) π z N := by
320   unfold ContinuousRecords.recordLaw
321   congr 1
322   funext h
323   unfold ContinuousRecords.recordDensity
324   rw [record_run_transport M b B Chat W T hc]
325   simp only [Embedding.coneInstance_mass,Embedding.transport_mass]
326 
327 /-- The initial check, rather than the operator match alone, supplies a genuine
328 fitted probability law. -/
329 theorem fitted_record_probability (M : Embedding E D) (b : Module.Basis R ℝ E)
330     (B Chat : A → Fin n → E →L[ℝ] E)
331     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
332     (T : E ≃ₗ[ℝ] E) (hc : ∀ a k z, Chat a k (T z)=T (B a k z))
333     (lhat : E →ₗ[ℝ] ℝ) (hm : lhat.comp T.toLinearMap=M.mass) (zhat : E)
334     (hinit : (M.J (T.symm zhat)).PosSemidef ∧ lhat zhat=1)
335     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (N : ℕ) :
336     IsProbabilityMeasure (ContinuousRecords.recordLaw (fittedInstrument M b B Chat W T hc) π zhat N) := by
337   have hb : zhat∈(M.transport T).coneInstance.base := (fitted_initial_check M T lhat hm zhat).mpr hinit
338   exact ContinuousRecords.recordLaw_probability (fittedInstrument M b B Chat W T hc) π ⟨zhat,hb⟩ N
339 
340 end PolynomialTransport
341 
342 
343 section Recognition
344 open PolynomialGram MatrixEmbedding MeasureTheory
345 variable {E D A R : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
346 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
347 variable [Fintype D] [DecidableEq D] [Fintype A] [Fintype R]
348 variable [MeasurableSpace A] [MeasurableSingletonClass A]
349 variable {n q bound : ℕ}
350 
351 /-- P60 starts from the linear coefficient/mass match and derives actual
352 polynomial/Gram transport, uniqueness under fitted observability, and equality
353 of all finite common-policy event laws. Fitted initial admissibility remains
354 a separate premise of probability validity. -/
355 theorem fixed_template_recognition (M : Embedding E D) (b : Module.Basis R ℝ E)
356     (B Chat : A → Fin n → E →L[ℝ] E)
357     (W : CoefficientCertificate b M.coneInstance M.J B q bound)
358     (T : E ≃ₗ[ℝ] E) (lhat : E →ₗ[ℝ] ℝ)
359     (hm : Matches (fun s : A × Fin n => (B s.1 s.2).toLinearMap)
360       (fun s : A × Fin n => (Chat s.1 s.2).toLinearMap) M.mass lhat T.toLinearMap) :
361     let hc : ∀ a k z, Chat a k (T z)=T (B a k z) :=
362       fun a k z => hm.coefficient_apply (a,k) z
363     lhat=(M.transport T).mass ∧
364     (∀ a u, (operatorPolynomial (Chat a) u).toLinearMap=
365       T.toLinearMap.comp ((operatorPolynomial (B a) u).toLinearMap.comp T.symm.toLinearMap)) ∧
366     ((transportedCertificate M b B Chat W T hc).gram0=W.gram0 ∧
367       (transportedCertificate M b B Chat W T hc).gram1=W.gram1) ∧
368     (CoefficientObservable (fun s : A × Fin n => (Chat s.1 s.2).toLinearMap) lhat →
369       ∀ U : E →ₗ[ℝ] E,
370         Matches (fun s : A × Fin n => (B s.1 s.2).toLinearMap)
371           (fun s : A × Fin n => (Chat s.1 s.2).toLinearMap) M.mass lhat U → U=T.toLinearMap) ∧
372     (∀ (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) z N,
373       ContinuousRecords.recordLaw (fittedInstrument M b B Chat W T hc) π (T z) N=
374         ContinuousRecords.recordLaw (PolynomialGramP53.instrument M b B W) π z N) ∧
375     (∀ zhat, (M.J (T.symm zhat)).PosSemidef ∧ lhat zhat=1 →
376       ∀ (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) N,
377         IsProbabilityMeasure (ContinuousRecords.recordLaw
378           (fittedInstrument M b B Chat W T hc) π zhat N)) := by
379   dsimp only
380   let hc : ∀ a k z, Chat a k (T z)=T (B a k z) := fun a k z => hm.coefficient_apply (a,k) z
381   refine ⟨matched_mass_transport M T lhat hm.2,?_,⟨rfl,rfl⟩,?_,?_,?_⟩
382   · exact polynomial_density_conjugate T B Chat hc
383   · intro ho U hU
384     exact (observable_match_unique ho T.toLinearMap U hm hU).symm
385   · exact record_law_transport M b B Chat W T hc
386   · intro zhat hz π N
387     exact fitted_record_probability M b B Chat W T hc lhat hm.2 zhat hz π N
388 
389 end Recognition
390 
391 namespace Boundaries
392 
393 /-- A degree-zero identity template in two coordinates. -/
394 def coefficients (_ : Unit) : State 2 →ₗ[ℝ] State 2 := LinearMap.id
395 
396 def mass : State 2 →ₗ[ℝ] ℝ := (LinearMap.proj 0 : State 2 →ₗ[ℝ] ℝ)+LinearMap.proj 1
397 
398 def singularReset : State 2 →ₗ[ℝ] State 2 where
399   toFun z := ![z 0+z 1,0]
400   map_add' z w := by
401     ext i
402     fin_cases i <;> simp [add_add_add_comm]
403   map_smul' a z := by
404     ext i
405     fin_cases i <;> simp [mul_add]
406 
407 theorem identity_matches : Matches coefficients coefficients mass mass LinearMap.id := by
408   constructor
409   · intro s
410     simp [coefficients]
411   · simp
412 
413 /-- The same exact coefficient and mass system has a singular solution. -/
414 theorem singular_matches : Matches coefficients coefficients mass mass singularReset := by
415   constructor
416   · intro s
417     simp [coefficients]
418   · apply LinearMap.ext
419     intro z
420     simp [mass,singularReset]
421 
422 theorem singular_not_injective : ¬ Function.Injective singularReset := by
423   intro h
424   have he : singularReset ![1,0]=singularReset ![0,1] := by
425     ext i
426     fin_cases i <;> norm_num [singularReset]
427   have hz := congrFun (h he) 0
428   norm_num at hz
429 
430 theorem distinct_matches : (LinearMap.id : State 2 →ₗ[ℝ] State 2) ≠ singularReset := by
431   intro h
432   apply singular_not_injective
433   rw [← h]
434   exact Function.injective_id
435 
436 theorem identity_word (w : List Unit) (z : State 2) : wordAction coefficients w z=z := by
437   induction w generalizing z with
438   | nil => rfl
439   | cons s w ih => exact ih z
440 
441 /-- The missing observable direction is the nonzero signed mass-zero vector. -/
442 theorem not_observable : ¬ CoefficientObservable coefficients mass := by
443   intro ho
444   have hz := observable_separates ho ![1,-1] (fun w => by rw [identity_word]; norm_num [mass])
445   have hc := congrFun hz 0
446   norm_num at hc
447 
448 
449 /-- Two genuine polynomial coefficient slots: an identity constant and a zero
450 linear term in the supplied template. -/
451 def templateCoefficient (s : Bool) : State 2 →ₗ[ℝ] State 2 := if s then 0 else LinearMap.id
452 
453 def secondOnly : State 2 →ₗ[ℝ] State 2 where
454   toFun z := ![0,z 1]
455   map_add' z w := by
456     ext i
457     fin_cases i <;> simp
458   map_smul' a z := by
459     ext i
460     fin_cases i <;> simp
461 
462 /-- Its fitted counterpart has density diag(1,1+u) on the same orthant. -/
463 def fittedCoefficient (s : Bool) : State 2 →ₗ[ℝ] State 2 :=
464   if s then secondOnly else LinearMap.id
465 
466 theorem singular_observable_matches :
467     Matches templateCoefficient fittedCoefficient mass mass singularReset := by
468   refine ⟨?_,singular_matches.2⟩
469   intro s
470   cases s
471   · simp [templateCoefficient,fittedCoefficient]
472   · apply LinearMap.ext
473     intro z
474     ext i
475     fin_cases i <;> simp [templateCoefficient,fittedCoefficient,secondOnly,singularReset]
476 
477 /-- Empty and one-letter fitted rows already span the two-dimensional dual. -/
478 theorem fitted_observable : CoefficientObservable fittedCoefficient mass := by
479   apply top_unique
480   intro f _
481   have hm : mass ∈ Submodule.span ℝ
482       (Set.range (fun w : List Bool => mass.comp (wordAction fittedCoefficient w))) := by
483     apply Submodule.subset_span
484     exact ⟨[],by simp⟩
485   have hr : mass.comp secondOnly ∈ Submodule.span ℝ
486       (Set.range (fun w : List Bool => mass.comp (wordAction fittedCoefficient w))) := by
487     apply Submodule.subset_span
488     exact ⟨[true],by simp [fittedCoefficient]⟩
489   have he : f=f (Pi.single (0:Fin 2) 1) • mass+
490       (f (Pi.single (1:Fin 2) 1)-f (Pi.single (0:Fin 2) 1)) • (mass.comp secondOnly) := by
491     apply (Pi.basisFun ℝ (Fin 2)).ext
492     intro j
493     fin_cases j <;> simp [Pi.basisFun_apply,mass,secondOnly]
494   rw [he]
495   exact Submodule.add_mem _ (Submodule.smul_mem _ _ hm) (Submodule.smul_mem _ _ hr)
496 
497 /-- Even a unique match selected by observable fitted rows can be singular. -/
498 theorem unique_singular_match (U : State 2 →ₗ[ℝ] State 2)
499     (hU : Matches templateCoefficient fittedCoefficient mass mass U) : U=singularReset :=
500   observable_match_unique fitted_observable U singularReset hU singular_observable_matches
501 
502 end Boundaries
503 
504 end Komorebi.LSM.CertifiedTemplate

Back to source controls