schlaefliCandidateZeroMom
plain-language theorem explainer
Names the zero-momentum Schläfli candidate Hessian on a 4×4 edge matrix as the already-assembled true-weight quadratic (orbit-count × Heron × star-deficit). Gravity analysts cite it when comparing the reduced flat second variation to continuum Einstein–Hilbert faces. The body is a pure alias of the committed geometry kernel.
Claim. For a $4\times 4$ real edge matrix $H$, the zero-momentum Schläfli candidate is the scalar quadratic form already built from the true-weight zero-momentum kernels (orbit counts, Heron factors, and star-deficit class weights).
background
This module tracks Gate A2 for 4D Regge calculus on a flat seed: elevating the nonlinear edge-length Regge action to a Schläfli-reduced edge Hessian, mirroring the closed 3D contract. Flat Freudenthal 4-simplex Schläfli identities and directional kills are already theorems pathwise; full off-flat pathwise Schläfli and therefore nonlinear elevation remain open.
Mat4 is the local alias for the preflight $4\times 4$ edge matrix type. The true-weight zero-momentum quadratic packages orbit-count, Heron, and star-deficit geometry into a single real quadratic form on that matrix. Upstream, SchlafliElevationToDistinctHingeOpen records the open claim that some independent nonlinear second variation $S''$ matches the canonical finite Hessian after the density weight $(2/N^4)$ factor.
The candidate defined here is the zero-momentum face of that geometry object, not yet identified with $S''(0)$ from the nonlinear action.
proof idea
Definitional one-line alias: the candidate is definitionally equal to trueWeightZeroMomQuadratic applied to the same matrix. No tactics or lemmas; the equality theorem later is just rfl.
why it matters
Gives a stable name for the reduced Hessian candidate that the module’s THEOREM tier identifies with assembled / distinct-hinge geometry. Downstream, it is shown to vanish on the Frobenius-normalized axis TT-plus mode and on the decoy gauge mode, and the definitional equality lemma pins the name to the kernel. That vanishing feeds the continuum-face comparison (symbolDir face $-1/16$ versus frozen EH $-1/4$) while the residual gap stays Schläfli elevation of the nonlinear action, not another incidence rescale. It does not close SchlafliElevationToDistinctHingeOpen, flip gap_action_recovery, or inhabit $S_{\mathrm{RS}}\to\mathrm{EH}$ in 4D. Framework-wise this sits in the gravity analysis stack under the forced $D=3$ spatial setting, but the declaration itself is pure 4D Regge bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.