hingeAreaFlat
plain-language theorem explainer
For each of the ten triangle hinges of the Freudenthal 4-simplex, returns the Euclidean area of that hinge evaluated on the flat seed edge lengths. Downstream Schläfli and second-variation arguments cite it as the positive measure factor in the flat summand table. The body is a thin composition: pull the three flat squared edges of the hinge, then apply the Heron-area map.
Claim. For each hinge index $h \in \{0,\ldots,9\}$ of the Freudenthal 4-simplex, let $(a,b,c)$ be the three squared edge lengths of the triangular boundary of $h$ at the flat seed. Define the flat hinge area by $\mathrm{Area}_\flat(h) := \sqrt{\mathrm{HeronSq}(a,b,c)}$.
background
This module lifts the 3D Gate-A2 Schläfli closed form (six edges, six hinges) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count equal ten. The local objects are squared-edge coordinates on the flat seed and the ten triangular faces that serve as Regge hinges.
hingeFlatEdgeSq packages, for hinge $h$, the three flat squared lengths on its boundary slots. The area map hingeArea a b c is the standard Heron square-root $\sqrt{\mathrm{heronSq}(a,b,c)}$ from the flat Hessian assembly (a separate constant $\sqrt{3/16}$ appears in the Wick interior-hinge path and is not used here).
The flat seed is the unique (up to scale) regular configuration at which the directional Schläfli identity is proved first; positive hinge areas are required so the identity is non-vacuous.
proof idea
Definitional one-liner. Bind $e := \mathrm{hingeFlatEdgeSq}(h)$, the triple of flat squared edge lengths on the three boundary slots of hinge $h$, then return $\mathrm{hingeArea}(e_1,e_2,e_3)$, i.e. the Heron square root of that triple. No tactics or lemmas beyond the two upstream defs.
why it matters
Supplies the strictly positive hinge measures that make the flat Freudenthal SchlaefliIdentityN witness non-vacuous (module tier tag: flat hinge areas; lesson against zero-measure shells). It is the measure field of flatHingeData and the denominator of flatAngleJacobian / flatSchlaefliData.dTheta_dL.
Parents include flatSchlaefliIdentity, flatSchlaefliSummand_seed_eq_area_angleKernel, freudenthal4SimplexFlatDirectionalSchlaefli, and the re-export flat_freudenthal_directional_schlaefli (Gate A2-style flat directional kill). The seed-row identity flatAngleJacobian_seed recovers angleKernel precisely by cancelling this area against the summand.
In the RS gravity stack this is the 4D flat input toward pathwise Schläfli and eventual $S_{RS}\to EH$ elevation; it does not close the open off-seed pathwise identity or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.