IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean · 1367 lines · 99 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
19import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
20
21/-!
22# All-Hinge Complex-First Wick Continuation of the (3,2) Causal 4-Simplex (Lane B2)
23
24QG Seven-Gaps campaign, lane B of the finishing charter, second deliverable:
25the split-form branch certificate and boundary continuation for ALL TEN
26triangular hinges of the threeTwo causal 4-simplex, at the physical point
27`a = 1`, `alpha = 1`, on the canonical upper-half-plane arc `zArc` of
28`WickActionComplexFirst`, plus the TWO remaining product-form kill
29certificates of the executed trace
30(`state/qg_full_theory/wick_arc_trace/RESULTS.txt`).
31
32## Hinge classes (opposite pair `{p, q}` determines the hinge)
33
34For the threeTwo type (lower slice `{0,1,2}`, upper slice `{3,4}`; timelike
35edges exactly the six cross edges, `CausalSimplex4D.isTimelike`):
36
37* opposite pair `(3,4)` (1 pair): the SPACELIKE hinge `(0,1,2)`; closed
38 forms `C_pp = C_qq = 6z - 2`, `C_pq = 5 - 6z`, `areaSq = 3/16`;
39* mixed pairs, one lower one upper (6 pairs): hinges with 2 timelike
40 triangle edges; ASYMMETRIC cofactors `C_pp = 8z - 4` (lower member),
41 `C_qq = 6z - 2` (upper member), `C_pq = -1`, `areaSq = z/4 - 1/16`;
42* pairs inside the lower triple (3 pairs): the UPPER-PAIR hinges
43 `(0,3,4)`, `(1,3,4)`, `(2,3,4)`; closed forms `C_pp = C_qq = 8z - 4`,
44 `C_pq = 3 - 4z`, `areaSq = z/4 - 1/16`.
45
46All closed forms kernel-checked below by explicit 5x5 minors, matching the
47trace's per-hinge table.
48
49## Honest endpoint disclosure for the spacelike hinge (0,1,2)
50
51At the Lorentzian endpoint `t = 0` the split cosine of the spacelike hinge
52equals `-(11/8)`, which sits exactly ON the arccos cut (`im = 0`,
53`|re| ≥ 1`): the classical Lorentzian boost angle at the spacelike hinge of
54a (3,2) simplex. This is an ALLOWED endpoint contact under the executed
55gate; the branch certificate is therefore stated on the OPEN interior only,
56where the cosine's imaginary part equals `-18 im z / normSq (6z - 2)`,
57strictly negative. The endpoint VALUE itself is still exact (the split
58form collapses to the cut-free rational function `(5 - 6z)/(6z - 2)`).
59
60## Product-form kill certificates (negative results, memorialized)
61
62The single-sqrt product transcription `csqrt (C_pp * C_qq)` is KILLED on
63the threeTwo type by two further interior branch crossings (the fourOne
64crossing `-32` is memorialized in the landed module):
65
66* mixed class: `(8z - 4)(6z - 2)` is exactly `-40` at
67 `Re z = 5/12`, `t* = 1 - arccos(5/12)/pi ≈ 0.6368017686`
68 (`product_form_crossing_threeTwo_mixed`);
69* upper-pair class: `(8z - 4)^2 = 16 (2z - 1)^2` is exactly `-48` at
70 `Re z = 1/2`, `t* = 2/3` EXACTLY
71 (`product_form_crossing_threeTwo_upper`).
72
73## Honesty tiers
74
75* MODEL: `hingeEdges32C`, `hingeMatrix32C`, `threeTwoCosPath` and the
76 explicit minor matrices are definitional (complexifications inherited
77 from `WickActionComplexFirst`; no new modeling choices).
78* THEOREM: every declared theorem below is sorry-free and kernel-checked.
79* OPEN: the action-level continuation (interior-hinge simplicial complex,
80 deficit angles, the continued Regge action) is NOT claimed (C12 lane).
81 No `FullTheoryLedger` flag is touched.
82-/
83
84namespace IndisputableMonolith
85namespace Gravity
86namespace SevenGaps
87namespace WickThreeTwoHinges
88
89open CausalSimplex4D
90open WickActionComplexFirst
91open WickFourOneAllHinges
92
93/-! ## §1. The threeTwo complex edge tuple and its bordered matrix (MODEL) -/
94
95/-- The threeTwo complex edge tuple at unit spacelike value and timelike
96value `z` (this is `continuationEdgesC threeTwo 1 1 t` at `z = zArc t`). -/
97noncomputable def hingeEdges32C (z : ℂ) : SqEdges10C :=
98 fun e => if isTimelike CausalPentType.threeTwo e then z else 1
99
100/-- THEOREM: the physical-point threeTwo continuation tuple is the
101two-value tuple at `z = zArc t`. -/
102theorem continuationEdgesC_physical32 (t : ℝ) :
103 continuationEdgesC CausalPentType.threeTwo 1 1 t
104 = hingeEdges32C (zArc t) := by
105 funext e
106 unfold continuationEdgesC hingeEdges32C zArc
107 by_cases h : isTimelike CausalPentType.threeTwo e = true
108 · rw [if_pos h, if_pos h]
109 · rw [if_neg h, if_neg h]
110 norm_num
111
112/-- The explicit bordered `6 × 6` matrix of the threeTwo tuple (spacelike
1131, timelike `z`): rows/cols 1..3 are the lower-slice vertices 0..2,
114rows/cols 4..5 the upper-slice vertices 3..4 (mirror of
115`CausalSimplex4D.pentMatrix32` at `p = 1`, `q = z`). -/
116def hingeMatrix32C (z : ℂ) : Matrix (Fin 6) (Fin 6) ℂ :=
117 fun i j =>
118 match i.val, j.val with
119 | 0, 0 => 0
120 | 0, _ => 1
121 | _, 0 => 1
122 | 1, 1 => 0
123 | 2, 2 => 0
124 | 3, 3 => 0
125 | 4, 4 => 0
126 | 5, 5 => 0
127 | 1, 2 => 1
128 | 2, 1 => 1
129 | 1, 3 => 1
130 | 3, 1 => 1
131 | 2, 3 => 1
132 | 3, 2 => 1
133 | 4, 5 => 1
134 | 5, 4 => 1
135 | _, _ => z
136
137/-- THEOREM: the general complex CM matrix of the threeTwo two-value tuple
138is the explicit matrix. -/
139theorem cmMatrixC_hingeEdges32 (z : ℂ) :
140 cmMatrixC (hingeEdges32C z) = hingeMatrix32C z := by
141 ext i j
142 fin_cases i <;> fin_cases j <;> rfl
143
144/-! ## §2. Per-pair 5x5 minors (kernel-checked; sympy-cross-checked) -/
145
146/-- Upper diagonal minor deleting CM row/col 4 (vertex 3): the remaining
147four vertices form the `(1,1,1; z,z,z)` tetrahedron, i.e. the landed
148`minorPPC` matrix. -/
149theorem submatrix32_44 (z : ℂ) :
150 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (4 : Fin 6))
151 (Fin.succAbove (4 : Fin 6)) = minorPPC z := by
152 ext i j
153 fin_cases i <;> fin_cases j <;> rfl
154
155/-- Upper diagonal minor deleting CM row/col 5 (vertex 4): again the landed
156`minorPPC`. -/
157theorem submatrix32_55 (z : ℂ) :
158 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (5 : Fin 6))
159 (Fin.succAbove (5 : Fin 6)) = minorPPC z := by
160 ext i j
161 fin_cases i <;> fin_cases j <;> rfl
162
163/-- Lower diagonal minor (delete any lower vertex; the three deletions give
164the SAME explicit matrix): the `2 + 2` tetrahedron with two spacelike and
165four timelike edges. -/
166def minor32LowerC (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
167 fun i j =>
168 match i.val, j.val with
169 | 0, 0 => 0
170 | 1, 1 => 0
171 | 1, 3 => z
172 | 1, 4 => z
173 | 2, 2 => 0
174 | 2, 3 => z
175 | 2, 4 => z
176 | 3, 1 => z
177 | 3, 2 => z
178 | 3, 3 => 0
179 | 4, 1 => z
180 | 4, 2 => z
181 | 4, 4 => 0
182 | _, _ => 1
183
184theorem submatrix32_11 (z : ℂ) :
185 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (1 : Fin 6))
186 (Fin.succAbove (1 : Fin 6)) = minor32LowerC z := by
187 ext i j
188 fin_cases i <;> fin_cases j <;> rfl
189
190theorem submatrix32_22 (z : ℂ) :
191 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (2 : Fin 6))
192 (Fin.succAbove (2 : Fin 6)) = minor32LowerC z := by
193 ext i j
194 fin_cases i <;> fin_cases j <;> rfl
195
196theorem submatrix32_33 (z : ℂ) :
197 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (3 : Fin 6))
198 (Fin.succAbove (3 : Fin 6)) = minor32LowerC z := by
199 ext i j
200 fin_cases i <;> fin_cases j <;> rfl
201
202set_option maxHeartbeats 8000000 in
203set_option maxRecDepth 16384 in
204/-- THEOREM (symbolic 5x5 determinant): the lower diagonal minor is
205`8z - 4` (trace closed form; at `z = 1` the regular value 4). -/
206theorem det_minor32LowerC (z : ℂ) :
207 Matrix.det (minor32LowerC z) = 8 * z - 4 := by
208 unfold minor32LowerC
209 -- Style note: bare `simp` retained deliberately, mirroring
210 -- `WickActionComplexFirst.det_minorPPC`.
211 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
212 ring
213
214/-- Off-diagonal minor at CM (4,5) (opposite pair (3,4), spacelike
215hinge). -/
216def minor32_45C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
217 fun i j =>
218 match i.val, j.val with
219 | 0, 0 => 0
220 | 1, 1 => 0
221 | 1, 4 => z
222 | 2, 2 => 0
223 | 2, 4 => z
224 | 3, 3 => 0
225 | 3, 4 => z
226 | 4, 1 => z
227 | 4, 2 => z
228 | 4, 3 => z
229 | _, _ => 1
230
231theorem submatrix32_45 (z : ℂ) :
232 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (4 : Fin 6))
233 (Fin.succAbove (5 : Fin 6)) = minor32_45C z := by
234 ext i j
235 fin_cases i <;> fin_cases j <;> rfl
236
237set_option maxHeartbeats 8000000 in
238set_option maxRecDepth 16384 in
239theorem det_minor32_45C (z : ℂ) : Matrix.det (minor32_45C z) = 6 * z - 5 := by
240 unfold minor32_45C
241 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
242 ring
243
244/-- Mixed off-diagonal minor at CM (1,4) (opposite pair (0,3)). -/
245def minor32_14C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
246 fun i j =>
247 match i.val, j.val with
248 | 0, 0 => 0
249 | 1, 2 => 0
250 | 1, 4 => z
251 | 2, 3 => 0
252 | 2, 4 => z
253 | 3, 1 => z
254 | 3, 2 => z
255 | 3, 3 => z
256 | 4, 1 => z
257 | 4, 2 => z
258 | 4, 3 => z
259 | 4, 4 => 0
260 | _, _ => 1
261
262theorem submatrix32_14 (z : ℂ) :
263 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (1 : Fin 6))
264 (Fin.succAbove (4 : Fin 6)) = minor32_14C z := by
265 ext i j
266 fin_cases i <;> fin_cases j <;> rfl
267
268set_option maxHeartbeats 8000000 in
269set_option maxRecDepth 16384 in
270theorem det_minor32_14C (z : ℂ) : Matrix.det (minor32_14C z) = 1 := by
271 unfold minor32_14C
272 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
273 ring
274
275/-- Mixed off-diagonal minor at CM (1,5) (opposite pair (0,4)). -/
276def minor32_15C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
277 fun i j =>
278 match i.val, j.val with
279 | 0, 0 => 0
280 | 1, 2 => 0
281 | 1, 4 => z
282 | 2, 3 => 0
283 | 2, 4 => z
284 | 3, 1 => z
285 | 3, 2 => z
286 | 3, 3 => z
287 | 3, 4 => 0
288 | 4, 1 => z
289 | 4, 2 => z
290 | 4, 3 => z
291 | _, _ => 1
292
293theorem submatrix32_15 (z : ℂ) :
294 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (1 : Fin 6))
295 (Fin.succAbove (5 : Fin 6)) = minor32_15C z := by
296 ext i j
297 fin_cases i <;> fin_cases j <;> rfl
298
299set_option maxHeartbeats 8000000 in
300set_option maxRecDepth 16384 in
301theorem det_minor32_15C (z : ℂ) : Matrix.det (minor32_15C z) = -1 := by
302 unfold minor32_15C
303 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
304 ring
305
306/-- Mixed off-diagonal minor at CM (2,4) (opposite pair (1,3)). -/
307def minor32_24C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
308 fun i j =>
309 match i.val, j.val with
310 | 0, 0 => 0
311 | 1, 1 => 0
312 | 1, 4 => z
313 | 2, 3 => 0
314 | 2, 4 => z
315 | 3, 1 => z
316 | 3, 2 => z
317 | 3, 3 => z
318 | 4, 1 => z
319 | 4, 2 => z
320 | 4, 3 => z
321 | 4, 4 => 0
322 | _, _ => 1
323
324theorem submatrix32_24 (z : ℂ) :
325 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (2 : Fin 6))
326 (Fin.succAbove (4 : Fin 6)) = minor32_24C z := by
327 ext i j
328 fin_cases i <;> fin_cases j <;> rfl
329
330set_option maxHeartbeats 8000000 in
331set_option maxRecDepth 16384 in
332theorem det_minor32_24C (z : ℂ) : Matrix.det (minor32_24C z) = -1 := by
333 unfold minor32_24C
334 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
335 ring
336
337/-- Mixed off-diagonal minor at CM (2,5) (opposite pair (1,4)). -/
338def minor32_25C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
339 fun i j =>
340 match i.val, j.val with
341 | 0, 0 => 0
342 | 1, 1 => 0
343 | 1, 4 => z
344 | 2, 3 => 0
345 | 2, 4 => z
346 | 3, 1 => z
347 | 3, 2 => z
348 | 3, 3 => z
349 | 3, 4 => 0
350 | 4, 1 => z
351 | 4, 2 => z
352 | 4, 3 => z
353 | _, _ => 1
354
355theorem submatrix32_25 (z : ℂ) :
356 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (2 : Fin 6))
357 (Fin.succAbove (5 : Fin 6)) = minor32_25C z := by
358 ext i j
359 fin_cases i <;> fin_cases j <;> rfl
360
361set_option maxHeartbeats 8000000 in
362set_option maxRecDepth 16384 in
363theorem det_minor32_25C (z : ℂ) : Matrix.det (minor32_25C z) = 1 := by
364 unfold minor32_25C
365 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
366 ring
367
368/-- Mixed off-diagonal minor at CM (3,4) (opposite pair (2,3)). -/
369def minor32_34C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
370 fun i j =>
371 match i.val, j.val with
372 | 0, 0 => 0
373 | 1, 1 => 0
374 | 1, 4 => z
375 | 2, 2 => 0
376 | 2, 4 => z
377 | 3, 1 => z
378 | 3, 2 => z
379 | 3, 3 => z
380 | 4, 1 => z
381 | 4, 2 => z
382 | 4, 3 => z
383 | 4, 4 => 0
384 | _, _ => 1
385
386theorem submatrix32_34 (z : ℂ) :
387 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (3 : Fin 6))
388 (Fin.succAbove (4 : Fin 6)) = minor32_34C z := by
389 ext i j
390 fin_cases i <;> fin_cases j <;> rfl
391
392set_option maxHeartbeats 8000000 in
393set_option maxRecDepth 16384 in
394theorem det_minor32_34C (z : ℂ) : Matrix.det (minor32_34C z) = 1 := by
395 unfold minor32_34C
396 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
397 ring
398
399/-- Mixed off-diagonal minor at CM (3,5) (opposite pair (2,4)). -/
400def minor32_35C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
401 fun i j =>
402 match i.val, j.val with
403 | 0, 0 => 0
404 | 1, 1 => 0
405 | 1, 4 => z
406 | 2, 2 => 0
407 | 2, 4 => z
408 | 3, 1 => z
409 | 3, 2 => z
410 | 3, 3 => z
411 | 3, 4 => 0
412 | 4, 1 => z
413 | 4, 2 => z
414 | 4, 3 => z
415 | _, _ => 1
416
417theorem submatrix32_35 (z : ℂ) :
418 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (3 : Fin 6))
419 (Fin.succAbove (5 : Fin 6)) = minor32_35C z := by
420 ext i j
421 fin_cases i <;> fin_cases j <;> rfl
422
423set_option maxHeartbeats 8000000 in
424set_option maxRecDepth 16384 in
425theorem det_minor32_35C (z : ℂ) : Matrix.det (minor32_35C z) = -1 := by
426 unfold minor32_35C
427 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
428 ring
429
430/-- Upper-pair off-diagonal minor at CM (1,2) (opposite pair (0,1)). -/
431def minor32_12C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
432 fun i j =>
433 match i.val, j.val with
434 | 0, 0 => 0
435 | 1, 3 => z
436 | 1, 4 => z
437 | 2, 2 => 0
438 | 2, 3 => z
439 | 2, 4 => z
440 | 3, 1 => z
441 | 3, 2 => z
442 | 3, 3 => 0
443 | 4, 1 => z
444 | 4, 2 => z
445 | 4, 4 => 0
446 | _, _ => 1
447
448theorem submatrix32_12 (z : ℂ) :
449 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (1 : Fin 6))
450 (Fin.succAbove (2 : Fin 6)) = minor32_12C z := by
451 ext i j
452 fin_cases i <;> fin_cases j <;> rfl
453
454set_option maxHeartbeats 8000000 in
455set_option maxRecDepth 16384 in
456theorem det_minor32_12C (z : ℂ) : Matrix.det (minor32_12C z) = 4 * z - 3 := by
457 unfold minor32_12C
458 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
459 ring
460
461/-- Upper-pair off-diagonal minor at CM (1,3) (opposite pair (0,2)). -/
462def minor32_13C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
463 fun i j =>
464 match i.val, j.val with
465 | 0, 0 => 0
466 | 1, 2 => 0
467 | 1, 3 => z
468 | 1, 4 => z
469 | 2, 3 => z
470 | 2, 4 => z
471 | 3, 1 => z
472 | 3, 2 => z
473 | 3, 3 => 0
474 | 4, 1 => z
475 | 4, 2 => z
476 | 4, 4 => 0
477 | _, _ => 1
478
479theorem submatrix32_13 (z : ℂ) :
480 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (1 : Fin 6))
481 (Fin.succAbove (3 : Fin 6)) = minor32_13C z := by
482 ext i j
483 fin_cases i <;> fin_cases j <;> rfl
484
485set_option maxHeartbeats 8000000 in
486set_option maxRecDepth 16384 in
487theorem det_minor32_13C (z : ℂ) : Matrix.det (minor32_13C z) = 3 - 4 * z := by
488 unfold minor32_13C
489 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
490 ring
491
492/-- Upper-pair off-diagonal minor at CM (2,3) (opposite pair (1,2)). -/
493def minor32_23C (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
494 fun i j =>
495 match i.val, j.val with
496 | 0, 0 => 0
497 | 1, 1 => 0
498 | 1, 3 => z
499 | 1, 4 => z
500 | 2, 3 => z
501 | 2, 4 => z
502 | 3, 1 => z
503 | 3, 2 => z
504 | 3, 3 => 0
505 | 4, 1 => z
506 | 4, 2 => z
507 | 4, 4 => 0
508 | _, _ => 1
509
510theorem submatrix32_23 (z : ℂ) :
511 Matrix.submatrix (hingeMatrix32C z) (Fin.succAbove (2 : Fin 6))
512 (Fin.succAbove (3 : Fin 6)) = minor32_23C z := by
513 ext i j
514 fin_cases i <;> fin_cases j <;> rfl
515
516set_option maxHeartbeats 8000000 in
517set_option maxRecDepth 16384 in
518theorem det_minor32_23C (z : ℂ) : Matrix.det (minor32_23C z) = 4 * z - 3 := by
519 unfold minor32_23C
520 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
521 ring
522
523/-! ## §3. Cofactor closed forms (THEOREM; trace receipt values) -/
524
525theorem cof32_d1 (z : ℂ) : cmCofactorC (hingeEdges32C z) 1 1 = 8 * z - 4 := by
526 unfold cmCofactorC cmCofactorSignC cmMinorC
527 rw [cmMatrixC_hingeEdges32, submatrix32_11, det_minor32LowerC,
528 if_pos (by decide : Even ((1 : Fin 6).val + (1 : Fin 6).val))]
529 ring
530
531theorem cof32_d2 (z : ℂ) : cmCofactorC (hingeEdges32C z) 2 2 = 8 * z - 4 := by
532 unfold cmCofactorC cmCofactorSignC cmMinorC
533 rw [cmMatrixC_hingeEdges32, submatrix32_22, det_minor32LowerC,
534 if_pos (by decide : Even ((2 : Fin 6).val + (2 : Fin 6).val))]
535 ring
536
537theorem cof32_d3 (z : ℂ) : cmCofactorC (hingeEdges32C z) 3 3 = 8 * z - 4 := by
538 unfold cmCofactorC cmCofactorSignC cmMinorC
539 rw [cmMatrixC_hingeEdges32, submatrix32_33, det_minor32LowerC,
540 if_pos (by decide : Even ((3 : Fin 6).val + (3 : Fin 6).val))]
541 ring
542
543theorem cof32_d4 (z : ℂ) : cmCofactorC (hingeEdges32C z) 4 4 = 6 * z - 2 := by
544 unfold cmCofactorC cmCofactorSignC cmMinorC
545 rw [cmMatrixC_hingeEdges32, submatrix32_44, det_minorPPC,
546 if_pos (by decide : Even ((4 : Fin 6).val + (4 : Fin 6).val))]
547 ring
548
549theorem cof32_d5 (z : ℂ) : cmCofactorC (hingeEdges32C z) 5 5 = 6 * z - 2 := by
550 unfold cmCofactorC cmCofactorSignC cmMinorC
551 rw [cmMatrixC_hingeEdges32, submatrix32_55, det_minorPPC,
552 if_pos (by decide : Even ((5 : Fin 6).val + (5 : Fin 6).val))]
553 ring
554
555theorem cof32_45 (z : ℂ) : cmCofactorC (hingeEdges32C z) 4 5 = 5 - 6 * z := by
556 unfold cmCofactorC cmCofactorSignC cmMinorC
557 rw [cmMatrixC_hingeEdges32, submatrix32_45, det_minor32_45C,
558 if_neg (by decide : ¬ Even ((4 : Fin 6).val + (5 : Fin 6).val))]
559 ring
560
561theorem cof32_14 (z : ℂ) : cmCofactorC (hingeEdges32C z) 1 4 = -1 := by
562 unfold cmCofactorC cmCofactorSignC cmMinorC
563 rw [cmMatrixC_hingeEdges32, submatrix32_14, det_minor32_14C,
564 if_neg (by decide : ¬ Even ((1 : Fin 6).val + (4 : Fin 6).val))]
565 ring
566
567theorem cof32_15 (z : ℂ) : cmCofactorC (hingeEdges32C z) 1 5 = -1 := by
568 unfold cmCofactorC cmCofactorSignC cmMinorC
569 rw [cmMatrixC_hingeEdges32, submatrix32_15, det_minor32_15C,
570 if_pos (by decide : Even ((1 : Fin 6).val + (5 : Fin 6).val))]
571 ring
572
573theorem cof32_24 (z : ℂ) : cmCofactorC (hingeEdges32C z) 2 4 = -1 := by
574 unfold cmCofactorC cmCofactorSignC cmMinorC
575 rw [cmMatrixC_hingeEdges32, submatrix32_24, det_minor32_24C,
576 if_pos (by decide : Even ((2 : Fin 6).val + (4 : Fin 6).val))]
577 ring
578
579theorem cof32_25 (z : ℂ) : cmCofactorC (hingeEdges32C z) 2 5 = -1 := by
580 unfold cmCofactorC cmCofactorSignC cmMinorC
581 rw [cmMatrixC_hingeEdges32, submatrix32_25, det_minor32_25C,
582 if_neg (by decide : ¬ Even ((2 : Fin 6).val + (5 : Fin 6).val))]
583 ring
584
585theorem cof32_34 (z : ℂ) : cmCofactorC (hingeEdges32C z) 3 4 = -1 := by
586 unfold cmCofactorC cmCofactorSignC cmMinorC
587 rw [cmMatrixC_hingeEdges32, submatrix32_34, det_minor32_34C,
588 if_neg (by decide : ¬ Even ((3 : Fin 6).val + (4 : Fin 6).val))]
589 ring
590
591theorem cof32_35 (z : ℂ) : cmCofactorC (hingeEdges32C z) 3 5 = -1 := by
592 unfold cmCofactorC cmCofactorSignC cmMinorC
593 rw [cmMatrixC_hingeEdges32, submatrix32_35, det_minor32_35C,
594 if_pos (by decide : Even ((3 : Fin 6).val + (5 : Fin 6).val))]
595 ring
596
597theorem cof32_12 (z : ℂ) : cmCofactorC (hingeEdges32C z) 1 2 = 3 - 4 * z := by
598 unfold cmCofactorC cmCofactorSignC cmMinorC
599 rw [cmMatrixC_hingeEdges32, submatrix32_12, det_minor32_12C,
600 if_neg (by decide : ¬ Even ((1 : Fin 6).val + (2 : Fin 6).val))]
601 ring
602
603theorem cof32_13 (z : ℂ) : cmCofactorC (hingeEdges32C z) 1 3 = 3 - 4 * z := by
604 unfold cmCofactorC cmCofactorSignC cmMinorC
605 rw [cmMatrixC_hingeEdges32, submatrix32_13, det_minor32_13C,
606 if_pos (by decide : Even ((1 : Fin 6).val + (3 : Fin 6).val))]
607 ring
608
609theorem cof32_23 (z : ℂ) : cmCofactorC (hingeEdges32C z) 2 3 = 3 - 4 * z := by
610 unfold cmCofactorC cmCofactorSignC cmMinorC
611 rw [cmMatrixC_hingeEdges32, submatrix32_23, det_minor32_23C,
612 if_neg (by decide : ¬ Even ((2 : Fin 6).val + (3 : Fin 6).val))]
613 ring
614
615/-! ## §4. The second denominator `8z - 4` never vanishes on the arc -/
616
617/-- THEOREM: `8z - 4 = 0` iff `z = 1/2`, excluded on the unit circle
618`|z| = 1` (the whole arc, endpoints included). -/
619theorem denom32_ne (t : ℝ) : 8 * zArc t - 4 ≠ 0 := by
620 intro h
621 have h8 : (8 : ℂ) * zArc t = 4 := by linear_combination h
622 have hns : Complex.normSq ((8 : ℂ) * zArc t) = Complex.normSq (4 : ℂ) := by
623 rw [h8]
624 rw [Complex.normSq_mul, normSq_zArc, mul_one, Complex.normSq_ofNat,
625 Complex.normSq_ofNat] at hns
626 norm_num at hns
627
628/-! ## §5. The split-form cosine paths and the three hinge classes -/
629
630/-- The split-form cosine path of the opposite pair `(p, q)` along the
631physical threeTwo arc (MODEL). -/
632noncomputable def threeTwoCosPath (p q : Fin 5) (t : ℝ) : ℂ :=
633 dihedralCosSplitC (continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
634
635theorem threeTwoCosPath_symm (p q : Fin 5) :
636 threeTwoCosPath q p = threeTwoCosPath p q :=
637 funext fun _ => dihedralCosSplitC_symm _ p q
638
639theorem threeTwoCosPath_apply_symm (p q : Fin 5) (t : ℝ) :
640 threeTwoCosPath q p t = threeTwoCosPath p q t :=
641 dihedralCosSplitC_symm _ p q
642
643/-- Transport of the boundary-continuation package across the pair swap. -/
644theorem boundary32_symm {p q : Fin 5}
645 (h : ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
646 ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) :
647 ContinuousOn (threeTwoCosPath q p) (Set.Icc 0 1)
648 ∧ threeTwoCosPath q p 1 = -(1 / 4 : ℂ) := by
649 rw [threeTwoCosPath_symm p q]
650 exact h
651
652/-! ### Class A: the spacelike hinge (0,1,2), opposite pair (3,4) -/
653
654/-- THEOREM (class-A collapse): the split cosine of the spacelike hinge
655collapses to `(5 - 6z)/(6z - 2)` everywhere on the arc. -/
656theorem threeTwoCosPath_eq_spacelike (t : ℝ) :
657 threeTwoCosPath 3 4 t = (5 - 6 * zArc t) / (6 * zArc t - 2) := by
658 unfold threeTwoCosPath dihedralCosSplitC dihedralDenomSplitC
659 rw [continuationEdgesC_physical32]
660 have hv3 : cmVertexIndexC 3 = 4 := rfl
661 have hv4 : cmVertexIndexC 4 = 5 := rfl
662 rw [hv3, hv4, cof32_d4, cof32_d5, cof32_45, csqrt_mul_self (denom_ne t)]
663
664/-- THEOREM (class-A branch certificate): branch regularity of the
665spacelike hinge on the FULL open interior. The Lorentzian ENDPOINT value
666`-(11/8)` sits exactly ON the arccos cut (the classical boost angle); that
667is an ALLOWED endpoint contact and is NOT part of this interior statement.
668On the interior the cosine's imaginary part is
669`-18 im z / normSq (6z - 2) ≠ 0`. -/
670theorem branchRegular_threeTwo_spacelike :
671 BranchRegularOn
672 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
673 3 4 (Set.Ioo 0 1) := by
674 intro t ht
675 dsimp only
676 have hy : 0 < (zArc t).im := zArc_im_pos ht
677 have hv3 : cmVertexIndexC 3 = 4 := rfl
678 have hv4 : cmVertexIndexC 4 = 5 := rfl
679 have him6 : (6 * zArc t - 2).im = 6 * (zArc t).im := by
680 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
681 Complex.im_ofNat]
682 ring
683 have hslit : 6 * zArc t - 2 ∈ Complex.slitPlane := by
684 apply Complex.mem_slitPlane_iff.mpr
685 right
686 rw [him6]
687 exact (mul_pos (by norm_num : (0 : ℝ) < 6) hy).ne'
688 refine ⟨?_, ?_, ?_⟩
689 · rw [hv3, continuationEdgesC_physical32, cof32_d4]
690 exact hslit
691 · rw [hv4, continuationEdgesC_physical32, cof32_d5]
692 exact hslit
693 · left
694 have hcos : dihedralCosSplitC
695 (continuationEdgesC CausalPentType.threeTwo 1 1 t) 3 4
696 = (5 - 6 * zArc t) / (6 * zArc t - 2) :=
697 threeTwoCosPath_eq_spacelike t
698 rw [hcos]
699 have hnum : (5 - 6 * zArc t).im * (6 * zArc t - 2).re
700 - (5 - 6 * zArc t).re * (6 * zArc t - 2).im
701 = -18 * (zArc t).im := by
702 simp only [Complex.sub_im, Complex.sub_re, Complex.mul_im,
703 Complex.mul_re, Complex.re_ofNat, Complex.im_ofNat]
704 ring
705 have hdiv : ((5 - 6 * zArc t) / (6 * zArc t - 2)).im
706 = (-18 * (zArc t).im) / Complex.normSq (6 * zArc t - 2) := by
707 rw [Complex.div_im, div_sub_div_same, hnum]
708 rw [hdiv]
709 apply div_ne_zero
710 · exact ne_of_lt (mul_neg_of_neg_of_pos (by norm_num) hy)
711 · exact (Complex.normSq_pos.mpr (denom_ne t)).ne'
712
713/-- THEOREM (class-A boundary continuation): continuous on the CLOSED
714interval; Lorentzian value `-(11/8)` (ON the arccos cut, allowed endpoint
715contact, disclosed above); Euclidean value `-(1/4)`. -/
716theorem boundary_threeTwo_spacelike :
717 ContinuousOn (threeTwoCosPath 3 4) (Set.Icc 0 1)
718 ∧ threeTwoCosPath 3 4 0 = -(11 / 8 : ℂ)
719 ∧ threeTwoCosPath 3 4 1 = -(1 / 4 : ℂ) := by
720 refine ⟨?_, ?_, ?_⟩
721 · have hmo : Continuous fun t => (5 - 6 * zArc t) / (6 * zArc t - 2) := by
722 apply Continuous.div
723 · exact continuous_const.sub (continuous_const.mul continuous_zArc)
724 · exact (continuous_const.mul continuous_zArc).sub continuous_const
725 · exact fun t => denom_ne t
726 exact hmo.continuousOn.congr fun t _ => threeTwoCosPath_eq_spacelike t
727 · rw [threeTwoCosPath_eq_spacelike 0, zArc_zero]
728 norm_num
729 · rw [threeTwoCosPath_eq_spacelike 1, zArc_one]
730 norm_num
731
732/-! ### Class B: the six mixed hinges (one lower, one upper vertex) -/
733
734/-- THEOREM (class-B split form): with lower cofactor `8z - 4`, upper
735cofactor `6z - 2`, numerator `-1`, the split cosine equals
736`-1 / (csqrt (8z-4) * csqrt (6z-2))` everywhere on the arc. No collapse
737to a rational function: the two square roots have DIFFERENT arguments. -/
738theorem threeTwoCosPath_eq_mixed (p q : Fin 5)
739 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
740 (cmVertexIndexC p) (cmVertexIndexC p) = 8 * z - 4)
741 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
742 (cmVertexIndexC q) (cmVertexIndexC q) = 6 * z - 2)
743 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
744 (cmVertexIndexC p) (cmVertexIndexC q) = -1) (t : ℝ) :
745 threeTwoCosPath p q t
746 = -1 / (csqrt (8 * zArc t - 4) * csqrt (6 * zArc t - 2)) := by
747 unfold threeTwoCosPath dihedralCosSplitC dihedralDenomSplitC
748 rw [continuationEdgesC_physical32, hpp, hqq, hpq]
749
750/-- THEOREM (class-B branch certificate, parametric): both cofactors stay
751in the open upper half-plane on the interior; each principal square root
752lies in the open first quadrant, so their product has strictly positive
753imaginary part and the cosine `-1/(s1*s2)` stays off the arccos cuts. -/
754theorem branchRegular_threeTwo_mixed_pair (p q : Fin 5)
755 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
756 (cmVertexIndexC p) (cmVertexIndexC p) = 8 * z - 4)
757 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
758 (cmVertexIndexC q) (cmVertexIndexC q) = 6 * z - 2)
759 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
760 (cmVertexIndexC p) (cmVertexIndexC q) = -1) :
761 BranchRegularOn
762 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
763 p q (Set.Ioo 0 1) := by
764 intro t ht
765 dsimp only
766 have hy : 0 < (zArc t).im := zArc_im_pos ht
767 have him8 : (8 * zArc t - 4).im = 8 * (zArc t).im := by
768 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
769 Complex.im_ofNat]
770 ring
771 have him6 : (6 * zArc t - 2).im = 6 * (zArc t).im := by
772 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
773 Complex.im_ofNat]
774 ring
775 have hup8 : 0 < (8 * zArc t - 4).im := by
776 rw [him8]
777 exact mul_pos (by norm_num : (0 : ℝ) < 8) hy
778 have hup6 : 0 < (6 * zArc t - 2).im := by
779 rw [him6]
780 exact mul_pos (by norm_num : (0 : ℝ) < 6) hy
781 refine ⟨?_, ?_, ?_⟩
782 · rw [continuationEdgesC_physical32, hpp]
783 exact Complex.mem_slitPlane_iff.mpr (Or.inr hup8.ne')
784 · rw [continuationEdgesC_physical32, hqq]
785 exact Complex.mem_slitPlane_iff.mpr (Or.inr hup6.ne')
786 · left
787 have hcos : dihedralCosSplitC
788 (continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
789 = -1 / (csqrt (8 * zArc t - 4) * csqrt (6 * zArc t - 2)) :=
790 threeTwoCosPath_eq_mixed p q hpp hqq hpq t
791 rw [hcos]
792 have hden : 0 < (csqrt (8 * zArc t - 4) * csqrt (6 * zArc t - 2)).im :=
793 mul_im_pos_of_Q1 (csqrt_mem_Q1 hup8) (csqrt_mem_Q1 hup6)
794 exact (neg_one_div_im_pos hden).ne'
795
796/-- THEOREM (class-B boundary continuation, parametric): continuous on the
797CLOSED interval (each square-root path continued across the Lorentzian
798endpoint cut contact within the closed upper half-plane); Lorentzian value
799`sqrt 6 / 24` (real; trace `+0.1020620726`), Euclidean value `-(1/4)`. -/
800theorem boundary_threeTwo_mixed_pair (p q : Fin 5)
801 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
802 (cmVertexIndexC p) (cmVertexIndexC p) = 8 * z - 4)
803 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
804 (cmVertexIndexC q) (cmVertexIndexC q) = 6 * z - 2)
805 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
806 (cmVertexIndexC p) (cmVertexIndexC q) = -1) :
807 ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
808 ∧ threeTwoCosPath p q 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
809 ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ) := by
810 have heq := threeTwoCosPath_eq_mixed p q hpp hqq hpq
811 have hw8 : Continuous fun t => 8 * zArc t - 4 :=
812 (continuous_const.mul continuous_zArc).sub continuous_const
813 have hw6 : Continuous fun t => 6 * zArc t - 2 :=
814 (continuous_const.mul continuous_zArc).sub continuous_const
815 have him8 : ∀ t : ℝ, (8 * zArc t - 4).im = 8 * (zArc t).im := by
816 intro t
817 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
818 Complex.im_ofNat]
819 ring
820 have him6 : ∀ t : ℝ, (6 * zArc t - 2).im = 6 * (zArc t).im := by
821 intro t
822 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
823 Complex.im_ofNat]
824 ring
825 refine ⟨?_, ?_, ?_⟩
826 · have hcs8 : ContinuousOn (fun t => csqrt (8 * zArc t - 4))
827 (Set.Icc 0 1) := by
828 apply continuousOn_csqrt_comp hw8 (fun t _ => denom32_ne t)
829 intro t ht
830 rw [him8]
831 exact mul_nonneg (by norm_num) (zArc_im_nonneg ht)
832 have hcs6 : ContinuousOn (fun t => csqrt (6 * zArc t - 2))
833 (Set.Icc 0 1) := by
834 apply continuousOn_csqrt_comp hw6 (fun t _ => denom_ne t)
835 intro t ht
836 rw [him6]
837 exact mul_nonneg (by norm_num) (zArc_im_nonneg ht)
838 have hdiv : ContinuousOn
839 (fun t => -1 / (csqrt (8 * zArc t - 4) * csqrt (6 * zArc t - 2)))
840 (Set.Icc 0 1) := by
841 apply ContinuousOn.div continuousOn_const (hcs8.mul hcs6)
842 intro t _
843 exact mul_ne_zero (csqrt_ne_zero (denom32_ne t))
844 (csqrt_ne_zero (denom_ne t))
845 exact hdiv.congr fun t _ => heq t
846 · rw [heq 0, zArc_zero]
847 have h12 : (8 * (-1 : ℂ) - 4) = ((-12 : ℝ) : ℂ) := by norm_num
848 have h8 : (6 * (-1 : ℂ) - 2) = ((-8 : ℝ) : ℂ) := by norm_num
849 rw [h12, h8, csqrt_ofReal_neg (by norm_num : (-12 : ℝ) < 0),
850 csqrt_ofReal_neg (by norm_num : (-8 : ℝ) < 0)]
851 have h12' : Real.sqrt (-(-12 : ℝ)) = Real.sqrt 12 := by norm_num
852 have h8' : Real.sqrt (-(-8 : ℝ)) = Real.sqrt 8 := by norm_num
853 rw [h12', h8']
854 have hr : Real.sqrt 12 * Real.sqrt 8 = 4 * Real.sqrt 6 := by
855 rw [← Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 12) 8,
856 show (12 * 8 : ℝ) = 4 ^ 2 * 6 by norm_num,
857 Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ (4 : ℝ) ^ 2) 6,
858 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
859 have hrC : ((Real.sqrt 12 : ℝ) : ℂ) * ((Real.sqrt 8 : ℝ) : ℂ)
860 = 4 * ((Real.sqrt 6 : ℝ) : ℂ) := by
861 rw [← Complex.ofReal_mul, hr]
862 push_cast
863 ring
864 have hS6 : ((Real.sqrt 6 : ℝ) : ℂ) * ((Real.sqrt 6 : ℝ) : ℂ) = 6 := by
865 rw [← Complex.ofReal_mul,
866 Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 6)]
867 norm_num
868 have hden : (((Real.sqrt 12 : ℝ) : ℂ) * Complex.I)
869 * (((Real.sqrt 8 : ℝ) : ℂ) * Complex.I) ≠ 0 := by
870 refine mul_ne_zero (mul_ne_zero ?_ Complex.I_ne_zero)
871 (mul_ne_zero ?_ Complex.I_ne_zero)
872 · exact Complex.ofReal_ne_zero.mpr
873 (ne_of_gt (Real.sqrt_pos.mpr (by norm_num)))
874 · exact Complex.ofReal_ne_zero.mpr
875 (ne_of_gt (Real.sqrt_pos.mpr (by norm_num)))
876 rw [div_eq_iff hden]
877 push_cast
878 linear_combination (((Real.sqrt 6 : ℝ) : ℂ) / 24) * hrC
879 + (1 / 6 : ℂ) * hS6
880 - ((((Real.sqrt 6 : ℝ) : ℂ) * ((Real.sqrt 12 : ℝ) : ℂ)
881 * ((Real.sqrt 8 : ℝ) : ℂ)) / 24) * Complex.I_mul_I
882 · rw [heq 1, zArc_one]
883 have h4a : (8 * (1 : ℂ) - 4) = 4 := by norm_num
884 have h4b : (6 * (1 : ℂ) - 2) = 4 := by norm_num
885 rw [h4a, h4b, csqrt_four]
886 norm_num
887
888/-! ### Class C: the three upper-pair hinges (opposite pair in the lower
889triple) -/
890
891/-- THEOREM (class-C collapse): with both cofactors `8z - 4` and numerator
892`3 - 4z`, the split cosine collapses to `(3 - 4z)/(8z - 4)` everywhere on
893the arc. -/
894theorem threeTwoCosPath_eq_upper (p q : Fin 5)
895 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
896 (cmVertexIndexC p) (cmVertexIndexC p) = 8 * z - 4)
897 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
898 (cmVertexIndexC q) (cmVertexIndexC q) = 8 * z - 4)
899 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
900 (cmVertexIndexC p) (cmVertexIndexC q) = 3 - 4 * z) (t : ℝ) :
901 threeTwoCosPath p q t = (3 - 4 * zArc t) / (8 * zArc t - 4) := by
902 unfold threeTwoCosPath dihedralCosSplitC dihedralDenomSplitC
903 rw [continuationEdgesC_physical32, hpp, hqq, hpq,
904 csqrt_mul_self (denom32_ne t)]
905
906/-- THEOREM (class-C branch certificate, parametric): the cofactor
907`8z - 4` stays in the open upper half-plane and the collapsed cosine has
908imaginary part `-8 im z / normSq (8z - 4) ≠ 0` on the interior (trace
909margin 0.4167, the worst interior-attained margin of the whole trace). -/
910theorem branchRegular_threeTwo_upper_pair (p q : Fin 5)
911 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
912 (cmVertexIndexC p) (cmVertexIndexC p) = 8 * z - 4)
913 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
914 (cmVertexIndexC q) (cmVertexIndexC q) = 8 * z - 4)
915 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
916 (cmVertexIndexC p) (cmVertexIndexC q) = 3 - 4 * z) :
917 BranchRegularOn
918 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
919 p q (Set.Ioo 0 1) := by
920 intro t ht
921 dsimp only
922 have hy : 0 < (zArc t).im := zArc_im_pos ht
923 have him8 : (8 * zArc t - 4).im = 8 * (zArc t).im := by
924 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
925 Complex.im_ofNat]
926 ring
927 have hslit : 8 * zArc t - 4 ∈ Complex.slitPlane := by
928 apply Complex.mem_slitPlane_iff.mpr
929 right
930 rw [him8]
931 exact (mul_pos (by norm_num : (0 : ℝ) < 8) hy).ne'
932 refine ⟨?_, ?_, ?_⟩
933 · rw [continuationEdgesC_physical32, hpp]
934 exact hslit
935 · rw [continuationEdgesC_physical32, hqq]
936 exact hslit
937 · left
938 have hcos : dihedralCosSplitC
939 (continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
940 = (3 - 4 * zArc t) / (8 * zArc t - 4) :=
941 threeTwoCosPath_eq_upper p q hpp hqq hpq t
942 rw [hcos]
943 have hnum : (3 - 4 * zArc t).im * (8 * zArc t - 4).re
944 - (3 - 4 * zArc t).re * (8 * zArc t - 4).im
945 = -8 * (zArc t).im := by
946 simp only [Complex.sub_im, Complex.sub_re, Complex.mul_im,
947 Complex.mul_re, Complex.re_ofNat, Complex.im_ofNat]
948 ring
949 have hdiv : ((3 - 4 * zArc t) / (8 * zArc t - 4)).im
950 = (-8 * (zArc t).im) / Complex.normSq (8 * zArc t - 4) := by
951 rw [Complex.div_im, div_sub_div_same, hnum]
952 rw [hdiv]
953 apply div_ne_zero
954 · exact ne_of_lt (mul_neg_of_neg_of_pos (by norm_num) hy)
955 · exact (Complex.normSq_pos.mpr (denom32_ne t)).ne'
956
957/-- THEOREM (class-C boundary continuation, parametric): continuous on the
958CLOSED interval; Lorentzian value `-(7/12)`, Euclidean value `-(1/4)`. -/
959theorem boundary_threeTwo_upper_pair (p q : Fin 5)
960 (hpp : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
961 (cmVertexIndexC p) (cmVertexIndexC p) = 8 * z - 4)
962 (hqq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
963 (cmVertexIndexC q) (cmVertexIndexC q) = 8 * z - 4)
964 (hpq : ∀ z : ℂ, cmCofactorC (hingeEdges32C z)
965 (cmVertexIndexC p) (cmVertexIndexC q) = 3 - 4 * z) :
966 ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
967 ∧ threeTwoCosPath p q 0 = -(7 / 12 : ℂ)
968 ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ) := by
969 have heq := threeTwoCosPath_eq_upper p q hpp hqq hpq
970 refine ⟨?_, ?_, ?_⟩
971 · have hmo : Continuous fun t => (3 - 4 * zArc t) / (8 * zArc t - 4) := by
972 apply Continuous.div
973 · exact continuous_const.sub (continuous_const.mul continuous_zArc)
974 · exact (continuous_const.mul continuous_zArc).sub continuous_const
975 · exact fun t => denom32_ne t
976 exact hmo.continuousOn.congr fun t _ => heq t
977 · rw [heq 0, zArc_zero]
978 norm_num
979 · rw [heq 1, zArc_one]
980 norm_num
981
982/-! ## §6. The ten instantiated hinges and the B2 headline -/
983
984/-- Pair (0,3): mixed hinge (1,2,4). -/
985theorem branchRegular32_pair03 :
986 BranchRegularOn
987 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
988 0 3 (Set.Ioo 0 1) :=
989 branchRegular_threeTwo_mixed_pair 0 3 cof32_d1 cof32_d4 cof32_14
990
991/-- Pair (0,4): mixed hinge (1,2,3). -/
992theorem branchRegular32_pair04 :
993 BranchRegularOn
994 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
995 0 4 (Set.Ioo 0 1) :=
996 branchRegular_threeTwo_mixed_pair 0 4 cof32_d1 cof32_d5 cof32_15
997
998/-- Pair (1,3): mixed hinge (0,2,4). -/
999theorem branchRegular32_pair13 :
1000 BranchRegularOn
1001 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1002 1 3 (Set.Ioo 0 1) :=
1003 branchRegular_threeTwo_mixed_pair 1 3 cof32_d2 cof32_d4 cof32_24
1004
1005/-- Pair (1,4): mixed hinge (0,2,3). -/
1006theorem branchRegular32_pair14 :
1007 BranchRegularOn
1008 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1009 1 4 (Set.Ioo 0 1) :=
1010 branchRegular_threeTwo_mixed_pair 1 4 cof32_d2 cof32_d5 cof32_25
1011
1012/-- Pair (2,3): mixed hinge (0,1,4). -/
1013theorem branchRegular32_pair23 :
1014 BranchRegularOn
1015 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1016 2 3 (Set.Ioo 0 1) :=
1017 branchRegular_threeTwo_mixed_pair 2 3 cof32_d3 cof32_d4 cof32_34
1018
1019/-- Pair (2,4): mixed hinge (0,1,3). -/
1020theorem branchRegular32_pair24 :
1021 BranchRegularOn
1022 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1023 2 4 (Set.Ioo 0 1) :=
1024 branchRegular_threeTwo_mixed_pair 2 4 cof32_d3 cof32_d5 cof32_35
1025
1026/-- Pair (0,1): upper-pair hinge (2,3,4). -/
1027theorem branchRegular32_pair01 :
1028 BranchRegularOn
1029 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1030 0 1 (Set.Ioo 0 1) :=
1031 branchRegular_threeTwo_upper_pair 0 1 cof32_d1 cof32_d2 cof32_12
1032
1033/-- Pair (0,2): upper-pair hinge (1,3,4). -/
1034theorem branchRegular32_pair02 :
1035 BranchRegularOn
1036 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1037 0 2 (Set.Ioo 0 1) :=
1038 branchRegular_threeTwo_upper_pair 0 2 cof32_d1 cof32_d3 cof32_13
1039
1040/-- Pair (1,2): upper-pair hinge (0,3,4). -/
1041theorem branchRegular32_pair12 :
1042 BranchRegularOn
1043 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
1044 1 2 (Set.Ioo 0 1) :=
1045 branchRegular_threeTwo_upper_pair 1 2 cof32_d2 cof32_d3 cof32_23
1046
1047theorem boundary32_pair03 :
1048 ContinuousOn (threeTwoCosPath 0 3) (Set.Icc 0 1)
1049 ∧ threeTwoCosPath 0 3 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
1050 ∧ threeTwoCosPath 0 3 1 = -(1 / 4 : ℂ) :=
1051 boundary_threeTwo_mixed_pair 0 3 cof32_d1 cof32_d4 cof32_14
1052
1053theorem boundary32_pair04 :
1054 ContinuousOn (threeTwoCosPath 0 4) (Set.Icc 0 1)
1055 ∧ threeTwoCosPath 0 4 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
1056 ∧ threeTwoCosPath 0 4 1 = -(1 / 4 : ℂ) :=
1057 boundary_threeTwo_mixed_pair 0 4 cof32_d1 cof32_d5 cof32_15
1058
1059theorem boundary32_pair13 :
1060 ContinuousOn (threeTwoCosPath 1 3) (Set.Icc 0 1)
1061 ∧ threeTwoCosPath 1 3 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
1062 ∧ threeTwoCosPath 1 3 1 = -(1 / 4 : ℂ) :=
1063 boundary_threeTwo_mixed_pair 1 3 cof32_d2 cof32_d4 cof32_24
1064
1065theorem boundary32_pair14 :
1066 ContinuousOn (threeTwoCosPath 1 4) (Set.Icc 0 1)
1067 ∧ threeTwoCosPath 1 4 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
1068 ∧ threeTwoCosPath 1 4 1 = -(1 / 4 : ℂ) :=
1069 boundary_threeTwo_mixed_pair 1 4 cof32_d2 cof32_d5 cof32_25
1070
1071theorem boundary32_pair23 :
1072 ContinuousOn (threeTwoCosPath 2 3) (Set.Icc 0 1)
1073 ∧ threeTwoCosPath 2 3 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
1074 ∧ threeTwoCosPath 2 3 1 = -(1 / 4 : ℂ) :=
1075 boundary_threeTwo_mixed_pair 2 3 cof32_d3 cof32_d4 cof32_34
1076
1077theorem boundary32_pair24 :
1078 ContinuousOn (threeTwoCosPath 2 4) (Set.Icc 0 1)
1079 ∧ threeTwoCosPath 2 4 0 = ((Real.sqrt 6 / 24 : ℝ) : ℂ)
1080 ∧ threeTwoCosPath 2 4 1 = -(1 / 4 : ℂ) :=
1081 boundary_threeTwo_mixed_pair 2 4 cof32_d3 cof32_d5 cof32_35
1082
1083theorem boundary32_pair01 :
1084 ContinuousOn (threeTwoCosPath 0 1) (Set.Icc 0 1)
1085 ∧ threeTwoCosPath 0 1 0 = -(7 / 12 : ℂ)
1086 ∧ threeTwoCosPath 0 1 1 = -(1 / 4 : ℂ) :=
1087 boundary_threeTwo_upper_pair 0 1 cof32_d1 cof32_d2 cof32_12
1088
1089theorem boundary32_pair02 :
1090 ContinuousOn (threeTwoCosPath 0 2) (Set.Icc 0 1)
1091 ∧ threeTwoCosPath 0 2 0 = -(7 / 12 : ℂ)
1092 ∧ threeTwoCosPath 0 2 1 = -(1 / 4 : ℂ) :=
1093 boundary_threeTwo_upper_pair 0 2 cof32_d1 cof32_d3 cof32_13
1094
1095theorem boundary32_pair12 :
1096 ContinuousOn (threeTwoCosPath 1 2) (Set.Icc 0 1)
1097 ∧ threeTwoCosPath 1 2 0 = -(7 / 12 : ℂ)
1098 ∧ threeTwoCosPath 1 2 1 = -(1 / 4 : ℂ) :=
1099 boundary_threeTwo_upper_pair 1 2 cof32_d2 cof32_d3 cof32_23
1100
1101/-- THEOREM (B2 headline): for EVERY hinge of the threeTwo causal
11024-simplex (1 spacelike + 6 mixed + 3 upper-pair; every unordered opposite
1103vertex pair, both orientations), at `a = 1`, `alpha = 1`:
1104(i) the split-form continuation is branch-regular on the FULL open arc
1105interior, and (ii) the split-form cosine path is continuous on the CLOSED
1106interval `[0,1]` and ends at the Euclidean regular-4-simplex value
1107`-(1/4)`. The spacelike hinge's Lorentzian ENDPOINT sits ON the arccos
1108cut (allowed contact, disclosed in `branchRegular_threeTwo_spacelike`);
1109its branch certificate, like all the others, is interior-only. -/
1110theorem wick_continuation_threeTwo_hinges :
1111 ∀ p q : Fin 5, p ≠ q →
1112 BranchRegularOn
1113 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
1114 (Set.Ioo 0 1)
1115 ∧ (ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
1116 ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) := by
1117 intro p q hpq
1118 fin_cases p <;> fin_cases q
1119 · exact absurd rfl hpq
1120 · exact ⟨branchRegular32_pair01,
1121 boundary32_pair01.1, boundary32_pair01.2.2⟩
1122 · exact ⟨branchRegular32_pair02,
1123 boundary32_pair02.1, boundary32_pair02.2.2⟩
1124 · exact ⟨branchRegular32_pair03,
1125 boundary32_pair03.1, boundary32_pair03.2.2⟩
1126 · exact ⟨branchRegular32_pair04,
1127 boundary32_pair04.1, boundary32_pair04.2.2⟩
1128 · exact ⟨branchRegularOn_symm branchRegular32_pair01,
1129 boundary32_symm ⟨boundary32_pair01.1, boundary32_pair01.2.2⟩⟩
1130 · exact absurd rfl hpq
1131 · exact ⟨branchRegular32_pair12,
1132 boundary32_pair12.1, boundary32_pair12.2.2⟩
1133 · exact ⟨branchRegular32_pair13,
1134 boundary32_pair13.1, boundary32_pair13.2.2⟩
1135 · exact ⟨branchRegular32_pair14,
1136 boundary32_pair14.1, boundary32_pair14.2.2⟩
1137 · exact ⟨branchRegularOn_symm branchRegular32_pair02,
1138 boundary32_symm ⟨boundary32_pair02.1, boundary32_pair02.2.2⟩⟩
1139 · exact ⟨branchRegularOn_symm branchRegular32_pair12,
1140 boundary32_symm ⟨boundary32_pair12.1, boundary32_pair12.2.2⟩⟩
1141 · exact absurd rfl hpq
1142 · exact ⟨branchRegular32_pair23,
1143 boundary32_pair23.1, boundary32_pair23.2.2⟩
1144 · exact ⟨branchRegular32_pair24,
1145 boundary32_pair24.1, boundary32_pair24.2.2⟩
1146 · exact ⟨branchRegularOn_symm branchRegular32_pair03,
1147 boundary32_symm ⟨boundary32_pair03.1, boundary32_pair03.2.2⟩⟩
1148 · exact ⟨branchRegularOn_symm branchRegular32_pair13,
1149 boundary32_symm ⟨boundary32_pair13.1, boundary32_pair13.2.2⟩⟩
1150 · exact ⟨branchRegularOn_symm branchRegular32_pair23,
1151 boundary32_symm ⟨boundary32_pair23.1, boundary32_pair23.2.2⟩⟩
1152 · exact absurd rfl hpq
1153 · exact ⟨branchRegular_threeTwo_spacelike,
1154 boundary_threeTwo_spacelike.1, boundary_threeTwo_spacelike.2.2⟩
1155 · exact ⟨branchRegularOn_symm branchRegular32_pair04,
1156 boundary32_symm ⟨boundary32_pair04.1, boundary32_pair04.2.2⟩⟩
1157 · exact ⟨branchRegularOn_symm branchRegular32_pair14,
1158 boundary32_symm ⟨boundary32_pair14.1, boundary32_pair14.2.2⟩⟩
1159 · exact ⟨branchRegularOn_symm branchRegular32_pair24,
1160 boundary32_symm ⟨boundary32_pair24.1, boundary32_pair24.2.2⟩⟩
1161 · exact ⟨branchRegularOn_symm branchRegular_threeTwo_spacelike,
1162 boundary32_symm ⟨boundary_threeTwo_spacelike.1,
1163 boundary_threeTwo_spacelike.2.2⟩⟩
1164 · exact absurd rfl hpq
1165
1166/-! ## §7. Hinge areas-squared (THEOREM) -/
1167
1168/-- THEOREM: threeTwo hinge areas-squared in closed form: the spacelike
1169hinge `(0,1,2)` has the constant `3/16`; every mixed hinge (shape
1170`(1, z, z)`) and every upper-pair hinge (shape `(z, z, 1)`) has
1171`z/4 - 1/16`. Cut avoidance on the open interior is inherited verbatim
1172from `WickFourOneAllHinges.fourOne_areaSq_interior_off_cut` (same two
1173closed forms; the Lorentzian endpoint contact at `-5/16` is allowed). -/
1174theorem threeTwo_areaSq_closed (z : ℂ) :
1175 hingeAreaSqC (hingeEdges32C z) 0 1 2 = (3 / 16 : ℂ)
1176 ∧ hingeAreaSqC (hingeEdges32C z) 0 1 3 = z / 4 - 1 / 16
1177 ∧ hingeAreaSqC (hingeEdges32C z) 0 1 4 = z / 4 - 1 / 16
1178 ∧ hingeAreaSqC (hingeEdges32C z) 0 2 3 = z / 4 - 1 / 16
1179 ∧ hingeAreaSqC (hingeEdges32C z) 0 2 4 = z / 4 - 1 / 16
1180 ∧ hingeAreaSqC (hingeEdges32C z) 1 2 3 = z / 4 - 1 / 16
1181 ∧ hingeAreaSqC (hingeEdges32C z) 1 2 4 = z / 4 - 1 / 16
1182 ∧ hingeAreaSqC (hingeEdges32C z) 0 3 4 = z / 4 - 1 / 16
1183 ∧ hingeAreaSqC (hingeEdges32C z) 1 3 4 = z / 4 - 1 / 16
1184 ∧ hingeAreaSqC (hingeEdges32C z) 2 3 4 = z / 4 - 1 / 16 := by
1185 refine ⟨triangleAreaSqC_ones, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
1186 · exact triangleAreaSqC_one_z_z z
1187 · exact triangleAreaSqC_one_z_z z
1188 · exact triangleAreaSqC_one_z_z z
1189 · exact triangleAreaSqC_one_z_z z
1190 · exact triangleAreaSqC_one_z_z z
1191 · exact triangleAreaSqC_one_z_z z
1192 · exact triangleAreaSqC_z_z_one z
1193 · exact triangleAreaSqC_z_z_one z
1194 · exact triangleAreaSqC_z_z_one z
1195
1196/-! ## §8. The two product-form kill certificates (gate FAIL events,
1197memorialized as kernel theorems) -/
1198
1199/-- The exact interior crossing parameter of the mixed-class product form:
1200`tStarMixed = 1 - arccos(5/12)/pi ≈ 0.6368017686` (RESULTS.txt §3). -/
1201noncomputable def tStarMixed : ℝ := 1 - Real.arccos (5 / 12) / Real.pi
1202
1203theorem tStarMixed_mem_Ioo : tStarMixed ∈ Set.Ioo (0 : ℝ) 1 := by
1204 have hpi := Real.pi_pos
1205 have h1 : 0 < Real.arccos (5 / 12) := Real.arccos_pos.mpr (by norm_num)
1206 have h2 : Real.arccos (5 / 12) ≤ Real.pi / 2 :=
1207 Real.arccos_le_pi_div_two.mpr (by norm_num)
1208 constructor
1209 · have hle : Real.arccos (5 / 12) / Real.pi ≤ 1 / 2 := by
1210 rw [div_le_iff₀ hpi]
1211 linarith
1212 unfold tStarMixed
1213 linarith
1214 · have hgt : 0 < Real.arccos (5 / 12) / Real.pi := div_pos h1 hpi
1215 unfold tStarMixed
1216 linarith
1217
1218theorem arg_tStarMixed :
1219 Real.pi * (1 - tStarMixed) = Real.arccos (5 / 12) := by
1220 have hpne : Real.pi ≠ 0 := Real.pi_ne_zero
1221 unfold tStarMixed
1222 have h : (1 : ℝ) - (1 - Real.arccos (5 / 12) / Real.pi)
1223 = Real.arccos (5 / 12) / Real.pi := by ring
1224 rw [h, mul_comm, div_mul_cancel₀ _ hpne]
1225
1226theorem cos_arg_tStarMixed :
1227 Real.cos (Real.pi * (1 - tStarMixed)) = 5 / 12 := by
1228 rw [arg_tStarMixed]
1229 exact Real.cos_arccos (by norm_num) (by norm_num)
1230
1231/-- THEOREM (exact crossing value, mixed class): at `tStarMixed` the
1232product-form denominator argument `(8z - 4)(6z - 2)` equals `-40`
1233EXACTLY. -/
1234theorem product_form_crossing_value_mixed :
1235 (8 * zArc tStarMixed - 4) * (6 * zArc tStarMixed - 2) = -40 := by
1236 have hz : zArc tStarMixed = ((5 / 12 : ℝ) : ℂ)
1237 + ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) * Complex.I := by
1238 rw [zArc_eq_exp, Complex.exp_mul_I, ← Complex.ofReal_cos,
1239 ← Complex.ofReal_sin, cos_arg_tStarMixed]
1240 have h84 : 8 * zArc tStarMixed - 4
1241 = -(2 / 3 : ℂ)
1242 + 8 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ)
1243 * Complex.I := by
1244 rw [hz]
1245 push_cast
1246 ring
1247 have h62 : 6 * zArc tStarMixed - 2
1248 = (1 / 2 : ℂ)
1249 + 6 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ)
1250 * Complex.I := by
1251 rw [hz]
1252 push_cast
1253 ring
1254 have hprod : (8 * zArc tStarMixed - 4) * (6 * zArc tStarMixed - 2)
1255 = -(1 / 3 : ℂ)
1256 - 48 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) ^ 2 := by
1257 rw [h84, h62]
1258 linear_combination
1259 (48 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) ^ 2)
1260 * Complex.I_sq
1261 have hs2 : Real.sin (Real.pi * (1 - tStarMixed)) ^ 2 = 119 / 144 := by
1262 rw [Real.sin_sq, cos_arg_tStarMixed]
1263 norm_num
1264 have hcast : ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) ^ 2
1265 = ((119 / 144 : ℝ) : ℂ) := by
1266 rw [← Complex.ofReal_pow, hs2]
1267 rw [hprod, hcast]
1268 push_cast
1269 norm_num
1270
1271/-- THEOREM (B2 kill certificate, mixed class): at the interior arc
1272parameter `tStarMixed ∈ (0,1)` the diagonal-cofactor product
1273`C_pp * C_qq = (8z-4)(6z-2)` of every mixed threeTwo hinge (here the
1274witness pair (0,3), CM rows 1 and 4, hinge `(1,2,4)`) equals `-40`
1275exactly, ON the `csqrt` branch cut (off `Complex.slitPlane`). This KILLS
1276the single-sqrt product transcription `csqrt (C_pp * C_qq)` on the
1277threeTwo mixed class (RESULTS.txt §3: `Re z = 5/12`, value `-40`,
1278`t* ≈ 0.6368017686`). -/
1279theorem product_form_crossing_threeTwo_mixed :
1280 tStarMixed ∈ Set.Ioo (0 : ℝ) 1
1281 ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 1 1
1282 * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 4 4
1283 = -40
1284 ∧ (-40 : ℂ) ∉ Complex.slitPlane := by
1285 refine ⟨tStarMixed_mem_Ioo, ?_, ?_⟩
1286 · rw [continuationEdgesC_physical32, cof32_d1, cof32_d4]
1287 exact product_form_crossing_value_mixed
1288 · intro hmem
1289 rw [Complex.mem_slitPlane_iff] at hmem
1290 simp at hmem
1291 linarith
1292
1293/-- The upper-pair crossing parameter is `2/3` EXACTLY (the only crossing
1294of the whole trace with a rational parameter): `z(2/3) = exp(i pi/3)
1295= 1/2 + i sqrt 3 / 2`, `Re z = 1/2`. -/
1296theorem cos_arg_twoThirds :
1297 Real.cos (Real.pi * (1 - 2 / 3)) = 1 / 2 := by
1298 rw [show Real.pi * (1 - 2 / 3 : ℝ) = Real.pi / 3 by ring,
1299 Real.cos_pi_div_three]
1300
1301/-- THEOREM (exact crossing value, upper-pair class): at `t = 2/3` the
1302product-form denominator argument `(8z - 4)^2 = 16 (2z - 1)^2` equals
1303`-48` EXACTLY. -/
1304theorem product_form_crossing_value_upper :
1305 (8 * zArc (2 / 3) - 4) * (8 * zArc (2 / 3) - 4) = -48 := by
1306 have hz : zArc (2 / 3) = ((1 / 2 : ℝ) : ℂ)
1307 + ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) * Complex.I := by
1308 rw [zArc_eq_exp, Complex.exp_mul_I, ← Complex.ofReal_cos,
1309 ← Complex.ofReal_sin, cos_arg_twoThirds]
1310 have h84 : 8 * zArc (2 / 3) - 4
1311 = 8 * ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) * Complex.I := by
1312 rw [hz]
1313 push_cast
1314 ring
1315 have hprod : (8 * zArc (2 / 3) - 4) * (8 * zArc (2 / 3) - 4)
1316 = -(64 : ℂ) * ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) ^ 2 := by
1317 rw [h84]
1318 linear_combination
1319 (64 * ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) ^ 2)
1320 * Complex.I_sq
1321 have hs2 : Real.sin (Real.pi * (1 - 2 / 3)) ^ 2 = 3 / 4 := by
1322 rw [Real.sin_sq, cos_arg_twoThirds]
1323 norm_num
1324 have hcast : ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) ^ 2
1325 = ((3 / 4 : ℝ) : ℂ) := by
1326 rw [← Complex.ofReal_pow, hs2]
1327 rw [hprod, hcast]
1328 push_cast
1329 norm_num
1330
1331/-- THEOREM (B2 kill certificate, upper-pair class): at the interior arc
1332parameter `t* = 2/3` EXACTLY, the diagonal-cofactor product
1333`C_pp * C_qq = (8z-4)^2` of every upper-pair threeTwo hinge (witness pair
1334(0,1), CM rows 1 and 2, hinge `(2,3,4)`) equals `-48` exactly, ON the
1335`csqrt` branch cut. This KILLS the single-sqrt product transcription on
1336the threeTwo upper-pair class (RESULTS.txt §3: `Re z = 1/2`, value `-48`,
1337`t* = 2/3` exactly). -/
1338theorem product_form_crossing_threeTwo_upper :
1339 (2 / 3 : ℝ) ∈ Set.Ioo (0 : ℝ) 1
1340 ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 1 1
1341 * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 2 2
1342 = -48
1343 ∧ (-48 : ℂ) ∉ Complex.slitPlane := by
1344 refine ⟨by norm_num, ?_, ?_⟩
1345 · rw [continuationEdgesC_physical32, cof32_d1, cof32_d2]
1346 exact product_form_crossing_value_upper
1347 · intro hmem
1348 rw [Complex.mem_slitPlane_iff] at hmem
1349 simp at hmem
1350 linarith
1351
1352/-! ## §9. Axiom audit
1353
1354Expected for each: `[propext, Classical.choice, Quot.sound]`. -/
1355
1356#print axioms wick_continuation_threeTwo_hinges
1357#print axioms branchRegular_threeTwo_spacelike
1358#print axioms boundary_threeTwo_spacelike
1359#print axioms threeTwo_areaSq_closed
1360#print axioms product_form_crossing_threeTwo_mixed
1361#print axioms product_form_crossing_threeTwo_upper
1362
1363end WickThreeTwoHinges
1364end SevenGaps
1365end Gravity
1366end IndisputableMonolith
1367