RotationApproximation.lean

1 import KomorebiLSM.RotationModel
2 import KomorebiLSM.LorentzBaseNorm
3 import KomorebiLSM.RegularPolygon
4 import KomorebiLSM.PolicyComparison
5 import KomorebiLSM.PositiveLift
6 import KomorebiLSM.BehaviorProbability
7 import Mathlib.Tactic.FinCases
8 import Mathlib.Tactic.NormNum
9 
10 /-! P47's explicit rational diamond approximation. The four actual generators
11 are (1,1,0), (1,0,1), (1,-1,0), and (1,0,-1). -/
12 set_option autoImplicit false
13 set_option maxHeartbeats 800000
14 namespace Komorebi.LSM.RotationApproximation
15 noncomputable section
16 open scoped BigOperators
17 open FiniteInstruments
18 
19 abbrev State := Fin 3 → ℝ
20 
21 noncomputable def mass : State →ₗ[ℝ] ℝ := LinearMap.proj 0
22 
23 def initial : State := ![1,1,0]
24 
25 def synthesisMatrix : Matrix (Fin 3) (Fin 4) ℝ :=
26   !![1,1,1,1; 1,0,-1,0; 0,1,0,-1]
27 
28 noncomputable def synthesis : (Fin 4 → ℝ) →ₗ[ℝ] State := synthesisMatrix.mulVecLin
29 
30 def rotationMatrix (α : ℝ) : Matrix (Fin 3) (Fin 3) ℝ :=
31   !![1,0,0; 0,3*α/5,-4*α/5; 0,4*α/5,3*α/5]
32 
33 def probeMatrix (o : Bool) : Matrix (Fin 3) (Fin 3) ℝ :=
34   if o then !![1/2,-1/2,0; 1/2,-1/2,0; 0,0,0]
35   else !![1/2,1/2,0; 1/2,1/2,0; 0,0,0]
36 
37 /-- False is the rotate action, true is the probe action. -/
38 def branchMatrix (α : ℝ) (s : Bool × Bool) : Matrix (Fin 3) (Fin 3) ℝ :=
39   if s.1 then probeMatrix s.2 else if s.2 then 0 else rotationMatrix α
40 
41 noncomputable def operator (α : ℝ) (s : Bool × Bool) : State →ₗ[ℝ] State :=
42   (branchMatrix α s).mulVecLin
43 
44 /-- Unused diamond mass is distributed uniformly over the four vertices. -/
45 def slack (α : ℝ) : ℝ := (1-7*α/5)/4
46 
47 def rotationLift (α : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
48   !![slack α+3*α/5, slack α, slack α, slack α+4*α/5;
49      slack α+4*α/5, slack α+3*α/5, slack α, slack α;
50      slack α, slack α+4*α/5, slack α+3*α/5, slack α;
51      slack α, slack α, slack α+4*α/5, slack α+3*α/5]
52 
53 def probeLift (o : Bool) : Matrix (Fin 4) (Fin 4) ℝ :=
54   if o then !![0,1/2,1,1/2; 0,0,0,0; 0,0,0,0; 0,0,0,0]
55   else !![1,1/2,0,1/2; 0,0,0,0; 0,0,0,0; 0,0,0,0]
56 
57 def liftMatrix (α : ℝ) (s : Bool × Bool) : Matrix (Fin 4) (Fin 4) ℝ :=
58   if s.1 then probeLift s.2 else if s.2 then 0 else rotationLift α
59 
60 /-- The displayed four-generator lift intertwines the actual matrices exactly. -/
61 theorem matrix_intertwining (α : ℝ) (s : Bool × Bool) :
62     branchMatrix α s * synthesisMatrix = synthesisMatrix * liftMatrix α s := by
63   rcases s with ⟨a,o⟩
64   cases a <;> cases o <;> ext i j <;> fin_cases i <;> fin_cases j <;>
65     norm_num [branchMatrix, rotationMatrix, probeMatrix, synthesisMatrix,
66       liftMatrix, rotationLift, probeLift, Matrix.mul_apply, Fin.sum_univ_succ, slack] <;> ring
67 
68 /-- Every lifted entry is nonnegative in the stated diamond attenuation range. -/
69 theorem lift_nonnegative (α : ℝ) (hα : 0 ≤ α) (hupper : α ≤ 5/7)
70     (s : Bool × Bool) (i j : Fin 4) : 0 ≤ liftMatrix α s i j := by
71   rcases s with ⟨a,o⟩
72   cases a <;> cases o <;> fin_cases i <;> fin_cases j <;>
73     norm_num [liftMatrix, rotationLift, probeLift, slack] <;> nlinarith
74 
75 /-- Column mass is one for each action, including all its observation branches. -/
76 theorem lift_mass (α : ℝ) (a : Bool) (j : Fin 4) :
77     ∑ o : Bool, ∑ i : Fin 4, liftMatrix α (a,o) i j = 1 := by
78   cases a <;> fin_cases j <;>
79     norm_num [liftMatrix, rotationLift, probeLift, slack, Fin.sum_univ_succ,
80       Fintype.sum_bool, Matrix.cons_val_two, Matrix.cons_val_three] <;> ring
81 
82 /-- The synthesis reads ordinary lifted probability mass in coordinate zero. -/
83 theorem synthesis_mass : mass.comp synthesis = FiniteInstruments.mass := by
84   apply LinearMap.ext
85   intro a
86   simp [mass, synthesis, synthesisMatrix, Matrix.mulVec, dotProduct,
87     Fin.sum_univ_succ, FiniteInstruments.mass_apply]
88 
89 /-- The initial state is the first diamond generator with a valid point prior. -/
90 theorem synthesis_initial : synthesis (FiniteBayes.pointMass (0 : Fin 4)) = initial := by
91   ext i
92   fin_cases i <;>
93     norm_num [synthesis, synthesisMatrix, initial, Matrix.mulVec, dotProduct,
94       Fin.sum_univ_succ, FiniteBayes.pointMass]
95 
96 /-- The exact matrix relation also holds as a relation of linear maps. -/
97 theorem operator_intertwining (α : ℝ) (s : Bool × Bool) :
98     (operator α s).comp synthesis = synthesis.comp (liftMatrix α s).mulVecLin := by
99   change (branchMatrix α s).mulVecLin.comp synthesisMatrix.mulVecLin =
100     synthesisMatrix.mulVecLin.comp (liftMatrix α s).mulVecLin
101   rw [← Matrix.mulVecLin_mul, ← Matrix.mulVecLin_mul]
102   exact congrArg Matrix.mulVecLin (matrix_intertwining α s)
103 
104 /-- A concrete finite stochastic instrument, without a supplied positivity witness. -/
105 noncomputable def diamondInstrument (α : ℝ) (hα : 0 ≤ α) (hupper : α ≤ 5/7) :
106     Instrument (Fin 4) Bool Bool where
107   matrix a o := liftMatrix α (a,o)
108   nonneg a o i j := lift_nonnegative α hα hupper (a,o) i j
109   mass_one := lift_mass α
110 
111 /-- The positive finite lift is correct on every word, not just a test prefix. -/
112 theorem diamond_word_probability (α : ℝ) (hα : 0 ≤ α) (hupper : α ≤ 5/7)
113     (w : List (Bool × Bool)) :
114     mass (wordAction (operator α) w initial) =
115       FiniteInstruments.mass (wordAction (diamondInstrument α hα hupper).branch w
116         (FiniteBayes.pointMass (0 : Fin 4))) := by
117   rw [← synthesis_initial]
118   exact PositiveLift.lifted_word_probability (operator α) synthesis mass synthesis_mass
119     (liftMatrix α) (operator_intertwining α) w (FiniteBayes.pointMass (0 : Fin 4))
120 
121 /-- The rational approximation is valid at all horizons. -/
122 theorem diamond_all_word_bounds (α : ℝ) (hα : 0 ≤ α) (hupper : α ≤ 5/7)
123     (w : List (Bool × Bool)) :
124     0 ≤ mass (wordAction (operator α) w initial) ∧
125       mass (wordAction (operator α) w initial) ≤ 1 := by
126   rw [diamond_word_probability α hα hupper]
127   exact (diamondInstrument α hα hupper).word_probability w _ (FiniteInstruments.point_prior 0)
128 
129 /-- The stated manuscript example alpha=2/3 is an exact rational certificate. -/
130 theorem rational_two_thirds_valid (w : List (Bool × Bool)) :
131     0 ≤ mass (wordAction (operator (2/3)) w initial) ∧
132       mass (wordAction (operator (2/3)) w initial) ≤ 1 :=
133   diamond_all_word_bounds (2/3) (by norm_num) (by norm_num) w
134 
135 /-- Explicit coordinate formula for the four-generator synthesis. -/
136 theorem synthesis_apply (a : Fin 4 → ℝ) :
137     synthesis a = ![a 0+a 1+a 2+a 3, a 0-a 2, a 1-a 3] := by
138   ext i
139   fin_cases i <;> simp [synthesis, synthesisMatrix, Matrix.mulVec, dotProduct,
140     Fin.sum_univ_succ, Matrix.cons_val_two] <;> ring
141 
142 /-- The actual normalized axes generate precisely the rational diamond cone. -/
143 theorem diamond_hull : PositiveLift.hull synthesis =
144     {z : State | |z 1|+|z 2| ≤ z 0} := by
145   ext z
146   constructor
147   · rintro ⟨a,ha,rfl⟩
148     simp only [synthesis_apply, Set.mem_ofPred_eq, Matrix.cons_val_one,
149       Matrix.cons_val_two, Matrix.head_cons, Matrix.tail_cons, Matrix.cons_val_zero]
150     have hx : |a 0-a 2| ≤ a 0+a 2 := by
151       simpa only [abs_of_nonneg (ha 0), abs_of_nonneg (ha 2)] using abs_sub (a 0) (a 2)
152     have hy : |a 1-a 3| ≤ a 1+a 3 := by
153       simpa only [abs_of_nonneg (ha 1), abs_of_nonneg (ha 3)] using abs_sub (a 1) (a 3)
154     linarith
155   · intro hz
156     change |z 1|+|z 2| ≤ z 0 at hz
157     let b : ℝ := (z 0-|z 1|-|z 2|)/2
158     let a : Fin 4 → ℝ := ![max (z 1) 0+b, max (z 2) 0,
159       max (-z 1) 0+b, max (-z 2) 0]
160     have hb : 0 ≤ b := by dsimp [b]; linarith
161     have hdiff : ∀ x : ℝ, max x 0-max (-x) 0=x := by
162       intro x
163       rcases le_total 0 x with h|h
164       · rw [max_eq_left h, max_eq_right (neg_nonpos.mpr h)]; ring
165       · rw [max_eq_right h, max_eq_left (neg_nonneg.mpr h)]; ring
166     have habs : ∀ x : ℝ, max x 0+max (-x) 0=|x| := by
167       intro x
168       rcases le_total 0 x with h|h
169       · rw [max_eq_left h, max_eq_right (neg_nonpos.mpr h),abs_of_nonneg h]; ring
170       · rw [max_eq_right h, max_eq_left (neg_nonneg.mpr h),abs_of_nonpos h]; ring
171     refine ⟨a, ?_, ?_⟩
172     · intro j
173       fin_cases j
174       · exact add_nonneg (le_max_right _ _) hb
175       · exact le_max_right _ _
176       · exact add_nonneg (le_max_right _ _) hb
177       · exact le_max_right _ _
178     · rw [synthesis_apply]
179       ext i
180       fin_cases i
181       · change (max (z 1) 0+b)+max (z 2) 0+(max (-z 1) 0+b)+max (-z 2) 0=z 0
182         dsimp [b]
183         nlinarith [habs (z 1), habs (z 2)]
184       · change (max (z 1) 0+b)-(max (-z 1) 0+b)=z 1
185         linarith [hdiff (z 1)]
186       · exact hdiff (z 2)
187 
188 /-- At alpha one these are literally the source model's branch operators. -/
189 theorem exact_operator (s : Bool × Bool) : operator 1 s = RotationModel.operator s := by
190   rw [RotationModel.operator_matrix]
191   change (branchMatrix 1 s).mulVecLin = (RotationModel.matrix s).mulVecLin
192   congr 1
193   rcases s with ⟨a,o⟩
194   cases a <;> cases o <;> ext i j <;> fin_cases i <;> fin_cases j <;>
195     norm_num [branchMatrix, rotationMatrix, probeMatrix, RotationModel.matrix,
196       RotationModel.rotationMatrix, RotationModel.probeMatrix0, RotationModel.probeMatrix1]
197 
198 /-- The attenuation leaves the probability mass unchanged. -/
199 theorem operator_mass (α : ℝ) (a : Bool) (z : State) :
200     ∑ o : Bool, mass (operator α (a,o) z)=mass z := by
201   cases a <;> simp [mass, operator, branchMatrix, probeMatrix, rotationMatrix,
202     Matrix.mulVec, dotProduct, Fin.sum_univ_succ]
203   all_goals ring
204 
205 /-- The actual attenuated rotation contracts the spatial Euclidean radius. -/
206 theorem rotation_radius (α : ℝ) (hα : 0 ≤ α) (z : State) :
207     Real.sqrt (((operator α (false,false) z) 1)^2+((operator α (false,false) z) 2)^2) =
208       α*Real.sqrt ((z 1)^2+(z 2)^2) := by
209   have he : ((operator α (false,false) z) 1)^2+((operator α (false,false) z) 2)^2 =
210       α^2*((z 1)^2+(z 2)^2) := by
211     simp [operator,branchMatrix,rotationMatrix,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
212     ring
213   rw [he, Real.sqrt_mul (sq_nonneg α), Real.sqrt_sq_eq_abs, abs_of_nonneg hα]
214 
215 /-- Every actual probe is the same reset as in the exact model. -/
216 theorem probe_reset (α : ℝ) (o : Bool) (z : State) :
217     operator α (true,o) z = ((if o then z 0-z 1 else z 0+z 1)/2) • initial := by
218   cases o <;> ext i <;> fin_cases i <;>
219     simp [operator,branchMatrix,probeMatrix,initial,Matrix.mulVec,dotProduct,
220       Fin.sum_univ_succ] <;> ring
221 
222 /-- Finite normalized vertices plus an actual inscribed ball provide invariant
223 operators. The regular-polygon geometry is a separate, reusable input. -/
224 theorem finite_hull_invariant {J : Type*} [Fintype J] [DecidableEq J]
225     (V : (J → ℝ) →ₗ[ℝ] State) (hn : mass.comp V=FiniteInstruments.mass)
226     (hvertices : ∀ j, Real.sqrt ((PositiveLift.generator V j 1)^2+
227       (PositiveLift.generator V j 2)^2) ≤ 1)
228     (hinit : initial ∈ PositiveLift.hull V)
229     (r : ℝ) (hball : ∀ z : State, mass z=1 →
230       Real.sqrt ((z 1)^2+(z 2)^2) ≤ r → z ∈ PositiveLift.hull V)
231     (α : ℝ) (hα : 0 ≤ α) (hαr : α ≤ r) (s : Bool × Bool) :
232     ∀ z ∈ PositiveLift.hull V, operator α s z ∈ PositiveLift.hull V := by
233   apply (PositiveLift.invariant_iff_generators V (operator α s)).mpr
234   intro j
235   have hmass := PositiveLift.mass_generator V mass hn j
236   have hm : PositiveLift.generator V j 0=1 := hmass
237   rcases s with ⟨a,o⟩
238   cases a <;> cases o
239   · apply hball
240     · simpa [mass,operator,branchMatrix,rotationMatrix,Matrix.mulVec,dotProduct,
241         Fin.sum_univ_succ] using hm
242     · rw [rotation_radius α hα]
243       exact (mul_le_mul_of_nonneg_left (hvertices j) hα).trans (by simpa using hαr)
244   · simpa [operator,branchMatrix] using PositiveLift.hull_zero V
245   · rw [probe_reset]
246     apply PositiveLift.hull_smul V _ hinit
247     have hs := Real.sq_sqrt (show 0 ≤ (PositiveLift.generator V j 1)^2+
248       (PositiveLift.generator V j 2)^2 by positivity)
249     have hn0 := Real.sqrt_nonneg ((PositiveLift.generator V j 1)^2+
250       (PositiveLift.generator V j 2)^2)
251     have hr0 := hvertices j
252     simp only [Bool.false_eq_true, reduceIte, hm]
253     nlinarith [sq_nonneg (PositiveLift.generator V j 2)]
254   · rw [probe_reset]
255     apply PositiveLift.hull_smul V _ hinit
256     have hs := Real.sq_sqrt (show 0 ≤ (PositiveLift.generator V j 1)^2+
257       (PositiveLift.generator V j 2)^2 by positivity)
258     have hn0 := Real.sqrt_nonneg ((PositiveLift.generator V j 1)^2+
259       (PositiveLift.generator V j 2)^2)
260     have hr0 := hvertices j
261     simp only [reduceIte, hm]
262     nlinarith [sq_nonneg (PositiveLift.generator V j 2)]
263 
264 /-- A finite positive stochastic lift is constructed from the vertex geometry,
265 with exact initial mass and every word probability retained. -/
266 theorem finite_vertex_certificate {J : Type*} [Fintype J] [DecidableEq J]
267     (V : (J → ℝ) →ₗ[ℝ] State) (hn : mass.comp V=FiniteInstruments.mass)
268     (hvertices : ∀ j, Real.sqrt ((PositiveLift.generator V j 1)^2+
269       (PositiveLift.generator V j 2)^2) ≤ 1)
270     (hinit : initial ∈ PositiveLift.hull V)
271     (r : ℝ) (hball : ∀ z : State, mass z=1 →
272       Real.sqrt ((z 1)^2+(z 2)^2) ≤ r → z ∈ PositiveLift.hull V)
273     (α : ℝ) (hα : 0 ≤ α) (hαr : α ≤ r) :
274     ∃ (M : Bool × Bool → Matrix J J ℝ) (a₀ : J → ℝ),
275       (∀ s i j, 0 ≤ M s i j) ∧ FiniteBayes.IsPrior a₀ ∧ V a₀=initial ∧
276       (∀ s, (operator α s).comp V=V.comp (M s).mulVecLin) ∧
277       (∀ a j, ∑ o : Bool, ∑ i, M (a,o) i j=1) ∧
278       (∀ w, mass (wordAction (operator α) w initial)=
279         FiniteInstruments.mass (wordAction (fun s => (M s).mulVecLin) w a₀)) := by
280   classical
281   have hi := finite_hull_invariant V hn hvertices hinit r hball α hα hαr
282   choose M hM he using fun s => (PositiveLift.positive_lift_iff V (operator α s)).mp (hi s)
283   obtain ⟨a₀,ha₀,hVa⟩ := hinit
284   have hp : FiniteBayes.IsPrior a₀ := by
285     refine ⟨ha₀, ?_⟩
286     have h := congrArg mass hVa
287     have hnormal := PositiveLift.normalized_mass V mass hn a₀
288     change mass (V a₀)=1 at h
289     exact hnormal.symm.trans h
290   refine ⟨M,a₀,hM,hp,hVa,he,PositiveLift.lifted_mass (operator α) V mass hn
291     (operator_mass α) M he, ?_⟩
292   intro w
293   rw [← hVa]
294   exact PositiveLift.lifted_word_probability (operator α) V mass hn M he w a₀
295 
296 /-- Both exact and attenuated models preserve the same actual Lorentz cone. -/
297 theorem cone_invariant (α : ℝ) (hα : 0 ≤ α) (hα1 : α ≤ 1)
298     (s : Bool × Bool) {z : State} (hz : z ∈ RotationModel.cone) :
299     operator α s z ∈ RotationModel.cone := by
300   rcases s with ⟨a,o⟩
301   cases a <;> cases o
302   · change Real.sqrt (((operator α (false,false) z) 1)^2+
303       ((operator α (false,false) z) 2)^2) ≤ (operator α (false,false) z) 0
304     rw [rotation_radius α hα]
305     have h0 : (operator α (false,false) z) 0=z 0 := by
306       simp [operator,branchMatrix,rotationMatrix,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
307     rw [h0]
308     have hmul := mul_le_mul_of_nonneg_right hα1
309       (Real.sqrt_nonneg ((z 1)^2+(z 2)^2))
310     have hmul' : α*Real.sqrt ((z 1)^2+(z 2)^2) ≤ Real.sqrt ((z 1)^2+(z 2)^2) := by
311       simpa only [one_mul] using hmul
312     exact hmul'.trans hz
313   · have hzero : operator α (false,true) z=0 := by simp [operator,branchMatrix]
314     rw [hzero]
315     exact RotationModel.cone_zero
316   · have he : operator α (true,false)=operator 1 (true,false) := rfl
317     rw [he,exact_operator]
318     exact RotationModel.operator_cone _ hz
319   · have he : operator α (true,true)=operator 1 (true,true) := rfl
320     rw [he,exact_operator]
321     exact RotationModel.operator_cone _ hz
322 
323 /-- The change of a rotate branch is purely spatial with exact known radius. -/
324 theorem rotation_difference_radius (α : ℝ) (hα1 : α ≤ 1) (z : State) :
325     Real.sqrt ((((operator 1 (false,false)-operator α (false,false)) z) 1)^2+
326       (((operator 1 (false,false)-operator α (false,false)) z) 2)^2) =
327       (1-α)*Real.sqrt ((z 1)^2+(z 2)^2) := by
328   have he : (((operator 1 (false,false)-operator α (false,false)) z) 1)^2+
329       (((operator 1 (false,false)-operator α (false,false)) z) 2)^2 =
330       (1-α)^2*((z 1)^2+(z 2)^2) := by
331     simp [operator,branchMatrix,rotationMatrix,dotProduct,Fin.sum_univ_succ]
332     ring
333   rw [he,Real.sqrt_mul (sq_nonneg (1-α)),Real.sqrt_sq_eq_abs,
334     abs_of_nonneg (sub_nonneg.mpr hα1)]
335 
336 /-- The actual finite-dimensional operators have canonical continuous versions. -/
337 noncomputable def continuousOperator (α : ℝ) (s : Bool × Bool) : State →L[ℝ] State :=
338   (operator α s).toContinuousLinearMap
339 
340 section LawComparison
341 variable (C : BaseNorm.ProbabilityCone State)
342 variable (hcarrier : C.carrier=RotationModel.cone) (hmass : C.mass=mass)
343 variable (hvalue : ∀ z : State, C.value z=max |z 0| (Real.sqrt ((z 1)^2+(z 2)^2)))
344 include hcarrier hmass
345 
346 /-- Positivity and exact action mass are established on the common Lorentz cone. -/
347 theorem common_cone_instrument (α : ℝ) (hα : 0 ≤ α) (hα1 : α ≤ 1) (a : Bool) :
348     C.Instrument (fun o => (continuousOperator α (a,o)).toLinearMap) := by
349   constructor
350   · intro o z hz
351     change operator α (a,o) z ∈ C.carrier
352     rw [hcarrier] at hz ⊢
353     exact cone_invariant α hα hα1 _ hz
354   · intro z
355     change (∑ o : Bool, C.mass (operator α (a,o) z))=C.mass z
356     simpa only [hmass] using operator_mass α a z
357 
358 include hvalue
359 
360 /-- Only the rotate action changes. Its summed branch discrepancy is at most
361 one minus attenuation in the actual Lorentz base norm. -/
362 theorem action_discrepancy (α : ℝ) (hα1 : α ≤ 1) (a : Bool)
363     (z : State) (hz : z ∈ C.base) :
364     C.discrepancy (fun o => operator 1 (a,o)) (fun o => operator α (a,o)) z ≤ 1-α := by
365   have hzcone : z ∈ RotationModel.cone := by rw [← hcarrier]; exact hz.1
366   have h0 : z 0=1 := by simpa only [hmass,mass,LinearMap.proj_apply] using hz.2
367   have hr : Real.sqrt ((z 1)^2+(z 2)^2) ≤ 1 := by
368     simpa only [RotationModel.cone_iff,h0] using hzcone
369   cases a
370   · have hz0 : ((operator 1 (false,false)-operator α (false,false)) z) 0=0 := by
371       simp [operator,branchMatrix,rotationMatrix,dotProduct,Fin.sum_univ_succ]
372     have hz1 : (operator 1 (false,true)-operator α (false,true)) z=0 := by
373       simp [operator,branchMatrix]
374     rw [BaseNorm.ProbabilityCone.discrepancy,Fintype.sum_bool,hz1,C.value_zero,zero_add,
375       hvalue,hz0,abs_zero,max_eq_right (Real.sqrt_nonneg _),rotation_difference_radius α hα1]
376     simpa only [mul_one] using mul_le_mul_of_nonneg_left hr (sub_nonneg.mpr hα1)
377   · have he : ∀ o : Bool, operator 1 (true,o)=operator α (true,o) := by
378       intro o
379       cases o <;> rfl
380     simp only [BaseNorm.ProbabilityCone.discrepancy,he,sub_self,LinearMap.zero_apply,
381       C.value_zero,Finset.sum_const_zero]
382     exact sub_nonneg.mpr hα1
383 
384 /-- P47's error bound holds for actual observation laws under an arbitrary
385 shared randomized history-dependent policy, including zero policy weights. -/
386 theorem shared_policy_tv_bound
387     (π : List (Bool × Bool) → Bool → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
388     (α : ℝ) (hα : 0 ≤ α) (hα1 : α ≤ 1) (n : ℕ) :
389     FiniteTV.distance
390       (ObservationTree.observationLaw C π (fun _ s => continuousOperator 1 s) n initial)
391       (ObservationTree.observationLaw C π (fun _ s => continuousOperator α s) n initial) ≤
392         min 1 ((n:ℝ)*(1-α)/2) := by
393   have hi : initial ∈ C.base := by
394     refine ⟨?_,?_⟩
395     · rw [hcarrier]
396       exact RotationModel.initial_mem
397     · rw [hmass]
398       rfl
399   have h := ObservationTree.shared_policy_observation_tv_bound C π hπ
400     (fun _ s => continuousOperator 1 s) (fun _ s => continuousOperator α s)
401     (fun _ a => common_cone_instrument C hcarrier hmass 1 (by norm_num) (by norm_num) a)
402     (fun _ a => common_cone_instrument C hcarrier hmass α hα hα1 a)
403     (fun _ => 1-α) (fun _ a z hz => action_discrepancy C hcarrier hmass hvalue α hα1 a z hz)
404     n initial initial hi hi
405   simpa only [sub_self,C.value_zero,zero_div,Finset.sum_const,Finset.card_range,
406     nsmul_eq_mul,zero_add] using h
407 
408 end LawComparison
409 
410 /-- The common-policy bound instantiated with the actual, constructed Lorentz
411 base norm; no norm estimate or discrepancy bound is assumed. -/
412 theorem model_shared_policy_tv_bound
413     (π : List (Bool × Bool) → Bool → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
414     (α : ℝ) (hα : 0 ≤ α) (hα1 : α ≤ 1) (n : ℕ) :
415     FiniteTV.distance
416       (ObservationTree.observationLaw LorentzBaseNorm.coneInstance π
417         (fun _ s => continuousOperator 1 s) n initial)
418       (ObservationTree.observationLaw LorentzBaseNorm.coneInstance π
419         (fun _ s => continuousOperator α s) n initial) ≤ min 1 ((n:ℝ)*(1-α)/2) := by
420   exact shared_policy_tv_bound LorentzBaseNorm.coneInstance
421     LorentzBaseNorm.coneInstance_carrier_eq LorentzBaseNorm.coneInstance_mass_eq
422     LorentzBaseNorm.value_eq_sqrt π hπ α hα hα1 n
423 
424 /-- Two exact rational word calculations show that attenuation changes the law. -/
425 theorem exact_and_two_thirds_probe :
426     mass (wordAction (operator 1) [(false,false),(true,false)] initial)=4/5 ∧
427     mass (wordAction (operator (2/3)) [(false,false),(true,false)] initial)=7/10 := by
428   norm_num [wordAction,operator,branchMatrix,probeMatrix,rotationMatrix,initial,mass,
429     Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
430 
431 /-- Embed the actual regular-polygon vertices at mass one. -/
432 def vertexMatrix (n : ℕ) : Matrix (Fin 3) (Fin n) ℝ := fun i j =>
433   LorentzBaseNorm.point 1 (RegularPolygon.vertex n j) i
434 
435 noncomputable def vertexSynthesis (n : ℕ) : (Fin n → ℝ) →ₗ[ℝ] State :=
436   (vertexMatrix n).mulVecLin
437 
438 theorem vertex_generator (n : ℕ) (j : Fin n) :
439     PositiveLift.generator (vertexSynthesis n) j=
440       LorentzBaseNorm.point 1 (RegularPolygon.vertex n j) := by
441   ext i
442   simp [PositiveLift.generator,vertexSynthesis,vertexMatrix,Matrix.mulVec,dotProduct,
443     FiniteBayes.pointMass]
444 
445 theorem vertex_mass (n : ℕ) : mass.comp (vertexSynthesis n)=FiniteInstruments.mass := by
446   ext a
447   simp [mass,vertexSynthesis,vertexMatrix,Matrix.mulVec,dotProduct,FiniteInstruments.mass_apply]
448 
449 /-- Mass-one embedding preserves convex combinations exactly. -/
450 theorem point_convex_combination (a b : ℝ) (hab : a+b=1) (x y : ℂ) :
451     LorentzBaseNorm.point 1 (a • x+b • y)=
452       a • LorentzBaseNorm.point 1 x+b • LorentzBaseNorm.point 1 y := by
453   ext i
454   fin_cases i
455   · change 1=a*1+b*1
456     linarith
457   · simp [LorentzBaseNorm.point]
458   · simp [LorentzBaseNorm.point]
459 
460 /-- Every point of the regular polygon is a positive combination of the
461 actual normalized synthesis columns. -/
462 theorem polygon_point_mem_hull (n : ℕ) {w : ℂ} (hw : w ∈ RegularPolygon.polygon n) :
463     LorentzBaseNorm.point 1 w ∈ PositiveLift.hull (vertexSynthesis n) := by
464   let S : Set ℂ := {w | LorentzBaseNorm.point 1 w ∈ PositiveLift.hull (vertexSynthesis n)}
465   have hs : Set.range (RegularPolygon.vertex n) ⊆ S := by
466     rintro _ ⟨j,rfl⟩
467     change LorentzBaseNorm.point 1 (RegularPolygon.vertex n j) ∈ PositiveLift.hull (vertexSynthesis n)
468     rw [← vertex_generator]
469     exact PositiveLift.generator_mem (vertexSynthesis n) j
470   have hc : Convex ℝ S := by
471     intro x hx y hy a b ha hb hab
472     change LorentzBaseNorm.point 1 (a • x+b • y) ∈ PositiveLift.hull (vertexSynthesis n)
473     rw [point_convex_combination a b hab]
474     exact PositiveLift.hull_convex (vertexSynthesis n) hx hy ha hb hab
475   exact (convexHull_min hs hc) hw
476 
477 /-- The finite vertex hull includes the full inscribed Euclidean disk. -/
478 theorem regular_polygon_inscribed_hull (n : ℕ) (hn : 3 ≤ n) (z : State)
479     (hm : mass z=1) (hz : Real.sqrt ((z 1)^2+(z 2)^2) ≤ Real.cos (Real.pi/(n:ℝ))) :
480     z ∈ PositiveLift.hull (vertexSynthesis n) := by
481   have hball : LorentzBaseNorm.spatial z ∈
482       Metric.closedBall (0:ℂ) (Real.cos (Real.pi/(n:ℝ))) := by
483     simpa only [Metric.mem_closedBall,dist_zero_right,LorentzBaseNorm.spatial_norm] using hz
484   have hp := RegularPolygon.closedBall_subset_polygon n hn hball
485   have he : LorentzBaseNorm.point 1 (LorentzBaseNorm.spatial z)=z := by
486     have h0 : z 0=1 := hm
487     simpa only [h0] using LorentzBaseNorm.point_mass_spatial z
488   rw [← he]
489   exact polygon_point_mem_hull n hp
490 
491 /-- P47's general n-vertex positive stochastic lift, constructed from the
492 proved inscribed-disk geometry of the actual regular polygon. -/
493 theorem regular_polygon_positive_lift (n : ℕ) (hn : 3 ≤ n)
494     (α : ℝ) (hα : 0 ≤ α) (hsmall : α ≤ Real.cos (Real.pi/(n:ℝ))) :
495     ∃ (M : Bool × Bool → Matrix (Fin n) (Fin n) ℝ) (a₀ : Fin n → ℝ),
496       (∀ s i j, 0 ≤ M s i j) ∧ FiniteBayes.IsPrior a₀ ∧ vertexSynthesis n a₀=initial ∧
497       (∀ s, (operator α s).comp (vertexSynthesis n)=(vertexSynthesis n).comp (M s).mulVecLin) ∧
498       (∀ a j, ∑ o : Bool, ∑ i, M (a,o) i j=1) ∧
499       (∀ w, mass (wordAction (operator α) w initial)=
500         FiniteInstruments.mass (wordAction (fun s => (M s).mulVecLin) w a₀)) := by
501   apply finite_vertex_certificate (vertexSynthesis n) (vertex_mass n) ?_ ?_
502     (Real.cos (Real.pi/(n:ℝ))) (regular_polygon_inscribed_hull n hn) α hα hsmall
503   · intro j
504     rw [vertex_generator, ← LorentzBaseNorm.spatial_norm,LorentzBaseNorm.spatial_point,
505       RegularPolygon.vertex_norm]
506   · change LorentzBaseNorm.point 1 (1:ℂ) ∈ PositiveLift.hull (vertexSynthesis n)
507     exact polygon_point_mem_hull n (RegularPolygon.one_mem_polygon n (by omega))
508 
509 /-- The explicit ceiling bound in the manuscript supplies a genuine finite
510 certificate for every positive attenuation loss no larger than one. -/
511 theorem sufficient_vertex_positive_lift (η : ℝ) (hη : 0 < η) (hη1 : η ≤ 1) :
512     let n := RegularPolygon.sufficientVertexCount η
513     ∃ (M : Bool × Bool → Matrix (Fin n) (Fin n) ℝ) (a₀ : Fin n → ℝ),
514       (∀ s i j, 0 ≤ M s i j) ∧ FiniteBayes.IsPrior a₀ ∧ vertexSynthesis n a₀=initial ∧
515       (∀ s, (operator (1-η) s).comp (vertexSynthesis n)=
516         (vertexSynthesis n).comp (M s).mulVecLin) ∧
517       (∀ a j, ∑ o : Bool, ∑ i, M (a,o) i j=1) ∧
518       (∀ w, mass (wordAction (operator (1-η)) w initial)=
519         FiniteInstruments.mass (wordAction (fun s => (M s).mulVecLin) w a₀)) := by
520   obtain ⟨hn,hsmall⟩ := RegularPolygon.sufficient_vertex_count η hη
521   exact regular_polygon_positive_lift _ hn (1-η) (sub_nonneg.mpr hη1) hsmall
522 
523 /-- The four rational generators span the actual three-dimensional state. -/
524 theorem diamond_synthesis_surjective : Function.Surjective synthesis := by
525   intro z
526   let b : ℝ := (z 0-z 1-z 2)/2
527   refine ⟨![z 1+b,z 2,b,0], ?_⟩
528   rw [synthesis_apply]
529   ext i
530   fin_cases i <;> simp [b]
531   all_goals ring
532 
533 /-- A genuine positive inradius forces the regular vertex synthesis to have
534 full row rank; the finite positive certificate does not assume this rank. -/
535 theorem regular_vertex_surjective (n : ℕ) (hn : 3 ≤ n) :
536     Function.Surjective (vertexSynthesis n) := by
537   let r : ℝ := Real.cos (Real.pi/(n:ℝ))
538   have hnR : (3:ℝ) ≤ n := by exact_mod_cast hn
539   have hn0 : (0:ℝ) < n := by linarith
540   have hr : 0 < r := by
541     dsimp [r]
542     apply Real.cos_pos_of_mem_Ioo
543     constructor
544     · have hangle : 0 ≤ Real.pi/(n:ℝ) := by positivity
545       linarith [Real.pi_pos]
546     · apply (div_lt_iff₀ hn0).mpr
547       nlinarith [Real.pi_pos]
548   have hpoint : ∀ w : ℂ, ‖w‖ ≤ r →
549       LorentzBaseNorm.point 1 w ∈ PositiveLift.hull (vertexSynthesis n) := by
550     intro w hw
551     apply polygon_point_mem_hull
552     apply RegularPolygon.closedBall_subset_polygon n hn
553     simpa only [Metric.mem_closedBall,dist_zero_right] using hw
554   obtain ⟨a₀,_ha₀,he₀⟩ := hpoint 0 (by simp; exact hr.le)
555   obtain ⟨a₁,_ha₁,he₁⟩ := hpoint (r:ℂ) (by simp [abs_of_pos hr])
556   obtain ⟨a₂,_ha₂,he₂⟩ := hpoint ((r:ℂ)*Complex.I) (by simp [abs_of_pos hr])
557   intro z
558   refine ⟨(z 0-z 1/r-z 2/r) • a₀+(z 1/r) • a₁+(z 2/r) • a₂, ?_⟩
559   rw [map_add,map_add,map_smul,map_smul,map_smul,he₀,he₁,he₂]
560   ext i
561   fin_cases i <;> simp [LorentzBaseNorm.point]
562   all_goals field_simp [ne_of_gt hr]
563   all_goals ring
564 
565 /-- The actual regular-polygon cone is invariant and contains the declared
566 initial state. This is the geometric component of P47. -/
567 theorem regular_polygon_invariant (n : ℕ) (hn : 3 ≤ n) (α : ℝ)
568     (hα : 0 ≤ α) (hsmall : α ≤ Real.cos (Real.pi/(n:ℝ))) :
569     initial ∈ PositiveLift.hull (vertexSynthesis n) ∧
570       ∀ s z, z ∈ PositiveLift.hull (vertexSynthesis n) →
571         operator α s z ∈ PositiveLift.hull (vertexSynthesis n) := by
572   obtain ⟨M,a₀,hM,ha,hVa,he,_hm,_hw⟩ := regular_polygon_positive_lift n hn α hα hsmall
573   refine ⟨⟨a₀,ha.1,hVa⟩,?_⟩
574   intro s
575   exact (PositiveLift.positive_lift_iff (vertexSynthesis n) (operator α s)).mpr
576     ⟨M s,hM s,he s⟩
577 
578 /-- P47's regular-polygon condition and its common-policy error bound refer
579 to exactly the same attenuation of the rational source model. -/
580 theorem regular_polygon_policy_error (n : ℕ) (hn : 3 ≤ n) (α : ℝ)
581     (hα : 0 ≤ α) (hsmall : α ≤ Real.cos (Real.pi/(n:ℝ)))
582     (π : List (Bool × Bool) → Bool → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h)) (T : ℕ) :
583     Function.Surjective (vertexSynthesis n) ∧
584     (initial ∈ PositiveLift.hull (vertexSynthesis n) ∧
585       ∀ s z, z ∈ PositiveLift.hull (vertexSynthesis n) →
586         operator α s z ∈ PositiveLift.hull (vertexSynthesis n)) ∧
587     FiniteTV.distance
588       (ObservationTree.observationLaw LorentzBaseNorm.coneInstance π
589         (fun _ s => continuousOperator 1 s) T initial)
590       (ObservationTree.observationLaw LorentzBaseNorm.coneInstance π
591         (fun _ s => continuousOperator α s) T initial) ≤ min 1 ((T:ℝ)*(1-α)/2) :=
592   ⟨regular_vertex_surjective n hn,regular_polygon_invariant n hn α hα hsmall,
593     model_shared_policy_tv_bound π hπ α hα (hsmall.trans (Real.cos_le_one _)) T⟩
594 
595 /-- The alpha=2/3 lifted matrices are literal casts of rational matrices. -/
596 theorem rational_lift_matrix (s : Bool × Bool) :
597     ∃ M : Matrix (Fin 4) (Fin 4) ℚ, M.map (algebraMap ℚ ℝ)=liftMatrix (2/3) s := by
598   rcases s with ⟨a,o⟩
599   cases a <;> cases o
600   · refine ⟨!![5/12,1/60,1/60,11/20; 11/20,5/12,1/60,1/60;
601       1/60,11/20,5/12,1/60; 1/60,1/60,11/20,5/12],?_⟩
602     ext i j
603     fin_cases i <;> fin_cases j <;>
604       norm_num [liftMatrix,rotationLift,slack,Matrix.cons_val_two,Matrix.cons_val_three]
605   · refine ⟨0,?_⟩
606     ext i j
607     simp [liftMatrix]
608   · refine ⟨!![1,1/2,0,1/2; 0,0,0,0; 0,0,0,0; 0,0,0,0],?_⟩
609     ext i j
610     fin_cases i <;> fin_cases j <;>
611       norm_num [liftMatrix,probeLift,Matrix.cons_val_two,Matrix.cons_val_three]
612   · refine ⟨!![0,1/2,1,1/2; 0,0,0,0; 0,0,0,0; 0,0,0,0],?_⟩
613     ext i j
614     fin_cases i <;> fin_cases j <;>
615       norm_num [liftMatrix,probeLift,Matrix.cons_val_two,Matrix.cons_val_three]
616 
617 /-- Every datum of the four-generator certificate is rational, including
618 synthesis columns and the normalized initial lifted state. -/
619 theorem rational_diamond_certificate_data :
620     (∃ V : Matrix (Fin 3) (Fin 4) ℚ, V.map (algebraMap ℚ ℝ)=synthesisMatrix) ∧
621     (∀ s, ∃ M : Matrix (Fin 4) (Fin 4) ℚ, M.map (algebraMap ℚ ℝ)=liftMatrix (2/3) s) ∧
622     (∃ a : Fin 4 → ℚ, ∀ j, (algebraMap ℚ ℝ) (a j)=FiniteBayes.pointMass (0:Fin 4) j) := by
623   refine ⟨?_,rational_lift_matrix,?_⟩
624   · refine ⟨!![1,1,1,1; 1,0,-1,0; 0,1,0,-1],?_⟩
625     ext i j
626     fin_cases i <;> fin_cases j <;> norm_num [synthesisMatrix]
627   · refine ⟨fun j => if j=0 then 1 else 0,?_⟩
628     intro j
629     by_cases hj : j=0 <;> simp [FiniteBayes.pointMass,hj]
630 
631 end
632 end Komorebi.LSM.RotationApproximation

Back to source controls