IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst
IndisputableMonolith/Gravity/SevenGaps/WickActionComplexFirst.lean · 872 lines · 67 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.Trigonometric.Basic
10import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
11import Mathlib.Analysis.SpecialFunctions.Sqrt
12import Mathlib.Tactic.Linarith
13import Mathlib.Tactic.LinearCombination
14import Mathlib.Tactic.FieldSimp
15import IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D
16
17/-!
18# Complex-First 4D Wick Continuation of the Regge Hinge Data (C11 lane)
19
20QG Seven-Gaps campaign, panel-locked flagship lane **C11** (panel P1-remainder,
21judge verdict C11; referee **PROCEED-WITH-MANDATE**). Hour-0 numeric gate
22receipt: `state/qg_full_theory/wick_arc_trace/RESULTS.txt` (executed
232026-07-16; exact sympy crossing certificates + split-reading pass).
24
25This module builds the complex-first formalization of the 4D Lorentzian Wick
26continuation of the *hinge data* (complex Cayley-Menger areas-squared and
27cofactor dihedral cosines) of the causal 4-simplex classes of
28`Gravity.SevenGaps.CausalSimplex4D`, culminating in a boundary-continuation
29theorem realized as a PATH-SELECTED continuation with a proved branch
30certificate on the full open arc interior.
31
32## Honest scope (mandated disclosure)
33
34This is a **hinge-data continuation** (dihedral cosines and areas-squared of
35triangular hinges of a single causal 4-simplex). It may be called an
36*action-level* continuation only if a genuine interior-hinge simplicial
37complex exists; that is the separate C12 lane's question and is **not**
38claimed here. The FullTheoryLedger gap `wick_action_continuation_4d` /
39`causalSimplex4DStatus.action_level_continuation_open` remains OPEN and no
40ledger flag is touched by this module.
41
42## The arc (S1)
43
44The continuation path on the timelike squared edge is the canonical
45upper-half-plane arc
46
47 `z(t) = alpha * a^2 * exp(i * pi * (1 - t))`, `t ∈ [0, 1]`,
48
49with `z(0) = -(alpha * a^2)` the **Lorentzian** endpoint and
50`z(1) = +(alpha * a^2)` the **Euclidean** endpoint, matching the repo sign
51convention `lorentzianSqEdges` / `euclideanSqEdges`
52(`CausalSimplex4D.lean:240-247`) and the executed gate (RESULTS.txt §1;
53the endpoints are identified against the kernel-checked real tuples in
54`continuationEdgesC_zero` / `continuationEdgesC_one` below). The interior
55`t ∈ (0,1)` lies strictly in the open upper half-plane.
56
57## Split-sqrt denominator is MANDATORY (S2; gate verdict)
58
59The complex cofactor dihedral cosine is defined with the denominator
60**definitionally in split form** `csqrt C_pp * csqrt C_qq`, NOT
61`csqrt (C_pp * C_qq)`. The hour-0 gate proved the product form is KILLED by
62interior branch crossings of the `Complex`-sqrt cut `(-∞, 0]`: exact
63certificates (RESULTS.txt §3, alpha = 1, a = 1):
64
65* fourOne timelike hinges and threeTwo (0,1,2): `C_pp*C_qq = 4*(3z-1)^2`
66 crosses at `Re z = 1/3`, value exactly `-32`,
67 `t* = 1 - arccos(1/3)/pi ≈ 0.6081734480`;
68* threeTwo mixed hinges: `(8z-4)(6z-2)` crosses at `Re z = 5/12`, value
69 exactly `-40`, `t* ≈ 0.6368017686`;
70* threeTwo upper-pair hinges: `16*(2z-1)^2` crosses at `Re z = 1/2`, value
71 exactly `-48`, `t* = 2/3` exactly;
72* analogous exact crossings at alpha = 0.5 and alpha = 2 (not tuned).
73
74These negative results are memorialized here as the kernel-checked theorem
75`product_form_crossing` below (the fourOne offender: at
76`tStar = 1 - arccos(1/3)/pi ∈ (0,1)` the cofactor product equals `-32`
77exactly, a point ON the sqrt branch cut, off `Complex.slitPlane`).
78
79## Mathlib cut conventions (verified against this toolchain)
80
81Mathlib (this pin) has **no** `Complex.sqrt` and **no** `Complex.arccos`.
82We therefore define `csqrt z := z ^ (1/2 : ℂ)` via `Complex.cpow`
83(principal branch: `exp (log z / 2)`, `Complex.log` uses `arg ∈ (-π, π]`,
84discontinuity exactly on `(-∞, 0]`; `Complex.continuousAt_cpow_const`
85requires membership in `Complex.slitPlane = {z | 0 < re z ∨ im z ≠ 0}`,
86which is exactly the complement of the cut). The `BranchRegularOn`
87predicate therefore encodes:
88
89* sqrt-cut avoidance as membership in `Complex.slitPlane` (Mathlib's own
90 slit-plane set, matching the cpow/log cut `(-∞, 0]`);
91* arccos-cut avoidance directly as the region condition
92 `im ≠ 0 ∨ (-1 < re ∧ re < 1)` (complement of the classical arccos cuts
93 `(-∞, -1]` and `[1, ∞)` on the real axis, where any principal
94 log-based `arccos` is continuous).
95
96## What is proved (S3/S4 receipts)
97
98For the traced fourOne timelike hinge — triangle `(0,1,4)`, opposite vertex
99pair `(2,3)` (CM rows/cols 3 and 4), at `a = 1`, `alpha = 1` (the Lean
100physical point `physicalCausalPent`):
101
102* `branchRegular_fourOne_hinge` : `BranchRegularOn` holds on the FULL open
103 arc interior `Set.Ioo 0 1` (not merely a subinterval). Closed forms
104 (kernel-checked 5x5 minors): `C_pp = C_qq = 6z - 2`, `C_pq = 1 - 2z`,
105 hinge `areaSq = z/4 - 1/16`. On the interior `im z > 0` forces every
106 cofactor off the sqrt cut, and the split cosine has
107 `im = -2 im z / normSq (6z-2) ≠ 0`, off the arccos cut (the trace's
108 worst interior margin 0.4167 lives on threeTwo hinges; this fourOne
109 hinge has margin 0.625, RESULTS.txt §3).
110* `wick_boundary_continuation_fourOne_hinge` : the split-form cosine path
111 is continuous on the CLOSED interval `[0,1]` (it equals the cut-free
112 rational function `(1 - 2z)/(6z - 2)` wherever `6z - 2 ≠ 0`, proved for
113 all `t ∈ ℝ` on this arc) and connects the Lorentzian endpoint value
114 `-(3/8)` at `t = 0` to the Euclidean regular-4-simplex value `-(1/4)`
115 at `t = 1` (`+C_pq` numerator convention of
116 `Geometry.DihedralCayleyMenger`; textbook `-C` interior cosine `+1/4`).
117* **Endpoint sign convention (S4, documented sign factor):** at the
118 Lorentzian endpoint the cofactors are negative (`C_pp = C_qq = -8`, ON
119 the sqrt cut boundary, `endpoint_cofactor_on_sqrt_cut`), and
120 `csqrt w * csqrt w = w` (not `|w|`), so the split form equals
121 `(-1) * (real product formula)`: split `-(3/8)` vs real-formula `+3/8`
122 (`lorentzian_endpoint_sign_factor`). NO unrestricted equality with the
123 real Lorentzian formula is claimed.
124
125## Honesty tiers (S5)
126
127* MODEL: `SqEdges10C`, `pentDistSqC`, `cmMatrixC`, `cmMinorC`,
128 `cmCofactorC`, `csqrt`, `dihedralDenomSplitC`, `dihedralCosSplitC`,
129 `triCMMatrixC`, `triangleAreaSqC`, `hingeAreaSqC`, `arcZ`,
130 `continuationEdgesC`, `OffArccosCut`, `BranchRegularOn` — definitional
131 complexifications of the repo's real CM/dihedral conventions
132 (`Geometry.CayleyMengerN`, `Geometry.DihedralCayleyMenger` 3D cofactor
133 convention lifted to the 4D bordered 6x6 matrix).
134* THEOREM: every declared theorem below is sorry-free and kernel-checked;
135 in particular `branchRegular_fourOne_hinge` (inhabited certificate, full
136 interior), `wick_boundary_continuation_fourOne_hinge`,
137 `lorentzian_endpoint_sign_factor`, `product_form_crossing`.
138* OPEN: the action-level continuation (interior-hinge complex, deficit
139 angles, the continued Regge action itself) — C12 lane; nothing here
140 closes it and no status flag is changed.
141-/
142
143namespace IndisputableMonolith
144namespace Gravity
145namespace SevenGaps
146namespace WickActionComplexFirst
147
148open CausalSimplex4D
149
150/-! ## §1. Complex edge data and the bordered complex CM matrix (MODEL) -/
151
152/-- Complex squared edge lengths of a 4-simplex, indexed by `Fin 10`
153(lexicographic edge order of `CausalSimplex4D.pentEdgeVertices`). -/
154abbrev SqEdges10C : Type := Fin 10 → ℂ
155
156/-- Complex squared-distance table of the 4-simplex from the `Fin 10` edge
157tuple (complexification of `CausalSimplex4D.pentDistSq`). -/
158def pentDistSqC (x : SqEdges10C) : Fin 5 → Fin 5 → ℂ := fun i j =>
159 match i.val, j.val with
160 | 0, 1 => x 0
161 | 1, 0 => x 0
162 | 0, 2 => x 1
163 | 2, 0 => x 1
164 | 0, 3 => x 2
165 | 3, 0 => x 2
166 | 0, 4 => x 3
167 | 4, 0 => x 3
168 | 1, 2 => x 4
169 | 2, 1 => x 4
170 | 1, 3 => x 5
171 | 3, 1 => x 5
172 | 1, 4 => x 6
173 | 4, 1 => x 6
174 | 2, 3 => x 7
175 | 3, 2 => x 7
176 | 2, 4 => x 8
177 | 4, 2 => x 8
178 | 3, 4 => x 9
179 | 4, 3 => x 9
180 | _, _ => 0
181
182/-- CM index to optional vertex: index `0` is the border row/column, index
183`k+1` is vertex `k` (complexified mirror of
184`Geometry.CayleyMengerN.cmIndexVertex` at `n = 4`). -/
185def cmIndexVertexC (i : Fin 6) : Option (Fin 5) :=
186 if h : i.val = 0 then none else some ⟨i.val - 1, by omega⟩
187
188/-- The bordered `6 × 6` complex Cayley-Menger matrix of a complex edge
189tuple (complexification of `Geometry.CayleyMengerN.cmMatrixN` at `n = 4`). -/
190def cmMatrixC (x : SqEdges10C) : Matrix (Fin 6) (Fin 6) ℂ :=
191 fun i j =>
192 match cmIndexVertexC i, cmIndexVertexC j with
193 | none, none => 0
194 | none, some _ => 1
195 | some _, none => 1
196 | some vi, some vj => pentDistSqC x vi vj
197
198/-- Delete row `r` and column `c` from the complex CM matrix and take the
199`5 × 5` determinant (mirror of `Geometry.CayleyMengerMatrix.cmMinor3`). -/
200noncomputable def cmMinorC (x : SqEdges10C) (r c : Fin 6) : ℂ :=
201 Matrix.det (Matrix.submatrix (cmMatrixC x) (Fin.succAbove r) (Fin.succAbove c))
202
203/-- Cofactor sign `(-1)^(r+c)` as a complex number. -/
204def cmCofactorSignC (r c : Fin 6) : ℂ :=
205 if Even (r.val + c.val) then 1 else -1
206
207/-- Complex Cayley-Menger cofactor `C_{r,c}` of the bordered `6 × 6` matrix
208(mirror of `Geometry.CayleyMengerMatrix.cmCofactor3`). -/
209noncomputable def cmCofactorC (x : SqEdges10C) (r c : Fin 6) : ℂ :=
210 cmCofactorSignC r c * cmMinorC x r c
211
212/-- Vertex index `0..4` to CM row/column index `1..5` (mirror of
213`Geometry.DihedralCayleyMenger.cmVertexIndex`). -/
214def cmVertexIndexC : Fin 5 → Fin 6
215 | 0 => 1
216 | 1 => 2
217 | 2 => 3
218 | 3 => 4
219 | 4 => 5
220
221/-! ## §2. Principal-branch complex square root and the SPLIT cosine (MODEL) -/
222
223/-- Principal-branch complex square root via `Complex.cpow`:
224`csqrt z = z ^ (1/2 : ℂ) = exp (log z / 2)` for `z ≠ 0`, with branch cut on
225`(-∞, 0]` (the complement of `Complex.slitPlane`). Mathlib (this pin) has
226no `Complex.sqrt`; this is the faithful principal-branch substitute. -/
227noncomputable def csqrt (z : ℂ) : ℂ := z ^ (1 / 2 : ℂ)
228
229/-- THEOREM: `csqrt z * csqrt z = z` for `z ≠ 0` (note: `= z`, NOT `= |z|`;
230this is the source of the documented Lorentzian endpoint sign factor). -/
231theorem csqrt_mul_self {z : ℂ} (hz : z ≠ 0) : csqrt z * csqrt z = z := by
232 unfold csqrt
233 rw [← Complex.cpow_add _ _ hz]
234 have h : (1 / 2 + 1 / 2 : ℂ) = 1 := by norm_num
235 rw [h, Complex.cpow_one]
236
237/-- The SPLIT-form denominator of the complex cofactor dihedral cosine at
238the hinge opposite the vertex pair `(p, q)`:
239`csqrt C_pp * csqrt C_qq` — definitionally split, per the hour-0 gate
240mandate (the single-sqrt product form `csqrt (C_pp * C_qq)` provably
241crosses the sqrt cut mid-arc; see `product_form_crossing`). -/
242noncomputable def dihedralDenomSplitC (x : SqEdges10C) (p q : Fin 5) : ℂ :=
243 csqrt (cmCofactorC x (cmVertexIndexC p) (cmVertexIndexC p))
244 * csqrt (cmCofactorC x (cmVertexIndexC q) (cmVertexIndexC q))
245
246/-- The complex cofactor dihedral cosine (split form) at the hinge opposite
247the vertex pair `(p, q)`; `+C_pq` numerator convention matching
248`Geometry.DihedralCayleyMenger.dihedralCos3Sq` (which proves `+1/3` on the
249regular unit tetrahedron in 3D; in 4D the same convention gives `-1/4` on
250the regular unit 4-simplex, textbook `-C` interior cosine `+1/4`). -/
251noncomputable def dihedralCosSplitC (x : SqEdges10C) (p q : Fin 5) : ℂ :=
252 cmCofactorC x (cmVertexIndexC p) (cmVertexIndexC q) / dihedralDenomSplitC x p q
253
254/-! ## §3. Complex triangle (hinge) area-squared (MODEL) -/
255
256/-- The bordered `4 × 4` complex CM matrix of a triangle with squared edge
257lengths `u = d(1,2)`, `v = d(1,3)`, `w = d(2,3)`. -/
258def triCMMatrixC (u v w : ℂ) : Matrix (Fin 4) (Fin 4) ℂ :=
259 fun i j =>
260 match i.val, j.val with
261 | 0, 0 => 0
262 | 0, _ => 1
263 | _, 0 => 1
264 | 1, 1 => 0
265 | 2, 2 => 0
266 | 3, 3 => 0
267 | 1, 2 => u
268 | 2, 1 => u
269 | 1, 3 => v
270 | 3, 1 => v
271 | 2, 3 => w
272 | 3, 2 => w
273 | _, _ => 0
274
275/-- Complex triangle area-squared, `-det(CM_4x4) / 16` (the `n = 2` case of
276`Geometry.CayleyMengerN.simplexVolumeSqN`, complexified). -/
277noncomputable def triangleAreaSqC (u v w : ℂ) : ℂ :=
278 -(Matrix.det (triCMMatrixC u v w)) / 16
279
280/-- Complex area-squared of the hinge triangle `{i, j, k}` of the 4-simplex
281with complex edge tuple `x`. -/
282noncomputable def hingeAreaSqC (x : SqEdges10C) (i j k : Fin 5) : ℂ :=
283 triangleAreaSqC (pentDistSqC x i j) (pentDistSqC x i k) (pentDistSqC x j k)
284
285/-! ## §4. The upper-half-plane Wick arc (S1, MODEL) -/
286
287/-- The canonical upper-half-plane continuation arc on the timelike squared
288edge: `arcZ a alpha t = alpha * a^2 * exp (i * pi * (1 - t))`.
289Endpoints: `t = 0` Lorentzian (`-(alpha * a^2)`), `t = 1` Euclidean
290(`+(alpha * a^2)`); interior strictly in `im > 0`. Matches the executed
291gate (RESULTS.txt §1) and the repo sign convention (see
292`continuationEdgesC_zero` / `continuationEdgesC_one`). -/
293noncomputable def arcZ (a alpha t : ℝ) : ℂ :=
294 ((alpha * a ^ 2 : ℝ) : ℂ) * Complex.exp (((Real.pi * (1 - t) : ℝ) : ℂ) * Complex.I)
295
296/-- The complex continuation of the causal squared-edge tuple along the
297Wick arc: timelike edges follow `arcZ`, spacelike edges stay `a^2` (S1). -/
298noncomputable def continuationEdgesC (ty : CausalPentType) (a alpha t : ℝ) :
299 SqEdges10C :=
300 fun e => if isTimelike ty e then arcZ a alpha t else ((a ^ 2 : ℝ) : ℂ)
301
302/-- THEOREM: Lorentzian endpoint `t = 0` of the arc. -/
303theorem arcZ_zero (a alpha : ℝ) : arcZ a alpha 0 = ((-(alpha * a ^ 2) : ℝ) : ℂ) := by
304 unfold arcZ
305 have h1 : (Real.pi * (1 - 0) : ℝ) = Real.pi := by ring
306 rw [h1, Complex.exp_pi_mul_I]
307 push_cast
308 ring
309
310/-- THEOREM: Euclidean endpoint `t = 1` of the arc. -/
311theorem arcZ_one (a alpha : ℝ) : arcZ a alpha 1 = ((alpha * a ^ 2 : ℝ) : ℂ) := by
312 unfold arcZ
313 have h1 : (Real.pi * (1 - 1) : ℝ) = 0 := by ring
314 rw [h1]
315 simp
316
317/-- THEOREM (endpoint identification): at `t = 0` the complex continuation
318tuple is exactly the kernel-checked real Lorentzian tuple of
319`CausalSimplex4D`, coerced to `ℂ`. -/
320theorem continuationEdgesC_zero (ty : CausalPentType) (a alpha : ℝ) :
321 continuationEdgesC ty a alpha 0
322 = fun e => ((lorentzianSqEdges ty a alpha e : ℝ) : ℂ) := by
323 funext e
324 unfold continuationEdgesC lorentzianSqEdges
325 by_cases h : isTimelike ty e = true
326 · rw [if_pos h, if_pos h, arcZ_zero]
327 · rw [if_neg h, if_neg h]
328
329/-- THEOREM (endpoint identification): at `t = 1` the complex continuation
330tuple is exactly the kernel-checked real Euclideanized (Wick-rotated)
331tuple of `CausalSimplex4D`, coerced to `ℂ`. -/
332theorem continuationEdgesC_one (ty : CausalPentType) (a alpha : ℝ) :
333 continuationEdgesC ty a alpha 1
334 = fun e => ((euclideanSqEdges ty a alpha e : ℝ) : ℂ) := by
335 funext e
336 unfold continuationEdgesC euclideanSqEdges
337 by_cases h : isTimelike ty e = true
338 · rw [if_pos h, if_pos h, arcZ_one]
339 · rw [if_neg h, if_neg h]
340
341/-! ## §5. The physical-point arc (`a = 1`, `alpha = 1`) -/
342
343/-- The physical-point arc `zArc t = exp (i * pi * (1 - t))` (unit lattice
344spacing, `alpha = 1`: the Lean physical point `physicalCausalPent`). -/
345noncomputable def zArc (t : ℝ) : ℂ := arcZ 1 1 t
346
347theorem zArc_eq_exp (t : ℝ) :
348 zArc t = Complex.exp (((Real.pi * (1 - t) : ℝ) : ℂ) * Complex.I) := by
349 unfold zArc arcZ
350 norm_num
351
352theorem zArc_re (t : ℝ) : (zArc t).re = Real.cos (Real.pi * (1 - t)) := by
353 rw [zArc_eq_exp]
354 exact Complex.exp_ofReal_mul_I_re _
355
356theorem zArc_im (t : ℝ) : (zArc t).im = Real.sin (Real.pi * (1 - t)) := by
357 rw [zArc_eq_exp]
358 exact Complex.exp_ofReal_mul_I_im _
359
360theorem zArc_zero : zArc 0 = -1 := by
361 unfold zArc
362 rw [arcZ_zero]
363 norm_num
364
365theorem zArc_one : zArc 1 = 1 := by
366 unfold zArc
367 rw [arcZ_one]
368 norm_num
369
370/-- THEOREM: the physical-point arc stays on the unit circle. -/
371theorem normSq_zArc (t : ℝ) : Complex.normSq (zArc t) = 1 := by
372 rw [Complex.normSq_apply, zArc_re, zArc_im]
373 have h := Real.sin_sq_add_cos_sq (Real.pi * (1 - t))
374 linear_combination h
375
376/-- THEOREM: on the open arc interior the continued edge lies strictly in
377the upper half-plane. -/
378theorem zArc_im_pos {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) : 0 < (zArc t).im := by
379 rw [zArc_im]
380 apply Real.sin_pos_of_pos_of_lt_pi
381 · have h1 : 0 < 1 - t := by linarith [ht.2]
382 exact mul_pos Real.pi_pos h1
383 · have h1 : 1 - t < 1 := by linarith [ht.1]
384 calc Real.pi * (1 - t) < Real.pi * 1 :=
385 mul_lt_mul_of_pos_left h1 Real.pi_pos
386 _ = Real.pi := mul_one _
387
388theorem continuous_zArc : Continuous zArc := by
389 have h : zArc = fun t : ℝ =>
390 Complex.exp (((Real.pi * (1 - t) : ℝ) : ℂ) * Complex.I) :=
391 funext zArc_eq_exp
392 rw [h]
393 exact Complex.continuous_exp.comp
394 ((Complex.continuous_ofReal.comp
395 (continuous_const.mul (continuous_const.sub continuous_id))).mul
396 continuous_const)
397
398/-- THEOREM: the traced hinge's cofactor `6 z - 2` never vanishes anywhere
399on the arc (including both endpoints): `|z| = 1` excludes `z = 1/3`. -/
400theorem denom_ne (t : ℝ) : 6 * zArc t - 2 ≠ 0 := by
401 intro h
402 have h6 : (6 : ℂ) * zArc t = 2 := by linear_combination h
403 have hns : Complex.normSq ((6 : ℂ) * zArc t) = Complex.normSq (2 : ℂ) := by
404 rw [h6]
405 rw [Complex.normSq_mul, normSq_zArc, mul_one, Complex.normSq_ofNat,
406 Complex.normSq_ofNat] at hns
407 norm_num at hns
408
409/-! ## §6. Closed forms for the traced (4,1) timelike hinge
410
411Hinge triangle `(0,1,4)`, opposite vertex pair `(2,3)` (CM rows/cols 3, 4),
412type fourOne, `a = 1`: the RESULTS.txt named offender/certificate hinge.
413The edge tuple has spacelike value `1` and timelike value `z`. -/
414
415/-- The fourOne complex edge tuple at unit spacelike value and timelike
416value `z` (this is `continuationEdgesC fourOne 1 1 t` at `z = zArc t`). -/
417noncomputable def hingeEdgesC (z : ℂ) : SqEdges10C :=
418 fun e => if isTimelike CausalPentType.fourOne e then z else 1
419
420/-- THEOREM: the physical-point continuation tuple is the two-value tuple
421at `z = zArc t`. -/
422theorem continuationEdgesC_physical (t : ℝ) :
423 continuationEdgesC CausalPentType.fourOne 1 1 t = hingeEdgesC (zArc t) := by
424 funext e
425 unfold continuationEdgesC hingeEdgesC zArc
426 by_cases h : isTimelike CausalPentType.fourOne e = true
427 · rw [if_pos h, if_pos h]
428 · rw [if_neg h, if_neg h]
429 norm_num
430
431/-- The explicit bordered `6 × 6` matrix of the fourOne tuple (spacelike 1,
432timelike `z`): rows/cols 1..5 are vertices 0..4, apex vertex 4 is row/col
4335 (mirror of `CausalSimplex4D.pentMatrix41` at `p = 1`, `q = z`). -/
434def hingeMatrixC (z : ℂ) : Matrix (Fin 6) (Fin 6) ℂ :=
435 fun i j =>
436 match i.val, j.val with
437 | 0, 0 => 0
438 | 0, _ => 1
439 | _, 0 => 1
440 | 1, 1 => 0
441 | 2, 2 => 0
442 | 3, 3 => 0
443 | 4, 4 => 0
444 | 5, 5 => 0
445 | 1, 5 => z
446 | 5, 1 => z
447 | 2, 5 => z
448 | 5, 2 => z
449 | 3, 5 => z
450 | 5, 3 => z
451 | 4, 5 => z
452 | 5, 4 => z
453 | _, _ => 1
454
455/-- THEOREM: the general complex CM matrix of the two-value tuple is the
456explicit matrix. -/
457theorem cmMatrixC_hingeEdges (z : ℂ) :
458 cmMatrixC (hingeEdgesC z) = hingeMatrixC z := by
459 ext i j
460 fin_cases i <;> fin_cases j <;> rfl
461
462/-- The `5 × 5` minor of `hingeMatrixC` deleting row 3, column 3 (also,
463by the vertex-2/vertex-3 symmetry, the (4,4) minor). -/
464def minorPPC (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
465 fun i j =>
466 match i.val, j.val with
467 | 0, 0 => 0
468 | 0, _ => 1
469 | _, 0 => 1
470 | 1, 1 => 0
471 | 2, 2 => 0
472 | 3, 3 => 0
473 | 4, 4 => 0
474 | 1, 4 => z
475 | 4, 1 => z
476 | 2, 4 => z
477 | 4, 2 => z
478 | 3, 4 => z
479 | 4, 3 => z
480 | _, _ => 1
481
482/-- The `5 × 5` minor of `hingeMatrixC` deleting row 3, column 4. -/
483def minorPQC (z : ℂ) : Matrix (Fin 5) (Fin 5) ℂ :=
484 fun i j =>
485 match i.val, j.val with
486 | 0, 0 => 0
487 | 0, _ => 1
488 | _, 0 => 1
489 | 1, 1 => 0
490 | 2, 2 => 0
491 | 4, 4 => 0
492 | 1, 4 => z
493 | 2, 4 => z
494 | 3, 4 => z
495 | 4, 1 => z
496 | 4, 2 => z
497 | 4, 3 => z
498 | _, _ => 1
499
500theorem submatrix_pp (z : ℂ) :
501 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (3 : Fin 6))
502 (Fin.succAbove (3 : Fin 6)) = minorPPC z := by
503 ext i j
504 fin_cases i <;> fin_cases j <;> rfl
505
506theorem submatrix_qq (z : ℂ) :
507 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (4 : Fin 6))
508 (Fin.succAbove (4 : Fin 6)) = minorPPC z := by
509 ext i j
510 fin_cases i <;> fin_cases j <;> rfl
511
512theorem submatrix_pq (z : ℂ) :
513 Matrix.submatrix (hingeMatrixC z) (Fin.succAbove (3 : Fin 6))
514 (Fin.succAbove (4 : Fin 6)) = minorPQC 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
520/-- THEOREM (symbolic 5x5 determinant): the diagonal minor is `6z - 2`
521(RESULTS.txt closed form `C_pp = C_qq = 6z - 2`; at `z = 1` this is the
522regular unit tetrahedron CM determinant 4). -/
523theorem det_minorPPC (z : ℂ) : Matrix.det (minorPPC z) = 6 * z - 2 := by
524 unfold minorPPC
525 -- Style note: bare `simp` retained deliberately, mirroring the proved
526 -- pattern of `CausalSimplex4D.det_pentMatrix41` (the default simp set's
527 -- numeric simprocs are needed to keep the expansion tractable).
528 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
529 ring
530
531set_option maxHeartbeats 8000000 in
532set_option maxRecDepth 16384 in
533/-- THEOREM (symbolic 5x5 determinant): the off-diagonal minor is `2z - 1`
534(cofactor sign `(-1)^7 = -1` gives `C_pq = 1 - 2z`). -/
535theorem det_minorPQC (z : ℂ) : Matrix.det (minorPQC z) = 2 * z - 1 := by
536 unfold minorPQC
537 -- Style note: bare `simp` retained deliberately; see `det_minorPPC`.
538 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
539 ring
540
541/-- THEOREM: closed form `C_pp = 6z - 2` (CM row/col 3, vertex 2). -/
542theorem cofactor_pp (z : ℂ) :
543 cmCofactorC (hingeEdgesC z) 3 3 = 6 * z - 2 := by
544 unfold cmCofactorC cmCofactorSignC cmMinorC
545 rw [cmMatrixC_hingeEdges, submatrix_pp, det_minorPPC,
546 if_pos (by decide : Even ((3 : Fin 6).val + (3 : Fin 6).val))]
547 ring
548
549/-- THEOREM: closed form `C_qq = 6z - 2` (CM row/col 4, vertex 3). -/
550theorem cofactor_qq (z : ℂ) :
551 cmCofactorC (hingeEdgesC z) 4 4 = 6 * z - 2 := by
552 unfold cmCofactorC cmCofactorSignC cmMinorC
553 rw [cmMatrixC_hingeEdges, submatrix_qq, det_minorPPC,
554 if_pos (by decide : Even ((4 : Fin 6).val + (4 : Fin 6).val))]
555 ring
556
557/-- THEOREM: closed form `C_pq = 1 - 2z` (CM rows/cols 3, 4). -/
558theorem cofactor_pq (z : ℂ) :
559 cmCofactorC (hingeEdgesC z) 3 4 = 1 - 2 * z := by
560 unfold cmCofactorC cmCofactorSignC cmMinorC
561 rw [cmMatrixC_hingeEdges, submatrix_pq, det_minorPQC,
562 if_neg (by decide : ¬ Even ((3 : Fin 6).val + (4 : Fin 6).val))]
563 ring
564
565set_option maxHeartbeats 2000000 in
566/-- THEOREM: closed form of the hinge area-squared, `areaSq = z/4 - 1/16`
567(hinge `(0,1,4)`: edges `(0,1) = 1` spacelike, `(0,4) = (1,4) = z`
568timelike; at `z = 1` this is the regular hinge value `3/16`). -/
569theorem hingeAreaSqC_closed (z : ℂ) :
570 hingeAreaSqC (hingeEdgesC z) 0 1 4 = z / 4 - 1 / 16 := by
571 unfold hingeAreaSqC triangleAreaSqC
572 have h1 : pentDistSqC (hingeEdgesC z) 0 1 = 1 := rfl
573 have h2 : pentDistSqC (hingeEdgesC z) 0 4 = z := rfl
574 have h3 : pentDistSqC (hingeEdgesC z) 1 4 = z := rfl
575 rw [h1, h2, h3]
576 unfold triCMMatrixC
577 -- Style note: bare `simp` retained deliberately; see `det_minorPPC`.
578 simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
579 ring
580
581/-! ## §7. Branch regularity (S3) -/
582
583/-- Off the classical arccos cuts `(-∞, -1]` and `[1, ∞)` on the real
584axis: the open region where any principal (log-based) complex arccos is
585continuous. Mathlib has no `Complex.arccos`; the cut region is encoded
586directly. -/
587def OffArccosCut (w : ℂ) : Prop := w.im ≠ 0 ∨ (-1 < w.re ∧ w.re < 1)
588
589/-- MODEL (S3 predicate): branch regularity of the split-form hinge
590continuation on a parameter set `s`: both diagonal cofactors stay off the
591`csqrt` branch cut (i.e. in `Complex.slitPlane`, the exact continuity
592region of `Complex.cpow (1/2)`), and the split cosine ratio stays off the
593arccos cuts. -/
594def BranchRegularOn (x : ℝ → SqEdges10C) (p q : Fin 5) (s : Set ℝ) : Prop :=
595 ∀ t ∈ s,
596 cmCofactorC (x t) (cmVertexIndexC p) (cmVertexIndexC p) ∈ Complex.slitPlane
597 ∧ cmCofactorC (x t) (cmVertexIndexC q) (cmVertexIndexC q) ∈ Complex.slitPlane
598 ∧ OffArccosCut (dihedralCosSplitC (x t) p q)
599
600/-- The split-form cosine path of the traced hinge along the physical
601arc: `t ↦ C_pq / (csqrt C_pp * csqrt C_qq)` at hinge `(0,1,4)`, opposite
602pair `(2,3)`, type fourOne, `a = alpha = 1`. -/
603noncomputable def hingeCosPath (t : ℝ) : ℂ :=
604 dihedralCosSplitC (continuationEdgesC CausalPentType.fourOne 1 1 t) 2 3
605
606/-- THEOREM (branch collapse of the split form): everywhere on the arc the
607split-form cosine equals the cut-free rational function
608`(1 - 2z)/(6z - 2)` (the two split square roots multiply back to the
609non-vanishing cofactor `6z - 2`). This holds for ALL `t : ℝ`, endpoints
610included. -/
611theorem hingeCosPath_eq_moebius (t : ℝ) :
612 hingeCosPath t = (1 - 2 * zArc t) / (6 * zArc t - 2) := by
613 unfold hingeCosPath dihedralCosSplitC dihedralDenomSplitC
614 rw [continuationEdgesC_physical]
615 have hv2 : cmVertexIndexC 2 = 3 := rfl
616 have hv3 : cmVertexIndexC 3 = 4 := rfl
617 rw [hv2, hv3, cofactor_pp, cofactor_qq, cofactor_pq,
618 csqrt_mul_self (denom_ne t)]
619
620/-- THEOREM (S3 inhabitation certificate, FULL open interior): the traced
621fourOne timelike hinge — triangle `(0,1,4)`, opposite pair `(2,3)`,
622`a = 1`, `alpha = 1` — is branch-regular on ALL of `Set.Ioo 0 1`: both
623cofactors `6z - 2` stay off the sqrt cut (their imaginary part `6 im z` is
624strictly positive) and the split cosine stays off the arccos cuts (its
625imaginary part `-2 im z / normSq (6z-2)` is strictly negative). This is
626the Lean transcription of the trace's interior margins (0.625 on this
627hinge; RESULTS.txt §3). -/
628theorem branchRegular_fourOne_hinge :
629 BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t)
630 2 3 (Set.Ioo 0 1) := by
631 intro t ht
632 dsimp only
633 have hy : 0 < (zArc t).im := zArc_im_pos ht
634 have hv2 : cmVertexIndexC 2 = 3 := rfl
635 have hv3 : cmVertexIndexC 3 = 4 := rfl
636 have him6 : (6 * zArc t - 2).im = 6 * (zArc t).im := by
637 simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
638 Complex.im_ofNat]
639 ring
640 have hslit : 6 * zArc t - 2 ∈ Complex.slitPlane := by
641 apply Complex.mem_slitPlane_iff.mpr
642 right
643 rw [him6]
644 exact (mul_pos (by norm_num : (0 : ℝ) < 6) hy).ne'
645 refine ⟨?_, ?_, ?_⟩
646 · rw [hv2, continuationEdgesC_physical, cofactor_pp]
647 exact hslit
648 · rw [hv3, continuationEdgesC_physical, cofactor_qq]
649 exact hslit
650 · left
651 have hpath : dihedralCosSplitC (continuationEdgesC CausalPentType.fourOne 1 1 t) 2 3
652 = hingeCosPath t := rfl
653 rw [hpath, hingeCosPath_eq_moebius t]
654 have hnum : (1 - 2 * zArc t).im * (6 * zArc t - 2).re
655 - (1 - 2 * zArc t).re * (6 * zArc t - 2).im = -2 * (zArc t).im := by
656 simp only [Complex.sub_im, Complex.sub_re, Complex.mul_im, Complex.mul_re,
657 Complex.one_im, Complex.one_re, Complex.re_ofNat, Complex.im_ofNat]
658 ring
659 have hdiv : ((1 - 2 * zArc t) / (6 * zArc t - 2)).im
660 = (-2 * (zArc t).im) / Complex.normSq (6 * zArc t - 2) := by
661 rw [Complex.div_im, div_sub_div_same, hnum]
662 rw [hdiv]
663 apply div_ne_zero
664 · have hlt : (-2 : ℝ) * (zArc t).im < 0 :=
665 mul_neg_of_neg_of_pos (by norm_num) hy
666 exact ne_of_lt hlt
667 · exact (Complex.normSq_pos.mpr (denom_ne t)).ne'
668
669/-- THEOREM: the hinge area-squared also stays off the sqrt cut on the full
670open interior (`im (z/4 - 1/16) = im z / 4 > 0`); at the Lorentzian
671endpoint it sits ON the cut boundary (`-5/16`, the imaginary Lorentzian
672area, an ALLOWED endpoint contact per the gate). -/
673theorem hingeAreaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
674 hingeAreaSqC (continuationEdgesC CausalPentType.fourOne 1 1 t) 0 1 4
675 ∈ Complex.slitPlane := by
676 rw [continuationEdgesC_physical, hingeAreaSqC_closed]
677 apply Complex.mem_slitPlane_iff.mpr
678 right
679 have hy : 0 < (zArc t).im := zArc_im_pos ht
680 have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
681 simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
682 ring
683 rw [him]
684 exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'
685
686/-! ## §8. The boundary-continuation theorem (S4) -/
687
688/-- THEOREM: the split-form cosine path is continuous on the CLOSED
689interval `[0, 1]` (it coincides there with the cut-free rational function
690of the arc, whose denominator never vanishes). -/
691theorem continuousOn_hingeCosPath : ContinuousOn hingeCosPath (Set.Icc 0 1) := by
692 have hmo : Continuous fun t => (1 - 2 * zArc t) / (6 * zArc t - 2) := by
693 apply Continuous.div
694 · exact continuous_const.sub (continuous_const.mul continuous_zArc)
695 · exact (continuous_const.mul continuous_zArc).sub continuous_const
696 · exact fun t => denom_ne t
697 exact hmo.continuousOn.congr fun t _ => hingeCosPath_eq_moebius t
698
699/-- THEOREM: Lorentzian endpoint value of the SPLIT form: `-(3/8)`.
700(The real product-form formula gives `+3/8` here; see
701`lorentzian_endpoint_sign_factor` for the documented sign factor.) -/
702theorem hingeCosPath_zero : hingeCosPath 0 = -(3 / 8 : ℂ) := by
703 rw [hingeCosPath_eq_moebius, zArc_zero]
704 norm_num
705
706/-- THEOREM: Euclidean endpoint value: `-(1/4)`, the regular unit
7074-simplex value in the `+C_pq` convention (textbook `-C` interior dihedral
708cosine `+1/4`; RESULTS.txt endpoint table). -/
709theorem hingeCosPath_one : hingeCosPath 1 = -(1 / 4 : ℂ) := by
710 rw [hingeCosPath_eq_moebius, zArc_one]
711 norm_num
712
713/-- THEOREM (S4, the boundary-continuation receipt): the split-form
714complex dihedral cosine of the traced fourOne timelike hinge is a
715continuous path on `[0, 1]` connecting the Lorentzian endpoint value
716`-(3/8)` at `t = 0` to the Euclidean regular-4-simplex value `-(1/4)` at
717`t = 1`. The Lorentzian endpoint carries the documented sign factor
718relative to the real product-form formula (`lorentzian_endpoint_sign_factor`);
719no unrestricted equality with the real Lorentzian formula is claimed. -/
720theorem wick_boundary_continuation_fourOne_hinge :
721 ContinuousOn hingeCosPath (Set.Icc 0 1)
722 ∧ hingeCosPath 0 = -(3 / 8 : ℂ)
723 ∧ hingeCosPath 1 = -(1 / 4 : ℂ) :=
724 ⟨continuousOn_hingeCosPath, hingeCosPath_zero, hingeCosPath_one⟩
725
726/-- The real product-form (single `Real.sqrt` of the cofactor product)
727Lorentzian value at the endpoint `z = -1`:
728`C_pq / Real.sqrt (C_pp * C_qq) = 3 / sqrt 64 = 3/8`. -/
729noncomputable def realLorentzianProductCos : ℝ :=
730 (1 - 2 * (-1 : ℝ)) / Real.sqrt ((6 * (-1 : ℝ) - 2) * (6 * (-1 : ℝ) - 2))
731
732theorem realLorentzianProductCos_eq : realLorentzianProductCos = 3 / 8 := by
733 unfold realLorentzianProductCos
734 have h64 : ((6 * (-1 : ℝ) - 2) * (6 * (-1 : ℝ) - 2)) = 64 := by norm_num
735 rw [h64, show (64 : ℝ) = 8 ^ 2 by norm_num,
736 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 8)]
737 norm_num
738
739/-- THEOREM (S4 documented sign convention): at the Lorentzian endpoint,
740where both cofactors are negative (`C_pp = C_qq = -8`), the split form
741equals `(-1) *` (the real product-form value): `csqrt w * csqrt w = w`,
742not `|w|`, so the split denominator is `-8` where `Real.sqrt 64 = +8`.
743The sign factor is exactly `-1` on this hinge (trace: split `-3/8` vs
744real-formula `+3/8`, RESULTS.txt §3 endpoint note). -/
745theorem lorentzian_endpoint_sign_factor :
746 hingeCosPath 0 = (-1 : ℂ) * ((realLorentzianProductCos : ℝ) : ℂ) := by
747 rw [hingeCosPath_zero, realLorentzianProductCos_eq]
748 push_cast
749 ring
750
751/-- THEOREM (endpoint cut contact, honest disclosure): at the Lorentzian
752endpoint the diagonal cofactor is `-8`, which lies ON the `csqrt` branch
753cut (off `Complex.slitPlane`). The branch certificate is therefore stated
754on the OPEN interior; the endpoint values themselves are still exact
755(`hingeCosPath_zero`) because the split form collapses to the cut-free
756rational function (`hingeCosPath_eq_moebius`). -/
757theorem endpoint_cofactor_on_sqrt_cut :
758 cmCofactorC (continuationEdgesC CausalPentType.fourOne 1 1 0) 3 3 = -8
759 ∧ (-8 : ℂ) ∉ Complex.slitPlane := by
760 constructor
761 · rw [continuationEdgesC_physical, cofactor_pp, zArc_zero]
762 ring
763 · intro hmem
764 rw [Complex.mem_slitPlane_iff] at hmem
765 simp at hmem
766 linarith
767
768/-! ## §9. The product-form negative certificate (gate FAIL, memorialized) -/
769
770/-- The exact interior crossing parameter of the product form on this
771hinge: `tStar = 1 - arccos(1/3)/pi ≈ 0.6081734480` (RESULTS.txt §3,
772named canonical offender). -/
773noncomputable def tStar : ℝ := 1 - Real.arccos (1 / 3) / Real.pi
774
775theorem tStar_mem_Ioo : tStar ∈ Set.Ioo (0 : ℝ) 1 := by
776 have hpi := Real.pi_pos
777 have h1 : 0 < Real.arccos (1 / 3) := Real.arccos_pos.mpr (by norm_num)
778 have h2 : Real.arccos (1 / 3) ≤ Real.pi / 2 :=
779 Real.arccos_le_pi_div_two.mpr (by norm_num)
780 constructor
781 · have hle : Real.arccos (1 / 3) / Real.pi ≤ 1 / 2 := by
782 rw [div_le_iff₀ hpi]
783 linarith
784 unfold tStar
785 linarith
786 · have hgt : 0 < Real.arccos (1 / 3) / Real.pi := div_pos h1 hpi
787 unfold tStar
788 linarith
789
790theorem arg_tStar : Real.pi * (1 - tStar) = Real.arccos (1 / 3) := by
791 have hpne : Real.pi ≠ 0 := Real.pi_ne_zero
792 unfold tStar
793 have h : (1 : ℝ) - (1 - Real.arccos (1 / 3) / Real.pi)
794 = Real.arccos (1 / 3) / Real.pi := by ring
795 rw [h, mul_comm, div_mul_cancel₀ _ hpne]
796
797theorem cos_arg_tStar : Real.cos (Real.pi * (1 - tStar)) = 1 / 3 := by
798 rw [arg_tStar]
799 exact Real.cos_arccos (by norm_num) (by norm_num)
800
801/-- THEOREM (exact crossing value): at `tStar` the arc point is
802`z = 1/3 + i * sin(arccos(1/3))` and the product-form denominator argument
803`C_pp * C_qq = (6z - 2)^2` equals `-32` EXACTLY: a real negative value in
804the interior of the arc. -/
805theorem product_form_crossing_value :
806 (6 * zArc tStar - 2) * (6 * zArc tStar - 2) = -32 := by
807 have hz : zArc tStar = ((1 / 3 : ℝ) : ℂ)
808 + ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) * Complex.I := by
809 rw [zArc_eq_exp, Complex.exp_mul_I, ← Complex.ofReal_cos,
810 ← Complex.ofReal_sin, cos_arg_tStar]
811 have h6z : 6 * zArc tStar - 2
812 = ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) * Complex.I * 6 := by
813 rw [hz]
814 push_cast
815 ring
816 have hprod : (6 * zArc tStar - 2) * (6 * zArc tStar - 2)
817 = -(36 : ℂ) * ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) ^ 2 := by
818 rw [h6z]
819 linear_combination (36 * ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) ^ 2)
820 * Complex.I_sq
821 have hs2 : Real.sin (Real.pi * (1 - tStar)) ^ 2 = 8 / 9 := by
822 rw [Real.sin_sq, cos_arg_tStar]
823 norm_num
824 have hcast : ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) ^ 2
825 = ((8 / 9 : ℝ) : ℂ) := by
826 rw [← Complex.ofReal_pow, hs2]
827 rw [hprod, hcast]
828 push_cast
829 norm_num
830
831/-- THEOREM (the gate's FAIL event, kernel-checked): at the interior arc
832parameter `tStar ∈ (0, 1)` the product `C_pp * C_qq` of the traced hinge's
833diagonal cofactors equals `-32` exactly, which lies ON the `csqrt` branch
834cut (off `Complex.slitPlane`). This is the negative certificate that
835KILLS the literal single-sqrt product transcription
836`csqrt (C_pp * C_qq)` of the 3D formula
837`Geometry.DihedralCayleyMenger.dihedralDenom3`, and it is why
838`dihedralDenomSplitC` is definitionally split (RESULTS.txt final verdict:
839product FAIL, split PASS). -/
840theorem product_form_crossing :
841 tStar ∈ Set.Ioo (0 : ℝ) 1
842 ∧ cmCofactorC (continuationEdgesC CausalPentType.fourOne 1 1 tStar) 3 3
843 * cmCofactorC (continuationEdgesC CausalPentType.fourOne 1 1 tStar) 4 4
844 = -32
845 ∧ (-32 : ℂ) ∉ Complex.slitPlane := by
846 refine ⟨tStar_mem_Ioo, ?_, ?_⟩
847 · rw [continuationEdgesC_physical, cofactor_pp, cofactor_qq]
848 exact product_form_crossing_value
849 · intro hmem
850 rw [Complex.mem_slitPlane_iff] at hmem
851 simp at hmem
852 linarith
853
854/-! ## §10. Axiom audit
855
856`#print axioms` receipts for the load-bearing theorems. Expected output
857for each: `[propext, Classical.choice, Quot.sound]` (the standard Mathlib
858trio; no `sorryAx`, no `Lean.ofReduceBool`, no repo-local axioms). The
859output appears as `info` lines in the build log. -/
860
861#print axioms branchRegular_fourOne_hinge
862#print axioms wick_boundary_continuation_fourOne_hinge
863#print axioms lorentzian_endpoint_sign_factor
864#print axioms product_form_crossing
865#print axioms hingeAreaSq_interior_off_cut
866#print axioms endpoint_cofactor_on_sqrt_cut
867
868end WickActionComplexFirst
869end SevenGaps
870end Gravity
871end IndisputableMonolith
872