flat_schlaefliN_kills
plain-language theorem explainer
On the flat Freudenthal 4-simplex, the weighted sum of dihedral-angle derivatives against every squared-edge coordinate vanishes: each column of the flat Schläfli table is zero. Anyone assembling Gate-A2-style Regge input in 4D cites this as the flat directional kill. The proof is a one-line application of the n-dimensional Schläfli eliminator to the non-vacuous flat identity witness.
Claim. For every squared-edge index $e \in \{0,\ldots,9\}$, $$\sum_{h=0}^{9} A_h \, \partial_{\ell_e}\theta_h = 0,$$ where $A_h > 0$ are the flat hinge areas of the Freudenthal 4-simplex and $\partial_{\ell_e}\theta_h$ are the flat directional derivatives of the dihedral angles with respect to squared edge lengths, packaged in the flat Schläfli data.
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 hinge count and the edge count equal ten. Schläfli data in dimension $n$ package, for each hinge, a measure (here the triangle area) and a table of directional derivatives of dihedral angles along squared-edge coordinates. The identity asserts that every edge-column of that table, weighted by hinge measures, sums to zero.
flatSchlaefliData is the concrete 10-by-10 package at the flat seed: hinge measures are the strictly positive flat areas, and the derivative table is the flat summand table divided by those areas. flatSchlaefliIdentity records that this package satisfies the abstract $n$-dimensional Schläfli identity, and is explicitly non-vacuous (positive areas).
Upstream, schlaefliN_kills_angle_term is the direct eliminator: any data satisfying the identity has vanishing measure-weighted angle-derivative columns. The module tags this flat directional kill as THEOREM-level Gate-A2-style input at the flat seed.
proof idea
One-line wrapper. Apply schlaefliN_kills_angle_term to flatSchlaefliData with the hypothesis flatSchlaefliIdentity, at the given edge index $e$. The eliminator simply projects the identity at $e$, so no further algebra is needed.
why it matters
This is the flat directional Schläfli kill for the Freudenthal 4-simplex: every affine velocity through the flat seed has vanishing first variation of the angle term. It is the 4D counterpart of the 3D closed-form tetrahedron Schläfli input and supplies the Gate-A2-style column-sum vanishing that Regge Hessian and curvature assemblies expect at flat space.
The module marks full pathwise identity off the flat seed on nondegenerate 4-simplices, remapped HasDerivAt for every hinge row, elevation to a candidate, and $S_{RS}\to$ Einstein-Hilbert convergence in 4D as still OPEN. This lemma closes only the flat seed case and does not flip gap-action recovery. No downstream consumers are wired yet in the graph; it stands as the certified flat kill ready for those assemblies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.