submatrix32_55
plain-language theorem explainer
Deleting row and column 5 from the complex (3,2)-hinge Cayley-Menger matrix recovers the already-landed principal minor minorPPC(z). Gravity/Wick-arc authors cite it when extracting the (5,5) cofactor along the physical arc. The proof is pure definitional equality: extensionality plus exhaustive Fin-cases.
Claim. For every $z\in\mathbb{C}$, the principal $5\times 5$ submatrix of the complex hinge Cayley-Menger matrix of the $(3,2)$ causal $4$-simplex obtained by deleting index $5$ equals the principal minor $\mathrm{minorPPC}(z)$.
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 $a=1$, $\alpha=1$, on the canonical upper-half-plane arc. The six vertices carry a Cayley-Menger matrix built from the ten hinge edge lengths (complexified); cofactors of that matrix supply the closed forms $C_{pp}$, $C_{qq}$, $C_{pq}$ that enter the split cosine of each triangular hinge.
Index 5 is the last CM coordinate (vertex 4 in 0-based labeling). The principal minor obtained by deleting that row and column is already identified, in the upstream Wick-action module, as the explicit $5\times 5$ matrix minorPPC. Sibling lemmas do the same for the other diagonal deletions; the three lower-vertex deletions collapse to one common explicit matrix (the $2+2$ tetrahedron with two spacelike and four timelike edges).
The module's hinge classification records that opposite pair $(3,4)$ is the unique spacelike hinge, with closed cofactor form $C_{pp}=C_{qq}=6z-2$. Establishing the submatrix identity is the bridge from the abstract CM cofactor to that rational expression.
proof idea
Term-level matrix extensionality: after ext i j both indices range over Fin 5. Nested fin_cases exhausts the twenty-five entries; each residual goal is definitional (rfl) against the corresponding entry of minorPPC z. No algebraic rewriting or determinant identities are required; the claim is pure index arithmetic via Fin.succAbove 5.
why it matters
Direct parent is cof32_d5, which rewrites the CM cofactor at $(5,5)$ through this submatrix identity, applies det_minorPPC, and obtains the closed form $6z-2$ by a short ring computation (even parity of the sign). That cofactor is exactly the diagonal entry $C_{pp}=C_{qq}$ for the spacelike hinge $(0,1,2)$ in the module's hinge table, and is the denominator of the cut-free rational split cosine $(5-6z)/(6z-2)$.
In the broader Seven-Gaps finishing charter this closes one kernel check of the per-hinge table against the executed Wick-arc trace. It sits inside the complex-first continuation that certifies branch placement on the open interior of the arc (where $\mathrm{Im},\cos<0$), with the Lorentzian endpoint contact at $t=0$ disclosed as an allowed cut touch rather than a failure. No T0-T8 forcing step is touched; the result is pure Regge/CM algebra supporting the gravity-side Wick certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.