minor32_35C
plain-language theorem explainer
Explicit 5×5 complex matrix for the mixed off-diagonal Cayley–Menger minor at position (3,5), opposite pair (2,4), on the (3,2) causal 4-simplex hinge. Gravity/QG workers cite it when checking mixed-hinge cofactors along the Wick arc. The body is a pure entrywise case table in z, zeros, and ones.
Claim. For each $z\in\mathbb{C}$, define the $5\times 5$ complex matrix $M_{35}(z)$ whose entries are $0$ on $(0,0)$, $(1,1)$, $(2,2)$, and $(3,4)$; equal to $z$ at $(1,4)$, $(2,4)$, $(3,1)$, $(3,2)$, $(3,3)$, $(4,1)$, $(4,2)$, $(4,3)$; and equal to $1$ at every remaining index. This is the mixed off-diagonal minor at Cayley–Menger slot $(3,5)$ for opposite pair $(2,4)$.
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex (lower slice ${0,1,2}$, upper ${3,4}$) by complex-first Wick continuation at the physical point $a=1$, $\alpha=1$ on the canonical upper-half-plane arc. Hinge class is fixed by the opposite pair ${p,q}$.
Mixed pairs (one lower, one upper vertex) give six hinges with two timelike triangle edges. Their closed cofactors are asymmetric: $C_{pp}=8z-4$ on the lower member, $C_{qq}=6z-2$ on the upper, $C_{pq}=-1$, and $\mathrm{areaSq}=z/4-1/16$. Those identities are kernel-checked by explicit $5\times 5$ minors of the complex hinge matrix.
This object is the minor obtained by deleting the complementary row/column pair so that the remaining block sits at CM index $(3,5)$ for opposite pair $(2,4)$. Sibling minors cover the other mixed and upper-pair slots.
proof idea
Definition only: no proof obligations. The matrix is given by a match on (i.val, j.val), listing the twelve special entries (four zeros, eight copies of the complex parameter $z$) and defaulting every other entry to $1$. Downstream proofs unfold this table and compute by finite case analysis on Fin 5.
why it matters
Supplies the concrete minor that submatrix32_35 identifies with the $(3,5)$-deletion of hingeMatrix32C, and that det_minor32_35C evaluates to $-1$. That constant determinant is the algebraic certificate behind the mixed-hinge off-diagonal cofactor $C_{pq}=-1$ in the closed-form table for all six mixed hinges of the (3,2) simplex.
In the broader Seven-Gaps finishing charter this is one kernel check on the split-form branch certificate for Wick continuation of every triangular hinge, matching the per-hinge trace table. It does not itself touch the spacelike-hinge endpoint cut or the product-form kill certificates; those live on other hinge classes and separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.