submatrix32_12
plain-language theorem explainer
Removing row index 1 and column index 2 from the complex 6×6 hinge matrix of the (3,2) causal 4-simplex yields the explicit 5×5 upper-pair off-diagonal minor at CM entry (1,2). Anyone computing cofactors of that hinge matrix cites this identification. The proof is pure matrix extensionality: case-split on the five residual indices and reduce by definitional equality.
Claim. For every complex $z$, the $5\times 5$ submatrix of the bordered hinge matrix of the $(3,2)$ simplex obtained by deleting row $1$ and column $2$ equals the explicitly tabulated upper-pair off-diagonal minor associated to Cayley–Menger indices $(1,2)$ (opposite vertex pair $(0,1)$).
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex on the complex arc, at the physical point $a=1$, $\alpha=1$. The lower slice is vertices ${0,1,2}$ and the upper slice ${3,4}$; the six cross edges are the timelike ones.
The bordered $6\times 6$ hinge matrix encodes the threeTwo edge data with spacelike length $1$ and timelike length $z$ (mirror of the real pentagon matrix at $p=1$, $q=z$). Rows/cols $1..3$ are the lower vertices and $4..5$ the upper ones. Cayley–Menger cofactors are signed determinants of $5\times 5$ minors obtained by deleting one row and one column of this matrix.
The named minor here is the upper-pair off-diagonal minor at CM position $(1,2)$, corresponding to opposite pair $(0,1)$. Upper-pair hinges (pairs inside the lower triple) have closed forms $C_{pp}=C_{qq}=8z-4$, $C_{pq}=3-4z$, and $\mathrm{areaSq}=z/4-1/16$.
proof idea
Pointwise matrix equality. Apply ext on the residual $5\times 5$ indices, then fin_cases on both row and column indices in Fin 5. Each of the twenty-five cells reduces by rfl to the matching clause of the explicit minor definition (border zeros, ones, and the $z$ entries on the continued timelike edges). No algebraic rewriting is required; the two matrices are definitionally identical entrywise after the succAbove deletions.
why it matters
Feeds the cofactor theorem that evaluates the Cayley–Menger cofactor at indices $(1,2)$ to the closed form $3-4z$. That identity is one of the kernel checks matching the per-hinge table for upper-pair hinges of the $(3,2)$ simplex. Together with the sibling submatrix lemmas, it closes the explicit-minor route to all ten hinge cofactors on the complex arc, supporting the split-form branch certificate and boundary continuation required by the Wick-action finishing charter. In the broader Recognition gravity stack this is bookkeeping for the complex-first Wick continuation, not a new physical law; it makes the $C_{pq}=3-4z$ formula machine-checked rather than hand-tabulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.