hingeAreaFlat_7
plain-language theorem explainer
The triangular hinge of index 7 on the flat Freudenthal 4-simplex has area √2/2. Anyone building the flat Schläfli summand table or proving strictly positive hinge areas cites this closed form. The proof unfolds the three squared edge lengths at the flat seed, evaluates Heron to 1/2, and rewrites √(1/2) as √2/2.
Claim. On the flat squared-edge seed of the Freudenthal 4-simplex, the area of triangular hinge $7$ equals $\sqrt{2}/2$.
background
The module lifts the 3D Gate-A2 Schläfli input to the Freudenthal (Kuhn) 4-simplex, where there are ten edges and ten triangular hinges ($n_H = n_E = 10$). Flat geometry is fixed by a seed list of squared edge lengths; each hinge area is then the ordinary triangle area of its three boundary edges.
Concretely, the boundary slots of a hinge pick three coordinates from the flat seed, and the area is Heron's formula applied to those three squared lengths. A small evaluation lemma says that if the squared Heron expression equals $x$, the area is $\sqrt{x}$. A companion identity rewrites $\sqrt{1/2}$ as $\sqrt{2}/2$.
This sits in the THEOREM tier for flat hinge areas and for a non-vacuous flat Schläfli witness with strictly positive areas.
proof idea
Unfold the area definition, the hinge's three flat squared edges, the boundary-slot table, and the flat seed list. The resulting Heron input is the triple $(1,3,2)$. A one-line norm_num check shows the squared Heron expression equals $1/2$. Rewrite the area as $\sqrt{1/2}$ via the evaluation lemma, then apply the half-square-root identity to obtain $\sqrt{2}/2$.
why it matters
Feeds the case analysis in the positivity theorem for all ten flat hinge areas, which is the non-vacuous positive-area witness required by the module's flat SchlaefliIdentityN theorem at $n_H = n_E = 10$. Without closed forms such as this one, the flat Schläfli summand table and the Gate-A2-style directional kill at the flat seed would rest on unevaluated symbols.
It does not touch the OPEN items: full pathwise identity off the flat seed on nondegenerate 4-simplices, remapped derivatives for every hinge row, elevation to the continuum candidate, or convergence of the RS action to Einstein-Hilbert in 4D. It also does not flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.