SchlaefliElevationToCandidateClosesEH
plain-language theorem explainer
Packages two open propositions as one Prop: Schläfli elevation of the nonlinear 4D Regge second variation onto the distinct-hinge candidate, and the continuum Einstein-Hilbert target that the Bloch symbol equal (-1/8) times the Frobenius norm squared on TT modes. Anyone auditing whether flat 4D Regge recovers EH cites this conjunction. The body is a pure definitional meet of those two named targets, not a proof.
Claim. The packaged claim that both of the following hold: (i) there exists a nonlinear flat second variation $S''$ of the edge-length Regge action, obtained by 4D pathwise Schläfli reduction, such that for every non-aliased lattice mode the weighted second-difference density equals the Schläfli candidate fold of the polarization at the real mode; and (ii) for every nonzero integer mode and every TT polarization $E$, the continuum symbol equals the scale-explicit Einstein-Hilbert face $(-1/8)\|E\|_F^2$.
background
This module tracks the 4D analogue of the 3D Regge TT flat second-variation contract. Gate A2 asks whether the true nonlinear Regge action elevates, via a Schläfli kill, to a reduced edge Hessian. In 3D that elevation is closed. In 4D the flat-seed Freudenthal Schläfli identities, directional kills, and seed-angle differentiability are theorems, but the full off-flat pathwise closed form is still missing, so elevation of the nonlinear action remains open.
The first conjunct is the open elevation statement: existence of an independent nonlinear $S''$ such that the density-weighted second difference equals the Schläfli candidate fold on non-aliased modes. The second conjunct is the named continuum EH target: for every nonzero integer mode and TT polarization, the continuum symbol equals the scale-explicit face $(-1/8)\cdot|E|_F^2$. Pure-gauge vanishing is tracked separately in the packaged closer.
Prior repair paths (distinct-hinge fold, full two-jet, mean-local Path B, density dictionary) already fix the candidate face at $-1/16$ with dictionary survivor $1$, which differs from frozen EH $-1/4$. The residual is therefore Schläfli elevation itself, not another incidence rescale.
proof idea
Definitional packaging only. The body is the propositional conjunction of the two upstream open targets Regge4DSchlafliElevationToCandidate and Regge4DContinuumEHTarget. No tactics, no lemmas applied, no witness constructed.
why it matters
Names the residual gap that blocks 4D Regge recovery of Einstein-Hilbert on the flat second variation. Module tier tags mark elevation and the continuum EH target as OPEN, while the candidate reduced Hessian, its Bloch face $-1/16$ on Frobenius-normalized axis TT, and the mismatch with frozen EH $-1/4$ are already THEOREM. Closing this packaged claim would be the missing step that makes the nonlinear $S''(0)$ land on the candidate whose continuum face could then be compared to EH.
Downstream use is currently empty; the declaration is a status flag rather than a lemma consumed by a parent theorem. It does not flip gap-action recovery and does not inhabit the 4D RS-converges-to-EH statement. Framework-wise it sits in the gravity analysis chain that must eventually match continuum GR structure before RS mass and coupling claims can rest on a discrete geometric action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.