hingeAreaSqC_closed
plain-language theorem explainer
Closed form for the complex Cayley-Menger area-squared of the mixed hinge (0,1,4): one spacelike edge of squared length 1 and two edges of squared length z yield area-squared z/4 − 1/16 (regular value 3/16 at z = 1). Anyone tracking the Wick arc of Regge hinge data on the fourOne causal 4-simplex cites this. The proof expands the 3×3 Cayley-Menger minor and reduces by ring.
Claim. For every $z \in \mathbb{C}$, the squared area of the triangular hinge with vertices $(0,1,4)$ built from the complexified edge data (squared length of $(0,1)$ equal to $1$, squared lengths of $(0,4)$ and $(1,4)$ equal to $z$) equals $z/4 - 1/16$.
background
This module formalizes the complex-first 4D Wick continuation of Regge hinge data (Cayley-Menger 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))$ from the Lorentzian endpoint $z(0) = -\alpha a^2$ to the Euclidean endpoint $z(1) = +\alpha a^2$. Scope is hinge-data only; full action-level continuation remains open (C12).
Hinge area-squared is the complex Cayley-Menger determinant of a triangular face, built from the three complex squared edge lengths via a $3\times 3$ bordered minor (triCMMatrixC). The edge assignment hingeEdgesC z places a unit spacelike edge on $(0,1)$ and the free complex parameter $z$ on the two remaining edges of hinge $(0,1,4)$. At $z = 1$ one recovers the regular Euclidean hinge value $3/16$.
proof idea
Unfold the area-squared definition down to the triangle Cayley-Menger form. Three definitional facts fix the edge data: squared length $(0,1)$ is $1$, and both $(0,4)$ and $(1,4)$ equal $z$. After rewriting those into the matrix, expand the $3\times 3$ determinant along the first row (Matrix.det_succ_row_zero with the usual Fin sum/succAbove simp set; same style as the sibling minor identity det_minorPPC). The resulting polynomial identity collapses by ring to $z/4 - 1/16$.
why it matters
Supplies the algebraic closed form that the interior branch-regularity theorem needs: hingeAreaSq_interior_off_cut rewrites through this identity and reads $\mathrm{Im}(z/4 - 1/16) = \mathrm{Im}(z)/4 > 0$ on the open arc, placing the area-squared in the slit plane (with allowed cut contact only at the Lorentzian endpoint). The sibling fourOne spacelike-hinge package also consumes the same edge-data setup when it records the constant $3/16$ values on purely spacelike hinges.
In the QG Seven-Gaps C11 lane this is the concrete hinge-area certificate on the Wick arc. It does not close the ledger gap wick_action_continuation_4d; that remains the separate C12 question about an interior-hinge simplicial complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.