theta_two_mul
plain-language theorem explainer
Doubling every component of the integer frequency vector doubles the cell phase on the N^{3} torus. Anyone collapsing product-to-sum Bloch cell-sums of cosines cites this homogeneity when the doubled mode 2m appears. The proof is a direct unfold of θ followed by ring arithmetic on the linear form.
Claim. For any $N\in\mathbb{N}$, frequency $m:\{0,1,2\}\to\mathbb{Z}$, and cell $x$ in the $N\times N\times N$ index cube, $\theta_N(2m,x)=2\,\theta_N(m,x)$, where $\theta_N(m,x)=2\pi(m_0 x_0+m_1 x_1+m_2 x_2)/N$.
background
This module records classical discrete Fourier orthogonality on finite torus cells Fin N × Fin N × Fin N. It is pure Mathlib analysis: no campaign imports and no physics claims. The intended consumer is the Regge TT continuum-symbol program, which sums products of phase-shifted cosines over cells and needs exact closed forms.
The cell phase is defined by $\theta_N(m,x)=2\pi(m_0 x_0+m_1 x_1+m_2 x_2)/N$ for commensurate wave vector $k=2\pi m/N$. Consumer phases arrive as $k\cdot(x+D/2)=\theta_N(m,x)+\alpha$ with constant offset $\alpha=k\cdot D/2$, so every identity is written in the shape $\theta+$ constant. Spatial dimension $D=3$ is the forced RS value (T8), which fixes the three-component index type.
Upstream, the 1D geometric sums expSum_eq_zero / expSum_eq_card and the 3D factorization cellSum_exp_eq_prod supply the vanishing criteria used later; the present lemma is only the elementary homogeneity of $\theta$ itself.
proof idea
One-line algebraic identity. Unfold the definition of $\theta$, push the natural-number and integer casts into $\mathbb{R}$, then apply ring to the linear form $m\mapsto 2m$. No external lemmas are required beyond the definition.
why it matters
Feeds the headline identity cellSum_cos_mul_cos: for non-aliased doubled frequency $(\exists i,,N\nmid 2m_i)$,
$\sum_x\cos(\theta_N(m,x)+\alpha)\cos(\theta_N(m,x)+\beta)=N^3\cos(\alpha-\beta)/2$.
The product-to-sum step splits into a constant $(A-B)$ half and an $(A+B)$ half at doubled frequency $2m$; homogeneity $\theta(2m,x)=2\theta(m,x)$ identifies that half so cellSum_cos_eq_zero can kill it.
In the broader RS gravity stack this is scaffolding for Crux-1c (Regge TT continuum symbol). The continuum target $-(1/4)$ remains open; the present lemma only clears the classical discrete Fourier bookkeeping on the torus. Landmarks T7 (eight-tick) and T8 ($D=3$) fix the ambient cell geometry but are not invoked in the proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.