schlaefliCandidate_vanishes_on_axisTTPlus
plain-language theorem explainer
The zero-momentum Schläfli candidate Hessian vanishes on the unnormalized plus TT polarization diag(0,0,1,−1). Gravity analysts working the 4D Regge flat second-variation gate cite this as a sanity check on the assembled true-weight quadratic. The proof is a one-line wrapper of the already-proved vanishing of that quadratic on the same axis.
Claim. The zero-momentum Schläfli candidate quadratic form evaluates to $0$ on the unnormalized plus transverse-traceless polarization $\mathrm{diag}(0,0,1,-1)$.
background
This module tracks Gate A2 for 4D Regge calculus: elevating the true nonlinear Regge action to a Schläfli-reduced edge Hessian. In 3D that elevation is closed; in 4D the flat-seed Freudenthal Schläfli identities and directional kills are theorems, but the full off-flat pathwise closed form (and therefore nonlinear elevation) remains open.
The zero-momentum candidate is the orbit-count × Heron × star-deficit class quadratic assembled from committed geometry kernels; by definition it is exactly the true-weight zero-momentum quadratic. The plus TT axis is the unnormalized matrix $\mathrm{diag}(0,0,1,-1)$ from the edge TT decomposition. Upstream, that true-weight quadratic is already known to vanish on this axis by summing orbit quadratics whose deficits are zero against the axis.
proof idea
One-line wrapper. The candidate is definitionally the true-weight zero-momentum quadratic, so the claim reduces to the upstream theorem that this quadratic vanishes on the plus TT axis. That upstream proof unfolds the quadratic and applies a Finset sum-to-zero via orbit deficits dotted into the axis being zero.
why it matters
Places a concrete vanishing fact on the THEOREM tier of the 4D flat second-variation status board: the candidate reduced Hessian is identified with the assembled geometry object and is zero on the plus TT axis at zero momentum. Downstream use is not yet wired in this graph (no used_by edges), but the module frames such vanishings as part of the candidate face analysis (Bloch continuum face on Frobenius-normalized axis TT, comparison to frozen EH).
It does not close the residual gap named in the module doc: full off-flat Freudenthal pathwise Schläfli and therefore elevation of the nonlinear action $S''(0)$ to the candidate. It also does not flip gap_action_recovery or inhabit continuum EH convergence. In the broader RS gravity stack this is bookkeeping on the Regge side of the continuum limit, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.