hingeAreaFlat_5
plain-language theorem explainer
On the flat Freudenthal 4-simplex seed, triangle-hinge 5 has area exactly √3/2. Cited by anyone building the flat Schläfli summand table or proving all ten flat hinge areas are strictly positive. Proof unfolds the three squared boundary lengths, evaluates Heron by norm_num to 3/4, then rewrites √(3/4) as √3/2.
Claim. The area of hinge $5$ at the flat squared-edge seed of the Freudenthal 4-simplex equals $\sqrt{3}/2$.
background
The module treats pathwise Schläfli for the Freudenthal/Kuhn 4-simplex ($n_H = n_E = 10$), the 4D analogue of the 3D tetrahedron Gate-A2 closed form. At the flat seed, squared edge lengths are the fixed vector seedFlatSqEdges (aliased as flatSqEdges). Each hinge is a triangular face whose three boundary edges are read off a combinatorial slot table.
hingeAreaFlat h extracts those three squared lengths via hingeFlatEdgeSq and feeds them to the Heron area. The private lemma heron_eval states that if the Heron squared-area polynomial equals $x$, the hinge area is $\sqrt{x}$. A companion rewrite sqrt_three_quarter records $\sqrt{3/4} = \sqrt{3}/2$.
proof idea
Simp unfolds hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges, and seedFlatSqEdges, exposing the three squared lengths $(3,4,1)$ on hinge 5. A one-line unfold heronSq; norm_num proves heronSq 3 4 1 = 3/4. Rewrite with heron_eval to obtain $\sqrt{3/4}$, then apply sqrt_three_quarter.
why it matters
Direct input to hingeAreaFlat_pos, which fin_cases over all ten hinges and rewrites each closed form to a strict positivity fact. That positivity is the module's non-vacuous flat SchlaefliIdentityN witness at $n_H = n_E = 10$ (lesson L-p1-schlaefli-not-vacuous-prop): areas must be strictly positive, not a zero-measure shell. Fills the THEOREM tier on flat hinge areas and the flat Schläfli summand table. Does not touch the OPEN items (full pathwise identity off the flat seed, remapped HasDerivAt for every hinge row, or $S_{RS}\to$ EH in 4D).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.