regge4DFlatSecondVariationStatus
plain-language theorem explainer
Status record for the 4D Regge flat second-variation program: candidate reduced Hessian identified, its Bloch face evaluated at −1/16, and flat Freudenthal Schläfli plus directional kill present as theorems. Full off-flat pathwise Schläfli and nonlinear elevation remain open; gap-action recovery stays false. Downstream honesty lemmas quote these flags by reflexivity. The body is a pure structure literal of booleans.
Claim. The 4D Regge flat second-variation status asserts: the candidate reduced edge Hessian is identified; its Bloch continuum face is evaluated; the flat Freudenthal 4-simplex Schläfli summand table and flat directional Schläfli kill are present; the full off-flat pathwise Schläfli form is absent; Schläfli elevation of the nonlinear action remains open; and gap-action recovery is false.
background
In Regge calculus the discrete Einstein–Hilbert action is a sum of hinge volumes times deficit angles. Gate A2 asks whether the true nonlinear Regge action, twice differentiated at a flat seed, equals a Schläfli-reduced edge Hessian (the candidate assembled from distinct-hinge geometry). In 3D that elevation is closed; in 4D only the flat-seed pieces are closed.
The module mirrors the 3D ReggeTTFlatSecondVariation contract. Upstream theorems in the pathwise Schläfli module supply the flat Freudenthal 4-simplex Schläfli identity (vanishing column sums, seed-hinge geometric match, seed-angle derivative) and the flat directional kill along every affine velocity. The full off-flat pathwise closed form is still missing, so elevation of $S''(0)$ to the candidate stays open.
The structure Regge4DFlatSecondVariationStatus is an honesty flag bundle. Its live mathematical obligation is the elevation proposition (nonlinear second variation equals the candidate), not a tautological assembly identity.
proof idea
Pure definitional structure literal. Each field is assigned a boolean constant (true or false) with no tactic proof and no lemma application. Downstream flag theorems recover the assignments by rfl.
why it matters
Pins the honest residual of the 4D continuum program: residual is Schläfli elevation of the nonlinear action, not another incidence rescale or fitted density factor. Feeds regge4DFlatSecondVariationStatus_flags (conjunction of the positive flags) and schlafli_does_not_flip_gap (pathwise absent, elevation open, gap-action recovery false). Module doc is explicit that this does not inhabit the 4D RS-to-EH convergence statement and does not flip gap-action recovery. Prior closed paths (distinct-hinge fold, full two-jet, mean-local Path B, density dictionary) already fail to close the gap; this status records that fact without overclaiming.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.