flatSchlaefliData
plain-language theorem explainer
Packages flat Freudenthal 4-simplex geometry into the n-dimensional Schläfli data structure at ten hinges and ten edges. Hinge measures are the closed-form flat triangle areas; angle derivatives are the flat summand table divided by those areas. Cited by the non-vacuous flat identity witness and the column-kill lemma. Pure structure assembly from already-proved flat tables.
Claim. Define flat Schläfli data $D$ of type $\mathrm{SchlaefliDataN}(10,10)$ by taking hinge measures $V_{2}(h)$ equal to the flat hinge areas $A_h^{\mathrm{flat}}$, and setting $\partial\theta_h/\partial L_e := S_{h,e}/A_h^{\mathrm{flat}}$, where $S_{h,e}$ is the flat Schläfli summand table entry for hinge $h$ and edge $e$.
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, where both the hinge count and the edge count equal ten. The ambient structure SchlaefliDataN nH nE packages, for each hinge, an $(n-2)$-measure and a full table of partials $\partial\theta_h/\partial L_e$. The identity asserted on such data is $\sum_h V_{n-2}(h),\partial\theta_h/\partial L_e=0$ for every edge coordinate $e$.
Upstream, hingeAreaFlat evaluates Heron area on the three squared edge lengths of each flat triangle hinge; those areas are strictly positive. The table flatSchlaefliSummand is the closed-form flat contribution $A_h,\partial\theta_h/\partial L_e$ at the seed, already known to have vanishing column sums (freudenthal4SimplexFlatSchlaefli). flatHingeData wraps those areas into HingeDataN with a nonnegativity proof from positivity.
proof idea
Definitional assembly, not a proof. The hinge field is exactly flatHingeData. The derivative field is the pointwise quotient of the flat summand table by the flat hinge area: $S_{h,e}/A_h^{\mathrm{flat}}$. No tactics; the quotient is well-defined because hingeAreaFlat_pos guarantees $A_h^{\mathrm{flat}}>0$.
why it matters
This is the concrete flat witness that feeds flatSchlaefliIdentity, the module's non-vacuous SchlaefliIdentityN theorem at $nH=nE=10$ with strictly positive areas (lesson against zero-measure shells). Downstream, flat_schlaefliN_kills rephrases the same column vanishing as the angle-term kill used by Gate A2-style directional arguments through the flat seed.
In the broader Regge/RS gravity stack it is the 4D analogue of the tetrahedron closed-form Schläfli input: a flat seed package on which pathwise directional kills and Hessian assembly can be stated. It does not yet discharge the open pathwise identity off the flat seed on Nondeg4Simplex, nor S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.