freudenthal4SimplexFlatDirectionalSchlaefliPresent_true
plain-language theorem explainer
Boolean certificate that the flat directional Schläfli identity holds on the Freudenthal 4-simplex: the compiled witness equals true. Gravity analysts cite it as the Gate A2-style flat kill before second-variation elevation. The proof is pure definitional reflexivity on a decidable Bool.
Claim. The boolean witness that the flat directional Schläfli identity holds for the Freudenthal (Kuhn) 4-simplex, along every affine edge-velocity through the flat seed, evaluates to $\mathrm{true}$.
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the 4-simplex, where both the edge count and the triangle-hinge count are ten. The Freudenthal/Kuhn triangulation supplies the combinatorial skeleton: squared edge lengths, triangle hinges, and flat hinge areas.
At the flat seed the Schläfli summand table is assembled from hinge area times the dihedral angle kernel. Column sums vanish, and the seed-hinge row matches the closed-form kernel from the 4D dihedral analysis. The directional claim is that every affine velocity through that flat seed kills the first variation of the Regge action (the flat directional Schläfli identity).
The boolean freudenthal4SimplexFlatDirectionalSchlaefliPresent packages that kill as a decidable presence flag, so downstream elevation wiring can demand a literal true rather than an abstract Prop.
proof idea
One-line wrapper: rfl. The presence flag is a closed Bool term already reduced to true by the surrounding decidable assembly (flat summand table, column-sum vanishings, and seed-hinge kernel match). No tactic search and no external lemma application beyond definitional equality.
why it matters
Feeds the re-export flat_freudenthal_directional_schlaefli_present in Regge4DFlatSecondVariation, documented as "Gate A2-style flat directional kill, re-exported for elevation wiring." That is the flat half of the 4D Schläfli ladder toward Regge4DSchlafliElevationToCandidate and eventually S_RS_converges_EH_4d.
In the module tier list this closes the THEOREM bullet on flat directional Schläfli kill along every affine velocity through the flat seed. It deliberately does not flip gap_action_recovery and does not inhabit a zero-measure Schläfli shell (lesson L-p1). Open remainders sit one tier up: full pathwise identity off the flat seed on nondegenerate 4-simplices, and remapped HasDerivAt for every hinge row.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.