threeTwo_areaSq_closed
plain-language theorem explainer
For every complex edge parameter z, the ten triangular hinges of the (3,2) causal 4-simplex have closed-form squared areas: the unique spacelike hinge is constantly 3/16, and each of the nine hinges with timelike edges is z/4 − 1/16. Gravity and QG workers cite this when assembling the full Wick hinge table or killing product-form branch transcriptions. The proof is a ten-conjunct refine that dispatches each hinge by one of three triangle-area lemmas.
Claim. For every $z \in \mathbb{C}$, the complex squared hinge areas of the $(3,2)$ causal edge set satisfy: the spacelike hinge on vertices $(0,1,2)$ has area squared $3/16$; each of the six mixed hinges (edge shape $(1,z,z)$) and each of the three upper-pair hinges (edge shape $(z,z,1)$) has area squared $z/4 - 1/16$.
background
Lane B2 of the QG Seven-Gaps campaign treats the all-hinge complex-first Wick continuation of the $(3,2)$ causal 4-simplex at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc. The five vertices split into a lower spacelike triple ${0,1,2}$ and an upper pair ${3,4}$; the six cross edges are the only timelike ones.
Hinges fall into three classes by opposite pair: the single spacelike hinge $(0,1,2)$ opposite $(3,4)$; six mixed hinges with two timelike triangle edges; and three upper-pair hinges $(0,3,4)$, $(1,3,4)$, $(2,3,4)$. Squared areas are read from $5\times 5$ Cayley–Menger minors via the complex hinge-area functional of WickActionComplexFirst.
The same two closed forms already appear for the $(4,1)$ type in WickFourOneAllHinges. Cut avoidance on the open arc interior is inherited from that module's interior-off-cut theorem; Lorentzian endpoint contact at $-5/16$ is an allowed gate contact, not a failure.
proof idea
Term-mode proof by refine into a ten-fold conjunction. The spacelike hinge $(0,1,2)$ is discharged by triangleAreaSqC_ones (all three triangle edges unit length, area squared constantly $3/16$). Each of the six mixed hinges is discharged by triangleAreaSqC_one_z_z z (edge shape $(1,z,z)$, closed form $z/4-1/16$). Each of the three upper-pair hinges is discharged by triangleAreaSqC_z_z_one z (edge shape $(z,z,1)$, same closed form). No further algebraic work: the three triangle lemmas already encode the Cayley–Menger evaluations on those edge patterns.
why it matters
This is the B2 areas-squared deliverable for the $(3,2)$ type: every hinge of the threeTwo simplex now has an exact closed form matching the executed Wick-arc trace table. Downstream, wick_hinge_areaSq_closed_forms_complete packages both causal types into the single B3 statement that all twenty hinge areas-squared are either $3/16$ (all-spacelike classes) or $z/4-1/16$ (any class with timelike edges).
The same closed forms feed the product-form kill certificate product_form_crossing_threeTwo_upper, which shows that at the interior arc parameter $t^*=2/3$ the diagonal-cofactor product of every upper-pair threeTwo hinge lands on the csqrt branch cut at $-48$, killing single-sqrt product transcription on that class.
Within the Seven-Gaps finishing charter this closes the hinge-data half of lane B2 and supplies the algebraic substrate for the split-form branch certificates and the two memorialized product-form FAIL events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.