flatHingeData
plain-language theorem explainer
Packages each of the ten triangle hinges of the flat Freudenthal 4-simplex as abstract hinge data whose measure is the closed-form flat hinge area. Anyone assembling the flat Schläfli identity witness at nH = nE = 10 cites this. The body is a two-field structure instance: area from the flat formula, nonnegativity from strict positivity.
Claim. For each hinge index $h \in \{0,\ldots,9\}$, the flat hinge record is the abstract hinge datum whose measure equals the flat triangle area of hinge $h$ on the Freudenthal 4-simplex seed, and that measure is nonnegative.
background
In Regge calculus the Schläfli identity equates a weighted sum of dihedral-angle derivatives to zero. Abstract hinge data for an $n$-simplex stores only the hinge measure (an $(n-2)$-volume) together with a nonnegativity certificate. Here $n=4$, so hinges are triangles and the measure is ordinary area.
This module lifts the 3D Gate-A2 closed-form Schläfli input from the tetrahedron ($n_H=n_E=6$) to the Freudenthal/Kuhn 4-simplex ($n_H=n_E=10$). The flat seed fixes all squared edge lengths; each of the ten hinges then has an explicit area hingeAreaFlat, obtained by feeding the three boundary edge squares into the Heron-style area formula. A companion lemma proves every such area is strictly positive (values $1/2$, $\sqrt{2}/2$, $\sqrt{3}/2$ on the orbit classes).
The present definition simply wraps those areas into the abstract hinge structure so they can be plugged into the finite Schläfli data bundle.
proof idea
Pure structure instance, not a tactic proof. The measure field is set to the already-computed flat hinge area for index $h$. The nonnegativity field is discharged in one step by le_of_lt applied to the strict-positivity theorem for that same area. No further algebraic work.
why it matters
This is the hinge column of the non-vacuous flat Schläfli witness. Downstream, flatSchlaefliData builds full Schläfli data at dimension 4 by taking these hinge records and setting the angle derivatives to (flat summand)/area; flatSchlaefliIdentity then proves the abstract Schläfli identity holds with strictly positive areas, discharging the module's THEOREM tag that the flat identity is not a zero-measure shell (lesson L-p1-schlaefli-not-vacuous-prop).
In the broader RS gravity stack this is Gate-A2-style input at the flat 4-simplex seed: it feeds the directional flat kill and the eventual elevation toward continuum Einstein-Hilbert recovery. It does not itself close the OPEN items (full pathwise identity off the flat seed, remapped derivatives on every hinge row, or $S_{RS}\to EH$ in 4D).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.