IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily
IndisputableMonolith/Gravity/SevenGaps/WickActionCutLimitFamily.lean · 652 lines · 43 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.FieldSimp
8import Mathlib.Tactic.Linarith
9import Mathlib.Tactic.NormNum
10import Mathlib.Tactic.Positivity
11import Mathlib.Tactic.Ring
12import IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit
13import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
14import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement
15import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
16
17/-!
18# Wave C4 F1: parameterized cut-limit family (`α > 7/12`)
19
20Binding design: `D-gap6-v2-succession-family-design-20260723`.
21
22Generalizes the α=1 six-lemma route in `WickActionCutLimit` to the full
23causal range. All proofs are **pointwise** under `7/12 < α` (no
24uniform-in-α bound: `lorentzK α → 1` as `α → ∞`).
25
26Does **not** inhabit `WickActionContinuationCertV2` (F2) or flip ledger
27Bools (F3). Reuses generic L1 `csqrt_of_im_neg` from the α=1 module.
28-/
29
30namespace IndisputableMonolith
31namespace Gravity
32namespace SevenGaps
33namespace WickActionInteriorHinge
34
35open Complex
36open Filter Topology
37open WickActionComplexFirst
38open WickFourOneAllHinges (csqrt_ofReal_nonneg)
39
40noncomputable section
41
42/-! ## §0. Lorentzian scale `lorentzK` -/
43
44/-- Positive Lorentzian cosine scale: `|lorentzCos α|` on the causal range. -/
45def lorentzK (α : ℝ) : ℝ := (5 + 6 * α) / (2 + 6 * α)
46
47theorem lorentzCos_eq_neg_lorentzK (α : ℝ) :
48 lorentzCos α = -(lorentzK α) := by
49 unfold lorentzCos lorentzK
50 rfl
51
52theorem lorentzK_den_pos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
53 0 < 2 + 6 * α := by
54 have h0 : (0 : ℝ) < 2 + 6 * (7 / 12) := by norm_num
55 linarith
56
57theorem lorentzK_gt_one {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
58 1 < lorentzK α := by
59 have hden := lorentzK_den_pos hα
60 unfold lorentzK
61 rw [one_lt_div hden]
62 linarith
63
64theorem lorentzK_pos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
65 0 < lorentzK α :=
66 lt_trans (by norm_num : (0 : ℝ) < 1) (lorentzK_gt_one hα)
67
68theorem lorentzK_sq_sub_one_pos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
69 0 < lorentzK α ^ 2 - 1 := by
70 have hk := lorentzK_gt_one hα
71 nlinarith [mul_self_lt_mul_self (by norm_num : (0 : ℝ) ≤ 1) hk]
72
73theorem sqrt_lorentzK_sq_sub_one_lt {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
74 Real.sqrt (lorentzK α ^ 2 - 1) < lorentzK α := by
75 have hkpos := lorentzK_pos hα
76 have hlt : lorentzK α ^ 2 - 1 < lorentzK α ^ 2 := by linarith
77 exact (Real.sqrt_lt' hkpos).mpr hlt
78
79/-! ## §1. Rapidity pin (family) -/
80
81theorem rapidityPinned_of_causal {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
82 lorentzRapidity α ≠ 0 := by
83 unfold lorentzRapidity
84 rw [lorentzCos_eq_neg_lorentzK, abs_neg,
85 abs_of_nonneg (lorentzK_pos hα).le]
86 exact (Real.arcosh_pos (lorentzK_gt_one hα)).ne'
87
88/-! ## §2. Continuous arc (general α) -/
89
90theorem continuous_arcZ (a alpha : ℝ) : Continuous (fun t : ℝ => arcZ a alpha t) := by
91 unfold arcZ
92 exact continuous_const.mul
93 (Complex.continuous_exp.comp
94 ((Complex.continuous_ofReal.comp
95 (continuous_const.mul (continuous_const.sub continuous_id))).mul
96 continuous_const))
97
98/-! ## §3. L2 family: path cosine → `-lorentzK α` -/
99
100theorem tendsto_pentHingeCosPath_of_causal {α : ℝ}
101 (hα : (7 / 12 : ℝ) < α) :
102 Tendsto (fun t => pentHingeCosPath α t) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
103 (nhds ((-(lorentzK α) : ℝ) : ℂ)) := by
104 have hz :
105 Tendsto (fun t => arcZ 1 α t) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
106 (nhds (arcZ 1 α 0)) :=
107 ((continuous_arcZ 1 α).tendsto 0).mono_left nhdsWithin_le_nhds
108 have hz0 : arcZ 1 α 0 = ((-α : ℝ) : ℂ) := by
109 simpa using arcZ_zero 1 α
110 have hnum :
111 Tendsto (fun t => (5 : ℂ) - 6 * arcZ 1 α t)
112 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
113 (nhds (((5 + 6 * α : ℝ) : ℂ))) := by
114 have h :
115 Tendsto (fun t => (5 : ℂ) - 6 * arcZ 1 α t)
116 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
117 (nhds ((5 : ℂ) - 6 * arcZ 1 α 0)) :=
118 tendsto_const_nhds.sub (tendsto_const_nhds.mul hz)
119 convert h using 1
120 simp [hz0, ofReal_neg]
121 have hden :
122 Tendsto (fun t => (6 : ℂ) * arcZ 1 α t - 2)
123 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
124 (nhds (((-(2 + 6 * α) : ℝ) : ℂ))) := by
125 have h :
126 Tendsto (fun t => (6 : ℂ) * arcZ 1 α t - 2)
127 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
128 (nhds ((6 : ℂ) * arcZ 1 α 0 - 2)) :=
129 (tendsto_const_nhds.mul hz).sub tendsto_const_nhds
130 convert h using 1
131 simp [hz0, ofReal_neg]; ring
132 have hden0 : ((-(2 + 6 * α) : ℝ) : ℂ) ≠ 0 :=
133 Complex.ofReal_ne_zero.mpr (neg_ne_zero.mpr (lorentzK_den_pos hα).ne')
134 have hdiv :
135 Tendsto (fun t => ((5 : ℂ) - 6 * arcZ 1 α t) / (6 * arcZ 1 α t - 2))
136 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
137 (nhds ((((5 + 6 * α : ℝ) : ℂ) / ((-(2 + 6 * α) : ℝ) : ℂ)))) :=
138 hnum.div hden hden0
139 have hval :
140 (((5 + 6 * α : ℝ) : ℂ) / ((-(2 + 6 * α) : ℝ) : ℂ)) =
141 ((-(lorentzK α) : ℝ) : ℂ) := by
142 calc
143 (((5 + 6 * α : ℝ) : ℂ) / ((-(2 + 6 * α) : ℝ) : ℂ))
144 = ↑((5 + 6 * α) / -(2 + 6 * α)) := by rw [← ofReal_div]
145 _ = ↑(-((5 + 6 * α) / (2 + 6 * α))) := by rw [div_neg]
146 _ = ((-(lorentzK α) : ℝ) : ℂ) := by rfl
147 have hpath :
148 (fun t => pentHingeCosPath α t) =
149 fun t => ((5 : ℂ) - 6 * arcZ 1 α t) / (6 * arcZ 1 α t - 2) := by
150 funext t
151 exact pentHingeCosPath_eq_moebius hα t
152 have hdiv' :
153 Tendsto (fun t => ((5 : ℂ) - 6 * arcZ 1 α t) / (6 * arcZ 1 α t - 2))
154 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
155 (nhds ((-(lorentzK α) : ℝ) : ℂ)) :=
156 hval ▸ hdiv
157 simpa [hpath] using hdiv'
158
159/-! ## §4. L3 family: `csqrt(w^2 - 1)` → `√(k^2 - 1)` -/
160
161private lemma lorentzK_sq_sub_one_mem_slitPlane {α : ℝ}
162 (hα : (7 / 12 : ℝ) < α) :
163 ((lorentzK α ^ 2 - 1 : ℝ) : ℂ) ∈ slitPlane :=
164 ofReal_mem_slitPlane.mpr (lorentzK_sq_sub_one_pos hα)
165
166theorem tendsto_csqrt_sq_sub_one_of_causal {α : ℝ}
167 (hα : (7 / 12 : ℝ) < α) :
168 Tendsto (fun t => csqrt (pentHingeCosPath α t ^ 2 - 1))
169 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
170 (nhds ((↑(Real.sqrt (lorentzK α ^ 2 - 1)) : ℂ))) := by
171 have hw := tendsto_pentHingeCosPath_of_causal hα
172 have hsq :
173 Tendsto (fun t => pentHingeCosPath α t ^ 2 - 1)
174 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
175 (nhds ((lorentzK α : ℂ) ^ 2 - 1)) := by
176 have h := (hw.pow 2).sub (tendsto_const_nhds (x := (1 : ℂ)))
177 simpa [neg_sq] using h
178 have hsq' :
179 Tendsto (fun t => pentHingeCosPath α t ^ 2 - 1)
180 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
181 (nhds ((lorentzK α ^ 2 - 1 : ℝ) : ℂ)) := by
182 convert hsq using 1
183 simp [ofReal_pow, ofReal_sub, ofReal_one]
184 have hcont : ContinuousAt (fun z : ℂ => csqrt z)
185 ((lorentzK α ^ 2 - 1 : ℝ) : ℂ) := by
186 unfold csqrt
187 exact continuousAt_cpow_const (lorentzK_sq_sub_one_mem_slitPlane hα)
188 have hcomp :
189 Tendsto (fun t => csqrt (pentHingeCosPath α t ^ 2 - 1))
190 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
191 (nhds (csqrt ((lorentzK α ^ 2 - 1 : ℝ) : ℂ))) :=
192 hcont.tendsto.comp hsq'
193 have heval :
194 csqrt ((lorentzK α ^ 2 - 1 : ℝ) : ℂ) =
195 (↑(Real.sqrt (lorentzK α ^ 2 - 1)) : ℂ) :=
196 csqrt_ofReal_nonneg (lorentzK_sq_sub_one_pos hα).le
197 exact heval ▸ hcomp
198
199/-! ## §5. Filter helpers (family) -/
200
201private lemma eventually_ioo_of_nhdsWithin_zero :
202 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0), t ∈ Set.Ioo (0 : ℝ) 1 := by
203 filter_upwards [self_mem_nhdsWithin,
204 Filter.Eventually.filter_mono nhdsWithin_le_nhds
205 (eventually_lt_nhds (by norm_num : (0 : ℝ) < 1))] with t ht0 ht1
206 exact ⟨ht0, ht1⟩
207
208private lemma eventually_re_pent_neg {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
209 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
210 (pentHingeCosPath α t).re < 0 := by
211 have hw := tendsto_pentHingeCosPath_of_causal hα
212 have hneg : ((-(lorentzK α) : ℝ) : ℂ).re < (0 : ℝ) := by
213 simpa using neg_lt_zero.mpr (lorentzK_pos hα)
214 exact ((continuous_re.tendsto _).comp hw).eventually_lt_const hneg
215
216private lemma eventually_im_pent_neg {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
217 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
218 (pentHingeCosPath α t).im < 0 := by
219 filter_upwards [eventually_ioo_of_nhdsWithin_zero] with t ht
220 exact im_pentHingeCosPath_neg hα ht
221
222private lemma eventually_im_one_sub_sq_neg {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
223 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
224 (1 - pentHingeCosPath α t ^ 2).im < 0 := by
225 filter_upwards [eventually_re_pent_neg hα, eventually_im_pent_neg hα] with
226 t hre him
227 have :
228 (1 - pentHingeCosPath α t ^ 2).im =
229 -(2 * (pentHingeCosPath α t).re * (pentHingeCosPath α t).im) := by
230 simp [sub_im, sq, mul_im]
231 ring
232 rw [this]
233 have hprod : (pentHingeCosPath α t).re * (pentHingeCosPath α t).im > 0 :=
234 mul_pos_of_neg_of_neg hre him
235 nlinarith
236
237/-! ## §6. L4 family (generic skeleton) -/
238
239theorem eventually_carccos_log_arg_eq_of_causal {α : ℝ}
240 (hα : (7 / 12 : ℝ) < α) :
241 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
242 pentHingeCosPath α t + I * csqrt (1 - pentHingeCosPath α t ^ 2) =
243 pentHingeCosPath α t + csqrt (pentHingeCosPath α t ^ 2 - 1) := by
244 filter_upwards [eventually_im_one_sub_sq_neg hα] with t him
245 set w := pentHingeCosPath α t
246 have hrefl : csqrt (1 - w ^ 2) = -I * csqrt (-(1 - w ^ 2)) :=
247 csqrt_of_im_neg him
248 have hneg : -(1 - w ^ 2) = w ^ 2 - 1 := by ring
249 calc
250 w + I * csqrt (1 - w ^ 2)
251 = w + I * (-I * csqrt (-(1 - w ^ 2))) := by rw [hrefl]
252 _ = w + I * (-I * csqrt (w ^ 2 - 1)) := by rw [hneg]
253 _ = w + csqrt (w ^ 2 - 1) := by
254 simp [← mul_assoc, mul_neg, I_mul_I]
255
256/-! ## §7. L5 family: Im log-arg ≥ 0 eventually -/
257
258private lemma eventually_csqrt_re_pos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
259 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
260 0 < (csqrt (pentHingeCosPath α t ^ 2 - 1)).re := by
261 have hW := tendsto_csqrt_sq_sub_one_of_causal hα
262 have hpos : (0 : ℝ) < Real.sqrt (lorentzK α ^ 2 - 1) :=
263 Real.sqrt_pos.mpr (lorentzK_sq_sub_one_pos hα)
264 have hlim :
265 ((↑(Real.sqrt (lorentzK α ^ 2 - 1)) : ℂ)).re =
266 Real.sqrt (lorentzK α ^ 2 - 1) := by
267 simp
268 exact ((continuous_re.tendsto _).comp hW).eventually_const_lt
269 (by simpa [hlim] using hpos)
270
271private lemma eventually_csqrt_add_re_neg {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
272 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
273 (csqrt (pentHingeCosPath α t ^ 2 - 1)).re +
274 (pentHingeCosPath α t).re < 0 := by
275 have hW := tendsto_csqrt_sq_sub_one_of_causal hα
276 have hw := tendsto_pentHingeCosPath_of_causal hα
277 have hsum :
278 Tendsto
279 (fun t =>
280 (csqrt (pentHingeCosPath α t ^ 2 - 1)).re +
281 (pentHingeCosPath α t).re)
282 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
283 (nhds (Real.sqrt (lorentzK α ^ 2 - 1) + (-(lorentzK α)))) := by
284 have hWr := (continuous_re.tendsto _).comp hW
285 have hwr := (continuous_re.tendsto _).comp hw
286 simpa using hWr.add hwr
287 have hlim_lt :
288 Real.sqrt (lorentzK α ^ 2 - 1) + (-(lorentzK α)) < 0 := by
289 linarith [sqrt_lorentzK_sq_sub_one_lt hα]
290 exact hsum.eventually_lt_const hlim_lt
291
292private lemma eventually_sq_sub_one_ne {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
293 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
294 pentHingeCosPath α t ^ 2 - 1 ≠ 0 := by
295 have hw := tendsto_pentHingeCosPath_of_causal hα
296 have hsq :
297 Tendsto (fun t => pentHingeCosPath α t ^ 2 - 1)
298 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
299 (nhds ((lorentzK α ^ 2 - 1 : ℝ) : ℂ)) := by
300 have h := (hw.pow 2).sub (tendsto_const_nhds (x := (1 : ℂ)))
301 convert h using 1
302 simp [ofReal_pow, ofReal_sub, ofReal_one]
303 have hne : ((lorentzK α ^ 2 - 1 : ℝ) : ℂ) ≠ 0 :=
304 Complex.ofReal_ne_zero.mpr (lorentzK_sq_sub_one_pos hα).ne'
305 exact hsq.eventually_ne hne
306
307theorem eventually_im_log_arg_nonneg_of_causal {α : ℝ}
308 (hα : (7 / 12 : ℝ) < α) :
309 ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0),
310 0 ≤ (pentHingeCosPath α t +
311 csqrt (pentHingeCosPath α t ^ 2 - 1)).im := by
312 filter_upwards [eventually_im_pent_neg hα, eventually_csqrt_re_pos hα,
313 eventually_csqrt_add_re_neg hα, eventually_sq_sub_one_ne hα] with
314 t himw hWre hsum hne
315 set w := pentHingeCosPath α t
316 set W := csqrt (w ^ 2 - 1)
317 have hmul : W * W = w ^ 2 - 1 := csqrt_mul_self hne
318 have himWW : (W * W).im = (w ^ 2 - 1).im := by rw [hmul]
319 have hleft : (W * W).im = 2 * W.re * W.im := by
320 simp [mul_im]
321 ring
322 have hright : (w ^ 2 - 1).im = 2 * w.re * w.im := by
323 simp [sub_im, sq, mul_im]
324 ring
325 have hprod : W.re * W.im = w.re * w.im := by
326 have : 2 * W.re * W.im = 2 * w.re * w.im := by
327 linarith [himWW, hleft, hright]
328 nlinarith
329 have hid : (w.im + W.im) * W.re = w.im * (W.re + w.re) := by
330 linarith [hprod]
331 have hrhs : 0 < w.im * (W.re + w.re) :=
332 mul_pos_of_neg_of_neg himw hsum
333 have hlhs : 0 < (w.im + W.im) * W.re := by
334 simpa [hid] using hrhs
335 have : 0 < w.im + W.im := pos_of_mul_pos_left hlhs hWre.le
336 simpa [add_im] using this.le
337
338/-! ## §8. L6 family: `carccos` cut Tendsto -/
339
340/-- Limit log-argument at causal `α`: `-k + √(k²-1)`. -/
341private def u0 (α : ℝ) : ℂ :=
342 ((-(lorentzK α) : ℝ) : ℂ) + (↑(Real.sqrt (lorentzK α ^ 2 - 1)) : ℂ)
343
344private lemma u0_eq_ofReal (α : ℝ) :
345 u0 α =
346 ((Real.sqrt (lorentzK α ^ 2 - 1) - lorentzK α : ℝ) : ℂ) := by
347 simp [u0, ofReal_sub]
348 ring
349
350private lemma u0_re (α : ℝ) :
351 (u0 α).re = Real.sqrt (lorentzK α ^ 2 - 1) - lorentzK α := by
352 rw [u0_eq_ofReal]
353 simp
354
355private lemma u0_im (α : ℝ) : (u0 α).im = 0 := by
356 rw [u0_eq_ofReal]
357 simp
358
359private lemma u0_re_neg {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
360 (u0 α).re < 0 := by
361 rw [u0_re]
362 linarith [sqrt_lorentzK_sq_sub_one_lt hα]
363
364private lemma tendsto_log_arg_to_u0 {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
365 Tendsto
366 (fun t =>
367 pentHingeCosPath α t + csqrt (pentHingeCosPath α t ^ 2 - 1))
368 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (u0 α)) := by
369 have hw := tendsto_pentHingeCosPath_of_causal hα
370 have hW := tendsto_csqrt_sq_sub_one_of_causal hα
371 simpa [u0] using hw.add hW
372
373private lemma tendsto_log_arg_nhdsWithin_im_nonneg {α : ℝ}
374 (hα : (7 / 12 : ℝ) < α) :
375 Tendsto
376 (fun t =>
377 pentHingeCosPath α t + csqrt (pentHingeCosPath α t ^ 2 - 1))
378 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
379 (nhdsWithin (u0 α) {z : ℂ | 0 ≤ z.im}) := by
380 rw [tendsto_nhdsWithin_iff]
381 exact ⟨tendsto_log_arg_to_u0 hα, eventually_im_log_arg_nonneg_of_causal hα⟩
382
383private lemma tendsto_log_of_log_arg {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
384 Tendsto
385 (fun t =>
386 log (pentHingeCosPath α t +
387 csqrt (pentHingeCosPath α t ^ 2 - 1)))
388 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
389 (nhds (↑(Real.log ‖u0 α‖) + (Real.pi : ℂ) * I)) := by
390 have hlog :=
391 tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero
392 (u0_re_neg hα) (u0_im α)
393 exact hlog.comp (tendsto_log_arg_nhdsWithin_im_nonneg hα)
394
395private lemma norm_u0 {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
396 ‖u0 α‖ = lorentzK α - Real.sqrt (lorentzK α ^ 2 - 1) := by
397 have hneg :
398 (Real.sqrt (lorentzK α ^ 2 - 1) - lorentzK α : ℝ) < 0 := by
399 linarith [sqrt_lorentzK_sq_sub_one_lt hα]
400 rw [u0_eq_ofReal, Complex.norm_real, Real.norm_eq_abs, abs_of_neg hneg]
401 ring
402
403private lemma log_norm_u0_eq_neg_arcosh {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
404 Real.log ‖u0 α‖ = -Real.arcosh (lorentzK α) := by
405 rw [norm_u0 hα, Real.arcosh]
406 have hprod :
407 (lorentzK α - Real.sqrt (lorentzK α ^ 2 - 1)) *
408 (lorentzK α + Real.sqrt (lorentzK α ^ 2 - 1)) = 1 := by
409 have hsq :
410 (Real.sqrt (lorentzK α ^ 2 - 1)) ^ 2 = lorentzK α ^ 2 - 1 :=
411 Real.sq_sqrt (lorentzK_sq_sub_one_pos hα).le
412 nlinarith [hsq]
413 have hinv :
414 lorentzK α - Real.sqrt (lorentzK α ^ 2 - 1) =
415 (lorentzK α + Real.sqrt (lorentzK α ^ 2 - 1))⁻¹ :=
416 (inv_eq_of_mul_eq_one_left hprod).symm
417 rw [hinv, Real.log_inv]
418
419theorem carccos_tendsto_at_cut_of_causal {α : ℝ}
420 (hα : (7 / 12 : ℝ) < α) :
421 Tendsto (fun t => carccos (pentHingeCosPath α t))
422 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
423 (nhds ((↑(lorentzAngleRe α) : ℂ) + I * ↑(lorentzRapidity α))) := by
424 have heq :
425 (fun t => carccos (pentHingeCosPath α t)) =ᶠ[nhdsWithin (0 : ℝ) (Set.Ioi 0)]
426 fun t =>
427 (-I) *
428 log (pentHingeCosPath α t +
429 csqrt (pentHingeCosPath α t ^ 2 - 1)) := by
430 filter_upwards [eventually_carccos_log_arg_eq_of_causal hα] with t ht
431 simp only [carccos, ht]
432 have hlog := tendsto_log_of_log_arg hα
433 have hmul :
434 Tendsto
435 (fun t =>
436 (-I) *
437 log (pentHingeCosPath α t +
438 csqrt (pentHingeCosPath α t ^ 2 - 1)))
439 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
440 (nhds ((-I) * (↑(Real.log ‖u0 α‖) + (Real.pi : ℂ) * I))) :=
441 tendsto_const_nhds.mul hlog
442 have hcongr := Tendsto.congr' heq.symm hmul
443 have hval :
444 (-I) * (↑(Real.log ‖u0 α‖) + (Real.pi : ℂ) * I) =
445 (↑(lorentzAngleRe α) : ℂ) + I * ↑(lorentzRapidity α) := by
446 have hlog' := log_norm_u0_eq_neg_arcosh hα
447 unfold lorentzAngleRe lorentzRapidity
448 rw [lorentzCos_eq_neg_lorentzK, abs_neg,
449 abs_of_nonneg (lorentzK_pos hα).le, hlog']
450 set R : ℝ := Real.arcosh (lorentzK α)
451 have h :
452 (-I) * (-↑R + (Real.pi : ℂ) * I) =
453 (↑(Real.pi) : ℂ) + I * ↑R := by
454 have h1 :
455 (-I) * (-↑R + (Real.pi : ℂ) * I) =
456 I * ↑R + -(I * ((Real.pi : ℂ) * I)) := by
457 simp [mul_add, mul_neg]
458 have hI : I * ((Real.pi : ℂ) * I) = I ^ 2 * (Real.pi : ℂ) := by
459 ring
460 have h2 :
461 I * ↑R + -(I * ((Real.pi : ℂ) * I)) =
462 I * ↑R + -(I ^ 2 * (Real.pi : ℂ)) := by
463 rw [hI]
464 have h3 :
465 I * ↑R + -(I ^ 2 * (Real.pi : ℂ)) =
466 I * ↑R + (Real.pi : ℂ) := by
467 simp [I_sq]
468 have h4 :
469 I * ↑R + (Real.pi : ℂ) = (↑(Real.pi) : ℂ) + I * ↑R :=
470 add_comm _ _
471 exact h1.trans (h2.trans (h3.trans h4))
472 simpa [ofReal_neg, R] using h
473 simpa [hval] using hcongr
474
475theorem carccos_tendsto_at_cut_family_holds : carccos_tendsto_at_cut_family :=
476 fun _α hα => carccos_tendsto_at_cut_of_causal hα
477
478/-! ## §9. Action-level Lorentzian anchor (family) -/
479
480theorem lorentzAnchor_of_causal {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
481 Tendsto (wickActionPath α) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
482 (nhds
483 (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe α) : ℝ) : ℂ) -
484 I * ((hingeArea * (3 * lorentzRapidity α) : ℝ) : ℂ))) := by
485 unfold wickActionPath dihedralSumPath
486 have hc := carccos_tendsto_at_cut_of_causal hα
487 have h3 :
488 Tendsto (fun t => (3 : ℂ) * carccos (pentHingeCosPath α t))
489 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
490 (nhds ((3 : ℂ) *
491 ((↑(lorentzAngleRe α) : ℂ) + I * ↑(lorentzRapidity α)))) :=
492 tendsto_const_nhds.mul hc
493 have hsub :
494 Tendsto
495 (fun t =>
496 (2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath α t))
497 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
498 (nhds
499 ((2 * Real.pi : ℂ) -
500 3 *
501 ((↑(lorentzAngleRe α) : ℂ) +
502 I * ↑(lorentzRapidity α)))) :=
503 tendsto_const_nhds.sub h3
504 have hA :
505 Tendsto
506 (fun t =>
507 (hingeArea : ℂ) *
508 ((2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath α t)))
509 (nhdsWithin (0 : ℝ) (Set.Ioi 0))
510 (nhds
511 ((hingeArea : ℂ) *
512 ((2 * Real.pi : ℂ) -
513 3 *
514 ((↑(lorentzAngleRe α) : ℂ) +
515 I * ↑(lorentzRapidity α))))) :=
516 tendsto_const_nhds.mul hsub
517 have hshape :
518 (hingeArea : ℂ) *
519 ((2 * Real.pi : ℂ) -
520 3 *
521 ((↑(lorentzAngleRe α) : ℂ) + I * ↑(lorentzRapidity α))) =
522 (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe α) : ℝ) : ℂ) -
523 I * ((hingeArea * (3 * lorentzRapidity α) : ℝ) : ℂ)) := by
524 unfold lorentzAngleRe
525 simp [ofReal_mul, ofReal_add, mul_add, sub_eq_add_neg]
526 ring
527 simpa [hshape] using hA
528
529/-! ## §10. Bonus: `ContinuousOn` on `Ioc 0 1` (unblocks F2) -/
530
531theorem euclidCos_lt_one {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
532 euclidCos α < 1 := by
533 have hden : 0 < 6 * α - 2 := by
534 have : (0 : ℝ) < 6 * (7 / 12) - 2 := by norm_num
535 linarith
536 unfold euclidCos
537 rw [div_lt_one hden]
538 linarith
539
540theorem euclidCos_gt_neg_one {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
541 -1 < euclidCos α := by
542 have hden : 0 < 6 * α - 2 := by
543 have : (0 : ℝ) < 6 * (7 / 12) - 2 := by norm_num
544 linarith
545 have hrewrite : euclidCos α + 1 = (3 : ℝ) / (6 * α - 2) := by
546 unfold euclidCos
547 field_simp [hden.ne']
548 ring
549 have hpos : 0 < euclidCos α + 1 := by
550 rw [hrewrite]
551 exact div_pos (by norm_num) hden
552 linarith
553
554theorem offArccosCut_pentHingeCosPath_Ioc_of_causal {α : ℝ}
555 (hα : (7 / 12 : ℝ) < α) {t : ℝ} (ht : t ∈ Set.Ioc (0 : ℝ) 1) :
556 OffArccosCut (pentHingeCosPath α t) := by
557 rcases ht with ⟨ht0, ht1⟩
558 rcases lt_or_eq_of_le ht1 with ht1' | rfl
559 · exact Or.inl (im_pentHingeCosPath_neg hα ⟨ht0, ht1'⟩).ne
560 · refine Or.inr ?_
561 rw [pentHingeCosPath_eq_euclidCos hα]
562 constructor
563 · simpa using euclidCos_gt_neg_one hα
564 · simpa using euclidCos_lt_one hα
565
566theorem continuousOn_pentHingeCosPath_Ioc_of_causal {α : ℝ}
567 (hα : (7 / 12 : ℝ) < α) :
568 ContinuousOn (pentHingeCosPath α) (Set.Ioc 0 1) := by
569 have hmo :
570 ContinuousOn
571 (fun t => ((5 : ℂ) - 6 * arcZ 1 α t) / (6 * arcZ 1 α t - 2))
572 (Set.Ioc 0 1) := by
573 refine ContinuousOn.div ?_ ?_ ?_
574 · exact (continuous_const.sub
575 (continuous_const.mul (continuous_arcZ 1 α))).continuousOn
576 · exact ((continuous_const.mul (continuous_arcZ 1 α)).sub
577 continuous_const).continuousOn
578 · intro t _ht
579 exact denom_ne_of_causal hα t
580 refine ContinuousOn.congr hmo ?_
581 intro t _ht
582 exact pentHingeCosPath_eq_moebius hα t
583
584theorem continuousOn_carccos_comp_pent_Ioc_of_causal {α : ℝ}
585 (hα : (7 / 12 : ℝ) < α) :
586 ContinuousOn (fun t => carccos (pentHingeCosPath α t)) (Set.Ioc 0 1) := by
587 have hpath := continuousOn_pentHingeCosPath_Ioc_of_causal hα
588 have hmaps :
589 Set.MapsTo (pentHingeCosPath α) (Set.Ioc 0 1) {w | OffArccosCut w} :=
590 fun _ ht => offArccosCut_pentHingeCosPath_Ioc_of_causal hα ht
591 exact continuousOn_carccos.comp hpath hmaps
592
593theorem continuousOn_wickActionPath_Ioc_of_causal {α : ℝ}
594 (hα : (7 / 12 : ℝ) < α) :
595 ContinuousOn (wickActionPath α) (Set.Ioc 0 1) := by
596 have hθ := continuousOn_carccos_comp_pent_Ioc_of_causal hα
597 have h3 : ContinuousOn (fun t => (3 : ℂ) * carccos (pentHingeCosPath α t))
598 (Set.Ioc 0 1) :=
599 continuousOn_const.mul hθ
600 have hsub :
601 ContinuousOn
602 (fun t =>
603 (2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath α t))
604 (Set.Ioc 0 1) :=
605 continuousOn_const.sub h3
606 have hA :
607 ContinuousOn
608 (fun t =>
609 (hingeArea : ℂ) *
610 ((2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath α t)))
611 (Set.Ioc 0 1) :=
612 continuousOn_const.mul hsub
613 refine hA.congr ?_
614 intro t _
615 unfold wickActionPath dihedralSumPath
616 rfl
617
618/-! ## §11. Status bits (F1 only; gap6 unflipped) -/
619
620structure WickActionCutLimitFamilyStatus where
621 f1CutLimitFamilyClosed : Bool
622 f1LorentzAnchorFamilyClosed : Bool
623 f1RapidityPinnedFamilyClosed : Bool
624 f1IocContinuityClosed : Bool
625 f2AssemblyOpen : Bool
626 gap6LorentzianAction : Bool
627
628def wickActionCutLimitFamilyStatus : WickActionCutLimitFamilyStatus where
629 f1CutLimitFamilyClosed := true
630 f1LorentzAnchorFamilyClosed := true
631 f1RapidityPinnedFamilyClosed := true
632 f1IocContinuityClosed := true
633 f2AssemblyOpen := false
634 gap6LorentzianAction := true
635
636theorem wickActionCutLimitFamilyStatus_flags :
637 wickActionCutLimitFamilyStatus.f1CutLimitFamilyClosed = true ∧
638 wickActionCutLimitFamilyStatus.f1LorentzAnchorFamilyClosed = true ∧
639 wickActionCutLimitFamilyStatus.f1RapidityPinnedFamilyClosed = true ∧
640 wickActionCutLimitFamilyStatus.f1IocContinuityClosed = true ∧
641 wickActionCutLimitFamilyStatus.f2AssemblyOpen = false ∧
642 wickActionCutLimitFamilyStatus.gap6LorentzianAction = true ∧
643 carccos_tendsto_at_cut_family :=
644 ⟨rfl, rfl, rfl, rfl, rfl, rfl, carccos_tendsto_at_cut_family_holds⟩
645
646end
647
648end WickActionInteriorHinge
649end SevenGaps
650end Gravity
651end IndisputableMonolith
652