recognitionExactJConvergesGaugeZero_closed
plain-language theorem explainer
On the canonical Recognition mesh of the periodic Freudenthal 4-torus, the normalized true-Regge quadratic Hessian of any pure-gauge edge variation tends to zero under mesh refinement. Gravity continuum-limit arguments cite this as the gauge face of the exact-J midpoint sequence. The proof feeds the discrete torus bridge a pure-gauge family and cancels the Rayleigh quotient by the exact midpoint m² TT gauge identity.
Claim. For every nonzero integer 4-mode $m$ and every wave $v$, the sequence sending mesh level $j$ to the true-Regge quadratic Hessian of the canonical Recognition mesh at mode $m$ on the pure-gauge family generated by $m$ and $v$, divided by the momentum norm squared on the torus of side $j$, tends to $0$ as $j\to\infty$.
background
This module sits in the QG full-theory campaign at the Recognition gate of 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 the geometric Option-C midpoint Bloch symbol on the same torus family.
The claim is the gauge-zero companion of the Recognition mesh midpoint sequence: pure-gauge faces must contribute nothing in the continuum limit. The pure-gauge family is the edge variation generated by an integer mode $m$ and a free wave $v$. The mesh true-Regge quadratic Hessian is the Hessian of the exact midpoint Bloch symbol on edge classes (MODEL identification with Option-C continuum geometry). Preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$.
Upstream, the discrete torus family bridge relates mesh Hessians to exact midpoint Bloch $m^2$ Rayleigh quotients, and the exact midpoint $m^2$ TT identity supplies the gauge-rayleigh vanishing used here.
proof idea
Tactic proof. Fix nonzero mode $m$ and wave $v$. Instantiate the pure-gauge edge matrix $E$ and the integer wave $k$ from $m$. Invoke the discrete torus family bridge on $(m,E)$. Nonvanishing of the wave norm of $k$ (and its preflight identity twin) licenses the exact midpoint Bloch $m^2$ gauge-rayleigh identity, which forces the normalized midpoint symbol on $E$ to vanish. Rewrite the bridge conclusion under the mesh Hessian, mesh wave, side, and canonical-mesh unfoldings to obtain the Tendsto-to-zero statement.
why it matters
Closes the pure-gauge face of the Recognition exact-J midpoint sequence on the 4-torus mesh. Together with the TT / EH faces, this is the gauge half of the composition that the module doc records as feeding RecognitionExactJConvergesEH (iterated $N\to\infty$ Tendsto to the scale-explicit Option-C continuum face). No downstream consumers are wired yet (used_by_count = 0), so the lemma is presently a leaf of the continuum-closure stack.
It does not flip gap_action_recovery, does not inhabit S_RS_converges_EH_4d, and does not elevate the Hessian to the literal nonlinear Regge action via Schläfli (still OPEN). Binding honesty: the exact-J action on the mesh is MODEL-identified with the Option-C midpoint Bloch symbol; star-edge origins for non-t11 orbits are landed elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.