exactJActionOnMesh
plain-language theorem explainer
Exact-J action on a Recognition Freudenthal mesh at amplitude ε equals half ε squared times the true-weight Regge quadratic Hessian on the same edge-class mode. Continuum-closure and Option-C Bloch bridge arguments cite this as the value-level MODEL binding exact-J to mesh geometry. The body is a direct homogeneous quadratic identification, not a test-variation pullback; Schläfli elevation of the Hessian remains open.
Claim. For a Recognition-native Freudenthal mesh $M$ (continuum index recording the 4-torus family), integer mode $m$, edge-class polarization $E\in\mathrm{Mat}_4$, and amplitude $\varepsilon\in\mathbb{R}$, the exact-$J$ mesh action is $S(M,m,E,\varepsilon)=\frac12\varepsilon^2\,H_{\mathrm{mesh}}(M,m,E)$, where $H_{\mathrm{mesh}}$ is the geometry-derived Option-C midpoint Bloch symbol (true-weight Regge quadratic Hessian) 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 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 carrier RecognitionFreudenthalMesh4D stores only a continuum index $j$ (torus side $j+3$); its exact flat cross-term Hessian is the concrete edge-class geometry. Integer modes IntMode4 are commensurate wave vectors $m:\mathrm{Fin},4\to\mathbb{Z}$ on the side-$N$ torus. Polarizations are preflight $4\times 4$ matrices.
Upstream, the mesh true-Regge quadratic Hessian is defined as the exact midpoint Bloch symbol of $E$ on the mesh wave of $m$: the assembled flat midpoint Hessian, still MODEL relative to fully nonlinear Regge (Schläfli elevation not closed for every orbit). The preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$.
proof idea
Definitional one-liner, not a proved theorem. The body sets the action equal to $\frac12\varepsilon^2$ times the already-assembled mesh true-Regge quadratic Hessian on $(M,m,E)$. No tactics, no lemmas applied at this site; the identification is the MODEL stated in the module binding notes (exact midpoint Bloch on edge classes at amplitude $\varepsilon$, homogeneous of degree two).
why it matters
Anchors the value-level exact-J side of the Recognition mesh bridge. Downstream, the equality-to-Hessian unfolds by rfl; vanishing at $\varepsilon=0$ is immediate by ring; the second central difference in amplitude is defined from this action; and for $\varepsilon\neq 0$ that second difference equals the mesh true-Regge Hessian exactly (pure quadratic action), which is the theorem ExactJEqualsTrueReggeHessian promised in the module doc.
That Hessian identity is the fixed-mesh step before the iterated $N\to\infty$ Tendsto that targets the scale-explicit Option-C continuum face. Binding honesty: Schläfli elevation of the Hessian to the literal nonlinear Regge action remains OPEN; the module does not consume amplitude-scaling refinement families as continuum premises, excludes arbitrary test-variation pullbacks, and does not flip gap_action_recovery or inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D convergence statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.