freudenthal4SimplexPathwiseSchlaefliPresent
plain-language theorem explainer
Boolean readiness flag fixed at false: the full off-flat pathwise Schläfli identity on a Freudenthal/Kuhn 4-simplex (ten hinges, ten edges) is not yet in the library. Gravity analysts cite it when separating closed flat Gate-A2 inputs from the still-open pathwise elevation. The body is the constant false, paired with a trivial equality lemma and a Prop target that would flip when the identity lands.
Claim. The readiness flag for a full pathwise Schläfli closed form on the Freudenthal 4-simplex (off the flat seed, in squared-edge coordinates) equals $\mathsf{false}$: that identity is recorded as absent.
background
This module lifts the 3D Gate-A2 input (tetrahedron six-edge Schläfli closed form) to the Freudenthal/Kuhn 4-simplex, where both the hinge count and the edge count equal ten. The closed tier already covers combinatorics, flat hinge areas, the flat Schläfli summand table with vanishing column sums, 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 that flat seed on nondegenerate 4-simplices: for every simplex and every edge, at every nondegenerate path point, the sum over faces of area times the partial of the dihedral angle in the squared edge length vanishes. The present declaration is the boolean ledger entry for that missing closed form, not a geometric theorem.
proof idea
One-line definition: the boolean is the constant false. No lemmas, no tactics. The sibling equality theorem is rfl against that constant; the Prop target is definitional equality of the flag to true.
why it matters
Serves as the typed OPEN marker for pathwise 4D Schläfli in the Regge analysis stack. Downstream, Freudenthal4SimplexPathwiseSchlaefli_absent re-exports the flag as the named missing identity (sum of $A_h \partial\theta_{\sigma,h}/\partial\ell_e^2 = 0$ on every nondegenerate path point). Freudenthal4SimplexPathwiseSchlaefliTarget is the Prop that becomes inhabited only when the flag flips to true. Flat-second-variation work (including decoy-gauge vanishing of the Schläfli candidate) can proceed while this remains false; the module doc lists the still-open elevation path (Regge4DSchlafliElevationToCandidate, $S_{RS}$ convergence to Einstein-Hilbert in 4D) and stresses that this gap does not flip gap_action_recovery and does not inhabit a vacuous zero-measure Schläfli shell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.