Pith. sign in
theorem

commensurateMomentum_zero

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode
domain
Gravity
line
386 · github
papers citing
none yet

plain-language theorem explainer

On the side-N spatial torus, the zero integer wave vector maps to the zero real momentum under the standard commensurate embedding k = 2π m / N. Anyone specializing Bloch or stencil identities at k = 0 cites this. The proof is a one-line pointwise simplification of the definition after function extensionality.

Claim. For every positive integer $N$, if $m\colon\{0,1,2\}\to\mathbb{Z}$ is the zero map, then the commensurate momentum $k_i = 2\pi m_i/N$ is the zero map $\{0,1,2\}\to\mathbb{R}$.

background

This module is Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C): hinge-aware zero-mode analysis for the Regge TT symbol. The assembled constant block at vanishing crystal momentum is the headline object; stencil and hinge contributions must cancel under a fixed assembly sign.

Commensurate momentum is the standard torus embedding of an integer wave vector $m$ on the side-$N$ lattice: each Cartesian component is $k_i = 2\pi m_i/N$. Plane-wave phases and midpoint Bloch factors are built from this $k$. The continuum second-variation phase $k\cdot x$ and the eight-tick phase ladder sit upstream as notation only; the present fact is purely about the discrete-to-real momentum map.

Zero momentum is the specialization point for the raw cell stencil identity that reduces the $k=0$ stencil to twice the per-cell assembled constant block.

proof idea

Term-mode proof by function extensionality on the three spatial indices, then simp against the definition of commensurate momentum. Each component is $2\pi\cdot 0/N = 0$, so the resulting real map is identically zero. No lemmas beyond the definition unfold are required.

why it matters

Feeds rawCellStencil_zeroMomentum, which states that the $k=0$ raw cell stencil equals twice the assembled constant block: the cell sum contributes $N^3$ identical copies and the $2/N^3$ normalization leaves a factor of two. That identity is a step toward the zero-mode headline assembledConstantBlock_eq_zero in this module.

In the Gate C-A3 story, the sympy diagnostic showed stencil-only residual and hinge contribution cancel under the relative-minus assembly convention. Specializing every Bloch phase and plane-wave velocity at vanishing $k$ needs a clean zero-momentum map; this lemma discharges that specialization without ad-hoc rewriting.

Framework-wise it is local gravity/analysis scaffolding for the TT zero mode on the periodic complex, not a forcing-chain (T0–T8) step. It closes a definitional edge so later hinge-cancellation and witness-split theorems can quote $k=0$ literally.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.