TorusNormalizedTendsto
plain-language theorem explainer
Predicate asserting that the Option-C midpoint Bloch mesh symbol, divided by torus momentum-squared, converges to a real value Λ along the side-(j+3) family. Gravity analysts cite it as the continuum-limit binder for normalized 4D Regge symbols on the periodic Freudenthal mesh. It is a pure definitional Prop packaging Filter.Tendsto; no proof content.
Claim. For an integer 4-mode $m\colon\{0,1,2,3\}\to\mathbb{Z}$, a $4\times 4$ matrix $E$, and $\Lambda\in\mathbb{R}$, the sequence $$j\mapsto \frac{S^{\mathrm{mid}}_j(m,E)}{\|k_j(m)\|^2}$$ tends to $\Lambda$ as $j\to\infty$, where $S^{\mathrm{mid}}_j$ is the exact midpoint Bloch trig-poly symbol on the side-$(j+3)$ 4-torus and $k_j(m)=2\pi m/(j+3)$.
background
The module develops the 4D torus continuum limit for the Regge action–symbol dictionary. Finite periodic Freudenthal meshes have side $N=j+3$, hence $N^4$ sites and density weight $N^{-4}$ (frozen against the wrong-power $N^{-2}$ decoy). Bookkeeping parallels the closed 3D path: the factors $(2/N^4)\cdot(N^4/2)=1$ cancel, so the canonical finite Hessian equals the distinct-hinge Bloch fold once Schläfli elevation and the 4D cell-sum identity close.
An integer mode $m$ is a commensurate wave vector on the torus; the real covector is $k=2\pi m/N$. Momentum-squared is the squared Euclidean norm of that covector. The numerator is the exact midpoint Bloch symbol (Option-C trig-poly mesh sequence), rebound from the flat Hessian on the real mode at side $N=j+3$. The continuum binder in the preflight is definitionally the same Tendsto statement.
proof idea
Definitional Prop, not a proved theorem. The body is a direct packaging of Filter.Tendsto at atTop into the neighborhood filter of $\Lambda$. The sequence maps each natural $j$ to the exact midpoint Bloch symbol at side $j+3$, divided by momentum-squared of the corresponding real mode. No lemmas are applied; equality with the preflight continuum-symbol predicate is later Iff.rfl.
why it matters
Names the continuum-limit obligation for the normalized Option-C midpoint symbol on the 4-torus family, matching the preflight continuum-symbol predicate. Downstream, torusNormalized_eq_continuumSymbol records the definitional equivalence, and TorusC2DensityExtensionOpen packages the open existence claim: for every nonzero TT-polarized mode there is some $\Lambda$ realizing this Tendsto. That open item is the C²/smooth density-extension gap from finite Fourier sums. The module status list marks continuum Tendsto as a DEFINITION binding to the midpoint mesh sequence; it does not discharge the open 4D cosine cell-sum identity, residual star-member offsets, or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.