recognitionExactJConvergesEH_of_normalized_mesh
plain-language theorem explainer
If the normalized true-Regge Hessian on the canonical Recognition mesh tends to the scale-explicit Einstein–Hilbert face on TT modes, the iterated continuum Prop for exact-J holds. Gravity continuum-closure work cites this to separate the algebraic/transported limit from the packaging of the Recognition gate. The proof is a short existential packaging: witness the amplitude Hessian by the mesh true-Regge Hessian and apply the given Tendsto hypothesis.
Claim. Assume that for every nonzero integer 4-mode $m$ and every TT matrix $E$ (symmetric, traceless, transverse to $m$), the ratio of the mesh true-Regge quadratic Hessian on the canonical Recognition mesh of side index $j$ to the squared momentum norm on the corresponding torus tends, as $j\to\infty$, to the scale-explicit continuum EH face of $E$. Then the Recognition exact-$J$ continuum statement holds: for each such $m,E$ there is a sequence $H_j$ equal to the exact-$J$ amplitude Hessian on that mesh with $H_j/|k|^2\to$ the same EH face.
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 the geometric Option-C midpoint Bloch symbol on that torus family. Preferred limit shape: amplitude Hessian at fixed mesh, then mesh side $N\to\infty$.
IsTT means algebraic TT: symmetric, Euclidean-traceless, and transverse to the mode. The canonical Recognition mesh is the standard family indexed by $j\in\mathbb{N}$. The target Prop RecognitionExactJConvergesEH asks, for each nonzero mode and TT matrix, for a sequence $H_j$ that is the exact-$J$ amplitude Hessian on mesh $j$ and whose $|k|^2$-normalized values tend to the scale-explicit Option-C EH face.
Binding honesty from the module: elevating the Hessian to the literal nonlinear Regge action via Schläfli remains open; the module does not consume amplitude-scaling refinement families as continuum premises, and it does not flip gap-action recovery or inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D statement.
proof idea
Term-mode packaging of an existential. Introduce mode $m$ and matrix $E$ with $m\neq 0$ and TT. Witness the required sequence by $H_j :=$ mesh true-Regge quadratic Hessian of the canonical Recognition mesh at $j$, evaluated on $(m,E)$.
The first conjunct (exact-$J$ amplitude Hessian exists and equals $H_j$) is discharged pointwise by exactJAmplitudeHessian_eq_mesh. The second conjunct (normalized Tendsto to the scale-explicit EH face) is exactly the hypothesis hlim applied to $m,E$. No further continuum analysis occurs in this lemma.
why it matters
This is the honest dependence cut for the Recognition iterated continuum Prop. The doc-comment is explicit: inhabit the hypothesis only when the algebraic/transported closer proves the normalized midpoint moment equals the Option-C face, rather than baking EH into the action definition.
In the QG full-theory campaign it sits at the Recognition gate of 4D continuum closure. Upstream infrastructure (edge TT decomposition, exact flat Hessian Bloch symbols, torus bridges, midpoint $m^2$ TT identities) supplies the geometric content that would discharge hlim. The module already records the companion theorems that amplitude Hessian equals mesh true-Regge Hessian by construction and that the iterated limit closes once the discrete torus bridge and midpoint faces are composed.
No downstream users are wired yet (used_by empty). It does not close gap-action recovery or the full RS-to-EH 4D convergence statement; those remain separate open gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.