freudenthal4SimplexFlatSchlaefliPresent
plain-language theorem explainer
Boolean presence flag recording that the flat Freudenthal 4-simplex Schläfli package is installed: ten hinges, ten edges, strictly positive flat areas, and a non-vacuous flat SchläfliIdentityN witness. Downstream second-variation and pathwise modules cite it as a preflight gate before assembling the flat Hessian or directional kill. The body is the constant true.
Claim. The flat Freudenthal (Kuhn) 4-simplex Schläfli data are marked present: a Boolean equal to $\mathrm{true}$ asserting that the $n_H = n_E = 10$ flat seed carries a non-vacuous Schläfli identity witness with strictly positive hinge areas.
background
The module lifts the 3D Gate-A2 tetrahedron input (six edges, six hinges, closed-form Schläfli) to the Freudenthal/Kuhn triangulation of the 4-simplex, where both the hinge count and the edge count equal ten. At the flat seed one needs squared edge lengths, flat hinge areas (via Heron-type formulae on triangular faces), and the flat Schläfli summand table whose column sums vanish.
SchläfliIdentityN is the discrete identity relating area-weighted dihedral variations to edge-length variations; the module insists on a non-vacuous witness (strictly positive areas), following the lesson that a zero-measure shell is not acceptable. The flag sits beside the combinatorial tables, flat-area evaluations, and the seed-hinge match to hingeArea · angleKernel from the 4D dihedral kernel.
Local setting is pathwise Schläfli at flat plus directional kill along affine velocities through the flat seed. Full pathwise identity off the flat seed on Nondeg4Simplex remains open.
proof idea
One-line definition: the Boolean is the constant true. No lemmas are applied. The companion theorem freudenthal4SimplexFlatSchlaefliPresent_true discharges equality to true by rfl, and the second-variation module re-exports that fact as a preflight alias.
why it matters
Serves as the preflight gate that the flat Freudenthal Schläfli package is online before second-variation work. Downstream, flat_freudenthal_schlaefli_present in Regge4DFlatSecondVariation is the local alias used when assembling the flat Hessian and continuum preflight matrices. Within the module, freudenthal4SimplexFlatSchlaefliPresent_true is the trivial witness that the flag holds.
In the Recognition gravity stack this is the 4D analogue of the Gate-A2 tetrahedron Schläfli input: without a non-vacuous flat identity at nH = nE = 10, directional Schläfli kill and later elevation toward the Einstein-Hilbert continuum limit cannot start. It does not close the open items (off-seed pathwise identity, full hinge-row HasDerivAt remapping, Regge4DSchlafliElevationToCandidate, or S_RS_converges_EH_4d), and it does not flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.