cmCofactorC
plain-language theorem explainer
Defines the complex Cayley–Menger cofactor C_{r,c} of the bordered 6×6 matrix built from complex squared edge lengths of a 4-simplex. Anyone working the C11 Wick hinge-data lane cites it as the atomic entry for split dihedral cosines and branch-regularity predicates. The body is the standard signed-minor product: sign(−1)^{r+c} times the 5×5 minor determinant.
Claim. For complex squared edge lengths $x$ of a 4-simplex and indices $r,c \in \{0,\ldots,5\}$, the complex Cayley–Menger cofactor is $C_{r,c}(x) := (-1)^{r+c}\,M_{r,c}(x)$, where $M_{r,c}(x)$ is the determinant of the $5\times 5$ submatrix obtained by deleting row $r$ and column $c$ from the bordered complex Cayley–Menger matrix of $x$.
background
Module C11 formalizes a complex-first 4D Lorentzian Wick continuation of hinge data (areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The continuation path on the timelike squared edge is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$, $t\in[0,1]$, with Lorentzian and Euclidean endpoints. Scope is hinge-data only; full action-level continuation remains open (C12).
Squared edges live in SqEdges10C ($\mathrm{Fin},10\to\mathbb{C}$), the complexification of the 4-simplex edge table. The bordered $6\times 6$ complex Cayley–Menger matrix is assembled from those edges. The minor deletes row $r$ and column $c$ and takes $\det$; the cofactor sign is $(-1)^{r+c}$ as a complex number. This mirrors the real 3D cofactor construction used for tetrahedron dihedral cosines, lifted to complex 4-simplex hinge geometry.
proof idea
Pure definitional wrapper: multiply the complex cofactor sign by the complex minor determinant. No tactics, no lemmas beyond the two sibling defs. Downstream closed forms (e.g. $C_{pp}=6z-2$) unfold this product, rewrite the hinge matrix and the relevant submatrix determinant, discharge the parity of $r+c$, and finish by ring.
why it matters
Atomic building block for the entire split-form hinge cosine stack in C11. The split denominator is $\sqrt{C_{pp}}\sqrt{C_{qq}}$ (mandatory: the product-under-one-sqrt form crosses the branch cut mid-arc). The split cosine is $C_{pq}$ over that denominator. Branch regularity on a parameter set requires both diagonal cofactors to stay in the slit plane (continuity region of complex square root) and the cosine ratio off the arccos cuts.
Closed-form theorems pin the hinge family: $C_{pp}=C_{qq}=6z-2$ and $C_{pq}=1-2z$. Those feed endpoint cofactor identities, product-form crossing certificates, and the path-selected boundary-continuation theorem 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.