submatrix32_45
plain-language theorem explainer
Deleting row 4 and column 5 from the complex bordered 6×6 (3,2) hinge matrix recovers the hand-written 5×5 off-diagonal minor for the spacelike opposite pair (3,4). Cofactor identities for that hinge cite this equality. The proof is a finite index case-split with reflexivity on each entry.
Claim. For every $z\in\mathbb{C}$, the $5\times 5$ submatrix of the bordered threeTwo hinge matrix at $z$ obtained by deleting row index $4$ and column index $5$ equals the explicitly tabulated off-diagonal minor for the opposite pair $(3,4)$ (spacelike hinge).
background
Lane B2 of the QG Seven-Gaps campaign treats the all-hinge complex-first Wick continuation of the (3,2) causal 4-simplex at the physical point, on the canonical upper-half-plane arc. The threeTwo type has lower slice ${0,1,2}$ and upper slice ${3,4}$, with timelike edges exactly the six cross edges.
The bordered $6\times 6$ hinge matrix places lower-slice vertices in rows/cols 1..3 and upper-slice vertices in 4..5 (mirror of the real pentagon matrix at spacelike edge length 1 and timelike length $z$). Cayley-Menger cofactors are read from $5\times 5$ minors of this matrix.
The opposite pair $(3,4)$ labels the unique spacelike hinge $(0,1,2)$. Its off-diagonal minor is tabulated entrywise (border row/column of ones, diagonal zeros on the lower triple, and a single $z$ in the remaining upper block). Closed forms later give $C_{pq}=5-6z$ for this hinge.
proof idea
Pointwise matrix extensionality on the two $\mathrm{Fin},5$ indices, then exhaustive fin_cases on both indices. Each of the twenty-five residual goals is definitional equality (rfl) between the submatrix projection of the match-defined hinge matrix and the match-defined minor. No algebraic lemmas are required.
why it matters
Feeds the cofactor theorem that evaluates the $(4,5)$ Cayley-Menger cofactor of the complex hinge edge data to the closed form $5-6z$. That identity is the off-diagonal entry in the spacelike-hinge class of the module doc (opposite pair $(3,4)$: $C_{pp}=C_{qq}=6z-2$, $C_{pq}=5-6z$, $\mathrm{areaSq}=3/16$), which the kernel checks against the executed Wick-arc trace table.
Without the submatrix identification, the cofactor rewrite chain cannot swap the abstract minor constructor for the concrete $5\times 5$ matrix whose determinant is already computed. The result is pure scaffolding glue inside the split-form branch certificate for all ten triangular hinges; it does not itself touch the arccos-cut endpoint analysis at the Lorentzian point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.