MatrixRotation.lean

1 import KomorebiLSM.RotationP46
2 import KomorebiLSM.MatrixEmbedding
3 import Mathlib.Analysis.Matrix.PosDef
4 import Mathlib.Algebra.Order.Star.Real
5 import Mathlib.Tactic
6 
7 /-! Proposition 51: an exact rational two-by-two matrix certificate for the
8 unchanged rational rotation process. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.MatrixRotation
11 open scoped BigOperators Matrix
12 open FiniteInstruments
13 
14 abbrev State := RotationModel.State
15 abbrev MatrixState := Matrix (Fin 2) (Fin 2) ℝ
16 
17 noncomputable def embedding : State →ₗ[ℝ] MatrixState where
18   toFun z := !![(z 0+z 1)/2,z 2/2; z 2/2,(z 0-z 1)/2]
19   map_add' z w := by
20     ext i j
21     fin_cases i <;> fin_cases j <;> simp <;> ring
22   map_smul' c z := by
23     ext i j
24     fin_cases i <;> fin_cases j <;> simp <;> ring
25 
26 @[simp] theorem embedding_apply (z : State) :
27     embedding z=!![(z 0+z 1)/2,z 2/2; z 2/2,(z 0-z 1)/2] := rfl
28 
29 theorem embedding_hermitian (z : State) : (embedding z).IsHermitian := by
30   unfold Matrix.IsHermitian
31   ext i j
32   fin_cases i <;> fin_cases j <;> simp [Matrix.conjTranspose_apply]
33 
34 theorem embedding_injective : Function.Injective embedding := by
35   intro z w h
36   have h0 := congrFun (congrFun h 0) 0
37   have h1 := congrFun (congrFun h 1) 1
38   have h2 := congrFun (congrFun h 0) 1
39   change (z 0+z 1)/2=(w 0+w 1)/2 at h0
40   change (z 0-z 1)/2=(w 0-w 1)/2 at h1
41   change z 2/2=w 2/2 at h2
42   ext i
43   fin_cases i <;> simp_all <;> linarith
44 
45 @[simp] theorem embedding_trace (z : State) : (embedding z).trace=RotationModel.mass z := by
46   simp [Matrix.trace,Fin.sum_univ_succ]
47   ring
48 
49 theorem embedding_det (z : State) :
50     (embedding z).det=((z 0)^2-(z 1)^2-(z 2)^2)/4 := by
51   simp [Matrix.det_fin_two]
52   ring
53 
54 /-- The elementary two-variable criterion, including a vanishing first pivot. -/
55 theorem binary_quadratic_nonneg (a b c : ℝ) (ha : 0 ≤ a) (hc : 0 ≤ c)
56     (hdet : b^2 ≤ a*c) (u v : ℝ) :
57     0 ≤ a*u^2+2*b*u*v+c*v^2 := by
58   by_cases ha0 : a=0
59   · have hb : b=0 := by nlinarith [sq_nonneg b]
60     subst a
61     subst b
62     simpa using mul_nonneg hc (sq_nonneg v)
63   · have ha' : 0<a := lt_of_le_of_ne ha (Ne.symm ha0)
64     apply nonneg_of_mul_nonneg_left _ ha'
65     calc
66       (a*u^2+2*b*u*v+c*v^2)*a = (a*u+b*v)^2+(a*c-b^2)*v^2 := by ring
67       _ ≥ 0 := add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hdet) (sq_nonneg _))
68 
69 theorem embedding_posSemidef_iff (z : State) :
70     (embedding z).PosSemidef ↔ z ∈ RotationModel.cone := by
71   constructor
72   · intro hz
73     have hd0 := hz.diag_nonneg (i:=0)
74     have hd1 := hz.diag_nonneg (i:=1)
75     have hdet := hz.det_nonneg
76     rw [embedding_det] at hdet
77     change 0 ≤ (z 0+z 1)/2 at hd0
78     change 0 ≤ (z 0-z 1)/2 at hd1
79     apply Real.sqrt_le_iff.mpr
80     constructor <;> nlinarith
81   · intro hz
82     change Real.sqrt ((z 1)^2+(z 2)^2) ≤ z 0 at hz
83     have hm : 0 ≤ z 0 := (Real.sqrt_nonneg _).trans hz
84     have hx := RotationModel.cone_spatial_abs hz
85     have hsq := Real.sq_sqrt (show 0 ≤ (z 1)^2+(z 2)^2 by positivity)
86     have hs := Real.sqrt_nonneg ((z 1)^2+(z 2)^2)
87     have hdiag0 : 0 ≤ (z 0+z 1)/2 := by linarith [neg_abs_le (z 1)]
88     have hdiag1 : 0 ≤ (z 0-z 1)/2 := by linarith [le_abs_self (z 1)]
89     have hdet : (z 2/2)^2 ≤ ((z 0+z 1)/2)*((z 0-z 1)/2) := by nlinarith
90     apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg (embedding_hermitian z)
91     intro v
92     have h := binary_quadratic_nonneg _ _ _ hdiag0 hdiag1 hdet (v 0) (v 1)
93     have he : star v ⬝ᵥ ((embedding z) *ᵥ v) =
94         (z 0+z 1)/2*(v 0)^2+2*(z 2/2)*(v 0)*(v 1)+(z 0-z 1)/2*(v 1)^2 := by
95       simp [Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
96       ring
97     rw [he]
98     exact h
99 
100 @[simp] theorem embedding_initial : embedding RotationModel.initial=!![1,0;0,0] := by
101   ext i j
102   fin_cases i <;> fin_cases j <;> norm_num [RotationModel.initial,Matrix.cons_val_two]
103 
104 def interiorWitness : State := ![1,0,0]
105 
106 theorem embedding_interior : (embedding interiorWitness).PosDef := by
107   have he : embedding interiorWitness=(1/2:ℝ) • (1:MatrixState) := by
108     ext i j
109     fin_cases i <;> fin_cases j <;> norm_num [interiorWitness,Matrix.one_apply,Matrix.cons_val_two]
110   rw [he]
111   exact Matrix.PosDef.one.smul (by norm_num)
112 
113 
114 /-- Integer matrices and rational weights are the complete congruence data. -/
115 def rotationKQ : Matrix (Fin 2) (Fin 2) ℚ := !![2,-1;1,2]
116 def probeK0Q : Matrix (Fin 2) (Fin 2) ℚ := !![1,0;0,0]
117 def probeK1Q : Matrix (Fin 2) (Fin 2) ℚ := !![0,1;0,0]
118 
119 noncomputable def rotationK : MatrixState := rotationKQ.map (algebraMap ℚ ℝ)
120 noncomputable def probeK0 : MatrixState := probeK0Q.map (algebraMap ℚ ℝ)
121 noncomputable def probeK1 : MatrixState := probeK1Q.map (algebraMap ℚ ℝ)
122 
123 def branchWeightQ (s : Bool × Bool) : ℚ :=
124   if s.1 then 1 else (if s.2 then 0 else 1/5)
125 
126 def branchKQ (s : Bool × Bool) : Matrix (Fin 2) (Fin 2) ℚ :=
127   if s.1 then (if s.2 then probeK1Q else probeK0Q)
128   else (if s.2 then 0 else rotationKQ)
129 
130 noncomputable def branchWeight (s : Bool × Bool) : ℝ := (algebraMap ℚ ℝ) (branchWeightQ s)
131 noncomputable def branchK (s : Bool × Bool) : MatrixState := (branchKQ s).map (algebraMap ℚ ℝ)
132 
133 noncomputable def congruence (K : MatrixState) : MatrixState →ₗ[ℝ] MatrixState :=
134   { toFun := fun X => K*X*Kᵀ
135     map_add' := fun X Y => by simp [Matrix.mul_add,Matrix.add_mul]
136     map_smul' := fun c X => by simp }
137 
138 @[simp] theorem congruence_apply (K X : MatrixState) : congruence K X=K*X*Kᵀ := rfl
139 
140 noncomputable def matrixOperator (s : Bool × Bool) : MatrixState →ₗ[ℝ] MatrixState :=
141   branchWeight s • congruence (branchK s)
142 
143 @[simp] theorem matrixOperator_apply (s : Bool × Bool) (X : MatrixState) :
144     matrixOperator s X=branchWeight s • (branchK s*X*(branchK s)ᵀ) := rfl
145 
146 theorem branchWeight_nonnegative (s : Bool × Bool) : 0 ≤ branchWeight s := by
147   rcases s with ⟨a,o⟩
148   cases a <;> cases o <;> norm_num [branchWeight,branchWeightQ]
149 
150 theorem embedding_rotate (z : State) :
151     embedding (RotationModel.rotate z)=(1/5:ℝ) • (rotationK*embedding z*rotationKᵀ) := by
152   ext i j
153   fin_cases i <;> fin_cases j <;>
154     simp [rotationK,rotationKQ,Matrix.mul_apply,Fin.sum_univ_succ] <;> ring
155 
156 theorem embedding_probe0 (z : State) :
157     embedding (RotationModel.probe0 z)=probeK0*embedding z*probeK0ᵀ := by
158   ext i j
159   fin_cases i <;> fin_cases j <;>
160     simp [probeK0,probeK0Q,RotationModel.initial,Matrix.mul_apply,Fin.sum_univ_succ,
161       Matrix.cons_val_two]
162 
163 theorem embedding_probe1 (z : State) :
164     embedding (RotationModel.probe1 z)=probeK1*embedding z*probeK1ᵀ := by
165   ext i j
166   fin_cases i <;> fin_cases j <;>
167     simp [probeK1,probeK1Q,RotationModel.initial,Matrix.mul_apply,Fin.sum_univ_succ,
168       Matrix.cons_val_two]
169 
170 theorem embedding_operator (s : Bool × Bool) (z : State) :
171     embedding (RotationModel.operator s z)=matrixOperator s (embedding z) := by
172   rcases s with ⟨a,o⟩
173   cases a <;> cases o
174   · simpa [branchWeight,branchWeightQ,branchK,branchKQ,rotationK] using embedding_rotate z
175   · rw [RotationModel.operator_rotate1,LinearMap.zero_apply,map_zero]
176     simp [branchWeight,branchWeightQ]
177   · simpa [branchWeight,branchWeightQ,branchK,branchKQ,probeK0] using embedding_probe0 z
178   · simpa [branchWeight,branchWeightQ,branchK,branchKQ,probeK1] using embedding_probe1 z
179 
180 theorem rotationK_gram : rotationKᵀ*rotationK=5 • (1:MatrixState) := by
181   ext i j
182   fin_cases i <;> fin_cases j <;>
183     norm_num [rotationK,rotationKQ,Matrix.mul_apply,Fin.sum_univ_succ,Matrix.one_apply]
184 
185 theorem probeK_gram : probeK0ᵀ*probeK0+probeK1ᵀ*probeK1=(1:MatrixState) := by
186   ext i j
187   fin_cases i <;> fin_cases j <;>
188     norm_num [probeK0,probeK0Q,probeK1,probeK1Q,Matrix.mul_apply,Fin.sum_univ_succ,
189       Matrix.one_apply]
190 
191 theorem matrixOperator_trace_mass (a : Bool) (X : MatrixState) :
192     ∑ o : Bool, (matrixOperator (a,o) X).trace=X.trace := by
193   cases a <;>
194     simp [matrixOperator,congruence,branchWeight,branchWeightQ,branchK,branchKQ,
195       rotationKQ,probeK0Q,probeK1Q,Matrix.trace,Matrix.mul_apply,Fin.sum_univ_succ] <;> ring
196 
197 theorem embedding_word (w : List (Bool × Bool)) (z : State) :
198     embedding (wordAction RotationModel.operator w z)=
199       wordAction matrixOperator w (embedding z) := by
200   induction w generalizing z with
201   | nil => rfl
202   | cons s w ih =>
203     simpa only [wordAction_cons,LinearMap.comp_apply,embedding_operator] using ih (RotationModel.operator s z)
204 
205 theorem word_probability_unchanged (w : List (Bool × Bool)) (z : State) :
206     (wordAction matrixOperator w (embedding z)).trace=
207       RotationModel.mass (wordAction RotationModel.operator w z) := by
208   rw [← embedding_word,embedding_trace]
209 
210 noncomputable def matrixProcess (w : List (Bool × Bool)) : ℝ :=
211   (wordAction matrixOperator w (embedding RotationModel.initial)).trace
212 
213 theorem matrixProcess_eq : matrixProcess=RotationModel.process := by
214   funext w
215   exact word_probability_unchanged w RotationModel.initial
216 
217 theorem matrixProcess_causal : Behavior.CausalLaw matrixProcess := by
218   rw [matrixProcess_eq]
219   exact RotationModel.process_causal
220 
221 theorem matrixProcess_probability (w : List (Bool × Bool)) :
222     0 ≤ matrixProcess w ∧ matrixProcess w ≤ 1 := matrixProcess_causal.word_bounds w
223 
224 
225 /-- The embedding itself has exact rational coefficients. -/
226 def embeddingQ : (Fin 3 → ℚ) →ₗ[ℚ] Matrix (Fin 2) (Fin 2) ℚ where
227   toFun z := !![(z 0+z 1)/2,z 2/2; z 2/2,(z 0-z 1)/2]
228   map_add' z w := by
229     ext i j
230     fin_cases i <;> fin_cases j <;> simp <;> ring
231   map_smul' c z := by
232     ext i j
233     fin_cases i <;> fin_cases j <;> simp <;> ring
234 
235 theorem embedding_rational_cast (z : Fin 3 → ℚ) :
236     (embeddingQ z).map (algebraMap ℚ ℝ)=embedding (fun i => (algebraMap ℚ ℝ) (z i)) := by
237   ext i j
238   fin_cases i <;> fin_cases j <;> simp [embeddingQ]
239 
240 theorem normalized_base_disk (z : State) :
241     (embedding z).PosSemidef ∧ (embedding z).trace=1 ↔
242       z 0=1 ∧ Real.sqrt ((z 1)^2+(z 2)^2) ≤ 1 := by
243   rw [embedding_posSemidef_iff,embedding_trace]
244   change (Real.sqrt ((z 1)^2+(z 2)^2) ≤ z 0 ∧ z 0=1) ↔ _
245   constructor
246   · rintro ⟨hr,hm⟩
247     exact ⟨hm,by simpa only [hm] using hr⟩
248   · rintro ⟨hm,hr⟩
249     exact ⟨by simpa only [hm] using hr,hm⟩
250 
251 theorem initial_matrix_normalized :
252     (embedding RotationModel.initial).PosSemidef ∧ (embedding RotationModel.initial).trace=1 :=
253   ⟨(embedding_posSemidef_iff _).mpr RotationModel.initial_mem,by simp⟩
254 
255 theorem no_finite_positive_generator_certificate (n : ℕ) :
256     ¬ ∃ V : (Fin n → ℝ) →ₗ[ℝ] State,
257       RotationModel.mass.comp V=FiniteInstruments.mass ∧
258       RotationModel.initial ∈ PositiveLift.hull V ∧
259       ∀ s z, z ∈ PositiveLift.hull V → RotationModel.operator s z ∈ PositiveLift.hull V := by
260   rintro ⟨V,hm,hi,hb⟩
261   exact RotationConeGeometry.no_finite_normalized_generator_certificate V hm hi hb
262 
263 
264 /-- Each matrix branch preserves the whole positive semidefinite cone. -/
265 theorem matrixOperator_posSemidef (s : Bool × Bool) {X : MatrixState} (hX : X.PosSemidef) :
266     (matrixOperator s X).PosSemidef := by
267   rw [matrixOperator_apply]
268   apply Matrix.PosSemidef.smul _ (branchWeight_nonnegative s)
269   simpa only [Matrix.conjTranspose_eq_transpose_of_trivial] using
270     hX.mul_mul_conjTranspose_same (branchK s)
271 
272 theorem matrix_word_posSemidef (w : List (Bool × Bool)) {X : MatrixState}
273     (hX : X.PosSemidef) : (wordAction matrixOperator w X).PosSemidef := by
274   induction w generalizing X with
275   | nil => exact hX
276   | cons s w ih =>
277     exact ih (matrixOperator_posSemidef s hX)
278 
279 theorem rational_branch_certificate (s : Bool × Bool) :
280     ∃ (c : ℚ) (K : Matrix (Fin 2) (Fin 2) ℚ), 0 ≤ c ∧
281       ∀ z : State, embedding (RotationModel.operator s z)=
282         (algebraMap ℚ ℝ) c •
283           (K.map (algebraMap ℚ ℝ)*embedding z*(K.map (algebraMap ℚ ℝ))ᵀ) := by
284   refine ⟨branchWeightQ s,branchKQ s,?_,embedding_operator s⟩
285   rcases s with ⟨a,o⟩
286   cases a <;> cases o <;> norm_num [branchWeightQ]
287 
288 /-- All clauses concern the unchanged source process, alongside its finite
289 positive-generator obstruction. Matrix positivity changes the certificate
290 language and does not attenuate the model. -/
291 theorem exact_rational_matrix_witness :
292     Function.Injective embedding ∧
293     (∀ z, (embedding z).IsHermitian) ∧
294     (∀ z, (embedding z).trace=RotationModel.mass z) ∧
295     (∀ z, (embedding z).PosSemidef ↔ z ∈ RotationModel.cone) ∧
296     (embedding interiorWitness).PosDef ∧
297     embedding RotationModel.initial=!![1,0;0,0] ∧
298     (∀ s, 0 ≤ branchWeight s) ∧
299     (∀ s z, embedding (RotationModel.operator s z)=matrixOperator s (embedding z)) ∧
300     (∀ a X, ∑ o : Bool, (matrixOperator (a,o) X).trace=X.trace) ∧
301     (∀ w, matrixProcess w=RotationModel.process w) ∧
302     (∀ n : ℕ, ¬ ∃ V : (Fin n → ℝ) →ₗ[ℝ] State,
303       RotationModel.mass.comp V=FiniteInstruments.mass ∧
304       RotationModel.initial ∈ PositiveLift.hull V ∧
305       ∀ s z, z ∈ PositiveLift.hull V → RotationModel.operator s z ∈ PositiveLift.hull V) := by
306   exact ⟨embedding_injective,embedding_hermitian,embedding_trace,embedding_posSemidef_iff,
307     embedding_interior,embedding_initial,branchWeight_nonnegative,embedding_operator,
308     matrixOperator_trace_mass,fun w => congrFun matrixProcess_eq w,
309     no_finite_positive_generator_certificate⟩
310 
311 
312 /-- The displayed rational witness is an instance of the generic matrix
313 embedding certificate language, with its actual interior matrix. -/
314 noncomputable def certificate : MatrixEmbedding.Embedding State (Fin 2) where
315   J := embedding
316   symmetric := embedding_hermitian
317   injective := embedding_injective
318   interior := interiorWitness
319   interior_posDef := embedding_interior
320 
321 @[simp] theorem certificate_mass : certificate.mass=RotationModel.mass := by
322   apply LinearMap.ext
323   intro z
324   exact embedding_trace z
325 
326 @[simp] theorem certificate_cone : certificate.cone=RotationModel.cone := by
327   ext z
328   exact embedding_posSemidef_iff z
329 
330 end Komorebi.LSM.MatrixRotation

Back to source controls