minorPQC
plain-language theorem explainer
Defines the explicit 5×5 complex matrix obtained by deleting row 3 and column 4 from the hinge matrix along the Wick arc parameter z. Gravity and Regge-calculus workers cite it when extracting the (p,q) cofactor of the complex Cayley–Menger hinge data. The body is a pure case table on Fin 5 indices; no proof is required.
Claim. For each complex parameter $z$, let $M(z)$ be the $5\times 5$ matrix obtained by deleting row $3$ and column $4$ from the complex hinge matrix. Explicitly, $M(z)_{ij}$ equals $0$ on the diagonal entries $(0,0)$, $(1,1)$, $(2,2)$, $(4,4)$; equals $z$ on the pairs connecting index $4$ with $\{1,2,3\}$; equals $1$ on the remaining off-diagonal first-row/column entries and elsewhere.
background
Module C11 formalizes the complex-first 4D Wick continuation of Regge hinge data for causal 4-simplices: complex Cayley–Menger areas-squared and cofactor dihedral cosines along the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$. Endpoints recover the Lorentzian and Euclidean squared-edge conventions of the causal-simplex library.
The hinge matrix is the $6\times 6$ complex matrix whose cofactors encode dihedral cosines. Deleting one row and one column produces a $5\times 5$ minor used in the cofactor formula. This definition writes that minor (row 3, column 4 deleted) as an explicit case table in $z\in\mathbb{C}$.
Scope is hinge-data continuation only. Full action-level continuation of an interior-hinge complex remains the open C12 ledger gap and is not claimed here.
proof idea
Definition by cases, not a theorem. The matrix is specified entrywise via a match on (i.val, j.val) for i,j : Fin 5: zeros on four diagonal slots, the arc parameter z on the six off-diagonal slots linking index 4 to {1,2,3}, ones on the first row/column (except the (0,0) zero) and on all remaining entries. Downstream proofs unfold this table and compute with Matrix.det_succ_row_zero or ext plus fin_cases.
why it matters
Feeds two immediate parents in the same module. submatrix_pq proves the definition equals the actual submatrix of hingeMatrixC z under Fin.succAbove 3 and Fin.succAbove 4, locking the case table to the geometric minor. det_minorPQC then evaluates the determinant symbolically as $2z-1$; with cofactor sign $(-1)^7=-1$ this yields the cofactor $C_{pq}=1-2z$ used in the complex dihedral cosine along the Wick arc.
That cofactor is part of the hinge-data continuation path selected for panel C11 (QG Seven-Gaps). It does not close the ledger gap wick_action_continuation_4d; the module disclosure keeps action-level continuation open for C12. Within C11 it is the concrete algebraic object whose determinant supplies the branch-ready cosine numerator/denominator pieces on the open arc interior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.