det_minor32_35C
plain-language theorem explainer
The 5×5 Cayley–Menger minor obtained by deleting row/column pair (3,5) of the complex hinge matrix for the (3,2) simplex has determinant identically −1 for every complex z. Gravity and QG workers cite it when assembling the mixed-hinge cofactor C_pq = −1. The proof unfolds the sparse minor and reduces the Laplace expansion by ring arithmetic.
Claim. For every $z \in \mathbb{C}$, the determinant of the $5\times 5$ complex matrix obtained as the mixed off-diagonal Cayley–Menger minor at index pair $(3,5)$ (opposite edge pair $(2,4)$ of the $(3,2)$ causal 4-simplex) equals $-1$.
background
Lane B2 of the QG Seven-Gaps campaign certifies Wick continuation for all ten triangular hinges of the threeTwo causal 4-simplex at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc. Hinges are classified by opposite vertex pairs: spacelike, mixed (one lower, one upper), and upper-pair.
Mixed hinges (six pairs) carry asymmetric closed cofactors $C_{pp}=8z-4$, $C_{qq}=6z-2$, and the constant off-diagonal $C_{pq}=-1$, with squared area $z/4-1/16$. The object minor32_35C is the explicit $5\times 5$ complex submatrix of the Cayley–Menger matrix after deleting the mixed index pair $(3,5)$ corresponding to opposite pair $(2,4)$; most entries are $0$, $1$, or $\pm z$ from the hinge edge lengths.
All closed forms in the module are kernel-checked by such explicit minors against the per-hinge table of the executed Wick-arc trace.
proof idea
Term-mode proof. Unfold the definition of the sparse $5\times 5$ minor, then apply Matrix.det_succ_row_zero together with the finite-sum expansions Fin.sum_univ_succ and Fin.succAbove to expand the determinant along the first row (which is almost entirely zero). The resulting polynomial identity collapses by ring to the constant $-1$, with no residual $z$ dependence.
why it matters
Feeds directly into cof32_35, which assembles the signed Cayley–Menger cofactor at $(3,5)$ and obtains $C_{pq}=-1$ for this mixed hinge. That constant off-diagonal cofactor is one of the three closed forms listed for mixed pairs in the module charter and is required for the split-form branch certificate on the physical arc.
Within the Seven-Gaps finishing charter this is a kernel check: the symbolic minor determinant must match the tabulated $C_{pq}=-1$ before the cosine/arccos branch analysis and the product-form kill certificates can be trusted. It is local linear algebra supporting the all-hinge Wick continuation, not a global forcing-chain step (T0–T8), but it closes an explicit gap in the gravity lane’s complex-first pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.