submatrix32_23
plain-language theorem explainer
Deleting row 2 and column 3 from the complex bordered 6×6 (3,2) hinge matrix recovers the hand-written 5×5 upper-pair off-diagonal minor at CM indices (2,3). Cofactor identities for upper-pair hinges of the threeTwo causal 4-simplex cite this equality. The proof is extensionality plus exhaustive Fin-5 case splits with definitional equality.
Claim. For every $z\in\mathbb{C}$, the submatrix of the bordered $6\times 6$ threeTwo hinge matrix at $z$ obtained by deleting row index $2$ and column index $3$ equals the explicitly tabulated $5\times 5$ upper-pair off-diagonal minor associated to the Cayley–Menger entry $(2,3)$.
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the (3,2) causal 4-simplex in the complex-first Wick setting. The lower slice is vertices ${0,1,2}$, the upper slice ${3,4}$; timelike edges are the six cross edges. Upper-pair hinges arise from opposite pairs inside the lower triple and carry closed cofactors $C_{pp}=C_{qq}=8z-4$, $C_{pq}=3-4z$.
The bordered hinge matrix is the explicit $6\times 6$ complex matrix of the threeTwo tuple (spacelike edge length 1, timelike length $z$), mirroring the real pentagon matrix at $(p,q)=(1,z)$. Rows/cols $1..3$ index the lower slice and $4..5$ the upper slice, with a bordering row/column of ones.
The target minor is the hand-coded $5\times 5$ matrix obtained by removing the CM indices corresponding to opposite pair $(1,2)$. Matching that table to the generic Matrix.submatrix deletion is the bookkeeping step needed before evaluating the determinant cofactor.
proof idea
Pointwise extensionality on the remaining $5\times 5$ index set: ext i j, then fin_cases on both $i$ and $j$ (twenty-five cells). Each cell reduces by rfl to the corresponding clause of the explicit minor definition, so the two matrices agree definitionally entrywise. No algebraic lemmas are required.
why it matters
Feeds the cofactor theorem that evaluates the signed $(2,3)$ Cayley–Menger cofactor of the threeTwo hinge edge data to the closed form $3-4z$. That identity is exactly the off-diagonal cofactor $C_{pq}$ listed for the three upper-pair hinges in the module charter, and it is kernel-checked against the executed Wick-arc trace table.
Together with the matching diagonal cofactors and area-squared formulae, these minors close the split-form branch certificates for the upper-pair class on the canonical upper-half-plane arc. The result is pure linear-algebra scaffolding inside the gravity/Seven-Gaps lane; it does not itself touch the T0–T8 forcing chain, but it is required infrastructure for the complex-first Wick continuation of the (3,2) simplex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.