det_minorPPC
plain-language theorem explainer
For complex edge parameter z, the determinant of the 5×5 diagonal Cayley-Menger minor (row/col 3 deleted from the hinge matrix) equals 6z−2. Gravity and Regge analysts cite it for closed-form CM cofactors C_pp = C_qq along the Wick arc. The proof unfolds the minor, expands the determinant by the first row with Fin-sum simp lemmas, and finishes by ring.
Claim. For every $z \in \mathbb{C}$, if $M(z)$ is the $5\times 5$ minor of the complex hinge Cayley-Menger matrix obtained by deleting row 3 and column 3, then $\det M(z) = 6z - 2$. At $z = 1$ this recovers the regular unit-tetrahedron CM minor value $4$.
background
Module C11 formalizes a complex-first 4D Wick continuation of Regge 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 $z(0)= -\alpha a^2$ to Euclidean $z(1)= +\alpha a^2$. Scope is hinge-level only; full action-level continuation remains open (C12).
The object here is the diagonal $5\times 5$ minor of the complex hinge CM matrix: delete row/col 3 (equivalently 4 by vertex-2/3 symmetry). Entries are the standard bordered Cayley-Menger pattern with squared edge lengths specialized to the hinge edge tuple in $z$. Upstream, the real 6×6 identity $\det(\mathrm{pentMatrix}_{41}(p,q)) = p^3(3p-8q)$ in CausalSimplex4D sets the same bare-simp expansion style used for these symbolic minors.
proof idea
One short tactic proof in the same mold as det_pentMatrix41. Unfold the minor matrix definition, then simp with Matrix.det_succ_row_zero, Fin.sum_univ_succ, and Fin.succAbove so the 5×5 determinant expands along the bordered first row into an explicit polynomial in $z$. Finish with ring to reach $6z-2$. Bare simp (not simp only) is intentional: numeric simprocs keep the expansion tractable, matching the proved 6×6 pattern.
why it matters
Supplies the closed form that turns CM cofactors into elementary polynomials on the Wick arc. Immediate parents: cofactor theorems for diagonal entries $C_{pp}=C_{qq}=6z-2$ (CM indices 3 and 4), and the parallel all-hinges cofactors in the (4,1) class that rewrite the same minor. Those cofactors feed dihedral-cosine and area-squared closed forms (e.g. hinge area-squared $z/4-1/16$) used in the boundary-continuation theorem with branch certificate on the open arc interior.
In the Seven-Gaps campaign this is panel-locked C11 infrastructure: symbolic certificates backing the RESULTS.txt gate, not a claim that the full simplicial action continues. The ledger gap on action-level 4D Wick continuation stays open. Landmark contact is local Regge/CM geometry on causal 4-simplices, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.