Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit

show as:
view Lean formalization →

Continuum-limit stage for Regge transverse-traceless Bloch modes. It packages midpoint-displacement phases, scaled cosine folds, and the cosine two-jet limit that turn finite-cell evaluators into continuum symbols. Downstream M2-tendsto and algebraic-closer modules cite these limits. Argument is analytic: Taylor/jet control of cos and scale tendsto on normalized real modes.

claimDefines the midpoint-displacement phase $\sum_i x_i(u_i/2)$, raw cosine evaluators and folds at lattice side-scale, normalized real modes, and proves $(\cos\theta-1)/\theta^2\to -1/2$ as $\theta\to 0$, plus the matching scaled fold limit for Regge TT symbols.

background

This module sits in the Regge TT gravity analysis pipeline, immediately after the finite Bloch assembly stage. That upstream stage builds a C-DAG1 finite-cell cosine evaluator from a bucket integer phase key, independent of any quadratic moment evaluator, for side lengths and commensurate integer wave vectors whose doubled frequency is non-aliased in one coordinate.

Here the continuum step begins. The midpoint-displacement phase is the literal linear form $\sum_i x_i(u_i/2)$. From it one builds raw cosine evaluators and folds at a lattice side-scale, together with real-mode norms and normalized real modes. The analytic core is the two-jet of cosine near zero and the corresponding scale-tendsto for the fold, which convert discrete Bloch data into continuum symbols used by later closers.

Notation is lattice-first: side scale, integer wave vectors, and fold-along-direction symbols, not continuum metric fields.

proof idea

Definition layer first: linear and quadratic raw phases, cosine evaluator and fold at scale, real-mode norm-squared and normalization, and side-scale bookkeeping, including the zero-fold identity.

Analytic layer: an iterated-derivative identity for $a\mapsto\cos(a\cdot)$ supplies the two-jet. The key lemma is the standard limit $(\cos\theta-1)/\theta^2\to -1/2$. That jet is then transferred to the scaled raw cosine fold, yielding the fold-scale tendsto used by continuum closers.

No algebraic TT isotropy identities live here; those are deferred to the algebraic closer.

why it matters in Recognition Science

Production stage C-DAG2 in the panel-locked D-dag order ReggeTTBlochAssembly → ReggeTTContinuumLimit → ReggeTTAlgebraicCloser → ReggeTTContinuumCloser (QG full-theory campaign, Paper C / Pillar 1).

ReggeBlochM2Tendsto4D imports the proved cosine two-jet to close the punctured Tendsto along symbolDir for axis TT and pure gauge, using also zero-momentum vanishing of the deficit kernel on those sectors. ReggeTTAlgebraicCloser is the sole production importer of the committed algebraic certificate spike and takes this continuum limit as its immediate predecessor before emitting the C8 closed form $(1/2)x^T\mathrm{adj}(E)x$ and the TT isotropy value $-1/4$.

Without the cosine two-jet and fold-scale tendsto, the finite Bloch assembly cannot pass to continuum TT symbols.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)