IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean · 1289 lines · 97 declarations
show as:
view math explainer →
1import Mathlib.Data.Complex.Basic
2import Mathlib.Data.Matrix.Basic
3import Mathlib.Algebra.BigOperators.Fin
4import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
5import Mathlib.Analysis.Complex.Basic
6import Mathlib.Analysis.Complex.Trigonometric
7import Mathlib.Analysis.SpecialFunctions.Exp
8import Mathlib.Analysis.SpecialFunctions.Pow.Complex
9import Mathlib.Analysis.SpecialFunctions.Pow.Real
10import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
11import Mathlib.Analysis.SpecialFunctions.Complex.Log
12import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
13import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
14import Mathlib.Analysis.SpecialFunctions.Sqrt
15import Mathlib.Tactic.Linarith
16import Mathlib.Tactic.LinearCombination
17import Mathlib.Tactic.FieldSimp
18import IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst
19
20/-!
21# All-Hinge Complex-First Wick Continuation of the (4,1) Causal 4-Simplex (Lane B1)
22
23QG Seven-Gaps campaign, lane B of the finishing charter. The landed module
24`WickActionComplexFirst` certifies the split-form branch regularity and the
25boundary continuation for ONE traced hinge of the fourOne causal 4-simplex
26(triangle `(0,1,4)`, opposite pair `(2,3)`). This module extends both
27certificates to ALL TEN triangular hinges of the fourOne type, at the
28physical point `a = 1`, `alpha = 1`, on the canonical upper-half-plane arc
29`zArc` of `WickActionComplexFirst`.
30
31## Hinge enumeration
32
33A hinge of the 4-simplex on vertices `Fin 5` is an unordered triple; its
34opposite pair is the complementary two vertices. Enumerating hinges is
35therefore enumerating unordered vertex pairs `{p, q}`. For the fourOne
36type (timelike edges exactly those touching the apex vertex 4,
37`CausalSimplex4D.isTimelike`):
38
39* opposite pair inside `{0,1,2,3}` (6 pairs): the hinge CONTAINS vertex 4
40 and has 2 timelike triangle edges (the trace's timelike class); closed
41 forms `C_pp = C_qq = 6z - 2`, `C_pq = 1 - 2z`, `areaSq = z/4 - 1/16`;
42* opposite pair containing vertex 4 (4 pairs): the hinge avoids vertex 4
43 and has 0 timelike triangle edges (the trace's spacelike class); closed
44 forms `C_pp = 6z - 2` (the lower member), `C_qq = 4` (the apex),
45 `C_pq = -1`, `areaSq = 3/16`.
46
47All closed forms are kernel-checked below by explicit 5x5 minor
48determinants (one per opposite pair), matching the executed trace receipt
49(`state/qg_full_theory/wick_arc_trace/RESULTS.txt`, full per-hinge table).
50Note the trace's summary section 3 swaps the two class COUNTS (it says
51"6 spacelike / 4 timelike"); the per-hinge table and the combinatorics
52(`C(4,3) = 4` triples avoiding vertex 4, `C(4,2) = 6` containing it) give
534 spacelike-class and 6 timelike-class hinges, and the table wins.
54
55## What is proved
56
57* `branchRegular_fourOne_allHinges`: for EVERY unordered opposite pair
58 (equivalently every hinge), `BranchRegularOn` holds on the FULL open
59 interior `Set.Ioo 0 1` of the physical arc.
60* `wick_boundary_continuation_fourOne_allHinges`: every split-form cosine
61 path is continuous on the CLOSED interval `[0,1]` and ends at the
62 Euclidean regular-4-simplex value `-(1/4)`.
63* `fourOne_lorentzian_endpoint_values`: the Lorentzian endpoint values:
64 `-(3/8)` for every timelike-class hinge (the documented split-form sign
65 factor of `WickActionComplexFirst.lorentzian_endpoint_sign_factor`), and
66 the purely imaginary value `(sqrt 2 / 8) * I` for every spacelike-class
67 hinge (the trace's `0 + 0.17677...j`, the imaginary Lorentzian dihedral
68 datum at a spacelike hinge).
69* `fourOne_areaSq_spacelike` / `fourOne_areaSq_timelike` /
70 `fourOne_areaSq_interior_off_cut`: the ten hinge areas-squared in closed
71 form and their sqrt-cut avoidance (constant `3/16` everywhere including
72 endpoints; `z/4 - 1/16` on the open interior, with the ALLOWED Lorentzian
73 endpoint contact at `-5/16` documented in the landed module).
74
75## Honesty tiers
76
77* MODEL: `fourOneCosPath` and the explicit minor matrices are definitional
78 (complexifications inherited from `WickActionComplexFirst`; no new
79 modeling choices).
80* THEOREM: every declared theorem below is sorry-free and kernel-checked.
81* OPEN: the action-level continuation (interior-hinge simplicial complex,
82 deficit angles, the continued Regge action itself) is NOT claimed; it is
83 the C12 lane's question. No `FullTheoryLedger` flag is touched.
84-/
85
86namespace IndisputableMonolith
87namespace Gravity
88namespace SevenGaps
89namespace WickFourOneAllHinges
90
91open CausalSimplex4D
92open WickActionComplexFirst
93
94/-! ## §1. Generic principal-branch square-root lemmas (MODEL-level tools)
95
96Mathlib (this pin) has no `Complex.sqrt`; `csqrt z = z ^ (1/2 : ℂ)` is the
97landed principal-branch substitute (cut on `(-∞, 0]`). The lemmas here are
98the reusable analytic tools for every hinge class: non-vanishing, the open
99first-quadrant image of the open upper half-plane, evaluation on positive
100and negative reals, and continuity along paths confined to the CLOSED upper
101half-plane minus the origin (the closed arc `[0,1]` maps there; the
102Lorentzian endpoint sits ON the cut, which is exactly the boundary case the
103within-set log continuity of Mathlib handles). -/
104
105/-- THEOREM: `csqrt` never vanishes off the origin. -/
106theorem csqrt_ne_zero {w : ℂ} (hw : w ≠ 0) : csqrt w ≠ 0 := by
107 intro h
108 unfold csqrt at h
109 rw [Complex.cpow_eq_zero_iff] at h
110 exact hw h.1
111
112/-- THEOREM: the principal square root maps the open upper half-plane into
113the open first quadrant (`arg w ∈ (0, π)` halves to `(0, π/2)`). -/
114theorem csqrt_mem_Q1 {w : ℂ} (hw : 0 < w.im) :
115 0 < (csqrt w).re ∧ 0 < (csqrt w).im := by
116 have hne : w ≠ 0 := by
117 intro h
118 rw [h] at hw
119 simp at hw
120 have h12c : (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) := by norm_num
121 have harg_pos : 0 < Complex.arg w := by
122 rcases lt_or_eq_of_le (Complex.arg_nonneg_iff.mpr hw.le) with h | h
123 · exact h
124 · exfalso
125 have h0 := Complex.arg_eq_zero_iff.mp h.symm
126 exact absurd h0.2 (ne_of_gt hw)
127 have harg_lt : Complex.arg w < Real.pi := by
128 rcases lt_or_eq_of_le (Complex.arg_le_pi w) with h | h
129 · exact h
130 · exfalso
131 have hpi := Complex.arg_eq_pi_iff.mp h
132 exact absurd hpi.2 (ne_of_gt hw)
133 have hcs : csqrt w = Complex.exp (Complex.log w * (1 / 2 : ℂ)) := by
134 unfold csqrt
135 rw [Complex.cpow_def_of_ne_zero hne]
136 have him2 : (Complex.log w * (1 / 2 : ℂ)).im = Complex.arg w / 2 := by
137 rw [h12c, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im,
138 Complex.log_im]
139 ring
140 rw [hcs]
141 constructor
142 · rw [Complex.exp_re, him2]
143 refine mul_pos (Real.exp_pos _) (Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩)
144 · have := Real.pi_pos
145 linarith
146 · linarith
147 · rw [Complex.exp_im, him2]
148 refine mul_pos (Real.exp_pos _) (Real.sin_pos_of_pos_of_lt_pi ?_ ?_)
149 · linarith
150 · have := Real.pi_pos
151 linarith
152
153/-- THEOREM: on nonnegative reals the principal square root is the real
154square root. -/
155theorem csqrt_ofReal_nonneg {r : ℝ} (hr : 0 ≤ r) :
156 csqrt ((r : ℝ) : ℂ) = ((Real.sqrt r : ℝ) : ℂ) := by
157 unfold csqrt
158 rw [show (1 / 2 : ℂ) = (((1 / 2 : ℝ)) : ℂ) by norm_num,
159 ← Complex.ofReal_cpow hr, ← Real.sqrt_eq_rpow]
160
161/-- THEOREM: `csqrt 4 = 2` (the constant apex cofactor of every
162spacelike-class fourOne hinge). -/
163theorem csqrt_four : csqrt 4 = 2 := by
164 rw [show (4 : ℂ) = ((4 : ℝ) : ℂ) by norm_num,
165 csqrt_ofReal_nonneg (by norm_num : (0 : ℝ) ≤ 4),
166 show (4 : ℝ) = 2 ^ 2 by norm_num,
167 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
168 norm_num
169
170/-- THEOREM: on negative reals (approached within the closed upper
171half-plane, the arc's Lorentzian endpoint case) the principal square root
172is `sqrt (-r) * I` (`arg = π` halves to `π/2`). -/
173theorem csqrt_ofReal_neg {r : ℝ} (hr : r < 0) :
174 csqrt ((r : ℝ) : ℂ) = ((Real.sqrt (-r) : ℝ) : ℂ) * Complex.I := by
175 have hne : ((r : ℝ) : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr hr.ne
176 have h12c : (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) := by norm_num
177 have hlog_re : (Complex.log ((r : ℝ) : ℂ)).re = Real.log (-r) := by
178 rw [Complex.log_re, Complex.norm_real, Real.norm_eq_abs, abs_of_neg hr]
179 have hlog_im : (Complex.log ((r : ℝ) : ℂ)).im = Real.pi := by
180 rw [Complex.log_im, Complex.arg_ofReal_of_neg hr]
181 have hre2 : (Complex.log ((r : ℝ) : ℂ) * (1 / 2 : ℂ)).re
182 = Real.log (-r) / 2 := by
183 rw [h12c, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im,
184 hlog_re, hlog_im]
185 ring
186 have him2 : (Complex.log ((r : ℝ) : ℂ) * (1 / 2 : ℂ)).im
187 = Real.pi / 2 := by
188 rw [h12c, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im,
189 hlog_re, hlog_im]
190 ring
191 have hexp : Real.exp (Real.log (-r) / 2) = Real.sqrt (-r) := by
192 rw [Real.sqrt_eq_rpow, Real.rpow_def_of_pos (by linarith : (0 : ℝ) < -r),
193 mul_one_div]
194 unfold csqrt
195 rw [Complex.cpow_def_of_ne_zero hne]
196 apply Complex.ext
197 · rw [Complex.exp_re, hre2, him2, Real.cos_pi_div_two, mul_zero]
198 simp [Complex.mul_re]
199 · rw [Complex.exp_im, hre2, him2, Real.sin_pi_div_two, mul_one, hexp]
200 simp [Complex.mul_im]
201
202/-- THEOREM: the imaginary part of `-1/u` is strictly positive whenever
203`im u > 0` (the arccos-cut avoidance workhorse for the mixed-denominator
204hinge classes). -/
205theorem neg_one_div_im_pos {u : ℂ} (hu : 0 < u.im) :
206 0 < ((-1 : ℂ) / u).im := by
207 have hne : u ≠ 0 := by
208 intro h
209 rw [h] at hu
210 simp at hu
211 have h : ((-1 : ℂ) / u).im = u.im / Complex.normSq u := by
212 rw [Complex.div_im]
213 simp only [Complex.neg_im, Complex.one_im, Complex.neg_re,
214 Complex.one_re, neg_zero]
215 ring
216 rw [h]
217 exact div_pos hu (Complex.normSq_pos.mpr hne)
218
219/-- THEOREM: products of open-first-quadrant numbers stay in the open upper
220half-plane. -/
221theorem mul_im_pos_of_Q1 {u v : ℂ} (hu : 0 < u.re ∧ 0 < u.im)
222 (hv : 0 < v.re ∧ 0 < v.im) : 0 < (u * v).im := by
223 rw [Complex.mul_im]
224 exact add_pos (mul_pos hu.1 hv.2) (mul_pos hu.2 hv.1)
225
226/-- THEOREM: the arc's imaginary part is nonnegative on the CLOSED interval
227(`sin (π (1 - t)) ≥ 0` for `t ∈ [0, 1]`). -/
228theorem zArc_im_nonneg {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
229 0 ≤ (zArc t).im := by
230 rw [zArc_im]
231 apply Real.sin_nonneg_of_nonneg_of_le_pi
232 · exact mul_nonneg Real.pi_pos.le (by linarith [ht.2])
233 · calc Real.pi * (1 - t) ≤ Real.pi * 1 :=
234 mul_le_mul_of_nonneg_left (by linarith [ht.1]) Real.pi_pos.le
235 _ = Real.pi := mul_one _
236
237/-- THEOREM (path continuity of `csqrt` across the closed upper half-plane):
238if a continuous path never vanishes on `[0,1]` and keeps a nonnegative
239imaginary part there, then `csqrt` composed with it is continuous on the
240CLOSED interval. Off the cut this is the continuity of `cpow (1/2)` on
241`Complex.slitPlane`; ON the cut (negative reals, the Lorentzian endpoint
242case) it is Mathlib's one-sided log continuity within `{im ≥ 0}`
243(`Complex.continuousWithinAt_log_of_re_neg_of_im_zero`). -/
244theorem continuousOn_csqrt_comp {w : ℝ → ℂ} (hw : Continuous w)
245 (hne : ∀ t ∈ Set.Icc (0 : ℝ) 1, w t ≠ 0)
246 (him : ∀ t ∈ Set.Icc (0 : ℝ) 1, 0 ≤ (w t).im) :
247 ContinuousOn (fun t => csqrt (w t)) (Set.Icc 0 1) := by
248 intro t0 ht0
249 unfold csqrt
250 by_cases hs : w t0 ∈ Complex.slitPlane
251 · have hc : ContinuousAt (fun z : ℂ => z ^ (1 / 2 : ℂ)) (w t0) :=
252 continuousAt_cpow_const hs
253 exact (hc.comp hw.continuousAt).continuousWithinAt
254 · have hne0 := hne t0 ht0
255 rw [Complex.mem_slitPlane_iff] at hs
256 push_neg at hs
257 obtain ⟨hre_le, him0⟩ := hs
258 have hre : (w t0).re < 0 := by
259 rcases lt_or_eq_of_le hre_le with h | h
260 · exact h
261 · exfalso
262 apply hne0
263 apply Complex.ext
264 · simpa using h
265 · simpa using him0
266 have hlog : ContinuousWithinAt Complex.log {z : ℂ | 0 ≤ z.im} (w t0) :=
267 Complex.continuousWithinAt_log_of_re_neg_of_im_zero hre him0
268 have hg : ContinuousWithinAt
269 (fun z : ℂ => Complex.exp (Complex.log z * (1 / 2 : ℂ)))
270 {z : ℂ | 0 ≤ z.im} (w t0) :=
271 Complex.continuous_exp.continuousAt.comp_continuousWithinAt
272 (hlog.mul continuousWithinAt_const)
273 have hcomp : ContinuousWithinAt
274 (fun t => Complex.exp (Complex.log (w t) * (1 / 2 : ℂ)))
275 (Set.Icc 0 1) t0 :=
276 hg.comp hw.continuousWithinAt (fun t ht => him t ht)
277 refine hcomp.congr (fun t ht => ?_) ?_
278 · rw [Complex.cpow_def_of_ne_zero (hne t ht)]
279 · rw [Complex.cpow_def_of_ne_zero hne0]
280
281/-! ## §2. Cofactor symmetry (MODEL-level bookkeeping)
282
283The complex CM matrix is symmetric, so `C_{rc} = C_{cr}` and the split-form
284cosine is symmetric in its vertex pair. This lets every hinge be certified
285once, in a canonical pair orientation. -/
286
287/-- THEOREM: the complex CM matrix is symmetric. -/
288theorem cmMatrixC_symm (x : SqEdges10C) (i j : Fin 6) :
289 cmMatrixC x j i = cmMatrixC x i j := by
290 fin_cases i <;> fin_cases j <;> rfl
291
292/-- THEOREM: minors of the symmetric CM matrix are symmetric in
293(row, column). -/
294theorem cmMinorC_symm (x : SqEdges10C) (r c : Fin 6) :
295 cmMinorC x r c = cmMinorC x c r := by
296 unfold cmMinorC
297 rw [← Matrix.det_transpose
298 (Matrix.submatrix (cmMatrixC x) (Fin.succAbove c) (Fin.succAbove r))]
299 congr 1
300 ext i j
301 simp only [Matrix.submatrix_apply, Matrix.transpose_apply]
302 exact cmMatrixC_symm x (Fin.succAbove c j) (Fin.succAbove r i)
303
304/-- THEOREM: cofactors of the symmetric CM matrix are symmetric. -/
305theorem cmCofactorC_symm (x : SqEdges10C) (r c : Fin 6) :
306 cmCofactorC x r c = cmCofactorC x c r := by
307 unfold cmCofactorC cmCofactorSignC
308 rw [cmMinorC_symm, Nat.add_comm r.val c.val]
309
310/-- THEOREM: the split-form cosine is symmetric in the opposite pair. -/
311theorem dihedralCosSplitC_symm (x : SqEdges10C) (p q : Fin 5) :
312 dihedralCosSplitC x q p = dihedralCosSplitC x p q := by
313 unfold dihedralCosSplitC dihedralDenomSplitC
314 rw [cmCofactorC_symm, mul_comm]
315
316/-- THEOREM: branch regularity is symmetric in the opposite pair. -/
317theorem branchRegularOn_symm {x : ℝ → SqEdges10C} {p q : Fin 5} {s : Set ℝ}
318 (h : BranchRegularOn x p q s) : BranchRegularOn x q p s := by
319 intro t ht
320 obtain ⟨h1, h2, h3⟩ := h t ht
321 refine ⟨h2, h1, ?_⟩
322 rw [dihedralCosSplitC_symm]
323 exact h3
324
325/-! ## §3. Per-pair 5x5 minors of the fourOne matrix (kernel-checked)
326
327`hingeMatrixC` (landed) is the bordered 6x6 complex CM matrix of the
328fourOne tuple at spacelike value 1, timelike value `z`. Each opposite
329vertex pair `(p, q)` needs the minors at CM rows/columns `(p+1, q+1)`.
330The landed module covers CM `(3,3)`, `(4,4)`, `(3,4)`; everything else is
331built here explicitly and evaluated with the landed heavy-simp pattern.
332Every determinant below was cross-checked against exact sympy expansion
333before formalization. -/
334
335/-- The diagonal minor deleting CM row/col 1 (vertex 0) equals the landed
336`minorPPC` matrix (vertices 0..3 are interchangeable in the fourOne
337tuple). -/
338theorem submatrix41_11 (z : ℂ) :
339 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (1 : Fin 6))
340 (Fin.succAbove (1 : Fin 6)) = minorPPC z := by
341 ext i j
342 fin_cases i <;> fin_cases j <;> rfl
343
344/-- Diagonal minor at CM row/col 2 (vertex 1), again `minorPPC`. -/
345theorem submatrix41_22 (z : ℂ) :
346 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (2 : Fin 6))
347 (Fin.succAbove (2 : Fin 6)) = minorPPC z := by
348 ext i j
349 fin_cases i <;> fin_cases j <;> rfl
350
351/-- The apex diagonal minor (delete CM row/col 5, vertex 4): the regular
352unit tetrahedron CM matrix. -/
353def minor41_55C : Matrix (Fin 5) (Fin 5) ℂ :=
354 fun i j =>
355 match i.val, j.val with
356 | 0, 0 => 0
357 | 1, 1 => 0
358 | 2, 2 => 0
359 | 3, 3 => 0
360 | 4, 4 => 0
361 | _, _ => 1
362
363theorem submatrix41_55 (z : ℂ) :
364 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (5 : Fin 6))
365 (Fin.succAbove (5 : Fin 6)) = minor41_55C := by
366 ext i j
367 fin_cases i <;> fin_cases j <;> rfl
368
369set_option maxHeartbeats 8000000 in
370set_option maxRecDepth 16384 in
371/-- THEOREM (symbolic 5x5 determinant): the apex diagonal minor is the
372regular unit tetrahedron value 4 (`C_qq = 4`, trace constant). -/
373theorem det_minor41_55C : Matrix.det minor41_55C = 4 := by
374 unfold minor41_55C
375 -- Style note: bare `simp` retained deliberately, mirroring the proved
376 -- pattern of `WickActionComplexFirst.det_minorPPC`.
377 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
378 norm_num
379
380/-- Off-diagonal minor at CM (1,2) (opposite pair (0,1)). -/
381def minor41_12C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
382 fun i j =>
383 match i.val, j.val with
384 | 0, 0 => 0
385 | 1, 4 => z
386 | 2, 2 => 0
387 | 2, 4 => z
388 | 3, 3 => 0
389 | 3, 4 => z
390 | 4, 1 => z
391 | 4, 2 => z
392 | 4, 3 => z
393 | 4, 4 => 0
394 | _, _ => 1
395
396theorem submatrix41_12 (z : ℂ) :
397 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (1 : Fin 6))
398 (Fin.succAbove (2 : Fin 6)) = minor41_12C z := by
399 ext i j
400 fin_cases i <;> fin_cases j <;> rfl
401
402set_option maxHeartbeats 8000000 in
403set_option maxRecDepth 16384 in
404theorem det_minor41_12C (z : ℂ) : Matrix.det (minor41_12C z) = 2 * z - 1 := by
405 unfold minor41_12C
406 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
407 ring
408
409/-- Off-diagonal minor at CM (1,3) (opposite pair (0,2)). -/
410def minor41_13C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
411 fun i j =>
412 match i.val, j.val with
413 | 0, 0 => 0
414 | 1, 2 => 0
415 | 1, 4 => z
416 | 2, 4 => z
417 | 3, 3 => 0
418 | 3, 4 => z
419 | 4, 1 => z
420 | 4, 2 => z
421 | 4, 3 => z
422 | 4, 4 => 0
423 | _, _ => 1
424
425theorem submatrix41_13 (z : ℂ) :
426 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (1 : Fin 6))
427 (Fin.succAbove (3 : Fin 6)) = minor41_13C z := by
428 ext i j
429 fin_cases i <;> fin_cases j <;> rfl
430
431set_option maxHeartbeats 8000000 in
432set_option maxRecDepth 16384 in
433theorem det_minor41_13C (z : ℂ) : Matrix.det (minor41_13C z) = 1 - 2 * z := by
434 unfold minor41_13C
435 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
436 ring
437
438/-- Off-diagonal minor at CM (1,4) (opposite pair (0,3)). -/
439def minor41_14C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
440 fun i j =>
441 match i.val, j.val with
442 | 0, 0 => 0
443 | 1, 2 => 0
444 | 1, 4 => z
445 | 2, 3 => 0
446 | 2, 4 => z
447 | 3, 4 => z
448 | 4, 1 => z
449 | 4, 2 => z
450 | 4, 3 => z
451 | 4, 4 => 0
452 | _, _ => 1
453
454theorem submatrix41_14 (z : ℂ) :
455 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (1 : Fin 6))
456 (Fin.succAbove (4 : Fin 6)) = minor41_14C z := by
457 ext i j
458 fin_cases i <;> fin_cases j <;> rfl
459
460set_option maxHeartbeats 8000000 in
461set_option maxRecDepth 16384 in
462theorem det_minor41_14C (z : ℂ) : Matrix.det (minor41_14C z) = 2 * z - 1 := by
463 unfold minor41_14C
464 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
465 ring
466
467/-- Off-diagonal minor at CM (2,3) (opposite pair (1,2)). -/
468def minor41_23C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
469 fun i j =>
470 match i.val, j.val with
471 | 0, 0 => 0
472 | 1, 1 => 0
473 | 1, 4 => z
474 | 2, 4 => z
475 | 3, 3 => 0
476 | 3, 4 => z
477 | 4, 1 => z
478 | 4, 2 => z
479 | 4, 3 => z
480 | 4, 4 => 0
481 | _, _ => 1
482
483theorem submatrix41_23 (z : ℂ) :
484 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (2 : Fin 6))
485 (Fin.succAbove (3 : Fin 6)) = minor41_23C z := by
486 ext i j
487 fin_cases i <;> fin_cases j <;> rfl
488
489set_option maxHeartbeats 8000000 in
490set_option maxRecDepth 16384 in
491theorem det_minor41_23C (z : ℂ) : Matrix.det (minor41_23C z) = 2 * z - 1 := by
492 unfold minor41_23C
493 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
494 ring
495
496/-- Off-diagonal minor at CM (2,4) (opposite pair (1,3)). -/
497def minor41_24C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
498 fun i j =>
499 match i.val, j.val with
500 | 0, 0 => 0
501 | 1, 1 => 0
502 | 1, 4 => z
503 | 2, 3 => 0
504 | 2, 4 => z
505 | 3, 4 => z
506 | 4, 1 => z
507 | 4, 2 => z
508 | 4, 3 => z
509 | 4, 4 => 0
510 | _, _ => 1
511
512theorem submatrix41_24 (z : ℂ) :
513 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (2 : Fin 6))
514 (Fin.succAbove (4 : Fin 6)) = minor41_24C z := by
515 ext i j
516 fin_cases i <;> fin_cases j <;> rfl
517
518set_option maxHeartbeats 8000000 in
519set_option maxRecDepth 16384 in
520theorem det_minor41_24C (z : ℂ) : Matrix.det (minor41_24C z) = 1 - 2 * z := by
521 unfold minor41_24C
522 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
523 ring
524
525/-- Spacelike-class off-diagonal minor at CM (1,5) (opposite pair (0,4)). -/
526def minor41_15C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
527 fun i j =>
528 match i.val, j.val with
529 | 0, 0 => 0
530 | 1, 2 => 0
531 | 2, 3 => 0
532 | 3, 4 => 0
533 | 4, 1 => z
534 | 4, 2 => z
535 | 4, 3 => z
536 | 4, 4 => z
537 | _, _ => 1
538
539theorem submatrix41_15 (z : ℂ) :
540 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (1 : Fin 6))
541 (Fin.succAbove (5 : Fin 6)) = minor41_15C z := by
542 ext i j
543 fin_cases i <;> fin_cases j <;> rfl
544
545set_option maxHeartbeats 8000000 in
546set_option maxRecDepth 16384 in
547theorem det_minor41_15C (z : ℂ) : Matrix.det (minor41_15C z) = -1 := by
548 unfold minor41_15C
549 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
550 ring
551
552/-- Spacelike-class off-diagonal minor at CM (2,5) (opposite pair (1,4)). -/
553def minor41_25C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
554 fun i j =>
555 match i.val, j.val with
556 | 0, 0 => 0
557 | 1, 1 => 0
558 | 2, 3 => 0
559 | 3, 4 => 0
560 | 4, 1 => z
561 | 4, 2 => z
562 | 4, 3 => z
563 | 4, 4 => z
564 | _, _ => 1
565
566theorem submatrix41_25 (z : ℂ) :
567 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (2 : Fin 6))
568 (Fin.succAbove (5 : Fin 6)) = minor41_25C z := by
569 ext i j
570 fin_cases i <;> fin_cases j <;> rfl
571
572set_option maxHeartbeats 8000000 in
573set_option maxRecDepth 16384 in
574theorem det_minor41_25C (z : ℂ) : Matrix.det (minor41_25C z) = 1 := by
575 unfold minor41_25C
576 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
577 ring
578
579/-- Spacelike-class off-diagonal minor at CM (3,5) (opposite pair (2,4)). -/
580def minor41_35C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
581 fun i j =>
582 match i.val, j.val with
583 | 0, 0 => 0
584 | 1, 1 => 0
585 | 2, 2 => 0
586 | 3, 4 => 0
587 | 4, 1 => z
588 | 4, 2 => z
589 | 4, 3 => z
590 | 4, 4 => z
591 | _, _ => 1
592
593theorem submatrix41_35 (z : ℂ) :
594 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (3 : Fin 6))
595 (Fin.succAbove (5 : Fin 6)) = minor41_35C z := by
596 ext i j
597 fin_cases i <;> fin_cases j <;> rfl
598
599set_option maxHeartbeats 8000000 in
600set_option maxRecDepth 16384 in
601theorem det_minor41_35C (z : ℂ) : Matrix.det (minor41_35C z) = -1 := by
602 unfold minor41_35C
603 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
604 ring
605
606/-- Spacelike-class off-diagonal minor at CM (4,5) (opposite pair (3,4)). -/
607def minor41_45C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
608 fun i j =>
609 match i.val, j.val with
610 | 0, 0 => 0
611 | 1, 1 => 0
612 | 2, 2 => 0
613 | 3, 3 => 0
614 | 4, 1 => z
615 | 4, 2 => z
616 | 4, 3 => z
617 | 4, 4 => z
618 | _, _ => 1
619
620theorem submatrix41_45 (z : ℂ) :
621 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (4 : Fin 6))
622 (Fin.succAbove (5 : Fin 6)) = minor41_45C z := by
623 ext i j
624 fin_cases i <;> fin_cases j <;> rfl
625
626set_option maxHeartbeats 8000000 in
627set_option maxRecDepth 16384 in
628theorem det_minor41_45C (z : ℂ) : Matrix.det (minor41_45C z) = 1 := by
629 unfold minor41_45C
630 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
631 ring
632
633/-! ## §4. Cofactor closed forms per CM index pair (THEOREM)
634
635Trace receipt closed forms: diagonal cofactors `6z - 2` at CM 1..4 and `4`
636at CM 5; off-diagonal `1 - 2z` inside CM 1..4 and `-1` against CM 5. -/
637
638theorem cofactor41_d1 (z : ℂ) : cmCofactorC (hingeEdgesC z) 1 1 = 6 * z - 2 := by
639 unfold cmCofactorC cmCofactorSignC cmMinorC
640 rw [cmMatrixC_hingeEdges, submatrix41_11, det_minorPPC,
641 if_pos (by decide : Even ((1 : Fin 6).val + (1 : Fin 6).val))]
642 ring
643
644theorem cofactor41_d2 (z : ℂ) : cmCofactorC (hingeEdgesC z) 2 2 = 6 * z - 2 := by
645 unfold cmCofactorC cmCofactorSignC cmMinorC
646 rw [cmMatrixC_hingeEdges, submatrix41_22, det_minorPPC,
647 if_pos (by decide : Even ((2 : Fin 6).val + (2 : Fin 6).val))]
648 ring
649
650theorem cofactor41_d5 (z : ℂ) : cmCofactorC (hingeEdgesC z) 5 5 = 4 := by
651 unfold cmCofactorC cmCofactorSignC cmMinorC
652 rw [cmMatrixC_hingeEdges, submatrix41_55, det_minor41_55C,
653 if_pos (by decide : Even ((5 : Fin 6).val + (5 : Fin 6).val))]
654 ring
655
656theorem cofactor41_12 (z : ℂ) : cmCofactorC (hingeEdgesC z) 1 2 = 1 - 2 * z := by
657 unfold cmCofactorC cmCofactorSignC cmMinorC
658 rw [cmMatrixC_hingeEdges, submatrix41_12, det_minor41_12C,
659 if_neg (by decide : ¬ Even ((1 : Fin 6).val + (2 : Fin 6).val))]
660 ring
661
662theorem cofactor41_13 (z : ℂ) : cmCofactorC (hingeEdgesC z) 1 3 = 1 - 2 * z := by
663 unfold cmCofactorC cmCofactorSignC cmMinorC
664 rw [cmMatrixC_hingeEdges, submatrix41_13, det_minor41_13C,
665 if_pos (by decide : Even ((1 : Fin 6).val + (3 : Fin 6).val))]
666 ring
667
668theorem cofactor41_14 (z : ℂ) : cmCofactorC (hingeEdgesC z) 1 4 = 1 - 2 * z := by
669 unfold cmCofactorC cmCofactorSignC cmMinorC
670 rw [cmMatrixC_hingeEdges, submatrix41_14, det_minor41_14C,
671 if_neg (by decide : ¬ Even ((1 : Fin 6).val + (4 : Fin 6).val))]
672 ring
673
674theorem cofactor41_23 (z : ℂ) : cmCofactorC (hingeEdgesC z) 2 3 = 1 - 2 * z := by
675 unfold cmCofactorC cmCofactorSignC cmMinorC
676 rw [cmMatrixC_hingeEdges, submatrix41_23, det_minor41_23C,
677 if_neg (by decide : ¬ Even ((2 : Fin 6).val + (3 : Fin 6).val))]
678 ring
679
680theorem cofactor41_24 (z : ℂ) : cmCofactorC (hingeEdgesC z) 2 4 = 1 - 2 * z := by
681 unfold cmCofactorC cmCofactorSignC cmMinorC
682 rw [cmMatrixC_hingeEdges, submatrix41_24, det_minor41_24C,
683 if_pos (by decide : Even ((2 : Fin 6).val + (4 : Fin 6).val))]
684 ring
685
686theorem cofactor41_15 (z : ℂ) : cmCofactorC (hingeEdgesC z) 1 5 = -1 := by
687 unfold cmCofactorC cmCofactorSignC cmMinorC
688 rw [cmMatrixC_hingeEdges, submatrix41_15, det_minor41_15C,
689 if_pos (by decide : Even ((1 : Fin 6).val + (5 : Fin 6).val))]
690 ring
691
692theorem cofactor41_25 (z : ℂ) : cmCofactorC (hingeEdgesC z) 2 5 = -1 := by
693 unfold cmCofactorC cmCofactorSignC cmMinorC
694 rw [cmMatrixC_hingeEdges, submatrix41_25, det_minor41_25C,
695 if_neg (by decide : ¬ Even ((2 : Fin 6).val + (5 : Fin 6).val))]
696 ring
697
698theorem cofactor41_35 (z : ℂ) : cmCofactorC (hingeEdgesC z) 3 5 = -1 := by
699 unfold cmCofactorC cmCofactorSignC cmMinorC
700 rw [cmMatrixC_hingeEdges, submatrix41_35, det_minor41_35C,
701 if_pos (by decide : Even ((3 : Fin 6).val + (5 : Fin 6).val))]
702 ring
703
704theorem cofactor41_45 (z : ℂ) : cmCofactorC (hingeEdgesC z) 4 5 = -1 := by
705 unfold cmCofactorC cmCofactorSignC cmMinorC
706 rw [cmMatrixC_hingeEdges, submatrix41_45, det_minor41_45C,
707 if_neg (by decide : ¬ Even ((4 : Fin 6).val + (5 : Fin 6).val))]
708 ring
709
710/-! ## §5. The two hinge classes, parametrically (THEOREM) -/
711
712/-- The split-form cosine path of the opposite pair `(p, q)` along the
713physical fourOne arc (MODEL; generalizes the landed `hingeCosPath`, which
714is the case `p = 2`, `q = 3`). -/
715noncomputable def fourOneCosPath (p q : Fin 5) (t : ℝ) : ℂ :=
716 dihedralCosSplitC (continuationEdgesC CausalPentType.fourOne 1 1 t) p q
717
718theorem fourOneCosPath_symm (p q : Fin 5) :
719 fourOneCosPath q p = fourOneCosPath p q :=
720 funext fun _ => dihedralCosSplitC_symm _ p q
721
722theorem fourOneCosPath_apply_symm (p q : Fin 5) (t : ℝ) :
723 fourOneCosPath q p t = fourOneCosPath p q t :=
724 dihedralCosSplitC_symm _ p q
725
726/-- Transport of the boundary-continuation package across the pair swap. -/
727theorem boundary_symm {p q : Fin 5}
728 (h : ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
729 ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ)) :
730 ContinuousOn (fourOneCosPath q p) (Set.Icc 0 1)
731 ∧ fourOneCosPath q p 1 = -(1 / 4 : ℂ) := by
732 rw [fourOneCosPath_symm p q]
733 exact h
734
735/-- THEOREM (timelike-class collapse): with both diagonal cofactors
736`6z - 2` and numerator `1 - 2z`, the split cosine collapses to the cut-free
737rational function everywhere on the arc. -/
738theorem fourOneCosPath_eq_timelike (p q : Fin 5)
739 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
740 (cmVertexIndexC p) (cmVertexIndexC p) = 6 * z - 2)
741 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
742 (cmVertexIndexC q) (cmVertexIndexC q) = 6 * z - 2)
743 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
744 (cmVertexIndexC p) (cmVertexIndexC q) = 1 - 2 * z) (t : ℝ) :
745 fourOneCosPath p q t = (1 - 2 * zArc t) / (6 * zArc t - 2) := by
746 unfold fourOneCosPath dihedralCosSplitC dihedralDenomSplitC
747 rw [continuationEdgesC_physical, hpp, hqq, hpq, csqrt_mul_self (denom_ne t)]
748
749/-- THEOREM (spacelike-class collapse): with diagonal cofactors `6z - 2`
750and `4` and numerator `-1`, the split cosine is `-1 / (csqrt (6z-2) * 2)`
751everywhere on the arc. -/
752theorem fourOneCosPath_eq_spacelike (p q : Fin 5)
753 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
754 (cmVertexIndexC p) (cmVertexIndexC p) = 6 * z - 2)
755 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
756 (cmVertexIndexC q) (cmVertexIndexC q) = 4)
757 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
758 (cmVertexIndexC p) (cmVertexIndexC q) = -1) (t : ℝ) :
759 fourOneCosPath p q t = -1 / (csqrt (6 * zArc t - 2) * 2) := by
760 unfold fourOneCosPath dihedralCosSplitC dihedralDenomSplitC
761 rw [continuationEdgesC_physical, hpp, hqq, hpq, csqrt_four]
762
763/-- THEOREM (timelike-class branch certificate, parametric): full open
764interior, exactly the landed single-hinge argument. -/
765theorem branchRegular_fourOne_timelike_pair (p q : Fin 5)
766 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
767 (cmVertexIndexC p) (cmVertexIndexC p) = 6 * z - 2)
768 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
769 (cmVertexIndexC q) (cmVertexIndexC q) = 6 * z - 2)
770 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
771 (cmVertexIndexC p) (cmVertexIndexC q) = 1 - 2 * z) :
772 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
773 p q (Set.Ioo 0 1) := by
774 intro t ht
775 dsimp only
776 have hy : 0 < (zArc t).im := zArc_im_pos ht
777 have him6 : (6 * zArc t - 2).im = 6 * (zArc t).im := by
778 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
779 Complex.im_ofNat]
780 ring
781 have hslit : 6 * zArc t - 2 ∈ Complex.slitPlane := by
782 apply Complex.mem_slitPlane_iff.mpr
783 right
784 rw [him6]
785 exact (mul_pos (by norm_num : (0 : ℝ) < 6) hy).ne'
786 refine ⟨?_, ?_, ?_⟩
787 · rw [continuationEdgesC_physical, hpp]
788 exact hslit
789 · rw [continuationEdgesC_physical, hqq]
790 exact hslit
791 · left
792 have hcos : dihedralCosSplitC
793 (continuationEdgesC CausalPentType.fourOne 1 1 t) p q
794 = (1 - 2 * zArc t) / (6 * zArc t - 2) :=
795 fourOneCosPath_eq_timelike p q hpp hqq hpq t
796 rw [hcos]
797 have hnum : (1 - 2 * zArc t).im * (6 * zArc t - 2).re
798 - (1 - 2 * zArc t).re * (6 * zArc t - 2).im = -2 * (zArc t).im := by
799 simp only [Complex.sub_im, Complex.sub_re, Complex.mul_im,
800 Complex.mul_re, Complex.one_im, Complex.one_re, Complex.re_ofNat,
801 Complex.im_ofNat]
802 ring
803 have hdiv : ((1 - 2 * zArc t) / (6 * zArc t - 2)).im
804 = (-2 * (zArc t).im) / Complex.normSq (6 * zArc t - 2) := by
805 rw [Complex.div_im, div_sub_div_same, hnum]
806 rw [hdiv]
807 apply div_ne_zero
808 · exact ne_of_lt (mul_neg_of_neg_of_pos (by norm_num) hy)
809 · exact (Complex.normSq_pos.mpr (denom_ne t)).ne'
810
811/-- THEOREM (spacelike-class branch certificate, parametric): the apex
812cofactor is the positive constant 4 (trivially off the cut), the lower
813cofactor stays in the open upper half-plane, and the cosine
814`-1 / (csqrt (6z-2) * 2)` has strictly positive imaginary part on the
815interior because `csqrt (6z-2)` lies in the open first quadrant. -/
816theorem branchRegular_fourOne_spacelike_pair (p q : Fin 5)
817 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
818 (cmVertexIndexC p) (cmVertexIndexC p) = 6 * z - 2)
819 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
820 (cmVertexIndexC q) (cmVertexIndexC q) = 4)
821 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
822 (cmVertexIndexC p) (cmVertexIndexC q) = -1) :
823 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
824 p q (Set.Ioo 0 1) := by
825 intro t ht
826 dsimp only
827 have hy : 0 < (zArc t).im := zArc_im_pos ht
828 have him6 : (6 * zArc t - 2).im = 6 * (zArc t).im := by
829 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
830 Complex.im_ofNat]
831 ring
832 have hup : 0 < (6 * zArc t - 2).im := by
833 rw [him6]
834 exact mul_pos (by norm_num : (0 : ℝ) < 6) hy
835 refine ⟨?_, ?_, ?_⟩
836 · rw [continuationEdgesC_physical, hpp]
837 exact Complex.mem_slitPlane_iff.mpr (Or.inr hup.ne')
838 · rw [continuationEdgesC_physical, hqq]
839 exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
840 · left
841 have hcos : dihedralCosSplitC
842 (continuationEdgesC CausalPentType.fourOne 1 1 t) p q
843 = -1 / (csqrt (6 * zArc t - 2) * 2) :=
844 fourOneCosPath_eq_spacelike p q hpp hqq hpq t
845 rw [hcos]
846 have hq1 := csqrt_mem_Q1 hup
847 have hden : 0 < (csqrt (6 * zArc t - 2) * 2).im := by
848 rw [Complex.mul_im]
849 simp only [Complex.re_ofNat, Complex.im_ofNat, mul_zero, zero_add]
850 linarith [hq1.2]
851 exact (neg_one_div_im_pos hden).ne'
852
853/-- THEOREM (timelike-class boundary continuation, parametric):
854continuous on the CLOSED interval, Lorentzian value `-(3/8)`, Euclidean
855value `-(1/4)`. -/
856theorem boundary_fourOne_timelike_pair (p q : Fin 5)
857 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
858 (cmVertexIndexC p) (cmVertexIndexC p) = 6 * z - 2)
859 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
860 (cmVertexIndexC q) (cmVertexIndexC q) = 6 * z - 2)
861 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
862 (cmVertexIndexC p) (cmVertexIndexC q) = 1 - 2 * z) :
863 ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
864 ∧ fourOneCosPath p q 0 = -(3 / 8 : ℂ)
865 ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
866 have heq := fourOneCosPath_eq_timelike p q hpp hqq hpq
867 refine ⟨?_, ?_, ?_⟩
868 · have hmo : Continuous fun t => (1 - 2 * zArc t) / (6 * zArc t - 2) := by
869 apply Continuous.div
870 · exact continuous_const.sub (continuous_const.mul continuous_zArc)
871 · exact (continuous_const.mul continuous_zArc).sub continuous_const
872 · exact fun t => denom_ne t
873 exact hmo.continuousOn.congr fun t _ => heq t
874 · rw [heq 0, zArc_zero]
875 norm_num
876 · rw [heq 1, zArc_one]
877 norm_num
878
879/-- THEOREM (spacelike-class boundary continuation, parametric):
880continuous on the CLOSED interval (via the closed-upper-half-plane
881continuity of `csqrt` along the arc; the Lorentzian endpoint has the
882cofactor `-8` ON the cut boundary, an allowed endpoint contact), Lorentzian
883value `(sqrt 2 / 8) * I` (purely imaginary), Euclidean value `-(1/4)`. -/
884theorem boundary_fourOne_spacelike_pair (p q : Fin 5)
885 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
886 (cmVertexIndexC p) (cmVertexIndexC p) = 6 * z - 2)
887 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
888 (cmVertexIndexC q) (cmVertexIndexC q) = 4)
889 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdgesC z)
890 (cmVertexIndexC p) (cmVertexIndexC q) = -1) :
891 ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
892 ∧ fourOneCosPath p q 0 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I
893 ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
894 have heq := fourOneCosPath_eq_spacelike p q hpp hqq hpq
895 have hwcont : Continuous fun t => 6 * zArc t - 2 :=
896 (continuous_const.mul continuous_zArc).sub continuous_const
897 have him6 : ∀ t : ℝ, (6 * zArc t - 2).im = 6 * (zArc t).im := by
898 intro t
899 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
900 Complex.im_ofNat]
901 ring
902 refine ⟨?_, ?_, ?_⟩
903 · have hcs : ContinuousOn (fun t => csqrt (6 * zArc t - 2))
904 (Set.Icc 0 1) := by
905 apply continuousOn_csqrt_comp hwcont (fun t _ => denom_ne t)
906 intro t ht
907 rw [him6]
908 exact mul_nonneg (by norm_num) (zArc_im_nonneg ht)
909 have hdiv : ContinuousOn (fun t => -1 / (csqrt (6 * zArc t - 2) * 2))
910 (Set.Icc 0 1) := by
911 apply ContinuousOn.div continuousOn_const (hcs.mul continuousOn_const)
912 intro t _
913 exact mul_ne_zero (csqrt_ne_zero (denom_ne t)) two_ne_zero
914 exact hdiv.congr fun t _ => heq t
915 · rw [heq 0, zArc_zero]
916 have h8 : (6 * (-1 : ℂ) - 2) = ((-8 : ℝ) : ℂ) := by norm_num
917 rw [h8, csqrt_ofReal_neg (by norm_num : (-8 : ℝ) < 0)]
918 have h82 : Real.sqrt (-(-8 : ℝ)) = 2 * Real.sqrt 2 := by
919 rw [show -(-8 : ℝ) = 2 ^ 2 * 2 by norm_num,
920 Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ (2 : ℝ) ^ 2),
921 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
922 rw [h82]
923 have hS : ((Real.sqrt 2 : ℝ) : ℂ) * ((Real.sqrt 2 : ℝ) : ℂ) = 2 := by
924 rw [← Complex.ofReal_mul,
925 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
926 norm_num
927 have hden : (((2 * Real.sqrt 2 : ℝ) : ℂ) * Complex.I) * 2 ≠ 0 := by
928 refine mul_ne_zero (mul_ne_zero ?_ Complex.I_ne_zero) two_ne_zero
929 exact Complex.ofReal_ne_zero.mpr
930 (ne_of_gt (mul_pos two_pos (Real.sqrt_pos.mpr (by norm_num))))
931 rw [div_eq_iff hden]
932 push_cast
933 linear_combination (-(Complex.I * Complex.I) / 2) * hS
934 - Complex.I_mul_I
935 · rw [heq 1, zArc_one]
936 have h4 : (6 * (1 : ℂ) - 2) = 4 := by norm_num
937 rw [h4, csqrt_four]
938 norm_num
939
940/-! ## §6. The ten instantiated hinges and the all-hinge headlines -/
941
942/-- Pair (0,1): hinge (2,3,4), timelike class. -/
943theorem branchRegular_pair01 :
944 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
945 0 1 (Set.Ioo 0 1) :=
946 branchRegular_fourOne_timelike_pair 0 1 cofactor41_d1 cofactor41_d2
947 cofactor41_12
948
949/-- Pair (0,2): hinge (1,3,4), timelike class. -/
950theorem branchRegular_pair02 :
951 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
952 0 2 (Set.Ioo 0 1) :=
953 branchRegular_fourOne_timelike_pair 0 2 cofactor41_d1 cofactor_pp
954 cofactor41_13
955
956/-- Pair (0,3): hinge (1,2,4), timelike class. -/
957theorem branchRegular_pair03 :
958 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
959 0 3 (Set.Ioo 0 1) :=
960 branchRegular_fourOne_timelike_pair 0 3 cofactor41_d1 cofactor_qq
961 cofactor41_14
962
963/-- Pair (1,2): hinge (0,3,4), timelike class. -/
964theorem branchRegular_pair12 :
965 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
966 1 2 (Set.Ioo 0 1) :=
967 branchRegular_fourOne_timelike_pair 1 2 cofactor41_d2 cofactor_pp
968 cofactor41_23
969
970/-- Pair (1,3): hinge (0,2,4), timelike class. -/
971theorem branchRegular_pair13 :
972 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
973 1 3 (Set.Ioo 0 1) :=
974 branchRegular_fourOne_timelike_pair 1 3 cofactor41_d2 cofactor_qq
975 cofactor41_24
976
977/-- Pair (2,3): hinge (0,1,4), the landed traced hinge. -/
978theorem branchRegular_pair23 :
979 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
980 2 3 (Set.Ioo 0 1) :=
981 branchRegular_fourOne_timelike_pair 2 3 cofactor_pp cofactor_qq cofactor_pq
982
983/-- Pair (0,4): hinge (1,2,3), spacelike class. -/
984theorem branchRegular_pair04 :
985 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
986 0 4 (Set.Ioo 0 1) :=
987 branchRegular_fourOne_spacelike_pair 0 4 cofactor41_d1 cofactor41_d5
988 cofactor41_15
989
990/-- Pair (1,4): hinge (0,2,3), spacelike class. -/
991theorem branchRegular_pair14 :
992 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
993 1 4 (Set.Ioo 0 1) :=
994 branchRegular_fourOne_spacelike_pair 1 4 cofactor41_d2 cofactor41_d5
995 cofactor41_25
996
997/-- Pair (2,4): hinge (0,1,3), spacelike class. -/
998theorem branchRegular_pair24 :
999 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
1000 2 4 (Set.Ioo 0 1) :=
1001 branchRegular_fourOne_spacelike_pair 2 4 cofactor_pp cofactor41_d5
1002 cofactor41_35
1003
1004/-- Pair (3,4): hinge (0,1,2), spacelike class. -/
1005theorem branchRegular_pair34 :
1006 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
1007 3 4 (Set.Ioo 0 1) :=
1008 branchRegular_fourOne_spacelike_pair 3 4 cofactor_qq cofactor41_d5
1009 cofactor41_45
1010
1011/-- THEOREM (B1 headline, branch certificates): for EVERY hinge of the
1012fourOne causal 4-simplex (every unordered opposite vertex pair, both
1013orientations), the split-form continuation is branch-regular on the FULL
1014open arc interior at the physical point `a = 1`, `alpha = 1`. The ten
1015hinges: (0,1,2)|(3,4), (0,1,3)|(2,4), (0,1,4)|(2,3), (0,2,3)|(1,4),
1016(0,2,4)|(1,3), (0,3,4)|(1,2), (1,2,3)|(0,4), (1,2,4)|(0,3),
1017(1,3,4)|(0,2), (2,3,4)|(0,1). -/
1018theorem branchRegular_fourOne_allHinges :
1019 ∀ p q : Fin 5, p ≠ q →
1020 BranchRegularOn
1021 (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
1022 (Set.Ioo 0 1) := by
1023 intro p q hpq
1024 fin_cases p <;> fin_cases q
1025 · exact absurd rfl hpq
1026 · exact branchRegular_pair01
1027 · exact branchRegular_pair02
1028 · exact branchRegular_pair03
1029 · exact branchRegular_pair04
1030 · exact branchRegularOn_symm branchRegular_pair01
1031 · exact absurd rfl hpq
1032 · exact branchRegular_pair12
1033 · exact branchRegular_pair13
1034 · exact branchRegular_pair14
1035 · exact branchRegularOn_symm branchRegular_pair02
1036 · exact branchRegularOn_symm branchRegular_pair12
1037 · exact absurd rfl hpq
1038 · exact branchRegular_pair23
1039 · exact branchRegular_pair24
1040 · exact branchRegularOn_symm branchRegular_pair03
1041 · exact branchRegularOn_symm branchRegular_pair13
1042 · exact branchRegularOn_symm branchRegular_pair23
1043 · exact absurd rfl hpq
1044 · exact branchRegular_pair34
1045 · exact branchRegularOn_symm branchRegular_pair04
1046 · exact branchRegularOn_symm branchRegular_pair14
1047 · exact branchRegularOn_symm branchRegular_pair24
1048 · exact branchRegularOn_symm branchRegular_pair34
1049 · exact absurd rfl hpq
1050
1051theorem boundary_pair01 :
1052 ContinuousOn (fourOneCosPath 0 1) (Set.Icc 0 1)
1053 ∧ fourOneCosPath 0 1 0 = -(3 / 8 : ℂ)
1054 ∧ fourOneCosPath 0 1 1 = -(1 / 4 : ℂ) :=
1055 boundary_fourOne_timelike_pair 0 1 cofactor41_d1 cofactor41_d2 cofactor41_12
1056
1057theorem boundary_pair02 :
1058 ContinuousOn (fourOneCosPath 0 2) (Set.Icc 0 1)
1059 ∧ fourOneCosPath 0 2 0 = -(3 / 8 : ℂ)
1060 ∧ fourOneCosPath 0 2 1 = -(1 / 4 : ℂ) :=
1061 boundary_fourOne_timelike_pair 0 2 cofactor41_d1 cofactor_pp cofactor41_13
1062
1063theorem boundary_pair03 :
1064 ContinuousOn (fourOneCosPath 0 3) (Set.Icc 0 1)
1065 ∧ fourOneCosPath 0 3 0 = -(3 / 8 : ℂ)
1066 ∧ fourOneCosPath 0 3 1 = -(1 / 4 : ℂ) :=
1067 boundary_fourOne_timelike_pair 0 3 cofactor41_d1 cofactor_qq cofactor41_14
1068
1069theorem boundary_pair12 :
1070 ContinuousOn (fourOneCosPath 1 2) (Set.Icc 0 1)
1071 ∧ fourOneCosPath 1 2 0 = -(3 / 8 : ℂ)
1072 ∧ fourOneCosPath 1 2 1 = -(1 / 4 : ℂ) :=
1073 boundary_fourOne_timelike_pair 1 2 cofactor41_d2 cofactor_pp cofactor41_23
1074
1075theorem boundary_pair13 :
1076 ContinuousOn (fourOneCosPath 1 3) (Set.Icc 0 1)
1077 ∧ fourOneCosPath 1 3 0 = -(3 / 8 : ℂ)
1078 ∧ fourOneCosPath 1 3 1 = -(1 / 4 : ℂ) :=
1079 boundary_fourOne_timelike_pair 1 3 cofactor41_d2 cofactor_qq cofactor41_24
1080
1081theorem boundary_pair23 :
1082 ContinuousOn (fourOneCosPath 2 3) (Set.Icc 0 1)
1083 ∧ fourOneCosPath 2 3 0 = -(3 / 8 : ℂ)
1084 ∧ fourOneCosPath 2 3 1 = -(1 / 4 : ℂ) :=
1085 boundary_fourOne_timelike_pair 2 3 cofactor_pp cofactor_qq cofactor_pq
1086
1087theorem boundary_pair04 :
1088 ContinuousOn (fourOneCosPath 0 4) (Set.Icc 0 1)
1089 ∧ fourOneCosPath 0 4 0 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I
1090 ∧ fourOneCosPath 0 4 1 = -(1 / 4 : ℂ) :=
1091 boundary_fourOne_spacelike_pair 0 4 cofactor41_d1 cofactor41_d5 cofactor41_15
1092
1093theorem boundary_pair14 :
1094 ContinuousOn (fourOneCosPath 1 4) (Set.Icc 0 1)
1095 ∧ fourOneCosPath 1 4 0 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I
1096 ∧ fourOneCosPath 1 4 1 = -(1 / 4 : ℂ) :=
1097 boundary_fourOne_spacelike_pair 1 4 cofactor41_d2 cofactor41_d5 cofactor41_25
1098
1099theorem boundary_pair24 :
1100 ContinuousOn (fourOneCosPath 2 4) (Set.Icc 0 1)
1101 ∧ fourOneCosPath 2 4 0 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I
1102 ∧ fourOneCosPath 2 4 1 = -(1 / 4 : ℂ) :=
1103 boundary_fourOne_spacelike_pair 2 4 cofactor_pp cofactor41_d5 cofactor41_35
1104
1105theorem boundary_pair34 :
1106 ContinuousOn (fourOneCosPath 3 4) (Set.Icc 0 1)
1107 ∧ fourOneCosPath 3 4 0 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I
1108 ∧ fourOneCosPath 3 4 1 = -(1 / 4 : ℂ) :=
1109 boundary_fourOne_spacelike_pair 3 4 cofactor_qq cofactor41_d5 cofactor41_45
1110
1111/-- THEOREM (B1 headline, boundary continuation): every split-form cosine
1112path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and
1113ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator
1114convention of the landed module; textbook `-C` interior cosine `+1/4`). -/
1115theorem wick_boundary_continuation_fourOne_allHinges :
1116 ∀ p q : Fin 5, p ≠ q →
1117 ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
1118 ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
1119 intro p q hpq
1120 fin_cases p <;> fin_cases q
1121 · exact absurd rfl hpq
1122 · exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩
1123 · exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩
1124 · exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩
1125 · exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩
1126 · exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩
1127 · exact absurd rfl hpq
1128 · exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩
1129 · exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩
1130 · exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩
1131 · exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩
1132 · exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩
1133 · exact absurd rfl hpq
1134 · exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩
1135 · exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩
1136 · exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩
1137 · exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩
1138 · exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩
1139 · exact absurd rfl hpq
1140 · exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩
1141 · exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩
1142 · exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩
1143 · exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩
1144 · exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩
1145 · exact absurd rfl hpq
1146
1147/-- THEOREM (B1 headline, Lorentzian endpoint values): the split-form value
1148at `t = 0` is `-(3/8)` for every timelike-class hinge (opposite pair inside
1149`{0,1,2,3}`; the documented sign factor of the landed module applies) and
1150the purely imaginary `(sqrt 2 / 8) * I` for every spacelike-class hinge
1151(opposite pair containing the apex). No unrestricted equality with the
1152real Lorentzian formula is claimed. -/
1153theorem fourOne_lorentzian_endpoint_values :
1154 (∀ p q : Fin 5, p ≠ q → p ≠ 4 → q ≠ 4 →
1155 fourOneCosPath p q 0 = -(3 / 8 : ℂ))
1156 ∧ (∀ p : Fin 5, p ≠ 4 →
1157 fourOneCosPath p 4 0 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I
1158 ∧ fourOneCosPath 4 p 0
1159 = ((Real.sqrt 2 / 8 : ℝ) : ℂ) * Complex.I) := by
1160 constructor
1161 · intro p q hpq hp4 hq4
1162 fin_cases p <;> fin_cases q
1163 · exact absurd rfl hpq
1164 · exact boundary_pair01.2.1
1165 · exact boundary_pair02.2.1
1166 · exact boundary_pair03.2.1
1167 · exact absurd rfl hq4
1168 · exact (fourOneCosPath_apply_symm 0 1 0).trans boundary_pair01.2.1
1169 · exact absurd rfl hpq
1170 · exact boundary_pair12.2.1
1171 · exact boundary_pair13.2.1
1172 · exact absurd rfl hq4
1173 · exact (fourOneCosPath_apply_symm 0 2 0).trans boundary_pair02.2.1
1174 · exact (fourOneCosPath_apply_symm 1 2 0).trans boundary_pair12.2.1
1175 · exact absurd rfl hpq
1176 · exact boundary_pair23.2.1
1177 · exact absurd rfl hq4
1178 · exact (fourOneCosPath_apply_symm 0 3 0).trans boundary_pair03.2.1
1179 · exact (fourOneCosPath_apply_symm 1 3 0).trans boundary_pair13.2.1
1180 · exact (fourOneCosPath_apply_symm 2 3 0).trans boundary_pair23.2.1
1181 · exact absurd rfl hpq
1182 · exact absurd rfl hq4
1183 · exact absurd rfl hp4
1184 · exact absurd rfl hp4
1185 · exact absurd rfl hp4
1186 · exact absurd rfl hp4
1187 · exact absurd rfl hp4
1188 · intro p hp4
1189 fin_cases p
1190 · exact ⟨boundary_pair04.2.1,
1191 (fourOneCosPath_apply_symm 0 4 0).trans boundary_pair04.2.1⟩
1192 · exact ⟨boundary_pair14.2.1,
1193 (fourOneCosPath_apply_symm 1 4 0).trans boundary_pair14.2.1⟩
1194 · exact ⟨boundary_pair24.2.1,
1195 (fourOneCosPath_apply_symm 2 4 0).trans boundary_pair24.2.1⟩
1196 · exact ⟨boundary_pair34.2.1,
1197 (fourOneCosPath_apply_symm 3 4 0).trans boundary_pair34.2.1⟩
1198 · exact absurd rfl hp4
1199
1200/-! ## §7. Hinge areas-squared: closed forms and cut avoidance (THEOREM)
1201
1202The remaining hinge datum. Two triangle shapes occur (`(1, z, z)` for
1203timelike-class hinges and `(1, 1, 1)` for spacelike-class hinges); the
1204`(z, z, 1)` shape is proved here as well for the threeTwo module. -/
1205
1206set_option maxHeartbeats 2000000 in
1207/-- THEOREM (4x4 symbolic determinant): `triangleAreaSqC 1 z z
1208= z/4 - 1/16` (the timelike-class hinge shape). -/
1209theorem triangleAreaSqC_one_z_z (z : ℂ) :
1210 triangleAreaSqC 1 z z = z / 4 - 1 / 16 := by
1211 unfold triangleAreaSqC triCMMatrixC
1212 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
1213 ring
1214
1215set_option maxHeartbeats 2000000 in
1216/-- THEOREM (4x4 symbolic determinant): `triangleAreaSqC z z 1
1217= z/4 - 1/16` (the threeTwo upper-pair hinge shape). -/
1218theorem triangleAreaSqC_z_z_one (z : ℂ) :
1219 triangleAreaSqC z z 1 = z / 4 - 1 / 16 := by
1220 unfold triangleAreaSqC triCMMatrixC
1221 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
1222 ring
1223
1224set_option maxHeartbeats 2000000 in
1225/-- THEOREM (4x4 symbolic determinant): the regular unit triangle,
1226`triangleAreaSqC 1 1 1 = 3/16`. -/
1227theorem triangleAreaSqC_ones : triangleAreaSqC 1 1 1 = (3 / 16 : ℂ) := by
1228 unfold triangleAreaSqC triCMMatrixC
1229 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
1230 norm_num
1231
1232/-- THEOREM: closed forms of the four spacelike-class fourOne hinge
1233areas-squared: constant `3/16` (all three triangle edges spacelike). -/
1234theorem fourOne_areaSq_spacelike (z : ℂ) :
1235 hingeAreaSqC (hingeEdgesC z) 0 1 2 = (3 / 16 : ℂ)
1236 ∧ hingeAreaSqC (hingeEdgesC z) 0 1 3 = (3 / 16 : ℂ)
1237 ∧ hingeAreaSqC (hingeEdgesC z) 0 2 3 = (3 / 16 : ℂ)
1238 ∧ hingeAreaSqC (hingeEdgesC z) 1 2 3 = (3 / 16 : ℂ) := by
1239 refine ⟨?_, ?_, ?_, ?_⟩ <;>
1240 exact triangleAreaSqC_ones
1241
1242/-- THEOREM: closed forms of the six timelike-class fourOne hinge
1243areas-squared: `z/4 - 1/16` (one spacelike edge, two timelike edges to the
1244apex). The landed `hingeAreaSqC_closed` is the (0,1,4) case. -/
1245theorem fourOne_areaSq_timelike (z : ℂ) :
1246 hingeAreaSqC (hingeEdgesC z) 0 1 4 = z / 4 - 1 / 16
1247 ∧ hingeAreaSqC (hingeEdgesC z) 0 2 4 = z / 4 - 1 / 16
1248 ∧ hingeAreaSqC (hingeEdgesC z) 0 3 4 = z / 4 - 1 / 16
1249 ∧ hingeAreaSqC (hingeEdgesC z) 1 2 4 = z / 4 - 1 / 16
1250 ∧ hingeAreaSqC (hingeEdgesC z) 1 3 4 = z / 4 - 1 / 16
1251 ∧ hingeAreaSqC (hingeEdgesC z) 2 3 4 = z / 4 - 1 / 16 := by
1252 refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;>
1253 exact triangleAreaSqC_one_z_z z
1254
1255/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the
1256sqrt cut EVERYWHERE (both endpoints included), and the timelike-class
1257area-squared `z/4 - 1/16` avoids it on the full open interior (its
1258Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED
1259endpoint contact documented in the landed module). -/
1260theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
1261 ((3 / 16 : ℂ) ∈ Complex.slitPlane)
1262 ∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by
1263 constructor
1264 · exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
1265 · apply Complex.mem_slitPlane_iff.mpr
1266 right
1267 have hy : 0 < (zArc t).im := zArc_im_pos ht
1268 have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
1269 simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
1270 ring
1271 rw [him]
1272 exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'
1273
1274/-! ## §8. Axiom audit
1275
1276Expected for each: `[propext, Classical.choice, Quot.sound]`. -/
1277
1278#print axioms branchRegular_fourOne_allHinges
1279#print axioms wick_boundary_continuation_fourOne_allHinges
1280#print axioms fourOne_lorentzian_endpoint_values
1281#print axioms fourOne_areaSq_spacelike
1282#print axioms fourOne_areaSq_timelike
1283#print axioms fourOne_areaSq_interior_off_cut
1284
1285end WickFourOneAllHinges
1286end SevenGaps
1287end Gravity
1288end IndisputableMonolith
1289