exactJActionOnMesh_at_zero
plain-language theorem explainer
The exact-J mesh action vanishes at zero amplitude for every Recognition Freudenthal 4-mesh, integer mode, and edge-class matrix. Anyone checking the quadratic Hessian or continuum amplitude expansion of the Option-C midpoint Bloch bridge will cite this. The proof unfolds the homogeneous degree-two definition and closes by ring.
Claim. For every Recognition Freudenthal 4-mesh $M$, integer torus mode $m$, and $4\times 4$ edge-class matrix $E$, the exact-$J$ mesh action at amplitude zero satisfies $S_{J}(M,m,E;0)=0$.
background
This module sits in the QG full-theory campaign at the Recognition gate of the 4D continuum closure. It builds a canonical Recognition mesh carrier on the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol on that torus family.
The exact-$J$ action on the mesh is defined, as a MODEL identification, by $$S_J(M,m,E;\varepsilon)=\tfrac12\varepsilon^2,H_{\mathrm{mesh}}(M,m,E),$$ where $H_{\mathrm{mesh}}$ is the true-weight Regge quadratic Hessian on the edge-class perturbation $\varepsilon\cdot E$. It is homogeneous of degree two in the fold amplitude; Schläfli elevation of that Hessian to the literal nonlinear Regge action remains open.
$M$ records only a continuum index $j$ (torus side $j+3$). The mode $m$ is an integer wave vector on the side-$N$ torus, and $E$ is the preflight $4\times 4$ matrix of edge-class data. The preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$.
proof idea
One-line algebraic check. Unfold the definition of the exact-$J$ mesh action to $\tfrac12\varepsilon^2 H_{\mathrm{mesh}}(M,m,E)$, substitute $\varepsilon=0$, and finish with ring. No mesh geometry, mode arithmetic, or Hessian identities are needed beyond the homogeneous quadratic form of the definition.
why it matters
Zero-amplitude vanishing is the base point of the amplitude expansion that feeds the Option-C midpoint Bloch bridge. The module's binding honesty records that the amplitude Hessian equals the mesh true-Regge Hessian by construction, and that iterated $N\to\infty$ Tendsto closes at the scale-explicit Option-C Einstein-Hilbert face. This lemma is the trivial but mandatory $\varepsilon=0$ anchor for that Hessian story: without $S_J(\varepsilon=0)=0$, the quadratic response and continuum limit statements would sit on a shifted action.
It does not flip gap_action_recovery and does not inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence theorem. No downstream consumers are wired yet in the graph; the declaration is local hygiene inside the Recognition-mesh exact-$J$ bridge, clearing the zero section before second-difference and Hessian equalities are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.