Gravity Analysis Regge Ttcontinuum Limit Raw Cosine Evaluator Eq Scale

The scale bridge

The declaration rawCosineEvaluator_eq_scale is a theorem in the Recognition Science library, a machine-checked collection of formal proofs. It states a precise equivalence: for any nonzero integer mode and any bucket, the cosine evaluator at the discrete commensurate momentum equals the cosine evaluator at the continuous scale q = 2π/N, where N is the side length of the lattice. In plain terms, the discrete world and the continuous world agree when you choose the matching scale. The proof is a direct expansion: it unfolds the definitions and verifies that the phase, the argument of the cosine, is identical in both cases.

What makes this useful is the limit it enables. The theorem is a bridge from finite sums over lattice points to smooth continuum integrals. When N grows, the scale 2π/N shrinks, and the cosine evaluator, divided by the square of that scale, tends to a fixed moment. That limit is the Regge TT moment, a quantity that carries the gravitational information. The theorem rawCosineFold_scale_tendsto proves this convergence: the finite raw cosine fold divided by q² approaches exactly the Regge TT moment as q goes to zero. The phase in the limit is the literal squared midpoint displacement, (sum_i x_i * (u_i / 2))², with no correction or fitted parameter.

The declaration does not claim that the continuum limit is the actual physical spacetime, nor that the Regge TT moment is the observed gravitational wave amplitude. It is a mathematical statement about a specific construction: a finite lattice approximation to a Regge calculus, with a particular cosine weight and a particular phase convention. The theorem does not prove that this limit is unique, that it matches experiment, or that it extends to higher orders. It is one step in a longer chain, a clean bridge from the discrete to the continuous within the framework.

For the reader, the consequence is simple: the framework's discrete gravity constructions have a well-defined smooth limit, and that limit is computed exactly, not approximated. The bridge is load-bearing for any further claim that the lattice model reproduces continuum physics.

/-- The commensurate evaluator is exactly the free-scale evaluator at
`q_N = 2*pi/N`. -/
theorem rawCosineEvaluator_eq_scale (N : ℕ) [NeZero N]
    (m : Fin 3 → ℤ) (b : Bucket) :
    rawCosineEvaluator N m b =
      rawCosineEvaluatorAtScale (sideScale N) (fun i => (m i : ℝ)) b := by
  unfold rawCosineEvaluator rawCosineEvaluatorAtScale rawPhaseLinear
    commensurateMomentum sideScale
  congr 1
  simp only [Fin.sum_univ_three]
  ring

/-- REUSABLE CONTINUOUS-VARIABLE HEADLINE: after assembled zero-mode
cancellation, the finite raw cosine fold divided by `q^2` tends exactly to
`reggeTTMoment` with the literal midpoint phase quadratic. -/
theorem rawCosineFold_scale_tendsto (x : Fin 3 → ℝ)
    (E : Fin 3 → Fin 3 → ℝ) :
    Filter.Tendsto
      (fun q : ℝ => rawCosineFoldAtScale q x E / q ^ (2 : ℕ))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ)
      (nhds
        (reggeTTMoment rawCosineSupport (rawPhaseQuadratic x)
          (rawBucketAmplitude E))) := by
  have hzero := rawCosineFoldAtScale_zero x E
  have hsum :
      Filter.Tendsto
        (fun q : ℝ =>
          ∑ b ∈ rawCosineSupport,
            ((Real.cos (q * rawPhaseLinear x b) - 1) / q ^ (2 : ℕ)) *
              rawBucketAmplitude E b)
        (nhdsWithin 0 {(0 : ℝ)}ᶜ)
        (nhds
          (∑ b ∈ rawCosineSupport,
            (-(rawPhaseLinear x b ^ (2 : ℕ)) / 2) *
              rawBucketAmplitude E b)) := by
    apply tendsto_finset_sum
    intro b _
    exact (cos_sub_one_div_sq_tendsto (rawPhaseLinear x b)).mul_const
      (rawBucketAmplitude E b)
  have hcongr :
      (fun q : ℝ => rawCosineFoldAtScale q x E / q ^ (2 : ℕ)) =ᶠ[
        nhdsWithin 0 {(0 : ℝ)}ᶜ]
      (fun q : ℝ =>
        ∑ b ∈ rawCosineSupport,
          ((Real.cos (q * rawPhaseLinear x b) - 1) / q ^ (2 : ℕ)) *
            rawBucketAmplitude E b) := by
    filter_upwards [self_mem_nhdsWithin] with q hq
    unfold rawCosineFoldAtScale reggeTTBlochFold
    have hzero' :
        ∑ b ∈ rawCosineSupport, rawBucketAmplitude E b = 0 := by
      simpa [rawCosineFoldAtScale, reggeTTBlochFold,
        rawCosineEvaluatorAtScale] using hzero
    calc
      (∑ b ∈ rawCosineSupport,
          rawCosineEvaluatorAtScale q x b * rawBucketAmplitude E b) /
            q ^ (2 : ℕ)
          =
        ((∑ b ∈ rawCosineSupport,
            rawCosineEvaluatorAtScale q x b * rawBucketAmplitude E b) -
          ∑ b ∈ rawCosineSupport, rawBucketAmplitude E b) /
            q ^ (2 : ℕ) := by rw [hzero', sub_zero]
      _ = ∑ b ∈ rawCosineSupport,
          ((Real.cos (q * rawPhaseLinear x b) - 1) / q ^ (2 : ℕ)) *
            rawBucketAmplitude E b := by
        rw [← Finset.sum_sub_distrib]
        simp_rw [Finset.sum_div]
        refine Finset.sum_congr rfl fun b _ => ?_
        unfold rawCosineEvaluatorAtScale
        field_simp [hq]
  refine hsum.congr' hcongr.symm |>.congr' ?_
  filter_upwards with _
  rfl

What this page does not claim

The theorem does not claim that the continuum limit is unique or that it matches any measured gravitational wave amplitude. The theorem does not establish that the Regge TT moment is the physical spacetime curvature. The theorem does not prove that the limit extends beyond the leading quadratic order.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: