IndisputableMonolith.Gravity.Analysis.BlochCellSum
Finite Bloch cell sums of complex exponentials and cosines on integer lattices. Supplies the algebraic identities that turn a product of one-dimensional geometric sums into a vanishing cosine cell sum when a doubled frequency is non-aliased. Downstream Regge TT assembly cites these lemmas to evaluate normalized finite-cell cosine modes without quadratic moment machinery.
claimOn a finite cell of side lengths $N_i$, the complex mode factors $e^{2\pi i a_i/N_i}$ are $N_i$-th roots of unity. Their multi-index cell sum factors as a product of geometric sums; when at least one doubled frequency is non-aliased, the real cosine cell sum vanishes identically.
background
This module sits in the gravity analysis layer that prepares finite-cell Bloch data for Regge TT assembly. The basic objects are unit-circle ratios $\exp(2\pi i a/N)$ for integer phase keys $a$ and cell sizes $N$, together with their real parts (cosines) and multi-dimensional products over a rectangular cell.
A one-dimensional geometric sum of an $N$-th root of unity is either $N$ (trivial mode) or $0$ (nontrivial). The cosine sum is the real part of that exponential sum. Multi-dimensional cell sums factor as products of the one-dimensional sums via a standard sum-of-products identity.
The local setting is pure complex analysis and finite Fourier arithmetic over $\mathbb{Z}/N\mathbb{Z}$; no continuum limit or metric dynamics is assumed here. The phase key is an integer bucket label, independent of any quadratic moment evaluator used elsewhere in the gravity stack.
proof idea
The module is a short ladder of elementary lemmas, not a single theorem. First, $\bigl(\exp(2\pi i a/N)\bigr)^N=1$, so each factor is an $N$-th root of unity; the exponential sum is then $N$ or $0$ according as the ratio is $1$ or not. Cosine sums inherit vanishing from the complex sum via $\mathrm{Re}$. A product identity converts a multi-index cell sum of products into a product of one-dimensional sums. The headline cell-sum cosine vanishing statement is the product of those one-dimensional vanishings when at least one coordinate has non-aliased doubled frequency.
why it matters in Recognition Science
ReggeTTBlochAssembly imports this module as the C-DAG1 finite-cell assembly stage. That parent defines the cosine evaluator directly from a bucket's integer phase key and needs, for every side length and commensurate integer wave vector whose doubled frequency is non-aliased in one coordinate, that the normalized canonical finite-cell cosine sum is zero (or the matching product formula when it is not). These identities discharge that algebraic step without coupling to quadratic moment evaluators, keeping the Bloch assembly purely kinematic. In the broader Recognition gravity path, clean finite-cell mode sums are the discrete substrate on which continuum or continuum-limit claims about residual gravity and TT structure can later rest.
scope and limits
- Does not define continuum Bloch waves or take any $N\to\infty$ limit.
- Does not couple cosine sums to quadratic moment or curvature evaluators.
- Does not prove dynamical gravity equations or residual-mass formulae.
- Does not treat non-rectangular cells or non-commensurate wave vectors.
- Does not assert physical units; all statements are pure finite Fourier arithmetic.
used by (1)
declarations in this module (16)
-
lemma
exp_ratio_pow_card -
lemma
exp_ratio_eq_one_iff -
lemma
exp_term_eq_pow -
theorem
expSum_eq_zero -
theorem
expSum_eq_card -
lemma
sum_cos_of_sum_exp_eq_zero -
theorem
cosSum_eq_zero -
def
theta -
lemma
theta_two_mul -
lemma
sum_mul_sum_prod -
theorem
cellSum_exp_eq_prod -
theorem
cellSum_cos_eq_zero -
theorem
cos_mul_cos -
theorem
cellSum_cos_mul_cos -
theorem
eventually_nonaliased -
theorem
cellSum_cos_sq_three_axis