Encyclopedia Gravity Gravity Analysis Regge Ttcontinuum Limit Raw Cosine Fold Scale Tendsto

ARTICLE 2 claims 2 theorems

Gravity Analysis Regge Ttcontinuum Limit Raw Cosine Fold Scale Tendsto

A limit theorem in the framework's gravity library shows how a discrete sum over cells approaches a continuous moment, and it does not claim to derive gravity itself.

Verify this page

The continuum limit

In the Recognition Science framework, a ledger is a discrete record of events, and the framework's gravity analysis works with a finite assembly of cells. The declaration rawCosineFold_scale_tendsto is a limit theorem about a particular sum, called a raw cosine fold, that runs over those cells. The theorem states that as a free scale parameter q tends to zero, the fold divided by q squared converges to a specific continuous quantity, the Regge TT moment, with the phase quadratic preserved exactly. In plain terms, it shows that a discrete cell sum, when scaled appropriately, becomes a smooth continuous expression in the limit of fine resolution.

The theorem is a statement about a mathematical limit, not about physical gravity. It establishes a precise correspondence between a finite, discrete construction and its continuous counterpart. The proof relies on a local cosine two-jet approximation, which means the cosine function is approximated by its second-order Taylor expansion near zero. The constant term is removed by a separate zero-mode theorem, and the result holds for any real scale q and any amplitude function E. The theorem is machine-checked in the framework's library of formal theorems, meaning the proof has been verified by a computer.

What the theorem does not claim is equally important. It does not claim that gravity emerges from this limit, nor that the Regge TT moment is the full gravitational action. It is a technical lemma about convergence of a specific sum. The theorem also does not specify the physical meaning of the scale q; that interpretation is left to other parts of the framework. The result is a precise mathematical statement, and its role in the broader framework is to connect the discrete cell assembly to a continuous moment, not to explain why gravity exists.

THEOREM rawCosineFold_scale_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
rawCosineFold_scale_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:145 
/-- 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
THEOREM rawCosineFold_scale_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
rawCosineFold_scale_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:145 
/-- 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 gravity emerges from the discrete sum. The theorem does not claim that the Regge TT moment is the complete gravitational action. The theorem does not assign a physical meaning to the scale q.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND