hingeAreaFlat_2
plain-language theorem explainer
At the flat Freudenthal 4-simplex seed, the triangular hinge indexed 2 has area exactly $\sqrt{3}/2$. Gravity and Regge analysts cite this when assembling the flat Schläfli summand table and when proving every flat hinge area is strictly positive. The proof unfolds the hinge's three squared edge lengths, evaluates Heron's formula to $3/4$, and rewrites the square root.
Claim. For the flat seed edge-squared assignment on the Freudenthal 4-simplex, the area of triangular hinge $2$ equals $\sqrt{3}/2$.
background
The module develops pathwise Schläfli identities for the Freudenthal (Kuhn) 4-simplex, with ten edges and ten triangle hinges, mirroring the 3D Gate-A2 closed-form input at $n_H=n_E=6$. The flat configuration is the seed squared-edge vector seedFlatSqEdges, aliased here as the flat edge-squared assignment.
Each hinge $h\in\mathrm{Fin},10$ has three boundary edge slots (ordered $v_0v_1$, $v_0v_2$, $v_1v_2$). The flat hinge edge-squared triple is the restriction of the seed to those slots. Hinge area is then Heron's formula: if $a,b,c$ are the three squared lengths, the area is $\sqrt{\mathrm{heronSq}(a,b,c)}$.
The private evaluation lemma says that whenever $\mathrm{heronSq}(a,b,c)=x$, the hinge area equals $\sqrt{x}$. A companion identity rewrites $\sqrt{3/4}=\sqrt{3}/2$.
proof idea
Unfold hinge area at index 2 through the flat edge-squared triple, boundary-slot table, and seed assignment. After simplification the three squared lengths are $1,4,3$. A short norm_num computation shows $\mathrm{heronSq}(1,4,3)=3/4$. Apply the Heron evaluation lemma to replace the area by $\sqrt{3/4}$, then the algebraic identity $\sqrt{3/4}=\sqrt{3}/2$.
why it matters
Strict positivity of all ten flat hinge areas is required for a non-vacuous flat $\mathrm{SchlaefliIdentityN}$ witness at $n_H=n_E=10$ (module tier tag; lesson against zero-measure shells). The parent theorem hingeAreaFlat_pos fin-cases over hinges and uses this closed form for index 2, discharging $0<\sqrt{3}/2$ by positivity.
That positivity feeds the flat Schläfli summand table, column-sum vanishing, and the Gate A2-style directional kill along every affine velocity through the flat seed. It does not yet close the open pathwise identity off the flat seed on nondegenerate 4-simplices, nor the elevation to the continuum Einstein-Hilbert candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.