freudenthal4SimplexPathwiseSchlaefliPresent_false
plain-language theorem explainer
Records that the full off-flat pathwise Schläfli closed form on the Freudenthal 4-simplex is still absent: the Boolean presence flag equals false. Downstream second-variation and elevation work cites this as the named missing identity. The proof is definitional reflexivity against the flag definition.
Claim. The Boolean flag asserting that a full pathwise Schläfli identity holds for every Freudenthal/Kuhn 4-simplex in squared-edge coordinates (off the flat seed) evaluates to false.
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 hinge count and the edge count are ten. It already proves flat combinatorics, flat hinge areas, a non-vacuous flat SchlaefliIdentityN witness with strictly positive areas, seed-hinge dihedral derivatives along squared-edge paths, and flat directional Schläfli kill along every affine velocity through the flat seed.
What remains open is the full pathwise identity off the flat seed on nondegenerate 4-simplices: for every simplex $\sigma$, every edge $e$, and every nondegenerate path point,
$$\sum_{h \subset \sigma} A_h(\sigma),\partial\theta_{\sigma,h}/\partial\ell_e^2 = 0.$$
The Boolean freudenthal4SimplexPathwiseSchlaefliPresent is the library's explicit status bit for that closed form; its definition is the constant false, with doc-comment "Full off-flat pathwise closed form is still absent."
proof idea
One-line definitional proof: rfl. The presence flag is defined as the Boolean constant false, so equality to false is immediate by reflexivity. No lemmas are applied.
why it matters
This theorem is the audited status witness for a named missing identity in 4D Regge calculus. Downstream, Freudenthal4SimplexPathwiseSchlaefli_absent in Regge4DFlatSecondVariation re-exports it and documents the target identity
$$\forall\sigma,,\forall e\in\mathrm{edges}(\sigma):\quad \sum_{h\subset\sigma} A_h(\sigma),\partial\theta_{\sigma,h}/\partial\ell_e^2=0$$
at every nondegenerate path point. That interface note states readiness only: once a concrete SchlaefliDataN 10 10 witness with SchlaefliIdentityN is supplied, the angle term dies in the second-variation assembly.
Module tier tags mark the off-flat pathwise identity, remapped HasDerivAt for every hinge row, Regge4DSchlafliElevationToCandidate, and S_RS_converges_EH_4d as OPEN. The flag does not flip gap_action_recovery and does not inhabit a zero-measure Schläfli shell. In the Recognition gravity stack this is the honest gate between proved flat directional kill and full Einstein-Hilbert recovery in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.