hingeAreaSqC
plain-language theorem explainer
Defines the complex area-squared of a triangular hinge on three vertices of a causal 4-simplex from a complex 10-edge squared-length tuple. Gravity and QG workers cite it as the Cayley–Menger area input to Wick-continued Regge hinge data. The body is a one-line composition of the complex triangle area-squared formula on the three pairwise complex squared distances.
Claim. Given a complex 10-tuple $x$ of squared edge lengths of a 4-simplex and three vertex indices $i,j,k\in\{0,\ldots,4\}$, the complex hinge area-squared is the complex triangle area-squared built from the three pairwise complex squared distances $d^2(i,j)$, $d^2(i,k)$, $d^2(j,k)$ extracted from $x$.
background
Module C11 formalizes a complex-first 4D Lorentzian Wick continuation of Regge hinge data (areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The path on a 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 endpoint $z(0)=-\alpha a^2$ and Euclidean endpoint $z(1)=+\alpha a^2$. Scope is hinge-data only; full action-level continuation remains open (C12 / ledger gap).
SqEdges10C is the type of complex squared edge lengths indexed by Fin 10 in the lexicographic edge order of the causal 4-simplex. Pairwise squared distances between vertices are read by the complexification of the real pentagon distance table. The hinge of interest is the triangle on three of the five simplex vertices; its area-squared is the standard (complexified) Heron/Cayley–Menger expression in those three edge squares.
Downstream closed forms specialize this definition on model edge tuples such as hingeEdgesC z, where one edge is spacelike of square $1$ and two edges carry the continued value $z$.
proof idea
Pure definition, not a theorem. Unfolding substitutes the three complex pairwise squared distances pentDistSqC x i j, pentDistSqC x i k, pentDistSqC x j k into triangleAreaSqC. No tactics or lemmas; noncomputable only because the ambient complex area formula is. Callers prove identities by unfolding this def together with the distance table on a concrete edge tuple.
why it matters
This is the area-squared primitive for the entire C11 hinge-data Wick lane. Closed-form theorems reduce it on model edges: hingeAreaSqC_closed gives $\mathrm{areaSq}=z/4-1/16$ on hinge $(0,1,4)$; fourOne_areaSq_spacelike / fourOne_areaSq_timelike and threeTwo_areaSq_closed cover the remaining fourOne and threeTwo classes; wick_hinge_areaSq_closed_forms_complete packages all twenty hinges as either the constant $3/16$ (all-spacelike) or $z/4-1/16$ (timelike-class).
Cut-avoidance on the open arc interior (hingeAreaSq_interior_off_cut and siblings) needs this value to land in the slit plane so complex square roots in dihedral cosines stay on the selected branch. That is the branch certificate for the path-selected continuation of hinge data. It does not close the FullTheoryLedger gap wick_action_continuation_4d: the module explicitly leaves action-level continuation (genuine interior-hinge complexes) to C12.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.