cmMinorC
plain-language theorem explainer
Defines the complex Cayley-Menger minor: delete row r and column c from the bordered 6×6 CM matrix built from complex squared edge lengths of a 4-simplex, then take the 5×5 determinant. Anyone computing complex cofactors or dihedral cosines along the Wick arc cites this. Body is a one-line Mathlib submatrix determinant.
Claim. Given complex squared edge lengths $x$ of a 4-simplex (indexed by $\mathrm{Fin}\,10$) and indices $r,c\in\{0,\ldots,5\}$, the minor $M_{r,c}(x)$ is the determinant of the $5\times 5$ matrix obtained by deleting row $r$ and column $c$ from the bordered $6\times 6$ complex Cayley-Menger matrix of $x$.
background
Module C11 formalizes complex-first 4D Wick continuation of hinge data (areas-squared and dihedral cosines) for causal 4-simplices. The continuation path is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean endpoints. Scope is hinge-data only; full action-level continuation remains open (C12).
SqEdges10C is the type of complex squared edge lengths on the ten edges of a 4-simplex. The bordered Cayley-Menger matrix cmMatrixC x is the standard $6\times 6$ complex matrix (border of ones, squared distances in the interior block) complexifying the real $n=4$ construction. Minors of that matrix enter cofactors, which yield dihedral cosines via classical CM identities.
Upstream, cmMatrixC fills entries from the edge tuple via a vertex-index map; the continuum bridge supplies the broader simplicial-action identification that motivates tracking areas and dihedrals under continuation.
proof idea
Pure definition, not a proof. Applies Mathlib Matrix.det to Matrix.submatrix (cmMatrixC x) (Fin.succAbove r) (Fin.succAbove c), which drops row $r$ and column $c$ by the successor-above embedding $\mathrm{Fin},5\hookrightarrow\mathrm{Fin},6$. Marked noncomputable because determinant over $\mathbb{C}$ is.
why it matters
Primitive for the entire complex cofactor stack in the C11 Wick lane. Downstream cmCofactorC multiplies this minor by the sign $(-1)^{r+c}$. Closed-form hinge theorems cofactor_pp, cofactor_pq, cofactor_qq unfold through it to obtain $C_{pp}=C_{qq}=6z-2$ and $C_{pq}=1-2z$ on the one-parameter hinge edge family. Symmetry cmMinorC_symm (WickFourOneAllHinges) and further 4-1 hinge cofactors also depend on it. Those cofactors feed path-selected branch certificates for dihedral cosines on the open arc interior. Does not close the ledger gap wick_action_continuation_4d; that remains C12.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.