Freudenthal4SimplexPathwiseSchlaefli_absent
plain-language theorem explainer
Records that the full off-flat pathwise Schläfli identity on Freudenthal/Kuhn 4-simplices is absent from the library: the presence flag is false. Anyone tracking Gate A2 elevation of the nonlinear 4D Regge action to a Schläfli-reduced edge Hessian cites this status fact. Proof is a one-line wrapper of the Boolean definitional equality.
Claim. The Boolean flag asserting that a full off-flat pathwise Schläfli closed form holds on every Freudenthal 4-simplex (in squared-edge coordinates) equals $\mathsf{false}$. Equivalently, the $n_H = n_E = 10$ instance of the $n$-dimensional Schläfli identity $\sum_h A_h(\sigma)\,\partial\theta_{\sigma,h}/\partial\ell_e^2 = 0$ along a general nondegenerate path is not supplied.
background
In Regge calculus the Schläfli identity kills the angle variation of the action, leaving only edge-length derivatives of hinge measures. The $n$-dimensional package SchlaefliDataN packages hinge measures and partials $\partial\theta_h/\partial L_e$; SchlaefliIdentityN is the statement $\sum_h V_{n-2}(h)\cdot\partial\theta_h/\partial L_e = 0$ for every edge coordinate $e$.
The 3D analog is closed: six-edge tetrahedron Schläfli is a theorem and elevates the true nonlinear Regge action to a Schläfli-reduced edge Hessian at flat space. In 4D the flat-seed Freudenthal closed form, seed-angle differentiability, and flat directional kill along every affine velocity are theorems in the pathwise module. What remains missing is the full off-flat pathwise identity on every Freudenthal/Kuhn 4-simplex along a general nondegenerate path (the $n_H=n_E=10$ squared-edge instance).
This module mirrors the 3D flat-second-variation contract: Gate A2 elevates the nonlinear action only after that pathwise identity is in hand. Until then elevation stays open.
proof idea
One-line term wrapper. The presence flag is defined as the Boolean constant false; the upstream lemma proves that equality by rfl. This declaration simply re-exports that definitional fact under the named-missing-identity label used by the second-variation status page.
why it matters
Pins the OPEN residual in 4D Regge flat second variation. Module doc states that flat Freudenthal Schläfli summand tables, seed-hinge match, seed-angle HasDerivAt, and flat directional kill are THEOREM, while full off-flat pathwise Schläfli and therefore elevation of nonlinear $S''(0)$ to the candidate Hessian remain OPEN. Prior repair paths (distinct-hinge fold, full two-jet, path-B mean-local, density dictionary) do not close the gap; the residual is Schläfli elevation, not another incidence rescale.
Downstream the flag blocks inhabiting a vacuous Prop shell and keeps Regge4DSchlafliElevationToCandidate from being claimed. It does not flip gap_action_recovery and does not inhabit continuum EH convergence. In the Recognition gravity stack this is the precise missing geometric identity between the proved flat-seed layer and Gate A2 action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.