flatSchlaefliSummandReal
plain-language theorem explainer
Real-valued alias of the flat Schläfli summand table on the Freudenthal 4-simplex: each hinge-edge pair (h,e) in Fin 10 × Fin 10 maps to a real number. Downstream column-sum theorems cite it when stating that every edge column vanishes at the flat seed. The body is a one-line abbreviation of the rational table cast to ℝ.
Claim. For hinge index $h\in\{0,\ldots,9\}$ and edge index $e\in\{0,\ldots,9\}$, the real flat Schläfli summand equals the rational flat Schläfli table entry $(h,e)$ viewed as a real number.
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 edge set and the triangle-hinge set have cardinality 10. The flat seed is the regular Euclidean configuration used as the base point for directional derivatives of dihedral angles and for the flat Hessian assembly of Regge calculus in 4D.
The Schläfli identity in discrete gravity relates hinge areas to dihedral-angle variations along edge lengths. At the flat seed the identity reduces to a numerical table: each entry is the contribution of one hinge to one edge coordinate. The upstream definition flatSchlaefliSummand builds that table by casting a rational matrix flatSchlaefliSummandQ to ℝ; the present abbreviation simply renames that real-valued map for use in real-arithmetic statements.
Module tier tags mark the flat summand table, vanishing column sums, and seed-hinge geometric match as THEOREM-level content, while full pathwise identity off the flat seed remains OPEN.
proof idea
One-line abbreviation: flatSchlaefliSummandReal is definitionally identical to flatSchlaefliSummand. No tactics, no lemmas. The upstream definition already performs the cast (flatSchlaefliSummandQ h e : ℝ).
why it matters
Gives a stable real-typed name for the flat Schläfli table so that real-sum theorems can state column vanishing without repeating the rational cast. The immediate parent is freudenthal4SimplexFlatSchlaefli_real, which asserts
$\sum_{h:0}^{9}\mathrm{flatSchlaefliSummandReal}(h,e)=0$
for every edge $e$, by reducing to the rational column-sum theorem.
That vanishing is the Gate-A2-style flat input at $n_H=n_E=10$: a non-vacuous SchlaefliIdentityN witness with strictly positive areas. It feeds the directional Schläfli kill along affine velocities through the flat seed and the seed-hinge match to hingeArea · angleKernel. It does not close the OPEN items (pathwise identity off flat, full remapped HasDerivAt, elevation to the EH candidate, or $S_{RS}$ convergence in 4D), and it does not flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.