submatrix32_35
plain-language theorem explainer
The 5×5 submatrix of the complex (3,2) hinge Cayley–Menger matrix obtained by deleting row index 3 and column index 5 equals the hand-written mixed minor for opposite pair (2,4). Cofactor and closed-form hinge certificates cite this equality. The proof is a finite case split on Fin 5 indices with definitional equality.
Claim. For every $z \in \mathbb{C}$, the submatrix of the bordered $6\times 6$ complex hinge matrix of the $(3,2)$ simplex at parameter $z$ obtained by deleting row $3$ and column $5$ (0-based) equals the explicit mixed off-diagonal $5\times 5$ minor associated to opposite pair $(2,4)$.
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex in the complex-first Wick setting. The ambient object is the bordered $6\times 6$ Cayley–Menger matrix of the threeTwo tuple (spacelike edge length 1, timelike edge length $z$): rows/cols 1..3 index the lower-slice vertices $0,1,2$ and rows/cols 4..5 the upper-slice vertices $3,4$.
Hinge closed forms are certified by explicit $5\times 5$ minors. The mixed class (one lower and one upper opposite vertex) has asymmetric cofactors; the minor at CM indices $(3,5)$ is the off-diagonal entry for opposite pair $(2,4)$. The hand-coded matrix minor32_35C packages that $5\times 5$ block entrywise (border row/column of ones, diagonal zeros on the remaining vertices, and the single $z$ in the surviving timelike slot).
This lemma identifies Mathlib's generic Matrix.submatrix deletion of row 3 and column 5 with that explicit minor, so later cofactor computations can rewrite into a concrete determinant.
proof idea
Pointwise extensionality on the two Fin 5 indices, then exhaustive fin_cases on both. Each of the 25 cells reduces by rfl to the corresponding match arm of the explicit minor definition, so the equality is purely definitional once indices are concrete.
why it matters
Feeds the cofactor identity cof32_35, which proves that the $(3,5)$ Cayley–Menger cofactor of the hinge edge tuple equals $-1$ for every complex $z$. That constant cofactor is one of the mixed-pair closed forms in the module charter ($C_{pq}=-1$ for hinges with two timelike triangle edges, area squared $z/4-1/16$).
Those closed forms are the kernel checks that match the executed Wick-arc trace table and underwrite the split-form branch certificates on the physical upper-half-plane arc. Without the submatrix identification, the cofactor proof cannot bridge Mathlib's generic minor construction to the hand-checked $5\times 5$ determinant. In the broader Recognition gravity stack this is bookkeeping inside the (3,2) simplex hinge analysis, not a forcing-chain step, but it is required scaffolding for the all-hinge Wick continuation deliverable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.