submatrix32_24
plain-language theorem explainer
Removing row index 2 and column index 4 from the bordered 6×6 complex hinge matrix of the (3,2) causal 4-simplex yields exactly the hand-written 5×5 mixed minor at CM entry (2,4). Anyone computing Cayley–Menger cofactors for the six mixed triangular hinges cites this identification. The proof is a pure matrix extensionality check: all 25 entries match by finite case split and reflexivity.
Claim. For every complex parameter $z$, the $5\times 5$ submatrix of the bordered hinge matrix $H_{32}(z)$ obtained by deleting row $2$ and column $4$ (0-based indices in $\mathrm{Fin}\,6$) equals the explicitly tabulated mixed minor $M_{24}(z)$ associated to the opposite pair $(1,3)$.
background
Lane B2 of the QG Seven-Gaps campaign treats the all-hinge complex-first Wick continuation of the (3,2) causal 4-simplex at the physical point $a=1$, $\alpha=1$. The lower slice is vertices ${0,1,2}$, the upper slice ${3,4}$; the six cross edges are the timelike ones.
The bordered matrix $H_{32}(z)$ is the complex Cayley–Menger matrix of that simplex (spacelike edge length 1, timelike length $z$), with a leading border row/column of ones. Mixed opposite pairs (one lower, one upper vertex) produce asymmetric triangular hinges whose cofactors are read from 5×5 minors of $H_{32}(z)$.
The definition $M_{24}(z)$ is the hand-expanded minor at CM position $(2,4)$, corresponding to opposite pair $(1,3)$. Establishing that the abstract Matrix.submatrix deletion equals this table is the bridge from the matrix API to the closed-form cofactor algebra used later in the module.
proof idea
Term-mode proof by matrix extensionality: ext i j reduces equality of two $5\times 5$ complex matrices to entrywise equality. Both index types are Fin 5, so fin_cases i followed by fin_cases j enumerates all 25 pairs; each residual goal is definitional (rfl) once the succAbove deletion maps and the match-table of $M_{24}(z)$ are unfolded. No algebraic lemmas are required beyond the definitions of $H_{32}(z)$ and $M_{24}(z)$.
why it matters
Parent theorem cof32_24 rewrites the abstract Cayley–Menger cofactor through this identification, then applies the already-proved determinant of $M_{24}(z)$ and the even-parity sign rule, concluding that the cofactor equals $-1$ identically in $z$. That constant cofactor is the closed form $C_{pq}=-1$ listed in the module doc for all six mixed hinges (2 timelike triangle edges, area squared $z/4-1/16$).
Those closed forms kernel-check the per-hinge table of the executed Wick-arc trace and feed the split-form branch certificates on the canonical upper-half-plane arc. Within Recognition Science gravity, the certificates close the complex-first continuation of every triangular hinge of the (3,2) 4-simplex, a required step of the Seven-Gaps finishing charter (lane B2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.