realMode
plain-language theorem explainer
Maps a commensurate integer 4-mode m on a periodic lattice of side N to the real Bloch wave covector k = 2π m / N. Gravity continuum-preflight and mesh-bridge code cite it whenever a finite-N symbol or fold must be evaluated at a physical wavevector. The body is a one-line componentwise scaling.
Claim. Given lattice side $N \in \mathbb{N}$ and an integer mode $m \colon \{0,1,2,3\} \to \mathbb{Z}$, define the real wave covector $k \colon \{0,1,2,3\} \to \mathbb{R}$ by $k_i = 2\pi\, m_i / N$ for each coordinate $i$.
background
This module freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys for the 4D Regge continuum-closure campaign before any continuum recovery is claimed. The carrier is the canonical periodic Freudenthal 4-torus of side $N \ge 3$.
Integer modes on that torus are maps $m \colon \mathrm{Fin},4 \to \mathbb{Z}$ (commensurate Brillouin-zone labels). Real wave covectors are maps $k \colon \mathrm{Fin},4 \to \mathbb{R}$. Continuum-family symbols and Bloch folds are evaluated at these real $k$, not at bare integers.
The conversion $k = 2\pi m / N$ is the standard discrete-to-continuum identification of lattice momenta on a periodic box of side $N$. Downstream finite symbols (exact flat cross-term fold, midpoint Bloch, legacy transported hinge fold) all take this real covector as input.
proof idea
Pure definition: componentwise, send each integer coordinate $m_i$ to $(2\pi), m_i / N$ after casting to $\mathbb{R}$. No lemmas, no tactics; the body is the formula itself.
why it matters
Every finite-$N$ continuum sequence in the preflight module is evaluated at realMode (torusSide j) m. That includes the ledger continuum object finiteExactReggeSymbol (definitionally the exact flat cross-term fold at this $k$), the comparison midpoint Bloch symbol, and the legacy distinct-hinge transported fold retained only for regression.
The Recognition mesh bridge reuses it as meshWave, so geometry-derived Option-C midpoint Bloch symbols on the Freudenthal mesh share the same momentum convention. Without a single frozen $k = 2\pi m / N$ map, TT-normalized EH matching and pure-gauge vanishing checks would not sit on a common wavevector.
This sits in the QG full-theory campaign's first binding increment: freeze mesh and symbol carriers before inhabiting continuum Tendsto props. It does not itself close continuum recovery (S_RS_converges_EH_4d remains open).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.