IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit
IndisputableMonolith/Gravity/SevenGaps/WickActionCutLimit.lean · 516 lines · 33 declarations
show as:
view math explainer →
1import Mathlib.Analysis.SpecialFunctions.Arcosh
2import Mathlib.Analysis.SpecialFunctions.Complex.Arg
3import Mathlib.Analysis.SpecialFunctions.Complex.Log
4import Mathlib.Analysis.SpecialFunctions.Pow.Complex
5import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
6import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
7import Mathlib.Tactic.Linarith
8import Mathlib.Tactic.NormNum
9import Mathlib.Tactic.Ring
10import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
11import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement
12import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
13
14/-!
15# Wave C4 N4: `carccos` cut-boundary limit (6-lemma route)
16
17Binding design: `D-gap6-n4-cut-limit-design-20260723`.
18
19Lands `carccos_tendsto_at_cut_one` and `lorentzAnchor_one` via L1–L6.
20Does **not** inhabit the gap6 terminal or flip ledger Bools.
21Family Prop left open in this session.
22-/
23
24namespace IndisputableMonolith
25namespace Gravity
26namespace SevenGaps
27namespace WickActionInteriorHinge
28
29open Complex
30open Filter Topology
31open WickActionComplexFirst
32open WickFourOneAllHinges (csqrt_ofReal_nonneg)
33
34noncomputable section
35
36/-! ## L1. Lower-half `csqrt` reflection -/
37
38theorem csqrt_of_im_neg {s : ℂ} (him : s.im < 0) :
39 csqrt s = -I * csqrt (-s) := by
40 have hs0 : s ≠ 0 := fun h => by
41 have : (0 : ℝ) < 0 := by simpa [h] using him
42 exact (lt_irrefl (0 : ℝ)) this
43 have hns0 : (-s) ≠ 0 := neg_ne_zero.mpr hs0
44 have hlog : log s = log (-s) - (Real.pi : ℂ) * I := by
45 apply Complex.ext
46 · simp [log_re, norm_neg]
47 · have harg : arg (-s) = arg s + Real.pi :=
48 arg_neg_eq_arg_add_pi_of_im_neg him
49 simp only [log_im, sub_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
50 linarith [harg]
51 unfold csqrt
52 rw [cpow_def_of_ne_zero hs0, cpow_def_of_ne_zero hns0, hlog]
53 have hmul :
54 (log (-s) - (Real.pi : ℂ) * I) * (1 / 2 : ℂ) =
55 log (-s) * (1 / 2 : ℂ) + (-(Real.pi : ℂ) / 2 * I) := by
56 ring
57 have hexp : exp (-(Real.pi : ℂ) / 2 * I) = -I := by
58 simpa [ofReal_div, ofReal_neg, ofReal_ofNat] using
59 (exp_neg_pi_div_two_mul_I : exp (-Real.pi / 2 * I) = -I)
60 rw [hmul, exp_add, hexp]
61 ring
62
63/-! ## L2. Path cosine → `-11/8` -/
64
65theorem tendsto_pentHingeCosPath_one :
66 Tendsto (fun t => pentHingeCosPath 1 t) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
67 (nhds ((-(11 / 8 : ℝ) : ℂ))) := by
68 have hz :
69 Tendsto zArc (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (zArc 0)) :=
70 (continuous_zArc.tendsto 0).mono_left nhdsWithin_le_nhds
71 have hz0 : zArc 0 = ((-1 : ℝ) : ℂ) := by
72 simp [zArc, arcZ_zero]
73 have hnum :
74 Tendsto (fun t => (5 : ℂ) - 6 * zArc t) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
75 (nhds ((11 : ℂ))) := by
76 have :
77 Tendsto (fun t => (5 : ℂ) - 6 * zArc t) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
78 (nhds ((5 : ℂ) - 6 * zArc 0)) :=
79 tendsto_const_nhds.sub (tendsto_const_nhds.mul hz)
80 convert this using 1
81 norm_num [hz0]
82 have hden :
83 Tendsto (fun t => (6 : ℂ) * zArc t - 2) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
84 (nhds ((-8 : ℂ))) := by
85 have :
86 Tendsto (fun t => (6 : ℂ) * zArc t - 2) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
87 (nhds ((6 : ℂ) * zArc 0 - 2)) :=
88 (tendsto_const_nhds.mul hz).sub tendsto_const_nhds
89 convert this using 1
90 norm_num [hz0]
91 have hden0 : ((-8 : ℂ) : ℂ) ≠ 0 := by norm_num
92 have hdiv :
93 Tendsto (fun t => ((5 : ℂ) - 6 * zArc t) / (6 * zArc t - 2))
94 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
95 (nhds (((11 : ℂ) / (-8 : ℂ)))) :=
96 hnum.div hden hden0
97 have hval : ((11 : ℂ) / (-8 : ℂ)) = ((-(11 / 8 : ℝ) : ℂ)) := by
98 norm_num
99 have hpath :
100 (fun t => pentHingeCosPath 1 t) =
101 fun t => ((5 : ℂ) - 6 * zArc t) / (6 * zArc t - 2) := by
102 funext t
103 exact pentHingeCosPath_eq_moebius_one t
104 simpa [hpath, hval] using hdiv
105
106/-! ## L3. `csqrt(w^2 - 1)` → `√57 / 8` -/
107
108private lemma sq_sub_one_limit :
109 ((11 / 8 : ℂ) ^ 2 - 1) = (57 / 64 : ℂ) := by
110 norm_num
111
112private lemma fiftySevenOver64_mem_slitPlane :
113 (57 / 64 : ℂ) ∈ slitPlane := by
114 have : ((57 / 64 : ℝ) : ℂ) ∈ slitPlane :=
115 ofReal_mem_slitPlane.mpr (by norm_num : (0 : ℝ) < 57 / 64)
116 simpa using this
117
118private lemma sqrt_fiftySeven_div_eight :
119 Real.sqrt (57 / 64) = Real.sqrt 57 / 8 := by
120 have h64 : Real.sqrt (64 : ℝ) = 8 := by
121 have : (64 : ℝ) = 8 ^ 2 := by norm_num
122 rw [this, Real.sqrt_sq (by norm_num)]
123 calc
124 Real.sqrt (57 / 64) = Real.sqrt 57 / Real.sqrt 64 :=
125 Real.sqrt_div (by norm_num : (0 : ℝ) ≤ 57) 64
126 _ = Real.sqrt 57 / 8 := by rw [h64]
127
128theorem tendsto_csqrt_sq_sub_one_one :
129 Tendsto (fun t => csqrt (pentHingeCosPath 1 t ^ 2 - 1))
130 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
131 (nhds ((↑(Real.sqrt 57) : ℂ) / 8)) := by
132 have hw := tendsto_pentHingeCosPath_one
133 have hsq :
134 Tendsto (fun t => pentHingeCosPath 1 t ^ 2 - 1)
135 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
136 (nhds ((11 / 8 : ℂ) ^ 2 - 1)) := by
137 have h := (hw.pow 2).sub (tendsto_const_nhds (x := (1 : ℂ)))
138 simpa [neg_sq] using h
139 have hsq' :
140 Tendsto (fun t => pentHingeCosPath 1 t ^ 2 - 1)
141 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
142 (nhds (57 / 64 : ℂ)) := by
143 simpa [sq_sub_one_limit] using hsq
144 have hcont : ContinuousAt (fun z : ℂ => csqrt z) (57 / 64 : ℂ) := by
145 unfold csqrt
146 exact continuousAt_cpow_const fiftySevenOver64_mem_slitPlane
147 have hcomp :
148 Tendsto (fun t => csqrt (pentHingeCosPath 1 t ^ 2 - 1))
149 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
150 (nhds (csqrt (57 / 64 : ℂ))) :=
151 hcont.tendsto.comp hsq'
152 have heval : csqrt (57 / 64 : ℂ) = (↑(Real.sqrt 57) : ℂ) / 8 := by
153 have h := csqrt_ofReal_nonneg (by norm_num : (0 : ℝ) ≤ 57 / 64)
154 have h64 : ((57 / 64 : ℝ) : ℂ) = (57 / 64 : ℂ) := by norm_num
155 rw [← h64, h, sqrt_fiftySeven_div_eight, ofReal_div, ofReal_ofNat]
156 exact heval ▸ hcomp
157
158/-! ## Filter helpers -/
159
160private lemma eventually_ioo_of_nhdsWithin_zero :
161 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0), t ∈ Set.Ioo (0 : ℝ) 1 := by
162 filter_upwards [self_mem_nhdsWithin,
163 Filter.Eventually.filter_mono nhdsWithin_le_nhds
164 (eventually_lt_nhds (by norm_num : (0 : ℝ) < 1))] with t ht0 ht1
165 exact ⟨ht0, ht1⟩
166
167private lemma eventually_re_pent_neg :
168 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
169 (pentHingeCosPath 1 t).re < 0 := by
170 have hw := tendsto_pentHingeCosPath_one
171 have hneg : ((-(11 / 8 : ℝ) : ℂ)).re < (0 : ℝ) := by norm_num
172 exact ((continuous_re.tendsto _).comp hw).eventually_lt_const hneg
173
174private lemma eventually_im_pent_neg :
175 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
176 (pentHingeCosPath 1 t).im < 0 := by
177 filter_upwards [eventually_ioo_of_nhdsWithin_zero] with t ht
178 exact im_pentHingeCosPath_neg_one ht
179
180private lemma eventually_im_one_sub_sq_neg :
181 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
182 (1 - pentHingeCosPath 1 t ^ 2).im < 0 := by
183 filter_upwards [eventually_re_pent_neg, eventually_im_pent_neg] with t hre him
184 have :
185 (1 - pentHingeCosPath 1 t ^ 2).im =
186 -(2 * (pentHingeCosPath 1 t).re * (pentHingeCosPath 1 t).im) := by
187 simp [sub_im, sq, mul_im]
188 ring
189 rw [this]
190 have hprod : (pentHingeCosPath 1 t).re * (pentHingeCosPath 1 t).im > 0 :=
191 mul_pos_of_neg_of_neg hre him
192 nlinarith
193
194/-! ## L4 -/
195
196theorem eventually_carccos_log_arg_eq :
197 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
198 pentHingeCosPath 1 t + I * csqrt (1 - pentHingeCosPath 1 t ^ 2) =
199 pentHingeCosPath 1 t + csqrt (pentHingeCosPath 1 t ^ 2 - 1) := by
200 filter_upwards [eventually_im_one_sub_sq_neg] with t him
201 set w := pentHingeCosPath 1 t
202 have hrefl : csqrt (1 - w ^ 2) = -I * csqrt (-(1 - w ^ 2)) :=
203 csqrt_of_im_neg him
204 have hneg : -(1 - w ^ 2) = w ^ 2 - 1 := by ring
205 calc
206 w + I * csqrt (1 - w ^ 2)
207 = w + I * (-I * csqrt (-(1 - w ^ 2))) := by rw [hrefl]
208 _ = w + I * (-I * csqrt (w ^ 2 - 1)) := by rw [hneg]
209 _ = w + csqrt (w ^ 2 - 1) := by
210 simp [← mul_assoc, mul_neg, I_mul_I]
211
212/-! ## L5 -/
213
214private lemma eventually_csqrt_re_pos :
215 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
216 0 < (csqrt (pentHingeCosPath 1 t ^ 2 - 1)).re := by
217 have hW := tendsto_csqrt_sq_sub_one_one
218 have hpos : (0 : ℝ) < Real.sqrt 57 / 8 :=
219 div_pos (Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 57)) (by norm_num)
220 have hlim : (((↑(Real.sqrt 57) : ℂ) / 8)).re = Real.sqrt 57 / 8 := by
221 simp [div_re, ofReal_re, ofReal_im]
222 exact ((continuous_re.tendsto _).comp hW).eventually_const_lt
223 (by simpa [hlim] using hpos)
224
225private lemma eventually_csqrt_add_re_neg :
226 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
227 (csqrt (pentHingeCosPath 1 t ^ 2 - 1)).re +
228 (pentHingeCosPath 1 t).re < 0 := by
229 have hW := tendsto_csqrt_sq_sub_one_one
230 have hw := tendsto_pentHingeCosPath_one
231 have hsum :
232 Tendsto
233 (fun t =>
234 (csqrt (pentHingeCosPath 1 t ^ 2 - 1)).re +
235 (pentHingeCosPath 1 t).re)
236 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
237 (nhds (Real.sqrt 57 / 8 + (-(11 / 8 : ℝ)))) := by
238 have hWr := (continuous_re.tendsto _).comp hW
239 have hwr := (continuous_re.tendsto _).comp hw
240 simpa using hWr.add hwr
241 have hlim_lt : Real.sqrt 57 / 8 + (-(11 / 8 : ℝ)) < 0 := by
242 have hsq : Real.sqrt 57 < 11 := by
243 have : (57 : ℝ) < 11 ^ 2 := by norm_num
244 exact (Real.sqrt_lt' (by norm_num)).2 (by simpa using this)
245 linarith
246 exact hsum.eventually_lt_const hlim_lt
247
248private lemma eventually_sq_sub_one_ne :
249 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
250 pentHingeCosPath 1 t ^ 2 - 1 ≠ 0 := by
251 have hw := tendsto_pentHingeCosPath_one
252 have hsq :
253 Tendsto (fun t => pentHingeCosPath 1 t ^ 2 - 1)
254 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
255 (nhds (57 / 64 : ℂ)) := by
256 have h := (hw.pow 2).sub (tendsto_const_nhds (x := (1 : ℂ)))
257 simpa [neg_sq, sq_sub_one_limit] using h
258 have hne : (57 / 64 : ℂ) ≠ 0 := by norm_num
259 exact hsq.eventually_ne hne
260
261theorem eventually_im_log_arg_nonneg :
262 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
263 0 ≤ (pentHingeCosPath 1 t +
264 csqrt (pentHingeCosPath 1 t ^ 2 - 1)).im := by
265 filter_upwards [eventually_im_pent_neg, eventually_csqrt_re_pos,
266 eventually_csqrt_add_re_neg, eventually_sq_sub_one_ne] with
267 t himw hWre hsum hne
268 set w := pentHingeCosPath 1 t
269 set W := csqrt (w ^ 2 - 1)
270 have hmul : W * W = w ^ 2 - 1 := csqrt_mul_self hne
271 have himWW : (W * W).im = (w ^ 2 - 1).im := by rw [hmul]
272 have hleft : (W * W).im = 2 * W.re * W.im := by
273 simp [mul_im]
274 ring
275 have hright : (w ^ 2 - 1).im = 2 * w.re * w.im := by
276 simp [sub_im, sq, mul_im]
277 ring
278 have hprod : W.re * W.im = w.re * w.im := by
279 have : 2 * W.re * W.im = 2 * w.re * w.im := by
280 linarith [himWW, hleft, hright]
281 nlinarith
282 have hid : (w.im + W.im) * W.re = w.im * (W.re + w.re) := by
283 linarith [hprod]
284 have hrhs : 0 < w.im * (W.re + w.re) :=
285 mul_pos_of_neg_of_neg himw hsum
286 have hlhs : 0 < (w.im + W.im) * W.re := by
287 simpa [hid] using hrhs
288 have : 0 < w.im + W.im := pos_of_mul_pos_left hlhs hWre.le
289 simpa [add_im] using this.le
290
291/-! ## L6 -/
292
293/-- Limit log-argument, written to match the sum of L2 and L3 limits. -/
294private def u0 : ℂ := (-(11 / 8 : ℝ) : ℂ) + (↑(Real.sqrt 57) : ℂ) / 8
295
296private lemma u0_eq_ofReal :
297 u0 = ((Real.sqrt 57 - 11) / 8 : ℝ) := by
298 simp [u0, ofReal_div, ofReal_sub, ofReal_ofNat]
299 ring
300
301private lemma u0_re : u0.re = (Real.sqrt 57 - 11) / 8 := by
302 rw [u0_eq_ofReal]
303 simp
304
305private lemma u0_im : u0.im = 0 := by
306 rw [u0_eq_ofReal]
307 simp
308
309private lemma sqrt57_lt_11 : Real.sqrt 57 < 11 := by
310 have : (57 : ℝ) < 11 ^ 2 := by norm_num
311 exact (Real.sqrt_lt' (by norm_num)).2 (by simpa using this)
312
313private lemma u0_re_neg : u0.re < 0 := by
314 rw [u0_re]
315 linarith [sqrt57_lt_11]
316
317private lemma tendsto_log_arg_to_u0 :
318 Tendsto
319 (fun t =>
320 pentHingeCosPath 1 t + csqrt (pentHingeCosPath 1 t ^ 2 - 1))
321 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds u0) := by
322 have hw := tendsto_pentHingeCosPath_one
323 have hW := tendsto_csqrt_sq_sub_one_one
324 simpa [u0] using hw.add hW
325
326private lemma tendsto_log_arg_nhdsWithin_im_nonneg :
327 Tendsto
328 (fun t =>
329 pentHingeCosPath 1 t + csqrt (pentHingeCosPath 1 t ^ 2 - 1))
330 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
331 (nhdsWithin u0 {z : ℂ | 0 ≤ z.im}) := by
332 rw [tendsto_nhdsWithin_iff]
333 exact ⟨tendsto_log_arg_to_u0, eventually_im_log_arg_nonneg⟩
334
335private lemma tendsto_log_of_log_arg :
336 Tendsto
337 (fun t =>
338 log (pentHingeCosPath 1 t +
339 csqrt (pentHingeCosPath 1 t ^ 2 - 1)))
340 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
341 (nhds (↑(Real.log ‖u0‖) + (Real.pi : ℂ) * I)) := by
342 have hlog :=
343 tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero u0_re_neg u0_im
344 exact hlog.comp tendsto_log_arg_nhdsWithin_im_nonneg
345
346private lemma norm_u0 :
347 ‖u0‖ = (11 - Real.sqrt 57) / 8 := by
348 have hneg : ((Real.sqrt 57 - 11) / 8 : ℝ) < 0 := by
349 linarith [sqrt57_lt_11]
350 rw [u0_eq_ofReal, Complex.norm_real, Real.norm_eq_abs, abs_of_neg hneg]
351 ring
352
353private lemma log_norm_u0_eq_neg_arcosh :
354 Real.log ‖u0‖ = -Real.arcosh (11 / 8) := by
355 rw [norm_u0, Real.arcosh]
356 have hsqrt :
357 Real.sqrt ((11 / 8 : ℝ) ^ 2 - 1) = Real.sqrt 57 / 8 := by
358 have : (11 / 8 : ℝ) ^ 2 - 1 = 57 / 64 := by norm_num
359 rw [this, sqrt_fiftySeven_div_eight]
360 have hsum :
361 (11 / 8 : ℝ) + Real.sqrt ((11 / 8) ^ 2 - 1) =
362 (11 + Real.sqrt 57) / 8 := by
363 rw [hsqrt]
364 ring
365 rw [hsum]
366 have hprod :
367 ((11 - Real.sqrt 57) / 8) * ((11 + Real.sqrt 57) / 8) = 1 := by
368 have h : (11 : ℝ) ^ 2 - (Real.sqrt 57) ^ 2 = 64 := by
369 rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 57)]
370 norm_num
371 field_simp
372 linarith [h]
373 have hinv :
374 (11 - Real.sqrt 57) / 8 = ((11 + Real.sqrt 57) / 8)⁻¹ :=
375 (inv_eq_of_mul_eq_one_left hprod).symm
376 rw [hinv, Real.log_inv]
377
378theorem carccos_tendsto_at_cut_one_holds :
379 Tendsto (fun t => carccos (pentHingeCosPath 1 t))
380 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
381 (nhds ((↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1))) := by
382 have heq :
383 (fun t => carccos (pentHingeCosPath 1 t)) =ᶠ[nhdsWithin (0 : ℝ) (Set.Ioi 0)]
384 fun t =>
385 (-I) *
386 log (pentHingeCosPath 1 t +
387 csqrt (pentHingeCosPath 1 t ^ 2 - 1)) := by
388 filter_upwards [eventually_carccos_log_arg_eq] with t ht
389 simp only [carccos, ht]
390 have hlog := tendsto_log_of_log_arg
391 have hmul :
392 Tendsto
393 (fun t =>
394 (-I) *
395 log (pentHingeCosPath 1 t +
396 csqrt (pentHingeCosPath 1 t ^ 2 - 1)))
397 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
398 (nhds ((-I) * (↑(Real.log ‖u0‖) + (Real.pi : ℂ) * I))) :=
399 tendsto_const_nhds.mul hlog
400 have hcongr := Tendsto.congr' heq.symm hmul
401 have hval :
402 (-I) * (↑(Real.log ‖u0‖) + (Real.pi : ℂ) * I) =
403 (↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1) := by
404 have hlog' := log_norm_u0_eq_neg_arcosh
405 unfold lorentzAngleRe lorentzRapidity
406 rw [lorentzCos_one, abs_neg,
407 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 11 / 8), hlog']
408 -- (-I) * (-↑R + π I) = ↑π + I ↑R
409 set R : ℝ := Real.arcosh (11 / 8)
410 have h :
411 (-I) * (-↑R + (Real.pi : ℂ) * I) =
412 (↑(Real.pi) : ℂ) + I * ↑R := by
413 have h1 :
414 (-I) * (-↑R + (Real.pi : ℂ) * I) =
415 I * ↑R + -(I * ((Real.pi : ℂ) * I)) := by
416 simp [mul_add, mul_neg]
417 have hI : I * ((Real.pi : ℂ) * I) = I ^ 2 * (Real.pi : ℂ) := by
418 ring
419 have h2 :
420 I * ↑R + -(I * ((Real.pi : ℂ) * I)) =
421 I * ↑R + -(I ^ 2 * (Real.pi : ℂ)) := by
422 rw [hI]
423 have h3 :
424 I * ↑R + -(I ^ 2 * (Real.pi : ℂ)) =
425 I * ↑R + (Real.pi : ℂ) := by
426 simp [I_sq]
427 have h4 :
428 I * ↑R + (Real.pi : ℂ) = (↑(Real.pi) : ℂ) + I * ↑R :=
429 add_comm _ _
430 exact h1.trans (h2.trans (h3.trans h4))
431 simpa [ofReal_neg, R] using h
432 simpa [hval] using hcongr
433
434theorem carccos_tendsto_at_cut_one_inhabited : carccos_tendsto_at_cut_one :=
435 carccos_tendsto_at_cut_one_holds
436
437theorem lorentzAnchor_one_holds : lorentzAnchor_one := by
438 unfold lorentzAnchor_one wickActionPath dihedralSumPath
439 have hc := carccos_tendsto_at_cut_one_holds
440 have h3 :
441 Tendsto (fun t => (3 : ℂ) * carccos (pentHingeCosPath 1 t))
442 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
443 (nhds ((3 : ℂ) *
444 ((↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1)))) :=
445 tendsto_const_nhds.mul hc
446 have hsub :
447 Tendsto
448 (fun t =>
449 (2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath 1 t))
450 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
451 (nhds
452 ((2 * Real.pi : ℂ) -
453 3 *
454 ((↑(lorentzAngleRe 1) : ℂ) +
455 I * ↑(lorentzRapidity 1)))) :=
456 tendsto_const_nhds.sub h3
457 have hA :
458 Tendsto
459 (fun t =>
460 (hingeArea : ℂ) *
461 ((2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath 1 t)))
462 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
463 (nhds
464 ((hingeArea : ℂ) *
465 ((2 * Real.pi : ℂ) -
466 3 *
467 ((↑(lorentzAngleRe 1) : ℂ) +
468 I * ↑(lorentzRapidity 1))))) :=
469 tendsto_const_nhds.mul hsub
470 have hshape :
471 (hingeArea : ℂ) *
472 ((2 * Real.pi : ℂ) -
473 3 *
474 ((↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1))) =
475 (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
476 I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)) := by
477 unfold lorentzAngleRe
478 simp [ofReal_mul, ofReal_add, mul_add, sub_eq_add_neg]
479 ring
480 simpa [hshape] using hA
481
482theorem lorentzAnchor_one_inhabited : lorentzAnchor_one :=
483 lorentzAnchor_one_holds
484
485structure WickActionCutLimitStatus where
486 n4CutLimitOneClosed : Bool
487 n4LorentzAnchorOneClosed : Bool
488 n4FamilyOpen : Bool
489 gap6LorentzianAction : Bool
490 terminalInhabitationOpen : Bool
491
492def wickActionCutLimitStatus : WickActionCutLimitStatus where
493 n4CutLimitOneClosed := true
494 n4LorentzAnchorOneClosed := true
495 n4FamilyOpen := false
496 gap6LorentzianAction := true
497 terminalInhabitationOpen := false
498
499theorem wickActionCutLimitStatus_flags :
500 wickActionCutLimitStatus.n4CutLimitOneClosed = true ∧
501 wickActionCutLimitStatus.n4LorentzAnchorOneClosed = true ∧
502 wickActionCutLimitStatus.n4FamilyOpen = false ∧
503 wickActionCutLimitStatus.gap6LorentzianAction = true ∧
504 wickActionCutLimitStatus.terminalInhabitationOpen = false ∧
505 carccos_tendsto_at_cut_one ∧
506 lorentzAnchor_one :=
507 ⟨rfl, rfl, rfl, rfl, rfl, carccos_tendsto_at_cut_one_inhabited,
508 lorentzAnchor_one_inhabited⟩
509
510end
511
512end WickActionInteriorHinge
513end SevenGaps
514end Gravity
515end IndisputableMonolith
516