eventually_nonaliased
plain-language theorem explainer
For any fixed nonzero integer mode m on the 3-torus, the non-aliasing condition needed by the cosine cell-sum identity holds for all large enough lattice sizes N. Bloch-assembly proofs for Regge-TT finite Hamiltonians cite this to pass from a fixed mode into the large-N regime. The argument picks a nonzero component of m and takes N past twice its absolute value, so N cannot divide 2 m_i.
Claim. Let $m:\{0,1,2\}\to\mathbb{Z}$ be a frequency vector with at least one nonzero component. Then eventually as $N\to\infty$ along the naturals, some component satisfies $N\nmid 2m_i$.
background
The module proves classical discrete Fourier orthogonality on Fin N index cubes for the ReggeTT continuum-symbol program (Crux-1c). Downstream cell sums of products $\cos(\theta_m x+\alpha)\cos(\theta_m x+\beta)$ with commensurate wave vector $k=2\pi m/N$ collapse to $N^3\cos(\alpha-\beta)/2$ precisely when the doubled frequency $2m$ is non-aliased: some component of $2m$ is not divisible by $N$.
Phase convention: $\theta_N(m,x)=2\pi(m\cdot x)/N$ on the 3-torus cell, with consumer phases arriving as $\theta+\text{constant}$. The headline identity needs the hypothesis $\exists i,,N\nmid 2m_i$. This lemma guarantees that hypothesis holds for all sufficiently large $N$ once $m$ is fixed and nonzero.
The file is Mathlib-only analysis and algebra; no campaign physics claims enter.
proof idea
Unpack a nonzero component $i$ of $m$. Rewrite $\forall^\infty N$ via Filter.eventually_atTop as existence of a threshold. Take the threshold $N_0=2|m_i|+1$. For $N\ge N_0$, assume toward contradiction that $N$ divides $2m_i$. Nonvanishing $2m_i\ne 0$ follows from mul_ne_zero with $2\ne 0$ and $m_i\ne 0$. Then Int.le_of_dvd with positivity of the absolute value yields $N\le|2m_i|$. Rewriting the absolute value as a natural absolute value, omega closes the contradiction $N\ge 2|m_i|+1>|2m_i|$.
why it matters
Sole downstream consumer is eventually_canonicalFiniteH_eq_rawCosineBlochFold in ReggeTTBlochAssembly: for every fixed nonzero integer mode, the canonical finite assembly identity holds at every sufficiently large side length, equating canonical finite $H$ to the raw-cosine Bloch fold. That step needs the non-aliasing gate cleared uniformly in large $N$ so the classical cell-sum orthogonality (headline cellSum_cos_mul_cos) can fire.
The module header is explicit that nothing here touches the $-(1/4)$ continuum target, which remains open. This lemma only supplies the divisibility side-condition that lets the discrete Fourier identities engage for fixed nonzero modes as the torus is refined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.