NonlinearFlatSecondVariation4D
plain-language theorem explainer
Type alias for an independent nonlinear flat second variation of the 4D edge-length Regge action. It re-exports the torus continuum-limit second-variation type so the open Schläfli-elevation gate can quantify over genuine nonlinear Hessians, not only the candidate fold. Anyone tracking the 4D elevation gap (mirroring the closed 3D tetra Schläfli path) cites this. The body is a one-line abbrev.
Claim. Write $\mathrm{NonlinearFlatSecondVariation4D}$ for the type of independent nonlinear flat second variations in four dimensions, identified with the nonlinear second-variation type already fixed by the 4D torus continuum-limit analysis.
background
This module mirrors the 3D Regge TT flat second-variation contract. Gate A2 elevates the true nonlinear Regge action to a Schläfli-reduced edge Hessian. In 3D that elevation is closed (tetra six-edge closed form to the true action second variation). In 4D the flat-seed Freudenthal closed form, flat directional Schläfli kill, and seed-angle differentiability are theorems, but the full off-flat pathwise Schläfli identity is still missing, so elevation of the nonlinear action remains open.
The residual is therefore Schläfli elevation itself, not another incidence rescale or fitted density factor. Prior paths (distinct-hinge fold, full two-jet, mean-local Path B) do not close the gap: the Bloch continuum face on Frobenius-normalized axis TT sits at $-1/16$, distinct from frozen Einstein–Hilbert $-1/4$, and the density-dictionary survivor is already $1$.
This abbrev names the independent nonlinear $S''$ type that any genuine elevation must inhabit, drawn from the 4D torus continuum-limit package rather than from the candidate fold alone.
proof idea
One-line type abbrev. It equates the local name to NonlinearSecondVariation4D from the 4D torus continuum-limit module. No proof obligations; pure re-export so downstream elevation statements can quantify over that type without importing the continuum-limit namespace at every use site.
why it matters
Parent consumer is the open proposition Regge4DSchlafliElevationToCandidate: existence of an $S''$ of this type, derived from the edge-length Regge action by the 4D pathwise Schläfli kill, such that for every non-aliased mode $(2/N^4)\cdot S''(N,m,E)$ equals the Schläfli candidate fold on the real mode. That statement is the 4D analogue of the closed 3D theorem elevating the true Regge action via Schläfli.
In the Recognition gravity stack this sits on the continuum face of the assembled edge Hessian and the flat Freudenthal pathwise theorems already proved in the Schläfli-pathwise module. It does not flip gap-action recovery and does not inhabit four-dimensional Einstein–Hilbert convergence of the RS action. Closing elevation would discharge the last named residual between the candidate reduced Hessian and a nonlinear $S''(0)$ forced by geometry rather than by fitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.