RecognitionExactJConvergesEH
plain-language theorem explainer
Packages the iterated continuum target for Recognition gravity on the 4-torus: nonzero integer modes and TT faces admit amplitude Hessians on the canonical Recognition mesh family whose |k|²-normalized values tend to the scale-explicit Option-C Einstein-Hilbert face. Continuum-closure and bridge authors cite it as the Prop discharged by the closed midpoint sequence. It is a propositional definition, not a proved theorem.
Claim. For every nonzero integer 4-mode $m$ and every transverse-traceless matrix $E$, there exists a sequence $H:\mathbb{N}\to\mathbb{R}$ such that each $H(j)$ is an exact-$J$ amplitude Hessian of the canonical Recognition mesh of side $j$ at $(m,E)$, and $H(j)/|k_m|^2$ tends, as $j\to\infty$, to the scale-explicit continuum Einstein-Hilbert face of $E$.
background
The 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 exact-$J$ action whose amplitude Hessian is identified with the geometric Option-C midpoint Bloch symbol on that torus family.
Preferred limit shape is iterated: form the amplitude Hessian at fixed mesh side, then send side $N\to\infty$. The continuum target after $|k|^2$ normalization is the scale-explicit Option-C EH face of the TT matrix $E$. The TT predicate selects transverse-traceless faces; pure-gauge faces are handled by a companion vanishing Prop.
Binding honesty in the module: elevating the Hessian to the literal nonlinear Regge action via Schläfli remains open; the construction does not consume amplitude-scaling refinement families as continuum premises, and arbitrary test-variation pullbacks are excluded by preflight.
proof idea
Propositional definition only: the body is the universal quantification over nonzero integer modes and TT faces, asserting existence of a real sequence $H_j$ that is an exact-$J$ amplitude Hessian on each canonical Recognition mesh and whose momentum-normalized values Tendsto the scale-explicit continuum EH face at infinity. No tactics or lemmas are applied here; discharge is deferred to the closed and of-normalized-mesh inhabitants in the same module.
why it matters
Names the Recognition half of the 4D continuum EH target that the module's THEOREM line claims closes by composing the discrete torus bridge with the exact midpoint $m^2$ TT and gauge faces. Downstream, recognitionExactJConvergesEH_closed inhabits it by feeding the mesh true-Regge quadratic Hessian sequence, and recognitionExactJConvergesEH_of_normalized_mesh factors the honest dependence on the algebraic/transported closer (Tendsto of the normalized midpoint moment to the Option-C face, without baking EH into the action). The gauge companion uses the same mesh family for vanishing on pure-gauge faces.
In the broader RS gravity stack this is the value-level bridge from exact-$J$ Recognition cost structure toward continuum Einstein-Hilbert response on the 4-torus. It does not flip gap-action recovery and does not inhabit the full $S_{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.