Regge4DFlatSecondVariationStatus
plain-language theorem explainer
Status record of honesty flags for the 4D flat Regge second-variation program: which pieces are closed theorems versus still open. Gravity analysts cite it to read off, without scanning the whole module, whether the Schläfli candidate, Bloch face, and Freudenthal flat kills are present, and whether elevation and gap-action recovery remain open. It is a plain structure of booleans; no proof.
Claim. A status bundle of seven boolean flags recording: whether the Schläfli-reduced edge Hessian candidate is identified; whether its Bloch continuum face is evaluated; whether the flat Freudenthal 4-simplex Schläfli table is present; whether the flat directional Schläfli kill is present; whether the full off-flat pathwise Schläfli form is present; whether Schläfli elevation of the nonlinear action remains open; and whether gap-action recovery is claimed.
background
This module mirrors the 3D ReggeTTFlatSecondVariation contract for Gate A2: elevate the true nonlinear Regge action to a Schläfli-reduced edge Hessian. In 3D that elevation is a theorem. In 4D the flat-seed Freudenthal closed form and flat directional Schläfli kill are theorems in the pathwise module (freudenthal4SimplexFlatSchlaefli, freudenthal4SimplexFlatDirectionalSchlaefli, seed-angle HasDerivAt), but the full off-flat pathwise closed form is absent, so elevation of the nonlinear action stays open.
The live elevation obligation is the proposition that there exists an independent nonlinear second variation $S''$ from the edge-length Regge action such that, for every non-aliased mode, the density-weighted $S''$ equals the Schläfli candidate fold on the real mode. Prior paths (distinct-hinge fold, full two-jet, path-B mean-local, density dictionary) do not close that residual; it is Schläfli elevation, not another incidence rescale.
proof idea
No proof: this is a structure declaration packing seven Bool fields. Downstream, a single definition inhabits it by assigning concrete flags (candidate and Bloch face true; flat Freudenthal Schläfli and directional kill true; full pathwise Schläfli false; elevation open; gap-action recovery false). The structure itself only names the honesty axes.
why it matters
Gives a single machine-readable snapshot of what the 4D flat second-variation stack has actually closed. Downstream regge4DFlatSecondVariationStatus fills the flags so importers need not re-audit the module. Tier tags bind: candidate Hessian and Bloch face at Frobenius-normalized axis TT equal to $-1/16$ (distinct from frozen EH $-1/4$) are theorem-side; flat Freudenthal Schläfli and directional kill are theorem-side; full pathwise Schläfli and therefore elevation of nonlinear $S''(0)$ to the candidate remain open. Does not flip gap-action recovery and does not inhabit continuum convergence of the RS action to 4D Einstein–Hilbert. Residual is Schläfli elevation, the 4D analogue of the closed 3D elevation theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.