freudenthal4SimplexFlatSchlaefli
plain-language theorem explainer
For each of the ten squared-edge coordinates on the flat Freudenthal 4-simplex, the sum of the ten flat Schläfli summands over triangle hinges is zero. Anyone assembling the 4D Regge Schläfli identity or the flat directional kill cites this column-sum vanishing. The proof expands the Fin 10 sum and checks the rational table by cases and norm_num.
Claim. For every edge index $e \in \{0,\ldots,9\}$, $$\sum_{h=0}^{9} S_{h,e} = 0,$$ where $S_{h,e}$ is the flat Schläfli summand $A_h \cdot (\partial \theta_h / \partial \ell_e^2)$ evaluated on the Freudenthal seed (as an exact rational, then cast to $\mathbb{R}$).
background
This module lifts the 3D Gate-A2 closed form for the tetrahedron (six edges, six hinges) to the Freudenthal/Kuhn 4-simplex, where both the edge set and the triangle-hinge set have cardinality ten. The local objects are squared edge lengths, flat hinge areas, and the dihedral angle response of each hinge to a squared-edge coordinate.
The flat Schläfli summand table records $A_h \cdot (\partial \theta_h / \partial \ell_e^2)$ as an exact rational matrix flatSchlaefliSummandQ, then casts entrywise to $\mathbb{R}$. Its documentation states that column sums vanish and that the seed row matches the geometric hinge-area times angle kernel. The private lemma sum10 simply unfolds $\sum_{h:Fin,10}$ into the ten-term addition used in the case check.
The ambient goal is a non-vacuous flat witness of the $n$-hinge Schläfli identity at $n_H = n_E = 10$, with strictly positive areas, feeding the flat directional contraction used as Gate A2-style input in 4D Regge calculus.
proof idea
Term-mode proof by exhaustive arithmetic. Rewrite the Fin 10 sum via sum10 into the explicit ten-term sum. Case-split on the edge index $e$ with fin_cases. On each branch, unfold flatSchlaefliSummand and the rational table flatSchlaefliSummandQ, then discharge the resulting rational identity with norm_num. No geometric lemmas are invoked; the vanishing is a finite check of the precomputed table.
why it matters
This is the flat closed-form column-sum theorem for the Freudenthal 4-simplex Schläfli table. It is the direct 4D analog of the 3D six-edge closed form and is tagged THEOREM in the module tier list: column sums vanish.
Downstream it is re-exported as flat_freudenthal_schlaefli_identity, supplies the sum hypothesis inside flatSchlaefliIdentity (the non-vacuous SchlaefliIdentityN witness with strictly positive areas), and is the algebraic engine behind the Gate A2-style flat directional kill freudenthal4SimplexFlatDirectionalSchlaefli and its coordinate form. Real and area-cancellation lemmas in the same file also reduce to it.
In the broader Recognition gravity stack this is scaffolding for pathwise Schläfli at flat, not a claim about the full off-seed identity on nondegenerate 4-simplices, nor about S_RS_converges_EH_4d or gap_action_recovery. Those remain open per the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.