exactJActionOnMesh_eq
plain-language theorem explainer
On a Recognition Freudenthal 4-mesh, the exact-J action at amplitude ε equals (1/2)ε² times the mesh true-Regge quadratic Hessian (Option-C midpoint Bloch symbol). Continuum-closure and Regge-bridge arguments cite this as the value-level identification. Proof is definitional reflexivity: the action is defined to be that quadratic form.
Claim. For every Recognition Freudenthal mesh $M$ (continuum index $j$, side $j+3$), integer mode $m\in\mathbb{Z}^{4}$, polarization $E\in\mathrm{Mat}_{4}(\mathbb{R})$, and amplitude $\varepsilon\in\mathbb{R}$, the exact-$J$ action on the mesh equals $\tfrac12\varepsilon^{2}$ times the geometry-derived Option-C midpoint Bloch Hessian of $E$ evaluated on the mesh wave of $m$.
background
This module is the Recognition gate of the 4D continuum-closure campaign. 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.
RecognitionFreudenthalMesh4D packages a continuum index $j$ (side $j+3$) and projects to the canonical Freudenthal torus. Integer modes IntMode4 are commensurate wave vectors $m:\mathrm{Fin},4\to\mathbb{Z}$. The mesh true-Regge quadratic Hessian is the assembled flat midpoint Bloch symbol of polarization $E$ on the mesh wave of $m$; the module marks it as MODEL relative to full nonlinear Regge (Schläfli elevation still open for some orbits).
The exact-J action is defined, not derived, as the homogeneous degree-two fold $\tfrac12\varepsilon^{2}$ times that Hessian. Preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$. Arbitrary test-variation pullbacks are excluded by preflight.
proof idea
One-line definitional equality via rfl. The left-hand side unfolds to the body of exactJActionOnMesh, which is literally $\tfrac12\varepsilon^{2}$ times meshTrueReggeQuadraticHessian M m E. No lemmas or algebraic rewriting are required.
why it matters
Pins the value-level MODEL identification that the module advertises as theorem-shaped: the amplitude Hessian of the exact-J mesh action equals the mesh true-Regge Hessian by construction. Downstream continuum arguments (iterated $N\to\infty$ Tendsto to the scale-explicit Option-C Einstein-Hilbert face) rely on this equality as the starting identification before composing discrete torus bridges with exact midpoint $m^{2}$ TT and gauge faces.
It does not elevate the Hessian to the literal nonlinear Regge action via Schläfli (still open), does not consume the Exact-J refinement family limit as a continuum premise, does not flip gap_action_recovery, and does not inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D convergence statement. In the broader RS forcing picture it is local gravity/continuum scaffolding, not a T0-T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.