hingeAreaFlat_4
plain-language theorem explainer
At the flat Freudenthal 4-simplex seed, the triangular area of hinge index 4 equals exactly 1. Anyone assembling the flat Schläfli summand table or the non-vacuous positivity witness cites this evaluation. The proof unfolds Heron on the three boundary squared lengths (2, 4, 2), reduces the radicand to 1, and takes the positive square root.
Claim. Let $A_4$ be the area of hinge $4$ on the flat Freudenthal $4$-simplex seed, obtained by applying Heron's formula to the three boundary squared edge lengths of that hinge. Then $A_4 = 1$.
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges) 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 corresponding squared lengths at the flat seed are packaged by hingeFlatEdgeSq, and the hinge area is Heron's formula on those three numbers: if $a,b,c$ are the squared side lengths, the squared area is heronSq a b c = (2ab+2bc+2ca-a^2-b^2-c^2)/16, and the area itself is its nonnegative square root.
The private lemma heron_eval simply rewrites the area as $\sqrt{x}$ once heronSq a b c = x is known. Hinge 4 draws slots 1, 3, 8, which evaluate to the triple $(2,4,2)$ on the flat seed.
proof idea
A short tactic proof. First simp only unfolds hingeAreaFlat, hingeFlatEdgeSq, hingeBoundarySlots, flatSqEdges, and seedFlatSqEdges, exposing the concrete Heron call on $(2,4,2)$. A local have computes heronSq 2 4 2 = 1 by unfolding the polynomial and norm_num. Then heron_eval rewrites the area as $\sqrt{1}$, and Real.sqrt_one finishes.
why it matters
Feeds directly into hingeAreaFlat_pos, which asserts $0 < \mathrm{hingeAreaFlat},h$ for every hinge by case analysis; the $h=4$ branch rewrites via this equality and checks $0<1$. That positivity lemma 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 so the identity is not a zero-measure shell.
Together with the sibling evaluations for the other nine hinges, it populates the flat Schläfli summand table and matches the seed-hinge row against hingeArea · angleKernel from the 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 items (full pathwise identity off the flat seed, elevation to the continuum candidate, or $S_{RS}\to EH$ in 4D).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.