torusNormalized_eq_continuumSymbol
plain-language theorem explainer
The torus-normalized continuum-limit predicate for the Option-C midpoint Bloch mesh symbol is definitionally the same proposition as the Regge 4D continuum-symbol binder. Anyone wiring the 4D action↔symbol dictionary can rewrite one into the other freely. The proof is a one-line definitional reflexivity (`Iff.rfl`).
Claim. For an integer 4-mode $m$, a $4\times 4$ matrix $E$, and a real $\Lambda$, the statement that the normalized Option-C midpoint Bloch mesh symbol tends to $\Lambda$ along the side-$N=j+3$ torus family is equivalent to the continuum-symbol predicate that the same $|k|^2$-normalized exact-action finite Hessian tends to $\Lambda$. The two propositions are definitionally identical.
background
This module builds the 4D torus continuum limit: a finite periodic Freudenthal action sequence on side $N=j+3$, with $N^4$ sites and density weight $N^{-4}$. The bookkeeping is the 4D analogue of the closed 3D path, where $(2/N^3)\cdot(N^3/2)=1$ cancels so the canonical finite Hessian equals the raw cosine fold; here the same identity is $(2/N^4)\cdot(N^4/2)=1$.
IntMode4 is an integer wave vector on the side-$N$ torus (commensurate modes). Mat4 is the preflight $4\times 4$ matrix type. The continuum-symbol predicate asserts that the concrete exact-action finite Hessian, normalized by momentum norm squared, tends to $\Lambda$ along $N=j+3$; its sequence is definitionally the midpoint Bloch symbol, not a constant face and not the legacy transported fold.
The local twin TorusNormalizedTendsto packages the same Tendsto along the torus family (side via familySide), matching the preflight binder by construction.
proof idea
One-line term proof: Iff.rfl. Both sides unfold to the same Tendsto of finiteExactMidpointBlochSymbol j m E divided by momentum-norm-squared of the side-$N$ mode, at atTop toward nhds Λ. The only surface difference is familySide versus torusSide; those sides are definitionally equal, so the two Props are identical and reflexivity closes the biconditional.
why it matters
Pins the action↔symbol dictionary name for the 4D torus continuum limit: the module-local normalized Tendsto is interchangeable with the preflight continuum-symbol binder. That lets later continuum arguments cite either name without a conversion lemma.
Parallel to the closed 3D path ReggeTTBlochAssembly → ReggeTTContinuumLimit. Module status: product mesh cardinality and density-weight identities, decoy discrimination against $N^{-2}$, and algebraic cell-sum cancellation are theorems; the continuum Tendsto binds to the Option-C midpoint trig-poly mesh sequence. Open (named): 4D cosine cell-sum identity and residual star-member offsets on the legacy fold. Does not flip gap_action_recovery. No downstream users yet in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.