RotationConeGeometry.lean

1 import KomorebiLSM.RotationDensity
2 import KomorebiLSM.LorentzBaseNorm
3 import KomorebiLSM.PositiveLiftTopology
4 import KomorebiLSM.RotationRank
5 import Mathlib.Analysis.Convex.Strict.Extreme
6 import Mathlib.Analysis.InnerProductSpace.Convex
7 import Mathlib.Analysis.Normed.Module.Convex
8 
9 set_option autoImplicit false
10 namespace Komorebi.LSM.RotationConeGeometry
11 open Set Metric
12 open RotationDensity
13 
14 /-- Distinct forward times give distinct actual rational rotations. -/
15 theorem rotation_power_injective : Function.Injective (fun n : ℕ => rotation ^ n) := by
16   apply injective_pow_iff_not_isOfFinOrder.mpr
17   intro h
18   obtain ⟨n, hn, he⟩ := h.exists_pow_eq_one
19   exact rotation_pow_ne_one n hn he
20 
21 /-- The unit disk cannot be the convex hull of finitely many complex points. -/
22 theorem disk_not_finite_convex_hull (s : Finset ℂ) :
23     convexHull ℝ (s : Set ℂ) ≠ closedBall 0 1 := by
24   intro he
25   have hi : Function.Injective (fun n : ℕ => ((rotation ^ n : Circle) : ℂ)) :=
26     Subtype.val_injective.comp rotation_power_injective
27   have hinf := Set.infinite_range_of_injective hi
28   have hsub : Set.range (fun n : ℕ => ((rotation ^ n : Circle) : ℂ)) ⊆ (s : Set ℂ) := by
29     rintro x ⟨n, rfl⟩
30     apply (extremePoints_convexHull_subset (𝕜 := ℝ) (A := (s : Set ℂ)))
31     rw [he, StrictConvexSpace.extremePoints_closedBall_eq_sphere]
32     simp
33   exact hinf (s.finite_toSet.subset hsub)
34 
35 /-- Dense forward rotated observations detect the full Euclidean radius. -/
36 theorem norm_le_of_rotated_re_le (w : ℂ) (t : ℝ)
37     (h : ∀ n : ℕ, (((rotation ^ n : Circle) : ℂ) * w).re ≤ t) : ‖w‖ ≤ t := by
38   have hall : ∀ u : Circle, ((u : ℂ) * w).re ≤ t := by
39     intro u
40     exact rotation_forward_dense.induction_on (p := fun u : Circle => ((u : ℂ) * w).re ≤ t) u
41       (isClosed_le (by fun_prop) continuous_const) h
42   by_cases hw : w = 0
43   · simpa [hw] using hall 1
44   · have hn : 0 < ‖w‖ := norm_pos_iff.mpr hw
45     let u : Circle := ⟨(star w) / (‖w‖ : ℂ), by
46       apply mem_sphere_zero_iff_norm.mpr
47       simp [ne_of_gt hn]⟩
48     have he : ((u : ℂ) * w).re = ‖w‖ := by
49       change (((star w) / (‖w‖ : ℂ)) * w).re = ‖w‖
50       simp only [Complex.mul_re, Complex.div_ofReal_re, Complex.div_ofReal_im,
51         Complex.star_def, Complex.conj_re, Complex.conj_im]
52       have hsq := Complex.normSq_eq_norm_sq w
53       rw [Complex.normSq_apply] at hsq
54       field_simp
55       nlinarith
56     simpa [he] using hall u
57 
58 
59 
60 open RotationModel FiniteInstruments
61 open LorentzBaseNorm (spatial point)
62 
63 /-- Complex multiplication is precisely the displayed rational spatial rotation. -/
64 theorem spatial_rotate (z : RotationModel.State) :
65     spatial (rotate z) = (rotation : ℂ) * spatial z := by
66   apply Complex.ext <;> simp [Complex.mul_re, Complex.mul_im]
67   ring
68 
69 /-- The chronological word consisting of n forward rotate branches. -/
70 def rotationWord (n : ℕ) : List (Bool × Bool) := List.replicate n (false,false)
71 
72 @[simp] theorem rotationWord_zero : rotationWord 0 = [] := rfl
73 @[simp] theorem rotationWord_succ (n : ℕ) :
74     rotationWord (n+1) = (false,false)::rotationWord n := rfl
75 
76 theorem rotationWord_mass (n : ℕ) (z : RotationModel.State) :
77     RotationModel.mass (wordAction operator (rotationWord n) z) = z 0 := by
78   induction n generalizing z with
79   | zero => simp [rotationWord]
80   | succ n ih =>
81     simp only [rotationWord_succ,wordAction_cons,LinearMap.comp_apply,operator_rotate0]
82     rw [ih,rotate_zero]
83 
84 theorem rotationWord_spatial (n : ℕ) (z : RotationModel.State) :
85     spatial (wordAction operator (rotationWord n) z) = ((rotation^n : Circle) : ℂ) * spatial z := by
86   induction n generalizing z with
87   | zero => simp [rotationWord]
88   | succ n ih =>
89     simp only [rotationWord_succ,wordAction_cons,LinearMap.comp_apply,operator_rotate0]
90     rw [ih,spatial_rotate]
91     simp only [pow_succ,Circle.coe_mul]
92     ring
93 
94 theorem rotationWord_initial (n : ℕ) :
95     wordAction operator (rotationWord n) initial = point 1 ((rotation^n : Circle) : ℂ) := by
96   rw [← LorentzBaseNorm.point_mass_spatial (wordAction operator (rotationWord n) initial)]
97   have hm := rotationWord_mass n initial
98   have hs := rotationWord_spatial n initial
99   change (wordAction operator (rotationWord n) initial) 0 = 1 at hm
100   rw [hm,hs]
101   have hi : spatial initial = (1 : ℂ) := rfl
102   rw [hi,mul_one]
103 
104 /-- Every all-test nonnegative state satisfies all rotated probe effects. -/
105 theorem allTests_rotated_probe_bound {z : RotationModel.State}
106     (hz : z ∈ TestDomains.allTests operator RotationModel.mass) (n : ℕ) :
107     (((rotation^n : Circle) : ℂ) * spatial z).re ≤ z 0 := by
108   have hp := hz (rotationWord n ++ [(true,true)])
109   change 0 ≤ RotationModel.mass (wordAction operator (rotationWord n ++ [(true,true)]) z) at hp
110   simp only [wordAction_append,LinearMap.comp_apply,wordAction_cons,wordAction_nil,
111     LinearMap.id_comp,operator_probe1] at hp
112   rw [probe1_apply,map_smul,initial_mass,smul_eq_mul,mul_one] at hp
113   have hm := rotationWord_mass n z
114   change (wordAction operator (rotationWord n) z) 0 = z 0 at hm
115   have hs := congrArg Complex.re (rotationWord_spatial n z)
116   simp only [LorentzBaseNorm.spatial_apply_re] at hs
117   rw [← hs]
118   linarith
119 
120 /-- The exact model's canonical all-future-test cone is the Lorentz cone. -/
121 theorem canonical_cone_eq : TestDomains.allTests operator RotationModel.mass = RotationModel.cone := by
122   apply Set.Subset.antisymm
123   · intro z hz
124     apply (LorentzBaseNorm.cone_iff_norm z).mpr
125     exact norm_le_of_rotated_re_le (spatial z) (z 0) (allTests_rotated_probe_bound hz)
126   · intro z hz w
127     exact all_word_mass_nonneg w hz
128 
129 /-- A fixed unit-mass slice is affine in its complex spatial coordinate. -/
130 theorem point_one_convex {C : Set RotationModel.State} (hc : Convex ℝ C) :
131     Convex ℝ {w : ℂ | point 1 w ∈ C} := by
132   intro w hw v hv a b ha hb hab
133   change point 1 (a • w + b • v) ∈ C
134   have he : point 1 (a • w + b • v) = a • point 1 w + b • point 1 v := by
135     funext i
136     fin_cases i <;> simp [LorentzBaseNorm.point,smul_eq_mul,hab]
137   rw [he]
138   exact hc hw hv ha hb hab
139 
140 /-- Closedness extends actual reachable forward powers to every boundary point. -/
141 theorem unit_boundary_mem {C : Set RotationModel.State}
142     (hclosed : IsClosed C) (hinit : initial ∈ C)
143     (hinv : ∀ z ∈ C, rotate z ∈ C) (u : Circle) : point 1 (u : ℂ) ∈ C := by
144   have horbit : ∀ n, point 1 ((rotation^n : Circle) : ℂ) ∈ C := by
145     intro n
146     rw [← rotationWord_initial]
147     induction n with
148     | zero => simpa [rotationWord] using hinit
149     | succ n ih =>
150       rw [show rotationWord (n+1)=rotationWord n ++ [(false,false)] by
151         exact List.replicate_succ']
152       simpa only [wordAction_append,wordAction_cons,wordAction_nil,LinearMap.id_comp,
153         LinearMap.comp_apply,operator_rotate0] using hinv _ ih
154   have hcont : Continuous (fun u : Circle => point 1 (u : ℂ)) := by
155     apply continuous_pi
156     intro i
157     fin_cases i
158     · change Continuous (fun _ : Circle => (1 : ℝ)); fun_prop
159     · change Continuous (fun u : Circle => (u : ℂ).re); fun_prop
160     · change Continuous (fun u : Circle => (u : ℂ).im); fun_prop
161   exact rotation_forward_dense.induction_on (p := fun u : Circle => point 1 (u : ℂ) ∈ C)
162     u (hclosed.preimage hcont) horbit
163 
164 /-- Convexity fills the disk once its entire reachable boundary is present. -/
165 theorem unit_disk_mem {C : Set RotationModel.State}
166     (hclosed : IsClosed C) (hconvex : Convex ℝ C) (hinit : initial ∈ C)
167     (hinv : ∀ z ∈ C, rotate z ∈ C) (w : ℂ) (hw : ‖w‖ ≤ 1) : point 1 w ∈ C := by
168   have hb : sphere (0 : ℂ) 1 ⊆ {w : ℂ | point 1 w ∈ C} := by
169     intro v hv
170     exact unit_boundary_mem hclosed hinit hinv ⟨v,hv⟩
171   have hh := convexHull_min hb (point_one_convex hconvex)
172   rw [convexHull_sphere_eq_closedBall (0 : ℂ) (by norm_num : (0 : ℝ) ≤ 1)] at hh
173   exact hh (by simpa only [mem_closedBall,dist_zero_right] using hw)
174 
175 /-- A closed convex conical set containing the exact rotation orbit contains
176 all Lorentz-positive states, including its zero-mass boundary. -/
177 theorem lorentz_subset_of_closed_invariant {C : Set RotationModel.State}
178     (hclosed : IsClosed C) (hconvex : Convex ℝ C)
179     (hscale : ∀ a : ℝ, 0 ≤ a → ∀ z ∈ C, a • z ∈ C)
180     (hinit : initial ∈ C) (hinv : ∀ z ∈ C, rotate z ∈ C) : RotationModel.cone ⊆ C := by
181   intro z hz
182   have hn := (LorentzBaseNorm.cone_iff_norm z).mp hz
183   have ht : 0 ≤ z 0 := (norm_nonneg (spatial z)).trans hn
184   by_cases hzero : z 0 = 0
185   · have hs : spatial z = 0 := norm_eq_zero.mp (le_antisymm (by simpa [hzero] using hn) (norm_nonneg _))
186     have he : z = 0 := LorentzBaseNorm.spatial_eq_zero_and_mass_eq_zero hs hzero
187     rw [he]
188     simpa using hscale 0 (by norm_num) initial hinit
189   · have htpos : 0 < z 0 := lt_of_le_of_ne ht (Ne.symm hzero)
190     have hw : ‖spatial z / (z 0 : ℂ)‖ ≤ 1 := by
191       rw [norm_div,Complex.norm_real,Real.norm_eq_abs,abs_of_pos htpos]
192       exact (div_le_one htpos).mpr hn
193     have hm := hscale (z 0) ht (point 1 (spatial z / (z 0 : ℂ)))
194       (unit_disk_mem hclosed hconvex hinit hinv _ hw)
195     have he : (z 0) • point 1 (spatial z / (z 0 : ℂ)) = z := by
196       rw [← LorentzBaseNorm.point_mass_spatial z]
197       funext i
198       fin_cases i <;> simp [LorentzBaseNorm.point,Pi.smul_apply,smul_eq_mul]
199       all_goals field_simp [hzero]
200     simpa only [he] using hm
201 
202 /-- Nonnegative mass on every invariant branch forces the reverse inclusion.
203 Together with reachability and closure the probability cone is unique. -/
204 theorem invariant_probability_cone_unique {C : Set RotationModel.State}
205     (hclosed : IsClosed C) (hconvex : Convex ℝ C)
206     (hscale : ∀ a : ℝ, 0 ≤ a → ∀ z ∈ C, a • z ∈ C)
207     (hinit : initial ∈ C) (hmass : ∀ z ∈ C, 0 ≤ RotationModel.mass z)
208     (hinv : ∀ s z, z ∈ C → operator s z ∈ C) : C = RotationModel.cone := by
209   apply Set.Subset.antisymm
210   · rw [← canonical_cone_eq]
211     exact TestDomains.allTests_greatest operator RotationModel.mass C hmass hinv
212   · exact lorentz_subset_of_closed_invariant hclosed hconvex hscale hinit
213       (fun z hz => by simpa only [operator_rotate0] using hinv (false,false) z hz)
214 
215 /-- The normalized base of any such finite synthesis would project to the disk. -/
216 theorem spatial_normalizedHull_eq_disk {J : Type*} [Fintype J] [DecidableEq J]
217     (V : (J → ℝ) →ₗ[ℝ] RotationModel.State)
218     (he : PositiveLift.hull V = RotationModel.cone) :
219     spatial '' PositiveLift.normalizedHull V RotationModel.mass = closedBall 0 1 := by
220   ext w
221   constructor
222   · rintro ⟨z,⟨hz,hm⟩,rfl⟩
223     rw [he] at hz
224     have hb := (LorentzBaseNorm.cone_iff_norm z).mp hz
225     change z 0 = 1 at hm
226     simpa only [mem_closedBall,dist_zero_right,hm] using hb
227   · intro hw
228     refine ⟨point 1 w,⟨?_,?_⟩,by simp⟩
229     · rw [he]
230       apply (LorentzBaseNorm.cone_iff_norm _).mpr
231       simpa only [LorentzBaseNorm.spatial_point,LorentzBaseNorm.point_zero,
232         mem_closedBall,dist_zero_right] using hw
233     · simp
234 
235 /-- No finite normalized positive-generator certificate exists for the exact
236 rational model. Redundant generators are covered as well. -/
237 theorem no_finite_normalized_generator_certificate {J : Type*} [Fintype J] [DecidableEq J]
238     (V : (J → ℝ) →ₗ[ℝ] RotationModel.State)
239     (hn : RotationModel.mass.comp V = FiniteInstruments.mass)
240     (hinit : initial ∈ PositiveLift.hull V)
241     (hinv : ∀ s z, z ∈ PositiveLift.hull V → operator s z ∈ PositiveLift.hull V) : False := by
242   have he := invariant_probability_cone_unique
243     (PositiveLift.hull_closed V RotationModel.mass hn) (PositiveLift.hull_convex V)
244     (fun a ha z hz => PositiveLift.hull_smul V ha hz) hinit
245     (fun z hz => PositiveLift.hull_mass_nonneg V RotationModel.mass hn hz) hinv
246   have hb := spatial_normalizedHull_eq_disk V he
247   rw [PositiveLift.normalizedHull_eq_convexHull V RotationModel.mass hn,
248     spatial.image_convexHull] at hb
249   let s : Finset ℂ := Finset.univ.image (fun j => spatial (PositiveLift.generator V j))
250   have hs : (s : Set ℂ) = spatial '' Set.range (PositiveLift.generator V) := by
251     ext w
252     simp [s]
253   exact disk_not_finite_convex_hull s (by rw [hs]; exact hb)
254 
255 /-- Collected P46 conclusions for the actual rational process. The finite
256 certificate obstruction allows every finite generator type and redundant maps. -/
257 theorem rational_rank_three_obstruction {J : Type*} [Fintype J] [DecidableEq J] :
258     (∀ s, ∃ M : Matrix (Fin 3) (Fin 3) ℚ, M.map (algebraMap ℚ ℝ) = RotationModel.matrix s) ∧
259     Behavior.CausalLaw process ∧
260     TestDomains.allTests operator RotationModel.mass = RotationModel.cone ∧
261     Module.finrank ℝ (Behavior.space process) = 3 ∧
262     (∀ C : Set RotationModel.State, IsClosed C → Convex ℝ C →
263       (∀ a : ℝ, 0 ≤ a → ∀ z ∈ C, a • z ∈ C) → initial ∈ C →
264       (∀ z ∈ C, 0 ≤ RotationModel.mass z) →
265       (∀ s z, z ∈ C → operator s z ∈ C) → C = RotationModel.cone) ∧
266     ¬ ∃ V : (J → ℝ) →ₗ[ℝ] RotationModel.State,
267       RotationModel.mass.comp V = FiniteInstruments.mass ∧
268       initial ∈ PositiveLift.hull V ∧
269       ∀ s z, z ∈ PositiveLift.hull V → operator s z ∈ PositiveLift.hull V := by
270   refine ⟨matrix_is_rational, process_causal, canonical_cone_eq,
271     behavior_dimension_three, ?_, ?_⟩
272   · intro C hc hv hs hi hm hb
273     exact invariant_probability_cone_unique hc hv hs hi hm hb
274   · rintro ⟨V,hn,hi,hb⟩
275     exact no_finite_normalized_generator_certificate V hn hi hb
276 
277 end Komorebi.LSM.RotationConeGeometry

Back to source controls