submatrix32_13
plain-language theorem explainer
Removing row index 1 and column index 3 from the complex (3,2) hinge matrix yields the explicit 5×5 upper-pair off-diagonal minor at CM entry (1,3). Anyone computing cofactors of the bordered Cayley–Menger matrix for the threeTwo simplex cites this identity. The proof is exhaustive entrywise equality on Fin 5 × Fin 5 via fin_cases.
Claim. For every complex $z$, the $5\times 5$ submatrix of the bordered $(3,2)$ hinge matrix obtained by deleting row $1$ and column $3$ equals the explicitly tabulated upper-pair off-diagonal minor associated to Cayley–Menger indices $(1,3)$ (opposite vertex pair $(0,2)$).
background
Lane B2 of the QG Seven-Gaps campaign treats the complex-first Wick continuation of all ten triangular hinges of the threeTwo causal 4-simplex at the physical point $a=1$, $\alpha=1$. The ambient object is the bordered $6\times 6$ hinge matrix whose rows/cols $1..3$ are the lower-slice vertices $0..2$ and rows/cols $4..5$ the upper-slice vertices $3..4$, with spacelike edge length $1$ and timelike edge length $z$.
Cofactors of that matrix are computed from $5\times 5$ minors. The definition minor32_13C hard-codes the upper-pair off-diagonal minor at Cayley–Menger position $(1,3)$, corresponding to opposite pair $(0,2)$: one of the three lower-triple pairs whose closed forms are $C_{pp}=C_{qq}=8z-4$, $C_{pq}=3-4z$. The present statement identifies that hand-written minor with the abstract Matrix.submatrix deletion of row $1$ and column $3$.
proof idea
Pure entrywise comparison. Extensionality on the two Fin 5 indices, then fin_cases on each index, reduces to twenty-five ground equalities between the submatrix lookup (via Fin.succAbove on the deleted row/column) and the match-table in the explicit minor. Each case is rfl. No algebraic lemmas are required beyond the definitions of the hinge matrix and the minor.
why it matters
Feeds the cofactor theorem that evaluates the $(1,3)$ Cayley–Menger cofactor of the hinge edge data to the closed form $3-4z$. That identity is one of the kernel checks matching the per-hinge table in the executed Wick-arc trace: upper-pair hinges inside the lower triple carry $C_{pq}=3-4z$ and $\mathrm{areaSq}=z/4-1/16$. Without the submatrix identification, the cofactor rewrite chain cannot switch from the abstract minor extractor to the determinant of the tabulated $5\times 5$ matrix. It is scaffolding glue inside the all-hinge split-form branch certificate, not a physics claim on its own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.