freudenthal4SimplexFlatSchlaefli_real
plain-language theorem explainer
For each of the ten squared-edge coordinates of the flat Freudenthal 4-simplex, the sum of the ten real Schläfli summands over triangle hinges vanishes. Anyone assembling the flat Gate-A2 input for 4D Regge calculus cites this column-sum identity. The proof is a one-line term wrapper of the rational closed-form column-sum theorem.
Claim. For every edge index $e \in \{0,\ldots,9\}$ of the flat Freudenthal 4-simplex, $\sum_{h=0}^{9} S_{h,e}^{\mathrm{flat}} = 0$, where $S_{h,e}^{\mathrm{flat}}$ is the real-valued flat Schläfli summand of hinge $h$ with respect to edge $e$.
background
The module lifts the 3D Gate-A2 closed form (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, where both the edge set and the triangle-hinge set have cardinality 10. The flat seed is the regular combinatorial 4-simplex with squared edge lengths fixed so that all hinge areas are strictly positive and dihedral defects vanish.
A flat Schläfli summand pairs a hinge area with the partial of the corresponding dihedral angle in a squared-edge coordinate. The real-valued table flatSchlaefliSummandReal is definitionally the same table as the rational closed form used upstream. The parent result states that every column of that table sums to zero: "Column sums of the summand table vanish."
This is the discrete Schläfli identity at the flat point, the 4D analogue of the classical relation $\sum A_h,d\theta_h = 0$ on a Euclidean simplex.
proof idea
One-line term wrapper: apply freudenthal4SimplexFlatSchlaefli e. That upstream theorem rewrites the ten-term sum via sum10, then fin_cases on the edge index and norm_num on each explicit rational entry of flatSchlaefliSummand / flatSchlaefliSummandQ. Because flatSchlaefliSummandReal is an abbrev for the same summand, the real-typed statement inherits the identity with no extra arithmetic.
why it matters
This is the real-typed packaging of the flat closed-form column-sum theorem that the module tags as THEOREM under Freudenthal 4-simplex combinatorics. It supplies the Gate-A2-style flat input at $n_H = n_E = 10$: every directional Schläfli kill along affine velocities through the flat seed rests on these vanishing column sums.
Downstream the module aims at a non-vacuous SchlaefliIdentityN witness with strictly positive areas, seed-hinge HasDerivAt along every squared-edge path, and eventually Regge4DSchlafliElevationToCandidate and $S_{RS}$ convergence to Einstein-Hilbert in 4D. Those remain OPEN; this declaration only seals the flat real column sums. It does not flip gap_action_recovery and deliberately avoids a zero-measure Schläfli shell (lesson L-p1-schlaefli-not-vacuous-prop).
In the broader RS gravity stack this is pure discrete differential geometry scaffolding for the Regge action, not a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.