LorentzBoundaryFragility.lean

1 import KomorebiLSM.LorentzCylinder
2 
3 /-! P72: a literal rank-one spatial perturbation of exactly prescribed
4 normalized base-norm size breaks every boundary image in positive dimension. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.LorentzBoundaryFragility
7 open LorentzCylinder
8 variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
9 
10 abbrev UnitSpatial (V : Type*) [NormedAddCommGroup V] := {v : V // ‖v‖≤1}
11 instance : Inhabited (UnitSpatial V) := ⟨⟨0,by simp⟩⟩
12 
13 /-- The supremum is over the literal normalized Lorentz base and actual cone infimum. -/
14 noncomputable def normalizedSize (Delta : State V →L[ℝ] State V) : ℝ :=
15   sSup (Set.range (fun v : UnitSpatial V => probabilityCone.value (Delta (1,v.1))))
16 
17 /-- The actual mass-row-zero outer product epsilon (0,e) lambda. -/
18 noncomputable def outwardPerturbation (epsilon : ℝ) (e : V) : State V →L[ℝ] State V :=
19   (ContinuousLinearMap.fst ℝ ℝ V).smulRight (0,epsilon • e)
20 
21 @[simp] theorem outwardPerturbation_apply (epsilon : ℝ) (e : V) (z : State V) :
22     outwardPerturbation epsilon e z=z.1 • (0,epsilon • e) := rfl
23 
24 @[simp] theorem outwardPerturbation_normalized (epsilon : ℝ) (e v : V) :
25     outwardPerturbation epsilon e (1,v)=(0,epsilon • e) := by
26   rw [outwardPerturbation_apply,one_smul]
27 
28 theorem outwardPerturbation_mass (epsilon : ℝ) (e : V) :
29     (ContinuousLinearMap.fst ℝ ℝ V).comp (outwardPerturbation epsilon e)=0 := by
30   apply ContinuousLinearMap.ext
31   intro z
32   change (outwardPerturbation epsilon e z).1=0
33   simp [outwardPerturbation_apply]
34 
35 /-- Its range is exactly the one-dimensional spatial line it adds. -/
36 theorem outwardPerturbation_range (epsilon : ℝ) (e : V) :
37     LinearMap.range (outwardPerturbation epsilon e).toLinearMap=
38       Submodule.span ℝ {(0,epsilon • e)} := by
39   apply le_antisymm
40   · rintro y ⟨z,rfl⟩
41     exact Submodule.smul_mem _ z.1 (Submodule.subset_span (Set.mem_singleton _))
42   · apply Submodule.span_le.mpr
43     intro y hy
44     rw [Set.mem_singleton_iff] at hy
45     subst y
46     exact ⟨(1,0),by simp⟩
47 
48 theorem outwardPerturbation_rank_one (epsilon : ℝ) (hepsilon : 0<epsilon)
49     (e : V) (he : ‖e‖=1) :
50     Module.finrank ℝ (LinearMap.range (outwardPerturbation epsilon e).toLinearMap)=1 := by
51   rw [outwardPerturbation_range]
52   apply finrank_span_singleton
53   intro h
54   have hz : epsilon • e=0 := congrArg Prod.snd h
55   have hn : ‖epsilon • e‖=epsilon := by
56     rw [norm_smul,Real.norm_eq_abs,abs_of_pos hepsilon,he,mul_one]
57   rw [hz,norm_zero] at hn
58   linarith
59 
60 /-- All normalized inputs receive the same spatial vector, so the supremum is exact. -/
61 theorem outwardPerturbation_size (epsilon : ℝ) (hepsilon : 0≤epsilon)
62     (e : V) (he : ‖e‖=1) : normalizedSize (outwardPerturbation epsilon e)=epsilon := by
63   have hvalue : ∀ v : UnitSpatial V,
64       probabilityCone.value (outwardPerturbation epsilon e (1,v.1))=epsilon := by
65     intro v
66     rw [outwardPerturbation_normalized,value_zero_mass,norm_smul,Real.norm_eq_abs,
67       abs_of_nonneg hepsilon,he,mul_one]
68   simp only [normalizedSize,hvalue,Set.range_const,csSup_singleton]
69 
70 /-- A unit outward ray exists also when the current boundary image is zero. -/
71 theorem exists_aligned_unit [Nontrivial V] (w : V) :
72     ∃ e : V,‖e‖=1 ∧ ∀ t : ℝ,0≤t → ‖w+t • e‖=‖w‖+t := by
73   by_cases hw : w=0
74   · obtain ⟨x,hx⟩ := exists_ne (0 : V)
75     have hxp : 0<‖x‖ := norm_pos_iff.mpr hx
76     let e : V := ‖x‖⁻¹ • x
77     have he : ‖e‖=1 := by
78       rw [norm_smul,Real.norm_eq_abs,abs_of_pos (inv_pos.mpr hxp),inv_mul_cancel₀ hxp.ne']
79     refine ⟨e,he,?_⟩
80     intro t ht
81     rw [hw,zero_add,norm_zero,norm_smul,Real.norm_eq_abs,abs_of_nonneg ht,he,mul_one,zero_add]
82   · have hwp : 0<‖w‖ := norm_pos_iff.mpr hw
83     let e : V := ‖w‖⁻¹ • w
84     have he : ‖e‖=1 := by
85       rw [norm_smul,Real.norm_eq_abs,abs_of_pos (inv_pos.mpr hwp),inv_mul_cancel₀ hwp.ne']
86     have hwrep : w=‖w‖ • e := by
87       change w=‖w‖ • (‖w‖⁻¹ • w)
88       rw [smul_smul,mul_inv_cancel₀ hwp.ne',one_smul]
89     refine ⟨e,he,?_⟩
90     intro t ht
91     calc
92       ‖w+t • e‖=‖(‖w‖+t) • e‖ := by conv_lhs => rw [hwrep,← add_smul]
93       _=‖w‖+t := by rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg (by positivity),he,mul_one]
94 
95 /-- The exact P72 obstruction, including nonzero and zero boundary images. -/
96 theorem boundary_fragility [Nontrivial V] (F : State V →L[ℝ] State V)
97     (_hF : ∀ z∈cone,F z∈cone) (v : V) (_hv : ‖v‖≤1)
98     (hboundary : (F (1,v)).1=‖(F (1,v)).2‖) (epsilon : ℝ) (hepsilon : 0<epsilon) :
99     ∃ Delta : State V →L[ℝ] State V,
100       (ContinuousLinearMap.fst ℝ ℝ V).comp Delta=0 ∧
101       Module.finrank ℝ (LinearMap.range Delta.toLinearMap)=1 ∧
102       normalizedSize Delta=epsilon ∧ (F+Delta) (1,v)∉cone := by
103   obtain ⟨e,he,halign⟩ := exists_aligned_unit (F (1,v)).2
104   refine ⟨outwardPerturbation epsilon e,outwardPerturbation_mass epsilon e,
105     outwardPerturbation_rank_one epsilon hepsilon e he,outwardPerturbation_size epsilon hepsilon.le e he,?_⟩
106   intro hcone
107   simp only [mem_cone,add_apply,outwardPerturbation_normalized,Prod.fst_add,Prod.snd_add,add_zero] at hcone
108   rw [halign epsilon hepsilon.le,← hboundary] at hcone
109   linarith
110 
111 /-- In zero spatial dimension, a zero mass row forces the entire perturbation to vanish. -/
112 theorem mass_row_zero_of_subsingleton [Subsingleton V] (Delta : State V →L[ℝ] State V)
113     (hm : (ContinuousLinearMap.fst ℝ ℝ V).comp Delta=0) : Delta=0 := by
114   apply ContinuousLinearMap.ext
115   intro z
116   apply Prod.ext
117   · exact congrArg (fun L : State V →L[ℝ] ℝ => L z) hm
118   · exact Subsingleton.elim _ _
119 
120 theorem zero_dimensional_impossibility [Subsingleton V] (epsilon : ℝ) (hepsilon : 0<epsilon) :
121     ¬∃ Delta : State V →L[ℝ] State V,
122       (ContinuousLinearMap.fst ℝ ℝ V).comp Delta=0 ∧ normalizedSize Delta=epsilon := by
123   rintro ⟨Delta,hm,hsize⟩
124   rw [mass_row_zero_of_subsingleton Delta hm] at hsize
125   have hzero : normalizedSize (0 : State V →L[ℝ] State V)=0 := by
126     simp [normalizedSize,probabilityCone.value_zero]
127   rw [hzero] at hsize
128   linarith
129 
130 /-- The source's d≥1 case is the actual finite Euclidean spatial space. -/
131 theorem euclidean_boundary_fragility {D : Type*} [Fintype D] [Nonempty D]
132     (F : State (EuclideanSpace ℝ D) →L[ℝ] State (EuclideanSpace ℝ D))
133     (hF : ∀ z∈cone,F z∈cone) (v : EuclideanSpace ℝ D) (hv : ‖v‖≤1)
134     (hboundary : (F (1,v)).1=‖(F (1,v)).2‖) (epsilon : ℝ) (hepsilon : 0<epsilon) :
135     ∃ Delta : State (EuclideanSpace ℝ D) →L[ℝ] State (EuclideanSpace ℝ D),
136       (ContinuousLinearMap.fst ℝ ℝ (EuclideanSpace ℝ D)).comp Delta=0 ∧
137       Module.finrank ℝ (LinearMap.range Delta.toLinearMap)=1 ∧
138       normalizedSize Delta=epsilon ∧ (F+Delta) (1,v)∉cone :=
139   boundary_fragility F hF v hv hboundary epsilon hepsilon
140 
141 end Komorebi.LSM.LorentzBoundaryFragility

Back to source controls