normalizedRealMode
plain-language theorem explainer
Integer lattice modes on the three-torus are converted to unit Euclidean directions in R^3 by dividing by the square root of the squared mode norm. Continuum and algebraic Regge-TT arguments cite this map so that cosine two-jet and moment evaluations sit on the sphere rather than on raw integer vectors. The body is a one-line pointwise cast-and-normalize definition.
Claim. For an integer mode $m:\{0,1,2\}\to\mathbb{Z}$, the normalized real mode is the map $i\mapsto m(i)/\sqrt{\sum_{j} m(j)^2}$ in $\mathbb{R}^3$, i.e. the real direction of $m$ with unit Euclidean norm (when $m\neq 0$).
background
This module is the C-DAG2 continuum stage for Regge TT: finite Bloch assembly is already in hand, cell sums are gone by exact Bloch orthogonality, and the remaining work is a local cosine two-jet limit of the raw bucket fold. Phases keep the doubled-midpoint convention $q\sum_i x_i(u_i/2)$, zero modes are stripped by the assembled zero-mode theorem, and the final continuum statements compose free-scale limits with $q_N=2\pi/N$ and momentum-norm normalization.
The sibling realModeNormSq is the squared Euclidean norm $\sum_i x_i^2$ of a real three-vector. Integer modes $m:\mathrm{Fin},3\to\mathbb{Z}$ are the discrete momenta on the three-torus; continuum and moment formulae need their direction on the unit sphere so that scale factors factor cleanly through momentumNormSq.
Downstream continuum work evaluates raw cosine folds and quadratic phases at this unit direction rather than at the raw integer vector, matching the module's claim that the final P1.1a limit is the raw Regge TT moment at the normalized real mode.
proof idea
Definition only: cast each integer component $m_i$ to $\mathbb{R}$, form the real vector, divide componentwise by $\sqrt{\mathrm{realModeNormSq}(m)}$. No lemmas or tactics; the norm is the sibling sum-of-squares on $\mathrm{Fin},3$.
why it matters
Unit directions are the geometric input to the continuum and algebraic closers for Regge TT. The final P1.1a headline canonicalFiniteH_div_momentumNormSq_tendsto states that the finite reduced Regge symbol divided by momentumNormSq tends to the raw Regge TT moment evaluated at this normalized real mode (phase still $(\sum_i x_i(u_i/2))^2$). The P1.1b headline reggeTTMoment_tt_value then evaluates that continuum moment on every nonzero integer mode and TT polarization and obtains exactly the continuum coefficient $-1/4$.
In the broader Recognition gravity stack this is bookkeeping for the discrete-to-continuum bridge on the three-torus (spatial $D=3$ from the forcing chain), not a new dynamical law. It lets scale drop out so the cosine two-jet and TT projector algebra can be stated on the unit sphere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.