submatrix32_25
plain-language theorem explainer
Removing row index 2 and column index 5 from the bordered 6×6 complex hinge matrix of the (3,2) causal 4-simplex yields exactly the hand-written 5×5 minor for the mixed opposite pair (1,4). Anyone computing Cayley–Menger cofactors along the Wick arc cites this identification. The proof is a pure entrywise exhaustion: extensionality plus fin_cases on both Fin 5 indices, each cell reducing by rfl.
Claim. For every complex parameter $z$, the $5\times 5$ submatrix of the bordered hinge matrix of the $(3,2)$ simplex obtained by deleting row $2$ and column $5$ equals the explicitly tabulated mixed off-diagonal minor associated with opposite pair $(1,4)$.
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex through the complex-first Wick arc. The ambient object is a bordered $6\times 6$ Cayley–Menger matrix whose first row/column is the usual $0,1$ border and whose remaining $5\times 5$ block encodes squared edge lengths: spacelike edges fixed at $1$, the six cross (timelike) edges equal to the complex parameter $z$.
Rows/cols $1..3$ correspond to the lower slice ${0,1,2}$ and rows/cols $4..5$ to the upper slice ${3,4}$. The mixed opposite pair $(1,4)$ produces an asymmetric hinge (two timelike triangle edges). Its cofactor is extracted from the $(2,5)$ entry of the bordered matrix (0-based indexing after the border), so one needs the concrete $5\times 5$ minor obtained by deleting that row and column.
hingeMatrix32C supplies the full bordered matrix by pattern-match on indices; minor32_25C is the hand-expanded $5\times 5$ array for the same deletion, with the characteristic $z$ placements of a mixed hinge.
proof idea
Term-mode proof by matrix extensionality. After ext i j both indices range over Fin 5. Nested fin_cases expands the $25$ cells; each cell is definitionally equal to the corresponding entry of the hand-written minor, discharged by rfl. No algebraic lemmas are required beyond the definitions of the two matrices and Matrix.submatrix / Fin.succAbove.
why it matters
The equality is the bridge from the abstract Cayley–Menger cofactor API to the closed-form minor used in the mixed-hinge certificates. Downstream, cof32_25 rewrites the cofactor of the hinge-edge matrix at position $(2,5)$ through this submatrix identity, evaluates the determinant of the explicit minor, inserts the odd-parity sign, and obtains the constant $-1$ predicted by the per-hinge table for mixed pairs.
That constant $C_{pq}=-1$ (together with the diagonal cofactors $8z-4$ and $6z-2$) feeds the split-form cosine and area-squared formulae for all six mixed hinges of the $(3,2)$ simplex on the physical Wick arc. The result is therefore one of the kernel-check steps that close Lane B2 of the Seven-Gaps finishing charter: every triangular hinge of the threeTwo 4-simplex now has an explicit, machine-checked complex continuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.