schlaefliCandidateFold
plain-language theorem explainer
Names the finite-momentum Schläfli candidate: the distinct-hinge (weight $1/r_\tau$) transported Bloch fold of true-weight kernels on a $4\times 4$ edge matrix at mode $m$. Gravity analysts cite it as the RHS that a nonlinear flat second variation $S''$ should match after 3D-style Schläfli elevation plus cell-sum dictionary. Pure one-line alias of the distinct-hinge Bloch fold.
Claim. For a $4\times 4$ real matrix $H$ and momentum $m\in\mathbb{R}^4$, define the Schläfli candidate fold as the distinct-hinge continuum Bloch fold of $H$ at $m$: sum over hinge-orbit types of $(1/r_\tau)$ times the orbit Bloch fold (true-weight kernels, not bare or fitted $2/r$).
background
This module tracks 4D Regge flat second variation under the Schläfli-elevation contract that closed in 3D. Gate A2 asks to elevate the true nonlinear Regge action to a Schläfli-reduced edge Hessian. Flat-seed Freudenthal Schläfli identities and directional kills are already theorems; the full off-flat pathwise closed form is still missing, so elevation of the nonlinear action remains open.
Mat4 is the local preflight alias for the $4\times 4$ edge Hessian. The upstream distinct-hinge fold blochFoldAllDistinctHinge is the continuum object that "true hinge sum wants: distinct hinges with full-star deficit, i.e. weight $1/r_\tau$ on each orbit fold. Not bare blochFoldAll, and not fitted $2/r$." That is the geometric RHS this definition packages for the elevation dictionary.
proof idea
One-line definitional alias: the candidate is definitionally equal to the distinct-hinge transported Bloch fold of $H$ at $m$. No algebraic work; the companion rfl lemma records the equality.
why it matters
This is the concrete geometric object on the right-hand side of the open elevation Prop: existence of an independent nonlinear $S''$ such that $(2/N^4)\cdot S''(N,m,E)$ equals the candidate fold at the real mode, for every non-aliased mode. Downstream, Regge4DSchlafliElevationToCandidate is exactly that Prop; elevation_iff_torus_open equates it to the torus-limit elevation statement; NonlinearFlatSecondVariation4D is the independent $S''$ type. Module tier tags mark elevation OPEN and stress that residual gap is Schläfli elevation of the nonlinear action, not another incidence rescale. Does not flip gap-action recovery or inhabit continuum EH convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.