Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.BlochCellSum

show as:
view Lean formalization →

Finite Bloch cell sums for complex exponentials and cosines on a discrete lattice torus. The module proves that geometric sums of N-th roots of unity vanish unless the mode is trivial, and that multi-dimensional cell sums factor as products of one-dimensional sums. Gravity analysts assembling Regge TT modes on finite cells cite these identities. Proofs are elementary complex-analysis reductions (geometric series and product expansions).

claimOn a finite cell of side $N$, the phase factors $e^{2\pi i a/N}$ are $N$-th roots of unity. One-dimensional sums $\sum_{k=0}^{N-1} e^{2\pi i m k/N}$ equal $N$ if $m\equiv 0\pmod{N}$ and $0$ otherwise; cosine sums vanish for non-trivial modes. Multi-dimensional cell sums factor as products of 1D sums, so the full cosine cell sum is zero whenever any coordinate mode is non-aliased and non-zero.

background

In discrete gravity and Regge calculus on a finite lattice, Bloch (plane-wave) modes are evaluated by summing complex exponentials over a rectangular cell. The basic building block is the ratio $\omega = \exp(2\pi i a/N)$, an $N$-th root of unity: $\omega^N = 1$.

The module works in $\mathbb{C}$ with Mathlib's exponential and trigonometric API. It introduces the phase map $\theta$ (linear in the integer wave index), the one-dimensional exponential sum over a side of length $N$, and the corresponding cosine sum. Multi-index cell sums are defined by ranging independently over each coordinate of the cell.

The local setting is the C-DAG1 finite-cell assembly stage of Recognition Science gravity analysis: cosine evaluators are built from integer phase keys, independently of quadratic moment evaluators, before modes are assembled into Regge TT contributions.

proof idea

The module is a short chain of elementary lemmas, not a single deep theorem.

First, $\omega^N = 1$ for $\omega = \exp(2\pi i a/N)$, so powers of the ratio collapse. The 1D exponential sum is identified with a geometric series: it equals the cardinality $N$ on the trivial mode and $0$ otherwise (via the standard root-of-unity filter). Cosine sums are recovered as real parts; if the complex sum vanishes then the cosine sum vanishes.

Multi-dimensional sums factor by writing the exponential of a sum of phases as a product and applying the product-of-sums identity. The cell exponential sum is therefore a product of 1D sums, and the cell cosine sum is zero as soon as any factor vanishes (non-aliased non-zero mode in one coordinate).

why it matters in Recognition Science

This module supplies the vanishing and factorization identities needed by ReggeTTBlochAssembly, the C-DAG1 finite-cell assembly stage. That downstream module defines the cosine evaluator from a bucket's integer phase key and requires, for every side length and commensurate integer wave vector whose doubled frequency is non-aliased in one coordinate, that the normalized canonical finite cell sum of cosines be zero (or equal the cell volume on the zero mode).

Without these cell-sum lemmas, the finite Bloch assembly cannot separate trivial zero modes from oscillatory contributions on the lattice torus. In the broader Recognition gravity stack, clean mode orthogonality on finite cells is a prerequisite for assembling discrete curvature and stress responses before continuum or phenomenological limits are taken.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (16)