momentumNormSq_torus_ne_zero
plain-language theorem explainer
On the continuum torus family of side length j+3, every nonzero integer 4-mode has strictly positive momentum-norm squared. Anyone normalizing finite-mesh midpoint Bloch symbols by that factor cites this nonvanishing lemma. The proof rewrites the norm as a squared torus scale times the integer-mode wave norm, then multiplies two nonzero real factors.
Claim. For every $j \in \mathbb{N}$ and every integer 4-mode $m \in \mathbb{Z}^4$ with $m \neq 0$, the momentum-norm squared of $m$ on the side-$(j+3)$ torus is nonzero: $\|k\|^2 \neq 0$ where $k = 2\pi m / (j+3)$.
background
The ambient module treats the TT directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field TT sector, then transports the torus-normalized continuum face via the banked $S_{RS}\to EH$ convergence on $H\pm K$ plus polarization.
An IntMode4 is an integer wave vector $m:\mathrm{Fin},4\to\mathbb{Z}$ (commensurate modes on the periodic lattice). The continuum family uses side length $N=j+3$ (torusSide). Momentum-norm squared is momentumNormSq N m := waveNormSq(realMode N m), i.e. the squared Euclidean norm of the real covector $k=2\pi m/N$.
Upstream, momentumNormSq_eq_scale_sq identifies this with a squared torus scale times the bare integer-mode wave norm, so nonvanishing reduces to scale $\neq 0$ and $m\neq 0$.
proof idea
Rewrite via momentumNormSq_eq_scale_sq, so the claim is $(\mathrm{torusScale},j)^2\cdot\mathrm{waveNormSq}_{\mathrm{int}}(m)\neq 0$.
First, torusScale j \neq 0: unfold to a multiple of $2\pi/(j+3)$; the numerator is nonzero by norm_num and Real.pi_ne_zero, the denominator by Nat.cast_ne_zero plus omega on $j+3\ge 3$.
Then mul_ne_zero of pow_ne_zero 2 on that scale with waveNormSq_intMode_ne_zero m hm finishes.
why it matters
This is the denominator guard for the normalized finite-mesh directional derivative hasDerivAt_finiteExactMidpointBlochSymbol_normalized, which divides the exact midpoint Bloch symbol by momentumNormSq (torusSide j) m. Without nonvanishing, that HasDerivAt statement is ill-formed.
Downstream it feeds the headline continuum theorem continuumTTFirstVariation_closed: the torus-normalized midpoint first variation tends to $-\tfrac14$ times the Frobenius pairing in the Euclidean weak-field TT sector. The module honesty clause still bars citing this as a source equation, Ricci/null focusing, or GAP1 closure; the missing object remains a Recognition-derived Freudenthal exact-$J$ metric refinement identifying sourced response with this midpoint variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.