triangleAreaSqC
plain-language theorem explainer
Complex Cayley–Menger area-squared of a triangle with squared edge lengths u, v, w in ℂ: −det(CM₄)/16. Gravity workers on the C11 Wick hinge-data lane cite it as the n=2 complex volume formula feeding every hinge area along the upper-half-plane arc. The body is a one-line definition wrapping the bordered 4×4 CM matrix determinant.
Claim. For complex squared edge lengths $u,v,w\in\mathbb{C}$, the complex triangle area-squared is $-\det(\mathrm{CM}_4(u,v,w))/16$, where $\mathrm{CM}_4$ is the bordered $4\times 4$ Cayley–Menger matrix of the triangle (the $n=2$ case of the simplex volume-squared formula, complexified).
background
Module C11 formalizes complex-first 4D Wick continuation of Regge hinge data (areas-squared and dihedral cosines) for causal 4-simplices. The arc on the timelike squared edge is $z(t)=\alpha a^2\exp(i\pi(1-t))$, $t\in[0,1]$, from Lorentzian to Euclidean endpoint; interior points sit in the open upper half-plane.
The bordered matrix triCMMatrixC u v w is the classical 4×4 Cayley–Menger matrix with squared edges $u=d(1,2)^2$, $v=d(1,3)^2$, $w=d(2,3)^2$, entries in ℂ. Real Cayley–Menger gives $16\cdot(\mathrm{area})^2=-\det(\mathrm{CM}_4)$ for a triangle; this definition complexifies that identity without taking a real square root.
Upstream hinge geometry (shared tetrahedron face ${0,1,2}$) and the 10-edge complex edge tuple supply the three squared lengths that later specializations feed in.
proof idea
Pure definition, not a proved theorem. Body is the single term $-\mathrm{Matrix.det}(\mathrm{triCMMatrixC},u,v,w)/16$. No tactics, no lemmas discharged here; correctness of special cases is proved downstream by unfolding this def and evaluating the 4×4 determinant symbolically.
why it matters
Primitive area-squared atom for the entire C11 hinge-data stack. Immediate consumer hingeAreaSqC pulls three complex squared distances from a 10-edge tuple and applies this formula to hinge triangle ${i,j,k}$.
Closed-form theorems rest on it: hingeAreaSqC_closed and triangleAreaSqC_one_z_z give $\mathrm{areaSq}=z/4-1/16$ for the timelike-class shape (edges $1,z,z$); triangleAreaSqC_ones recovers the regular unit value $3/16$. Those identities feed Lorentzian endpoint values and the four-one all-hinges continuation in WickFourOneAllHinges.
Scope stays hinge-data only: the FullTheoryLedger gap on genuine action-level 4D continuation (C12) remains open; this def does not touch that ledger flag. It is the complex $n=2$ Cayley–Menger building block the Wick arc needs before dihedral cosines and branch certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.