RotationModel.lean

1 import KomorebiLSM.BehaviorProbability
2 import Mathlib.Analysis.SpecialFunctions.Sqrt
3 import Mathlib.Tactic
4 
5 /-! The exact rational controlled rotation process in Proposition 46.
6 The three coordinates are mass and two signed spatial coordinates. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.RotationModel
9 open scoped BigOperators
10 open FiniteInstruments
11 
12 abbrev State := Fin 3 → ℝ
13 
14 noncomputable def mass : State →ₗ[ℝ] ℝ := LinearMap.proj 0
15 
16 def initial : State := ![1,1,0]
17 
18 noncomputable def rotationMatrix : Matrix (Fin 3) (Fin 3) ℝ :=
19   !![1,0,0; 0,3/5,-4/5; 0,4/5,3/5]
20 
21 noncomputable def probeMatrix0 : Matrix (Fin 3) (Fin 3) ℝ :=
22   !![1/2,1/2,0; 1/2,1/2,0; 0,0,0]
23 
24 noncomputable def probeMatrix1 : Matrix (Fin 3) (Fin 3) ℝ :=
25   !![1/2,-1/2,0; 1/2,-1/2,0; 0,0,0]
26 
27 /-- Exact rational matrices whose real casts define the process. -/
28 def rotationMatrixQ : Matrix (Fin 3) (Fin 3) ℚ :=
29   !![1,0,0; 0,3/5,-4/5; 0,4/5,3/5]
30 def probeMatrix0Q : Matrix (Fin 3) (Fin 3) ℚ :=
31   !![1/2,1/2,0; 1/2,1/2,0; 0,0,0]
32 def probeMatrix1Q : Matrix (Fin 3) (Fin 3) ℚ :=
33   !![1/2,-1/2,0; 1/2,-1/2,0; 0,0,0]
34 
35 noncomputable def rotate : State →ₗ[ℝ] State := rotationMatrix.mulVecLin
36 noncomputable def probe0 : State →ₗ[ℝ] State := probeMatrix0.mulVecLin
37 noncomputable def probe1 : State →ₗ[ℝ] State := probeMatrix1.mulVecLin
38 
39 noncomputable def matrix (s : Bool × Bool) : Matrix (Fin 3) (Fin 3) ℝ :=
40   if s.1 then (if s.2 then probeMatrix1 else probeMatrix0)
41   else (if s.2 then 0 else rotationMatrix)
42 
43 noncomputable def operator (s : Bool × Bool) : State →ₗ[ℝ] State :=
44   if s.1 then (if s.2 then probe1 else probe0)
45   else (if s.2 then 0 else rotate)
46 
47 @[simp] theorem operator_rotate0 : operator (false,false) = rotate := rfl
48 @[simp] theorem operator_rotate1 : operator (false,true) = 0 := rfl
49 @[simp] theorem operator_probe0 : operator (true,false) = probe0 := rfl
50 @[simp] theorem operator_probe1 : operator (true,true) = probe1 := rfl
51 
52 theorem operator_matrix (s : Bool × Bool) : operator s = (matrix s).mulVecLin := by
53   rcases s with ⟨a,o⟩
54   cases a <;> cases o <;> simp [operator,matrix,rotate,probe0,probe1]
55 
56 @[simp] theorem mass_apply (z : State) : mass z = z 0 := rfl
57 
58 @[simp] theorem rotate_apply (z : State) :
59     rotate z = ![z 0, (3/5:ℝ)*z 1-(4/5:ℝ)*z 2, (4/5:ℝ)*z 1+(3/5:ℝ)*z 2] := by
60   ext i
61   fin_cases i <;> simp [rotate,rotationMatrix,Matrix.mulVec,dotProduct,Fin.sum_univ_succ,sub_eq_add_neg,neg_div,neg_mul]
62 
63 @[simp] theorem probe0_apply (z : State) :
64     probe0 z = ((z 0+z 1)/2) • initial := by
65   ext i
66   fin_cases i <;> simp [probe0,probeMatrix0,initial,Matrix.mulVec,dotProduct,Fin.sum_univ_succ] <;> ring
67 
68 @[simp] theorem probe1_apply (z : State) :
69     probe1 z = ((z 0-z 1)/2) • initial := by
70   ext i
71   fin_cases i <;> simp [probe1,probeMatrix1,initial,Matrix.mulVec,dotProduct,Fin.sum_univ_succ] <;> ring
72 
73 /-- Every actual branch matrix is the real cast of an exact rational matrix. -/
74 theorem matrix_is_rational (s : Bool × Bool) :
75     ∃ M : Matrix (Fin 3) (Fin 3) ℚ, M.map (algebraMap ℚ ℝ) = matrix s := by
76   rcases s with ⟨a,o⟩
77   cases a <;> cases o
78   · refine ⟨rotationMatrixQ, ?_⟩
79     ext i j
80     fin_cases i <;> fin_cases j <;> norm_num [matrix,rotationMatrixQ,rotationMatrix]
81   · refine ⟨0, ?_⟩
82     ext i j
83     simp [matrix]
84   · refine ⟨probeMatrix0Q, ?_⟩
85     ext i j
86     fin_cases i <;> fin_cases j <;> norm_num [matrix,probeMatrix0Q,probeMatrix0]
87   · refine ⟨probeMatrix1Q, ?_⟩
88     ext i j
89     fin_cases i <;> fin_cases j <;> norm_num [matrix,probeMatrix1Q,probeMatrix1]
90 
91 /-- The Lorentz cone, expressed in the actual three coordinates. -/
92 def cone : Set State := {z | Real.sqrt ((z 1)^2+(z 2)^2) ≤ z 0}
93 
94 @[simp] theorem cone_iff (z : State) : z ∈ cone ↔ Real.sqrt ((z 1)^2+(z 2)^2) ≤ z 0 := Iff.rfl
95 
96 theorem cone_zero : (0 : State) ∈ cone := by simp [cone]
97 
98 @[simp] theorem initial_zero : initial 0 = 1 := rfl
99 @[simp] theorem initial_one : initial 1 = 1 := rfl
100 @[simp] theorem initial_two : initial 2 = 0 := rfl
101 
102 theorem initial_mem : initial ∈ cone := by
103   change Real.sqrt ((1:ℝ)^2+0^2) ≤ 1
104   norm_num
105 
106 @[simp] theorem initial_mass : mass initial = 1 := rfl
107 
108 theorem cone_mass_nonneg {z : State} (hz : z ∈ cone) : 0 ≤ mass z :=
109   (Real.sqrt_nonneg _).trans hz
110 
111 theorem cone_spatial_abs {z : State} (hz : z ∈ cone) : |z 1| ≤ z 0 := by
112   have hsq : |z 1| ≤ Real.sqrt ((z 1)^2+(z 2)^2) := by
113     rw [← Real.sqrt_sq_eq_abs]
114     exact Real.sqrt_le_sqrt (by nlinarith [sq_nonneg (z 2)])
115   exact hsq.trans hz
116 
117 theorem cone_scale {z : State} (hz : z ∈ cone) {c : ℝ} (hc : 0 ≤ c) : c • z ∈ cone := by
118   change Real.sqrt ((c*z 1)^2+(c*z 2)^2) ≤ c*z 0
119   have he : (c*z 1)^2+(c*z 2)^2 = c^2*((z 1)^2+(z 2)^2) := by ring
120   rw [he,Real.sqrt_mul (sq_nonneg c),Real.sqrt_sq_eq_abs,abs_of_nonneg hc]
121   exact mul_le_mul_of_nonneg_left hz hc
122 
123 @[simp] theorem rotate_zero (z : State) : rotate z 0 = z 0 := by
124   rw [rotate_apply]
125   rfl
126 @[simp] theorem rotate_one (z : State) : rotate z 1 = (3/5:ℝ)*z 1-(4/5:ℝ)*z 2 := by
127   rw [rotate_apply]
128   rfl
129 @[simp] theorem rotate_two (z : State) : rotate z 2 = (4/5:ℝ)*z 1+(3/5:ℝ)*z 2 := by
130   rw [rotate_apply]
131   rfl
132 
133 theorem rotate_spatial_square (z : State) :
134     (rotate z 1)^2+(rotate z 2)^2 = (z 1)^2+(z 2)^2 := by
135   rw [rotate_one,rotate_two]
136   ring
137 
138 theorem rotate_cone {z : State} (hz : z ∈ cone) : rotate z ∈ cone := by
139   change Real.sqrt ((rotate z 1)^2+(rotate z 2)^2) ≤ rotate z 0
140   rw [rotate_spatial_square,rotate_zero]
141   exact hz
142 
143 theorem probe0_cone {z : State} (hz : z ∈ cone) : probe0 z ∈ cone := by
144   rw [probe0_apply]
145   apply cone_scale initial_mem
146   have h := neg_abs_le (z 1)
147   have hx := cone_spatial_abs hz
148   linarith
149 
150 theorem probe1_cone {z : State} (hz : z ∈ cone) : probe1 z ∈ cone := by
151   rw [probe1_apply]
152   apply cone_scale initial_mem
153   have h := le_abs_self (z 1)
154   have hx := cone_spatial_abs hz
155   linarith
156 
157 theorem operator_cone (s : Bool × Bool) {z : State} (hz : z ∈ cone) : operator s z ∈ cone := by
158   rcases s with ⟨a,o⟩
159   cases a <;> cases o <;> simp only [operator_rotate0,operator_rotate1,operator_probe0,operator_probe1,LinearMap.zero_apply]
160   · exact rotate_cone hz
161   · exact cone_zero
162   · exact probe0_cone hz
163   · exact probe1_cone hz
164 
165 theorem word_cone (w : List (Bool × Bool)) {z : State} (hz : z ∈ cone) :
166     wordAction operator w z ∈ cone := by
167   induction w generalizing z with
168   | nil => exact hz
169   | cons s w ih => exact ih (operator_cone s hz)
170 
171 /-- Every future experiment has nonnegative mass on the actual Lorentz cone. -/
172 theorem all_word_mass_nonneg (w : List (Bool × Bool)) {z : State} (hz : z ∈ cone) :
173     0 ≤ mass (wordAction operator w z) := cone_mass_nonneg (word_cone w hz)
174 
175 /-- The actual branch operators conserve mass for both actions. -/
176 theorem operator_mass (a : Bool) (z : State) : ∑ o, mass (operator (a,o) z) = mass z := by
177   rw [Fintype.sum_bool]
178   cases a
179   · change mass (0 : State) + mass (rotate z) = mass z
180     simp
181   · change mass (probe1 z) + mass (probe0 z) = mass z
182     rw [probe0_apply,probe1_apply,map_smul,map_smul,initial_mass]
183     simp only [mass_apply,smul_eq_mul]
184     ring
185 
186 noncomputable def process (w : List (Bool × Bool)) : ℝ := mass (wordAction operator w initial)
187 
188 noncomputable def realization : Behavior.Realization process State where
189   initial := initial
190   operator := operator
191   readout := mass
192   correct _ := rfl
193 
194 /-- Every normalized point of the invariant cone defines a genuine causal law. -/
195 theorem causal_of_normalized_cone (z : State) (hz : z ∈ cone) (hm : mass z = 1) :
196     Behavior.CausalLaw (fun w => mass (wordAction operator w z)) := by
197   refine ⟨hm,?_,?_⟩
198   · intro w
199     exact all_word_mass_nonneg w hz
200   · intro h a
201     simpa only [wordAction_append,wordAction_cons,wordAction_nil,
202       LinearMap.id_comp,LinearMap.comp_apply] using operator_mass a (wordAction operator h z)
203 
204 theorem normalized_word_probability (z : State) (hz : z ∈ cone) (hm : mass z = 1)
205     (w : List (Bool × Bool)) :
206     0 ≤ mass (wordAction operator w z) ∧ mass (wordAction operator w z) ≤ 1 :=
207   (causal_of_normalized_cone z hz hm).word_bounds w
208 
209 /-- Conditioning a positive branch remains in the normalized cone. -/
210 theorem posterior_cone (s : Bool × Bool) (z : State) (hz : z ∈ cone)
211     (hp : 0 < mass (operator s z)) :
212     normalize mass (operator s z) ∈ cone ∧ mass (normalize mass (operator s z)) = 1 := by
213   exact ⟨cone_scale (operator_cone s hz) (inv_nonneg.mpr hp.le),
214     normalize_mass mass (operator s z) (ne_of_gt hp)⟩
215 
216 /-- Every positive probe output is reset to the declared boundary state. -/
217 theorem probe0_posterior (z : State) (hp : 0 < (z 0+z 1)/2) :
218     normalize mass (probe0 z) = initial := by
219   rw [probe0_apply]
220   unfold FiniteInstruments.normalize
221   rw [map_smul,initial_mass]
222   simp only [smul_eq_mul,mul_one]
223   rw [smul_smul,inv_mul_cancel₀ (ne_of_gt hp),one_smul]
224 
225 theorem probe1_posterior (z : State) (hp : 0 < (z 0-z 1)/2) :
226     normalize mass (probe1 z) = initial := by
227   rw [probe1_apply]
228   unfold FiniteInstruments.normalize
229   rw [map_smul,initial_mass]
230   simp only [smul_eq_mul,mul_one]
231   rw [smul_smul,inv_mul_cancel₀ (ne_of_gt hp),one_smul]
232 
233 /-- This is a causal law from the constructed cone, not from entrywise positivity. -/
234 theorem process_causal : Behavior.CausalLaw process := by
235   refine ⟨initial_mass,?_,?_⟩
236   · intro w
237     exact cone_mass_nonneg (word_cone w initial_mem)
238   · intro h a
239     simpa only [process,wordAction_append,wordAction_cons,wordAction_nil,
240       LinearMap.id_comp,LinearMap.comp_apply] using operator_mass a (wordAction operator h initial)
241 
242 theorem process_probability (w : List (Bool × Bool)) : 0 ≤ process w ∧ process w ≤ 1 :=
243   process_causal.word_bounds w
244 
245 end Komorebi.LSM.RotationModel

Back to source controls