sideScale
plain-language theorem explainer
Defines the continuous momentum scale q_N = 2π/N for a side-N torus in the Regge TT continuum analysis. Anyone citing the finite-to-continuum cosine two-jet limit or the momentum-norm factorization uses this scale. The body is a one-line real arithmetic definition, not a proof.
Claim. For each natural number $N$, the side scale is $q_N := 2\pi/N \in \mathbb{R}$. This is the continuous scale attached to side-$N$ commensurate momentum on the torus.
background
The 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. The reusable free-scale theorem works with an arbitrary real scale $q$ whose phase is $q \sum_i x_i (u_i/2)$, keeping the doubled-midpoint convention.
Commensurate finite modes live on a side-$N$ lattice. Their continuous scale must be the fundamental Brillouin spacing $2\pi/N$, so that integer mode vectors $m$ map to physical wavevectors $q_N m$. Downstream, the momentum-norm squared factors exactly as $q_N^2$ times the Euclidean norm of the real mode, and the finite cosine evaluator is identified with the free-scale evaluator at this $q_N$.
proof idea
Pure definition: unfold to $2\cdot\pi$ divided by the real cast of $N$. No lemmas, no tactics.
why it matters
This is the concrete $q_N$ that glues the free-scale continuum jet to the finite assembly. It is unfolded in three places in the same module: the identity that the commensurate raw cosine evaluator equals the free-scale evaluator at $q_N$; the exact factorization of momentum-norm squared into $q_N^2$ times real-mode norm squared; and the headline P1.1a theorem that the reduced finite Regge symbol over momentum-norm squared tends to the raw Regge TT moment at the normalized real mode.
In the broader gravity chain this is the continuum bridge after hinge-aware zero-mode cancellation removes the constant block. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is local continuum bookkeeping for the Regge TT symbol on the three-torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.