hingeAreaFlat_3
plain-language theorem explainer
At the flat Freudenthal 4-simplex seed, the triangular hinge with index 3 has area exactly $\sqrt{2}/2$. Gravity analysts cite this when assembling the flat Schläfli summand table and when proving that every flat hinge area is strictly positive. The proof unfolds the hinge-boundary edge squares, evaluates Heron's formula by norm_num, and rewrites $\sqrt{1/2}$ as $\sqrt{2}/2$.
Claim. For the flat seed edge-length configuration of the Freudenthal 4-simplex, the area of triangular hinge $3$ equals $\sqrt{2}/2$.
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, which has ten edges and ten triangle hinges. The flat seed is the squared-edge vector seedFlatSqEdges, aliased here as flatSqEdges.
Each hinge $h\in\mathrm{Fin},10$ has three boundary edge slots (v0v1, v0v2, v1v2) given by hingeBoundarySlots. The triple of squared lengths at the flat seed is hingeFlatEdgeSq h, and hingeAreaFlat h is the ordinary Heron area of that triple. Heron's squared quantity is heronSq; the private lemma heron_eval says that if heronSq a b c = x then the hinge area is $\sqrt{x}$.
The local goal is a non-vacuous flat SchlaefliIdentityN witness at $n_H=n_E=10$: strictly positive hinge areas so the identity is not a zero-measure shell.
proof idea
Unfold hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges, and seedFlatSqEdges. For hinge 3 the boundary squared edges are $2,3,1$. A one-line norm_num check gives heronSq 2 3 1 = 1/2. Apply heron_eval to replace the area by $\sqrt{1/2}$, then sqrt_half rewrites that as $\sqrt{2}/2$.
why it matters
Feeds hingeAreaFlat_pos, which cases on all ten hinges and quotes this identity (with positivity of $\sqrt{2}/2$) for index 3. That positivity theorem is the module's non-vacuous flat Schläfli witness: every flat hinge area is strictly positive, so the flat summand table is not a zero-measure shell (lesson L-p1-schlaefli-not-vacuous-prop).
Together with the sibling closed forms for the other hinge indices, it supplies the area factors in the flat Schläfli summand table and the seed-hinge row that must match hingeArea · angleKernel from the 4D dihedral kernel. It is Gate-A2-style input at flat for the directional Schläfli kill along every affine velocity through the seed. It does not close the open pathwise identity off the flat seed, nor S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.