det_minor32_45C
plain-language theorem explainer
The determinant of the explicit 5×5 off-diagonal Cayley–Menger minor for the spacelike hinge of the (3,2) causal 4-simplex equals 6z−5 on the complex plane. QG and gravity workers cite it when building the mixed cofactor C_{pq}=5−6z for opposite pair (3,4). The proof unfolds the minor and collapses the determinant by first-row expansion plus ring arithmetic.
Claim. For every $z\in\mathbb{C}$, if $M(z)$ is the explicit $5\times 5$ complex matrix obtained by deleting row index $4$ and column index $5$ from the Cayley–Menger matrix of the $(3,2)$ hinge edge data, then $\det M(z)=6z-5$.
background
Lane B2 of the QG Seven-Gaps campaign certifies Wick continuation for all ten triangular hinges of the threeTwo causal 4-simplex (lower slice ${0,1,2}$, upper slice ${3,4}$) at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc. Opposite pairs label hinges; the single spacelike hinge is opposite pair $(3,4)$, with closed forms $C_{pp}=C_{qq}=6z-2$ and $C_{pq}=5-6z$.
The object here is the off-diagonal minor at Cayley–Menger indices $(4,5)$ for that spacelike hinge: a concrete $5\times 5$ complex matrix whose nonzero pattern encodes the remaining edge lengths after the two deleted vertices. Its determinant is the unsigned building block of the corresponding cofactor.
Upstream, the minor is defined entrywise by a finite case match on row and column indices (zeros on the diagonal slots that survive deletion, a lone $z$ in one off-diagonal slot, and the remaining hinge lengths). The Loom det import is unrelated scaffolding; the proof uses Mathlib matrix determinants.
proof idea
Term-mode tactic proof. Unfold the explicit entrywise definition of the minor. Apply Matrix.det_succ_row_zero together with Fin.sum_univ_succ and Fin.succAbove to expand the $5\times 5$ determinant along the first row and reduce the finite sums over Fin. The resulting polynomial identity is discharged by ring, yielding $6z-5$.
why it matters
Direct input to the cofactor theorem for CM indices $(4,5)$: after inserting the sign of the $(4,5)$ position (odd parity), one obtains $C_{pq}=5-6z$ for the spacelike hinge. That closed form is the off-diagonal entry in the split-form branch certificate for opposite pair $(3,4)$, matching the executed per-hinge table of the Wick-arc trace.
Within the module taxonomy this is the unique spacelike hinge (one of ten); its cofactors feed the all-hinge complex-first continuation and the honest endpoint disclosure that the split cosine meets the arccos cut exactly at the Lorentzian endpoint $t=0$. The identity is kernel-checked algebra, not a numerical fit, so it locks the rational factor $(5-6z)/(6z-2)$ used on the open arc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.