Regge4DSchlafliElevationToCandidate
plain-language theorem explainer
Open Schläfli-elevation obligation for 4D flat Regge: existence of a nonlinear second-variation functional S'' derived from the edge-length action by pathwise Schläfli reduction, matching the candidate fold on every non-aliased torus mode. Cited by anyone tracking Gate A2 and the 4D continuum limit of Regge gravity. Pure Prop definition packaging that existence claim; no proof attached.
Claim. There exists a nonlinear flat second-variation functional $S''$ such that for every lattice size $N\ge 1$, integer mode $m\in\mathbb{Z}^4$, and edge perturbation $E\in M_4(\mathbb{R})$, if $m$ is non-aliased (some $i$ with $N\nmid 2m_i$), then the density-weighted second difference equals the Schläfli candidate fold: $w(N)\,S''(N,m,E)=\mathrm{SchläfliCandidateFold}(E,\,2\pi m/N)$, where $w(N)=2/N^4$.
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 (trueReggeAction_secondVariation_flat_schlaefli). In 4D the flat-seed Freudenthal closed form, flat directional Schläfli kill, and seed-angle differentiability are theorems in Regge4DSchlaefliPathwise; the full off-flat pathwise closed form is still missing, so nonlinear elevation stays open.
Modes live on the side-$N$ torus: an integer wave vector $m\in\mathbb{Z}^4$ maps to the real covector $k=2\pi m/N$. Non-aliased modes are those with some component not divisible by $N/\gcd(2,N)$ in the stated sense. The right-hand side is the already-identified candidate reduced Hessian (distinct-hinge / assembled geometry object) evaluated on that covector. The left-hand side is a density-weighted second difference of an independent nonlinear $S''$ of type NonlinearFlatSecondVariation4D.
Prior repair paths (distinct-hinge fold, full two-jet, mean-local Path B, density dictionary) do not close the gap: the residual is Schläfli elevation of the nonlinear action, not another incidence rescale.
proof idea
Definition only: the body is the raw existence Prop, not a proved theorem. No tactics, no lemmas applied. Downstream aliases (Regge4DSchlafliFiniteMomentumOpen, Regge4DSchlafliBridgeOpen, Regge4DSchlafliSecondVariation) are one-line renames of this same Prop. Closing it would require constructing $S''$ from the nonlinear edge-length Regge action via a full off-flat Freudenthal4SimplexPathwiseSchlaefli identity, then verifying the density-weighted match on non-aliased modes.
why it matters
This is the live Gate A2 residual in 4D Regge analysis. Module doc is explicit: elevation of the nonlinear action stays OPEN because full off-flat pathwise Schläfli is absent. Downstream, elevation_iff_torus_open equates it with the torus-limit elevation Prop; bridge and finite-momentum aliases re-export it; Regge4DSchlafliSecondVariation retires an old tautology in favor of this obligation.
Packaged with the continuum EH target as SchlaefliElevationToCandidateClosesEH. Even if elevation held, the candidate continuum face on Frobenius-normalized axis TT at symbolDir is $-1/16$, while the Einstein-Hilbert TT coefficient is $-1/4$ (schlaefli_elevation_to_candidate_misses_eh_face). So elevation alone does not restore EH. Module flags: does not flip gap_action_recovery; does not inhabit S_RS_converges_EH_4d. Framework role is honesty bookkeeping on the discrete-to-continuum gravity chain, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.