exactJSecondDiff
plain-language theorem explainer
Defines the second central difference in amplitude of the exact-J mesh action on a Recognition Freudenthal 4-torus carrier. Gravity continuum-closure work cites it as the discrete amplitude Hessian whose ε→0 limit is the true-Regge quadratic form. The body is the standard three-point stencil (S(ε)−2S(0)+S(−ε))/ε² applied to the quadratic exact-J action.
Claim. For a Recognition Freudenthal mesh $M$, integer mode $m$, edge-class matrix $E$, and amplitude $\varepsilon\in\mathbb{R}$, the amplitude second central difference is $$\Delta_2 S(M,m,E;\varepsilon)=\frac{S(M,m,E;\varepsilon)-2S(M,m,E;0)+S(M,m,E;-\varepsilon)}{\varepsilon^2},$$ where $S$ is the exact-$J$ action on the mesh (modelled as the true-weight Regge quadratic Hessian at fold $\varepsilon\cdot E$).
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. Preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$.
RecognitionFreudenthalMesh4D packages a continuum index $j$ (torus side $j+3$). The exact-$J$ action on the mesh is defined as $S=\frac12\varepsilon^2$ times the mesh true-Regge quadratic Hessian on the edge-class perturbation $\varepsilon\cdot E$; it is homogeneous of degree two in the fold, not an arbitrary pullback substitute. Schläfli elevation of that Hessian to the full nonlinear Regge action remains open.
The second central difference is the classical finite-difference probe of that quadratic tangent. Downstream, its $\varepsilon\to 0$ filter limit is the existence predicate for the amplitude Hessian.
proof idea
Pure definition: the three-point central second difference of exactJActionOnMesh in the amplitude argument, divided by $\varepsilon^2$. No lemmas are applied at the definition site. Algebraic content appears only downstream, where unfolding against the quadratic model $S=\frac12\varepsilon^2 H$ cancels to $H$ for $\varepsilon\neq 0$.
why it matters
This is the discrete amplitude Hessian object that the Recognition mesh bridge equates to true-Regge geometry. It feeds four in-module results: equality with the mesh true-Regge Hessian for $\varepsilon\neq 0$; independence of amplitude (quadraticity); the existence predicate ExactJAmplitudeHessianExists (Tendsto as $\varepsilon\to 0$ away from zero); and the theorem that the amplitude Hessian exists and equals the mesh Hessian.
In the module's binding honesty, that equality is the proved claim ExactJEqualsTrueReggeHessian by construction. The iterated $N\to\infty$ continuum face to the scale-explicit Option-C Einstein-Hilbert symbol composes on top of this Hessian match. The definition does not itself flip gap-action recovery or inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D convergence statement; those remain separate open gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.