submatrix32_44
plain-language theorem explainer
Deleting row and column 4 from the bordered 6×6 complex hinge matrix of the (3,2) causal 4-simplex yields exactly the landed 5×5 minorPPC tetrahedron matrix. Anyone computing Cayley–Menger cofactors for the upper-slice hinges cites this identification. The proof is pure definitional equality: extensionality plus exhaustive Fin cases.
Claim. For every $z \in \mathbb{C}$, the $5 \times 5$ principal submatrix of the bordered complex hinge matrix of the $(3,2)$ simplex obtained by deleting index $4$ equals the standard landed minor $\mathrm{minorPPC}(z)$ (the $(1,1,1;z,z,z)$ tetrahedron pattern).
background
Lane B2 of the QG Seven-Gaps campaign continues the all-hinge complex-first Wick analysis of the threeTwo causal 4-simplex at the physical point $a=1$, $\alpha=1$. The object hingeMatrix32C z is the explicit bordered $6\times 6$ Cayley–Menger matrix: index 0 is the CM border of ones, indices 1–3 are the lower-slice vertices ${0,1,2}$ with spacelike edge length 1, and indices 4–5 are the upper-slice vertices ${3,4}$ with cross edges of complex length $z$.
The target minor minorPPC z is the canonical $5\times 5$ matrix already used in the WickActionComplexFirst arc: it encodes the tetrahedron with three unit edges and three edges of length $z$. Deleting CM row/col 4 (vertex 3) leaves precisely those four geometric vertices plus the border, so the submatrix must match minorPPC entrywise.
Cofactors of the full hinge matrix are built from such $5\times 5$ minors; closed forms such as $C_{pp}=6z-2$ for upper-slice members are read off their determinants.
proof idea
One-line structural proof. Apply matrix extensionality to reduce to entrywise equality on $\mathrm{Fin},5\times\mathrm{Fin},5$. Exhaust both indices by fin_cases; each of the 25 residual goals is definitional (rfl) against the match-table definitions of hingeMatrix32C and minorPPC. No algebraic lemmas are required.
why it matters
Feeds directly into cof32_d4, which evaluates the $(4,4)$ Cayley–Menger cofactor of the (3,2) hinge edge set as $6z-2$. That closed form is one of the kernel-checked entries in the per-hinge table for upper-pair and mixed hinges (module header: $C_{qq}=6z-2$ for upper members). Together with the sibling submatrix identities, it discharges the explicit-minor half of the split-form branch certificates on the canonical upper-half-plane arc, completing Lane B2 of the Seven-Gaps finishing charter for all ten triangular hinges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.