submatrix32_33
plain-language theorem explainer
Deleting row and column index 3 from the 6×6 complex hinge Cayley–Menger matrix of a (3,2) simplex yields the named lower 5×5 minor, for every complex parameter z. Gravity and Regge analysts cite this when extracting the (3,3) cofactor along mixed hinges. The proof is pure entrywise exhaustion on Fin 5 after matrix extensionality.
Claim. For every $z\in\mathbb{C}$, the $5\times 5$ submatrix of the complex hinge Cayley–Menger matrix at $z$ obtained by deleting row and column index $3$ equals the lower diagonal minor at $z$.
background
Module 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 $a=1$, $\alpha=1$, on the canonical upper-half-plane arc. Hinges are classified by opposite vertex pairs: spacelike, mixed (one lower, one upper), and upper-pair. Mixed hinges carry asymmetric cofactors, with the lower-member diagonal cofactor closed form $C_{pp}=8z-4$.
The complex hinge matrix is the $6\times 6$ Cayley–Menger matrix built from the ten complexified edge lengths of the simplex (six timelike cross edges). Removing one row and the matching column produces a $5\times 5$ principal minor whose determinant, signed, is the corresponding cofactor. The lower minor is the explicit matrix object used for the index-3 deletion.
Upstream scaffolding supplies the hinge edge list, the matrix constructor, and the certified analytic value layer used elsewhere in the campaign; this lemma itself is purely combinatorial matrix identity.
proof idea
Term-style tactic proof. Apply matrix extensionality to reduce equality of $5\times 5$ matrices to equality of all entries. Both index types are Fin 5; run fin_cases on the row index and nested fin_cases on the column index, then close each of the 25 goals by rfl (definitional agreement between Matrix.submatrix of the hinge matrix under Fin.succAbove 3 and the named lower minor).
why it matters
Direct prerequisite of cof32_d3, which unfolds the complex cofactor at position $(3,3)$ and rewrites via this identity plus the determinant of the lower minor to obtain the closed form $8z-4$. That formula is exactly the mixed-hinge lower-member cofactor listed in the module charter and matched to the executed Wick-arc trace table.
In the Recognition gravity stack this closes one kernel check on the (3,2) simplex hinge spectrum: the same $8z-4$ appears for all three lower-pair upper hinges and for the lower leg of each mixed hinge. It sits inside the broader Seven-Gaps finishing charter (lane B), not the T0–T8 forcing chain, but it is required before branch certificates and product-form kill certificates can be stated on the physical arc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.