Pith. sign in
def

sideScale

definition
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit
domain
Gravity
line
60 · github
papers citing
none yet

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.