exactJSecondDiff_independent_of_amplitude
plain-language theorem explainer
For any fixed Recognition Freudenthal 4-mesh, integer mode, and polarization matrix, the amplitude second central difference of the exact-J mesh action is the same at every nonzero amplitude. Gravity continuum auditors cite this to treat the action as purely quadratic in amplitude. The proof is a two-line rewrite through the identity that equates that second difference to the mesh true-Regge Hessian.
Claim. Let $M$ be a Recognition Freudenthal 4-mesh, $m$ an integer 4-mode, and $E$ a $4\times 4$ polarization matrix. For all real amplitudes $\varepsilon_1,\varepsilon_2\neq 0$, the second central difference of the exact-$J$ action on $M$ at amplitude $\varepsilon_1$ equals the same second difference at $\varepsilon_2$.
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.
RecognitionFreudenthalMesh4D packages continuum index $j$ (side $j+3$); the exact flat cross-term Hessian on this carrier is the concrete edge-class geometry. The second central difference exactJSecondDiff is $(S(\varepsilon)-2S(0)+S(-\varepsilon))/\varepsilon^2$ for the exact-$J$ action on the mesh. Upstream, exactJSecondDiff_eq_meshHessian states that for every $\varepsilon\neq 0$ this second difference equals the mesh true-Regge quadratic Hessian exactly (pure quadratic action).
Preferred limit shape in the module is amplitude Hessian at fixed mesh, then $N\to\infty$. The binding is MODEL-level Regge identification: elevating the Hessian to the literal nonlinear Regge action via Schläfli remains open.
proof idea
One short tactic proof. Rewrite the left-hand side by exactJSecondDiff_eq_meshHessian at $\varepsilon_1\neq 0$, and the right-hand side by the same theorem at $\varepsilon_2\neq 0$. Both sides become the mesh true-Regge quadratic Hessian, which does not depend on amplitude, so they agree. No further algebra is needed.
why it matters
Doc-comment: the action is quadratic (not a definitional zero shell); its amplitude second difference is independent of $\varepsilon$ for $\varepsilon\neq 0$. That is the value-level certificate that the Recognition mesh exact-$J$ action is purely quadratic in amplitude, so the amplitude Hessian is well-defined and constant off zero.
It underwrites the module THEOREM that the amplitude Hessian exists and equals the mesh true-Regge Hessian by construction, and feeds the preferred continuum path (fixed-mesh amplitude Hessian, then $N\to\infty$ toward the Option-C EH face). No downstream users are wired yet in the graph; the lemma is a local bridge fact inside the Recognition-mesh exact-$J$ package. It does not flip gap_action_recovery or inhabit S_RS_converges_EH_4d, and it does not close the open Schläfli lift from Hessian to full nonlinear Regge action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.