flatSchlaefliIdentity
plain-language theorem explainer
Flat Freudenthal 4-simplex data satisfies the n-dimensional Schläfli identity at ten hinges and ten edges, with strictly positive triangle areas. Anyone assembling Gate-A2 style Regge input in 4D cites this as the non-vacuous flat witness. The proof cancels the positive area factors against the normalized angle derivatives and invokes the already-proved vanishing of the summand column sums.
Claim. For the flat Freudenthal 4-simplex Schläfli data (ten triangle hinges, ten edges), with hinge measures equal to the positive flat triangle areas and angle derivatives equal to the flat summands divided by those areas, one has $\sum_{h=1}^{10} V_{2}(h)\,\partial\theta_h/\partial L_e = 0$ for every edge coordinate $e$.
background
The 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 count and the triangle-hinge count equal ten. The n-dimensional Schläfli identity asserts that for every edge coordinate $e$, the weighted sum of dihedral-angle derivatives vanishes: $\sum_h V_{n-2}(h),\partial\theta_h/\partial L_e = 0$.
Here the hinge measure $V_2(h)$ is the flat triangle area of hinge $h$, obtained from the three squared edge lengths of that face via the usual Heron-type formula; each such area is strictly positive. The angle-derivative table is defined by normalizing a closed-form rational summand table by those areas. Upstream, the column sums of the un-normalized summand table are already known to vanish identically on every edge (flat closed-form theorem).
proof idea
Fix an arbitrary edge index $e$. Invoke the flat closed-form column-sum theorem: the sum over the ten hinges of the un-normalized summands is zero. Unfold the flat Schläfli data so that each term is area times (summand/area). By Finset congruence and field simplification, using strict positivity of every hinge area, the area factors cancel and the weighted sum collapses exactly to the un-normalized column sum, hence to zero. That is the Schläfli identity proposition.
why it matters
This is the module's non-vacuous flat SchlaefliIdentityN witness at $n_H = n_E = 10$, the 4D analogue of the tetrahedron six-edge closed form. It deliberately avoids a zero-measure shell: areas are strictly positive, matching the lesson that Schläfli identities must not be inhabited vacuously.
Downstream, flat_schlaefliN_kills applies the generic eliminator to this witness and obtains the concrete vanishing of the measure-weighted angle terms on every edge. That kill is the Gate-A2-style flat directional input for the pathwise Schläfli program. Open items remain: the full pathwise identity off the flat seed on nondegenerate 4-simplices, remapped derivatives for every hinge row, elevation to the Regge candidate, and convergence of the RS action to Einstein-Hilbert in 4D. The result does not flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.