HolonomyExamples.lean

1 import KomorebiSpace.HolonomyViews
2 import Mathlib.Tactic.FinCases
3 
4 set_option autoImplicit false
5 
6 /-!
7 # A nontrivial reflection loop with a nonzero exact core
8 
9 Three views, sup-norm plane values. Two overlaps are identity and the third
10 reflects the second coordinate. Parallel data are precisely constant horizontal
11 vectors. The explicitly constructed repair has sharp residual gain 3/2.
12 -/
13 noncomputable section
14 namespace KomorebiSpace
15 namespace HolonomyTransport
16 namespace ReflectionTriangle
17 
18 abbrev Plane := ℝ × ℝ
19 
20 def reflection : Plane ≃ₗᵢ[ℝ] Plane where
21   toFun z := (z.1,-z.2)
22   invFun z := (z.1,-z.2)
23   left_inv := by intro z; simp
24   right_inv := by intro z; simp
25   map_add' := by
26     intro z w
27     apply Prod.ext
28     · rfl
29     · change -(z.2+w.2) = -z.2 + -w.2
30       abel
31   map_smul' := by intro c z; simp
32   norm_map' := by
33     intro z
34     change ‖(z.1,-z.2)‖=‖z‖
35     simp only [Prod.norm_def, norm_neg]
36 
37 def twisted (i j : Fin 3) : Prop := (i=0 ∧ j=2) ∨ (i=2 ∧ j=0)
38 
39 instance (i j : Fin 3) : Decidable (twisted i j) := by unfold twisted; infer_instance
40 
41 def edgeTransport (i j : Fin 3) : Plane ≃ₗᵢ[ℝ] Plane :=
42   if twisted i j then reflection else LinearIsometryEquiv.refl ℝ Plane
43 
44 def connection : Connection (Fin 3) Plane where
45   transport := edgeTransport
46   self_apply := by intro i z; fin_cases i <;> rfl
47   reverse_apply := by intro i j z; fin_cases i <;> fin_cases j <;> simp [edgeTransport, twisted, reflection, Fin.ext_iff]
48 
49 abbrev graph : SimpleGraph (Fin 3) := ⊤
50 
51 def routing : OverlapTransport.Routing graph (0 : Fin 3) where
52   path i := by
53     by_cases h : (0 : Fin 3)=i
54     · subst i; exact .nil
55     · exact (show graph.Adj 0 i from h).toWalk
56   at_anchor := rfl
57 
58 def loop : graph.Walk (0 : Fin 3) 0 :=
59   .cons (by decide : graph.Adj 0 1)
60     (.cons (by decide : graph.Adj 1 2) (.cons (by decide : graph.Adj 2 0) .nil))
61 
62 @[simp] theorem loop_transport (z : Plane) : connection.walkTransport loop z = reflection z := rfl
63 
64 theorem loop_nontrivial : connection.walkTransport loop (0,1) ≠ (0,1) := by
65   intro he
66   have h := congrArg Prod.snd he
67   norm_num [loop_transport, reflection] at h
68 
69 @[simp] theorem edgeTransport_fst (i j : Fin 3) (z : Plane) :
70     (connection.transport i j z).1 = z.1 := by
71   change ((if twisted i j then reflection else LinearIsometryEquiv.refl ℝ Plane) z).1 = _
72   split <;> rfl
73 
74 @[simp] theorem edgeTransport_horizontal (i j : Fin 3) (a : ℝ) :
75     connection.transport i j (a,0) = (a,0) := by
76   change (if twisted i j then reflection else LinearIsometryEquiv.refl ℝ Plane) (a,0) = _
77   split <;> simp [reflection]
78 
79 theorem parallel_iff (x : Fin 3 → Plane) :
80     connection.Parallel graph x ↔ ∃ a : ℝ, ∀ i, x i = (a,0) := by
81   constructor
82   · intro hx
83     have h10 : x 1 = x 0 := hx 0 1 (by decide)
84     have h21 : x 2 = x 1 := hx 1 2 (by decide)
85     have h20 := h21.trans h10
86     have hr := hx 0 2 (by decide)
87     have hv : (x 0).2 = 0 := by
88       have he := congrArg Prod.snd hr
89       change -(x 2).2 = (x 0).2 at he
90       rw [h20] at he
91       linarith
92     refine ⟨(x 0).1, ?_⟩
93     intro i
94     have hz : x 0 = ((x 0).1,0) := Prod.ext rfl hv
95     fin_cases i
96     · exact hz
97     · exact h10.trans hz
98     · exact h20.trans hz
99   · rintro ⟨a,ha⟩
100     intro i j _hij
101     rw [ha i, ha j, edgeTransport_horizontal]
102 
103 theorem fixedSpace_iff (z : Plane) :
104     z ∈ Rooted.fixedSpace connection routing ↔ z.2=0 := by
105   rw [← Rooted.anchor_extendable_iff]
106   constructor
107   · rintro ⟨x,hx,he⟩
108     obtain ⟨a,ha⟩ := (parallel_iff x).mp hx
109     rw [← he, ha 0]
110   · intro hz
111     refine ⟨fun _ => z, (parallel_iff _).mpr ?_, rfl⟩
112     exact ⟨z.1, fun _ => Prod.ext rfl hz⟩
113 
114 theorem nonzero_exact_section :
115     connection.Parallel graph (fun _ => (7,0)) ∧
116       (fun _ : Fin 3 => ((7,0) : Plane)) ≠ 0 := by
117   constructor
118   · exact (parallel_iff _).mpr ⟨7,fun _ => rfl⟩
119   · intro h; have he := congrArg (fun x : Fin 3 → Plane => (x 0).1) h; norm_num at he
120 
121 theorem inadmissible_anchor :
122     ¬ ∃ x : Fin 3 → Plane, connection.Parallel graph x ∧ x 0=(7,1) := by
123   intro h
124   have hf := (Rooted.anchor_extendable_iff connection routing (7,1)).mp h
125   have he := (fixedSpace_iff (7,1)).mp hf
126   norm_num at he
127 
128 /-- Preserve the compatible horizontal coordinate, not an impossible full anchor. -/
129 def repair (x : Fin 3 → Plane) (_i : Fin 3) : Plane := ((x 0).1,0)
130 
131 theorem repair_parallel (x : Fin 3 → Plane) : connection.Parallel graph (repair x) :=
132   (parallel_iff _).mpr ⟨(x 0).1, fun _ => rfl⟩
133 
134 @[simp] theorem repair_protected (x : Fin 3 → Plane) : (repair x 0).1=(x 0).1 := rfl
135 
136 @[simp] theorem repair_idempotent (x : Fin 3 → Plane) : repair (repair x)=repair x := rfl
137 
138 theorem repair_unique (x : Fin 3 → Plane) :
139     ∃! y : Fin 3 → Plane, connection.Parallel graph y ∧ (y 0).1=(x 0).1 := by
140   refine ⟨repair x, ⟨repair_parallel x,rfl⟩, ?_⟩
141   intro y hy
142   obtain ⟨a,ha⟩ := (parallel_iff y).mp hy.1
143   have he : a=(x 0).1 := by simpa only [ha 0] using hy.2
144   funext i
145   rw [ha i,he]
146   rfl
147 
148 /-- Three signed differences force a 3/2 bound on every vertical value. -/
149 theorem vertical_estimate (a b c ε : ℝ)
150     (h01 : |b-a| ≤ ε) (h02 : |-c-a| ≤ ε) (h12 : |c-b| ≤ ε) :
151     |a| ≤ (3/2:ℝ)*ε ∧ |b| ≤ (3/2:ℝ)*ε ∧ |c| ≤ (3/2:ℝ)*ε := by
152   obtain ⟨ha1,ha2⟩ := abs_le.mp h01
153   obtain ⟨hb1,hb2⟩ := abs_le.mp h02
154   obtain ⟨hc1,hc2⟩ := abs_le.mp h12
155   constructor
156   · apply abs_le.mpr; constructor <;> linarith
157   · constructor <;> apply abs_le.mpr <;> constructor <;> linarith
158 
159 theorem edge_coordinate_bounds (x : Fin 3 → Plane) (i j : Fin 3) (h : graph.Adj i j) :
160     |(connection.defect x i j).1| ≤ ‖connection.differential graph x‖ ∧
161     |(connection.defect x i j).2| ≤ ‖connection.differential graph x‖ := by
162   have he : ‖connection.defect x i j‖ ≤ ‖connection.differential graph x‖ :=
163     norm_le_pi_norm (connection.differential graph x) ⟨(i,j),h⟩
164   exact ⟨(norm_fst_le _).trans he, (norm_snd_le _).trans he⟩
165 
166 theorem repair_error (x : Fin 3 → Plane) :
167     ‖x-repair x‖ ≤ (3/2:ℝ) * ‖connection.differential graph x‖ := by
168   let ε := ‖connection.differential graph x‖
169   have hε : 0 ≤ ε := norm_nonneg _
170   have h01 := edge_coordinate_bounds x 0 1 (by decide)
171   have h02 := edge_coordinate_bounds x 0 2 (by decide)
172   have h12 := edge_coordinate_bounds x 1 2 (by decide)
173   have hv := vertical_estimate (x 0).2 (x 1).2 (x 2).2 ε h01.2 h02.2 h12.2
174   apply (pi_norm_le_iff_of_nonneg (mul_nonneg (by norm_num) hε)).mpr
175   intro i
176   change max |(x i).1-(x 0).1| |(x i).2-0| ≤ (3/2:ℝ)*ε
177   rw [sub_zero]
178   apply max_le
179   · fin_cases i
180     · simp; positivity
181     · exact h01.1.trans (by linarith)
182     · exact h02.1.trans (by linarith)
183   · fin_cases i
184     · exact hv.1
185     · exact hv.2.1
186     · exact hv.2.2
187 
188 /-- A nonzero horizontal signal and an input attaining the full repair gain. -/
189 def sharpData : Fin 3 → Plane := ![(7,3/2),(7,1/2),(7,-1/2)]
190 
191 theorem sharp_residual_norm : ‖connection.differential graph sharpData‖=1 := by
192   apply le_antisymm
193   · apply (pi_norm_le_iff_of_nonneg zero_le_one).mpr
194     intro a
195     rcases a with ⟨⟨i,j⟩,h⟩
196     fin_cases i <;> fin_cases j <;>
197       norm_num [Connection.differential_apply, Connection.defect, connection,
198         edgeTransport, twisted, reflection, sharpData, Prod.norm_def, Fin.ext_iff] at *
199   · have he := norm_le_pi_norm (connection.differential graph sharpData)
200       (⟨(0,1),by decide⟩ : OverlapTransport.Edges graph)
201     norm_num [Connection.differential_apply, Connection.defect, connection,
202       edgeTransport, twisted, sharpData, Prod.norm_def, Fin.ext_iff] at he ⊢
203     exact he
204 
205 theorem sharp_error : ‖sharpData-repair sharpData‖=(3/2:ℝ) := by
206   apply le_antisymm
207   · simpa only [sharp_residual_norm, mul_one] using repair_error sharpData
208   · have he := norm_le_pi_norm (sharpData-repair sharpData) 0
209     norm_num [sharpData, repair, Prod.norm_def] at he ⊢
210     exact he
211 
212 theorem repair_bound_sharp :
213     (∀ x : Fin 3 → Plane, ‖x-repair x‖ ≤ (3/2:ℝ)*‖connection.differential graph x‖) ∧
214     ‖sharpData-repair sharpData‖=(3/2:ℝ)*‖connection.differential graph sharpData‖ := by
215   exact ⟨repair_error, by rw [sharp_error,sharp_residual_norm,mul_one]⟩
216 
217 end ReflectionTriangle
218 end HolonomyTransport
219 end KomorebiSpace
220 end

Back to source controls