submatrix_qq
plain-language theorem explainer
Deleting row and column index 4 from the complex bordered hinge matrix yields exactly the named 5×5 principal minor used for the qq cofactor. Anyone computing Cayley–Menger cofactors along the Wick arc of a causal 4-simplex cites this identification. The proof is entrywise exhaustion on Fin 5 × Fin 5 by definitional equality.
Claim. For every $z \in \mathbb{C}$, the $5\times 5$ submatrix of the bordered complex hinge matrix $H(z)$ obtained by deleting row and column index $4$ equals the principal minor $\mathrm{minor}_{PP}(z)$ (the explicit $5\times 5$ matrix used for the $(4,4)$ cofactor).
background
Module C11 formalizes the complex-first 4D Wick continuation of hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The continuation path is the upper-half-plane arc $z(t)=\alpha a^2 e^{i\pi(1-t)}$ from Lorentzian to Euclidean endpoints. Scope is hinge-data only; full action-level continuation remains open (C12).
The bordered $6\times 6$ matrix $H(z)=\mathrm{hingeMatrixC}(z)$ encodes the fourOne edge tuple with spacelike edges 1 and one complex timelike edge $z$, mirroring the real pentMatrix41 at $p=1$, $q=z$. Rows/cols 1..5 are vertices 0..4; the border is the usual Cayley–Menger ones-row.
The object $\mathrm{minor}_{PP}(z)$ is the explicit $5\times 5$ matrix obtained by deleting a principal vertex block. By vertex-2/vertex-3 symmetry it is also the $(4,4)$ minor of $H(z)$. This lemma pins that matrix identity so later cofactor algebra can rewrite through a single named minor.
proof idea
Pure definitional identification. Apply matrix extensionality to reduce to equality of all entries $(i,j)\in\mathrm{Fin},5\times\mathrm{Fin},5$. Exhaust both indices by fin_cases; each of the 25 cases is rfl against the match-clauses defining $H(z)$ and $\mathrm{minor}_{PP}(z)$ under the embedding Fin.succAbove 4 (skip index 4). No algebraic lemmas are needed.
why it matters
Feeds cofactor_qq, which unfolds the complex Cayley–Menger cofactor at indices $(4,4)$ and rewrites via this submatrix identity plus det_minorPPC to obtain the closed form $C_{qq}=6z-2$. That closed cofactor is a building block for complex dihedral cosines along the Wick arc of the hinge data.
In the QG Seven-Gaps C11 lane this is bookkeeping that makes the path-selected boundary continuation algebraically tractable. It does not close the FullTheoryLedger gap wick_action_continuation_4d (action-level continuation remains open). Landmark context: hinge-level Wick data for causal 4-simplices, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.