exactJSecondDiff_eq_meshHessian
plain-language theorem explainer
For nonzero amplitude ε, the second finite difference of the exact-J mesh action equals the mesh true-Regge quadratic Hessian on a Recognition Freudenthal 4-mesh. Continuum-closure and Option-C bridge arguments cite this to treat the amplitude Hessian as pure quadratic Regge geometry. The proof unfolds the second-difference and action definitions, then cancels by field simplification and ring.
Claim. Let $M$ be a Recognition-native Freudenthal 4-mesh, $m$ an integer Bloch mode, $E$ a $4\times 4$ edge-class matrix, and $\varepsilon\in\mathbb{R}$ with $\varepsilon\neq 0$. Then the amplitude second difference of the exact midpoint-$J$ action on the mesh equals the mesh true-Regge quadratic Hessian: $\Delta^2_\varepsilon S_J(M,m,E;\varepsilon)=H_{\mathrm{Regge}}^{\mathrm{mesh}}(M,m,E)$.
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 meant to match the geometric Option-C midpoint Bloch symbol on the same torus family.
A RecognitionFreudenthalMesh4D is mesh data indexed by a continuum level $j$ (side length $j+3$); it records the torus family and carries the exact flat cross-term Hessian as concrete edge-class geometry. The exact-$J$ action on the mesh is defined as the exact midpoint Bloch symbol on edge classes at amplitude $\varepsilon$ (the geometric Option-C continuum object). The amplitude second difference is the usual second finite difference of that action in $\varepsilon$; the mesh true-Regge quadratic Hessian is the pure quadratic form assembled from that edge-class geometry.
Binding honesty in the module: elevating the Hessian to the literal nonlinear Regge action via Schläfli remains open; the preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$.
proof idea
Term-mode algebraic identity, not a deep geometric argument. Unfold the second-difference definition and the exact-$J$ action-on-mesh definition so both sides are explicit rational expressions in $\varepsilon$. From $\varepsilon\neq 0$ obtain $\varepsilon^2\neq 0$ via pow_ne_zero. Clear denominators with field_simp, then finish by ring. The equality is therefore definitional once the quadratic scaling in amplitude is written out: the second difference extracts exactly the mesh true-Regge quadratic Hessian and drops all higher-order shells.
why it matters
This is the local algebraic hinge that makes the amplitude Hessian exist and equal the mesh true-Regge Hessian (exactJAmplitudeHessian_eq_mesh). The same identity immediately yields amplitude-independence of the second difference for any two nonzero $\varepsilon$ values (exactJSecondDiff_independent_of_amplitude), confirming the action is genuinely quadratic rather than a definitional zero shell.
In the Recognition framework this lands the value-level bridge from exact-$J$ on the Recognition mesh to the Option-C midpoint Bloch symbol on the Freudenthal 4-torus family. Downstream continuum work composes the discrete torus bridge with exact midpoint $m^2$ TT and gauge faces to obtain the scale-explicit Einstein-Hilbert face under $N\to\infty$. It does not flip gap-action recovery and does not inhabit the full $S_{RS}\to EH$ 4D convergence statement; Schläfli elevation of the Hessian to nonlinear Regge remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.