recognitionExactJConvergesEH_closed
plain-language theorem explainer
For every nonzero integer 4-mode and TT edge polarization, the Recognition mesh amplitude Hessians exist and, after momentum-norm normalization, tend as mesh side N→∞ to the scale-explicit Option-C Einstein–Hilbert face. Gravity continuum-closure arguments cite this as the value-level Recognition gate. The proof builds the Hessian sequence from the mesh true-Regge symbol, then composes the discrete torus bridge with the exact midpoint m² TT identity.
Claim. For every nonzero integer mode $m\in\mathbb{Z}^4$ and every $4\times 4$ edge matrix $E$ that is transverse-traceless relative to the real wave $k_i=m_i$, there exists a sequence $H:\mathbb{N}\to\mathbb{R}$ such that each $H(j)$ is the exact-$J$ amplitude Hessian on the canonical Recognition Freudenthal mesh of side $j$, and $H(j)/|k|_{N_j}^2$ tends (as $j\to\infty$) to the scale-explicit Option-C continuum EH face of $E$.
background
This module is the Recognition gate of the 4D continuum-closure campaign. It builds a canonical mesh carrier on the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is identified with the geometric Option-C midpoint Bloch symbol on that torus family.
The target proposition RecognitionExactJConvergesEH asks: for each mesh, take the amplitude Hessian, then send mesh side $N\to\infty$ to the scale-explicit Option-C EH face after $|k|^2$ normalization. The mesh true-Regge quadratic Hessian is the geometry-derived Option-C midpoint Bloch symbol on the Freudenthal mesh (model relative to fully nonlinear Regge: assembled flat midpoint Hessian, not yet Schläfli-elevated on every orbit).
Upstream, the amplitude Hessian is already known to exist and equal that mesh Hessian by construction. The discrete torus family bridge and the exact midpoint $m^2$ TT identity (Rayleigh quotient equals $-\tfrac18$ times Frobenius norm squared of $E$) supply the continuum face after preflight norm identifications.
proof idea
Tactic proof of the proposition. Fix nonzero mode $m$ and TT polarization $E$. Define the Hessian sequence by evaluating the mesh true-Regge quadratic Hessian on the canonical Recognition mesh of index $j$.
Existence of each exact-$J$ amplitude Hessian is immediate from the sibling theorem that the amplitude Hessian equals the mesh true-Regge Hessian.
For the Tendsto clause: set $k$ to the real wave of $m$. Invoke the discrete torus family bridge, nonvanishing of the integer-mode wave norm, and the exact midpoint Bloch $m^2$ identity equating the Rayleigh quotient to $-\tfrac18,|E|_F^2,|k|^2$. Transport Frobenius and wave norms across the preflight/identity modules by definitional equality, cancel $|k|^2$ by field simplification, and match the continuum EH scale-explicit face. Rewrite the bridge conclusion under the mesh/wave unfoldings to finish.
why it matters
Closes the Recognition-gate continuum statement advertised in the module: iterated $N\to\infty$ Tendsto lands on the scale-explicit Option-C face. Together with the already-proved amplitude-Hessian-equals-mesh-true-Regge theorem, this is the value-level bridge from the Recognition mesh exact-$J$ construction to the geometric EH face used in the 4D Regge continuum program.
No downstream consumers are wired yet (used_by empty); the declaration is the terminal closure of this bridge module. Binding honesty from the module doc still applies: elevating the Hessian to the literal nonlinear Regge action via Schläfli remains open; the module does not consume the Exact-$J$ refinement family limit, does not flip gap-action recovery, and does not inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D convergence package. In the broader RS forcing picture this is continuum gravity analysis on the Recognition mesh, not a T0–T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.