Freudenthal4SimplexPathwiseSchlaefliTarget
plain-language theorem explainer
Defines the proposition that the Freudenthal 4-simplex has a full off-flat pathwise Schläfli closed form. Anyone tracking Gate-A2 elevation from tetrahedra to 4-simplices cites this as the named target Prop. It is literally the Boolean presence flag set equal to true; that flag is currently false.
Claim. The proposition asserting that the Freudenthal 4-simplex pathwise Schläfli closed form is present, i.e. that the Boolean presence flag equals $\mathrm{true}$.
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 edge count and the triangle-hinge count are ten. The local program proves flat combinatorics, positive-area flat Schläfli witnesses, seed-hinge dihedral derivatives, and 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, together with remapped hinge-row derivatives and the elevation to a Regge–Einstein–Hilbert candidate. The Boolean freudenthal4SimplexPathwiseSchlaefliPresent records that gap: its doc-comment states "Full off-flat pathwise closed form is still absent," and its value is false.
proof idea
Pure definitional abbreviation: the target Prop is definitionally the equality of the presence Boolean to true. No lemmas, no tactics.
why it matters
Names the missing off-flat pathwise closed form so downstream code can state openness cleanly. The immediate consumer is Freudenthal4SimplexPathwiseSchlaefliTarget_open, which proves the negation by reducing to false ≠ true. In the module tier list this sits under OPEN (full pathwise identity off the flat seed; elevation to the 4D Regge candidate; convergence of the RS action to Einstein–Hilbert in 4D). It does not touch gap-action recovery and deliberately avoids a vacuous zero-measure Schläfli shell. Within Recognition gravity this is the 4D Gate-A2-style checkpoint still awaiting a closed-form witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.