minorPPC
plain-language theorem explainer
Explicit 5×5 principal minor of the complex bordered hinge Cayley–Menger matrix for the four-one edge tuple, obtained by deleting one base-vertex row/column (equivalently the opposite base vertex by symmetry). Gravity/Wick authors cite it as the landed diagonal block whose determinant is the closed form 6z−2. The body is a pure entrywise case match on Fin 5, not a derived construction.
Claim. For $z\in\mathbb{C}$, define the $5\times 5$ complex matrix $M_{PP}(z)$ by the bordered Cayley–Menger pattern: entry $(0,0)$ is $0$, the rest of the first row and column are $1$, the four remaining diagonal entries are $0$, the three pairs coupling indices $\{1,2,3\}$ to index $4$ equal $z$ symmetrically, and all other off-diagonal entries equal $1$. This is the principal minor of the $6\times 6$ hinge matrix after deleting row/column $3$ (and, by base-vertex symmetry, after deleting row/column $4$).
background
Module C11 formalizes a complex-first 4D Wick continuation of hinge data (complex Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The path is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean squared-edge endpoints. Scope is deliberately hinge-level only; full action-level continuation remains open (C12).
The parent object is the bordered $6\times 6$ hinge matrix for the four-one tuple (one spacelike edge fixed at $1$, one timelike edge the complex parameter $z$), mirroring the real pentagon matrix of the causal simplex library. Rows/cols $1..5$ index vertices $0..4$, with apex vertex $4$ in the last slot.
Diagonal $5\times 5$ minors of that matrix are the natural blocks for cofactors and split-sqrt dihedral denominators. This definition freezes the concrete entry pattern of those minors so later determinant and submatrix lemmas can cite a single named matrix rather than re-expanding Matrix.submatrix each time.
proof idea
Definition, not a theorem. The body is an exhaustive match on (i.val, j.val) for i,j : Fin 5, writing the bordered Cayley–Menger pattern directly: border zero at $(0,0)$ with ones on the rest of the border; zeros on the remaining diagonal; $z$ on the three symmetric pairs linking ${1,2,3}$ to $4$; ones elsewhere. No lemmas are applied. Downstream submatrix_pp / submatrix_qq (and the four-one variants deleting other base vertices) prove by ext and fin_cases that this pattern equals the corresponding Matrix.submatrix of hingeMatrixC z.
why it matters
Names the diagonal minor that the symbolic determinant theorem evaluates as $\det M_{PP}(z)=6z-2$ (gate closed form $C_{pp}=C_{qq}=6z-2$; at $z=1$ this recovers the regular unit-tetrahedron CM determinant $4$). That identity feeds cofactor signs and the split-sqrt dihedral cosine denominators along the Wick arc.
Used by the local submatrix landing lemmas (submatrix_pp, submatrix_qq) and by the four-one all-hinges layer (submatrix41_11, submatrix41_22, branch-regularity symmetry), plus three-two hinge submatrices. Those landings let opposite-pair branch regularity and dihedral continuation reuse one matrix rather than four ad-hoc blocks.
Sits inside the C11 hinge-data continuation mandate. It does not close the ledger gap wick_action_continuation_4d; that remains the separate C12 question about a genuine interior-hinge complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.