Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit

show as:
view Lean formalization →

Continuum-limit layer for Regge transverse-traceless (TT) Bloch data: scaled cosine folds and two-jet expansions that turn finite-cell phase keys into continuum symbols. Gravity analysts cite it for the proved limit $({\cos\theta-1})/\theta^2\to-1/2$ and the scale-tendsto of the raw cosine fold. The module packages phase linear/quadratic forms, normalized real modes, and those Tendsto lemmas as the bridge from C-DAG1 assembly to algebraic and 4D closers.

claimOn scaled Regge TT Bloch cells, define the midpoint-displacement phase $\sum_i x_i(u_i/2)$, the associated raw cosine evaluator and fold at side scale $s$, and normalized real modes. Prove $\frac{\cos\theta-1}{\theta^2}\to -\tfrac12$ as $\theta\to 0$ and that the raw cosine fold tends to its continuum quadratic symbol under mesh refinement $s\to 0$.

background

Recognition Science gravity work here follows a panel-locked D-dag: finite Bloch assembly, then continuum limit, then algebraic closer. The upstream module ReggeTTBlochAssembly is C-DAG1: "the cosine evaluator is defined directly from a bucket's integer phase key, independently of any quadratic moment evaluator," for side lengths and commensurate integer wave vectors with non-aliased doubled frequency.

This module sits one stage later. It introduces literal midpoint-displacement phases (linear in displacements $x_i$ and half-link directions $u_i/2$), quadratic phase companions, side-scale parameters, and normalized real modes built from squared mode norms. The cosine fold at a given scale is the finite-cell object whose continuum symbol is the TT kinetic/deficit kernel used downstream.

Notation is classical analysis on the lattice: iterated derivatives of $2\cos$, scale-dependent evaluators, and filter Tendsto statements as the mesh (side scale) goes to zero, without yet closing full 4D spacetime limits.

proof idea

Definition-heavy front half: raw linear and quadratic phases, cosine evaluator/fold at scale, real-mode norm and normalization, and side-scale bookkeeping, plus elementary vanishing lemmas (fold at zero scale).

Analytic back half: calculus identities for iterated derivatives of $2\cos$ multiples, then the standard two-jet limit $(\cos\theta-1)/\theta^2\to-1/2$, packaged as cos_sub_one_div_sq_tendsto. The scale-tendsto of the raw cosine fold reduces the mesh limit of the finite fold to that two-jet plus the assembled Bloch phase structure from the import. No single master theorem; a ladder of defs feeding two named Tendsto results.

why it matters in Recognition Science

Production stage C-DAG2 on the QG full-theory path (Paper C / Pillar 1): ReggeTTBlochAssembly → ReggeTTContinuumLimit → ReggeTTAlgebraicCloser → ReggeTTContinuumCloser. Downstream ReggeBlochM2Tendsto4D "uses the proved cosine two-jet cos_sub_one_div_sq_tendsto and the already-proved zero-momentum vanishing of the deficit kernel on axisTTPlus / decoyGauge" to close punctured Tendsto along symbolDir for axis TT and pure gauge.

ReggeTTAlgebraicCloser imports this stage as the sole production path into the C8 closed form $\tfrac12 x^T\mathrm{adj}(E)x$ and the TT isotropy value $-1/4$. Without the continuum two-jet and fold-scale limits, the algebraic certificate and 4D symbol limits have no analytic input from the finite Bloch cosine assembly.

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)