Encyclopedia Gravity Gravity Analysis Regge Ttcontinuum Limit

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttcontinuum Limit

A machine-checked proof shows that a discrete lattice model of gravity recovers a continuous cosine law as the grid spacing shrinks.

Verify this page

The continuum limit

In numerical analysis, a continuum limit is what happens to a discrete approximation as its grid spacing goes to zero. The Regge TT continuum limit is the version of that idea used inside Recognition Science's gravity analysis. It takes a finite lattice of cells, each carrying a phase, and asks what smooth function emerges when the lattice is refined without bound. The answer, proved in the framework's machine-checked library of formal theorems, is that the discrete cosine fold converges to a continuous cosine moment with a specific quadratic phase.

The proof works in three stages. First, the library shows that the sum over cells vanishes at zero scale, because the assembled constant block cancels exactly. Second, a reusable theorem establishes that the raw cosine fold, divided by the square of the scale parameter, tends to a limit given by the second derivative of the cosine at zero. That derivative is minus the square of the phase, which is the standard small-angle behavior of a cosine. Third, the library composes these results with the specific scale choice q_N = 2*pi/N, where N is the number of lattice cells per side, and with the exact momentum normalization.

The final theorem, canonicalFiniteH_div_momentumNormSq_tendsto, states that for every fixed nonzero integer mode, the finite reduced Regge symbol divided by the squared momentum norm converges to exactly the raw Regge TT moment at the normalized real mode direction. In plain language: as the lattice gets finer, the discrete gravity symbol approaches a continuous limit that depends only on the direction of the mode, not on the lattice spacing. The phase that survives is the literal midpoint-displacement phase, the square of the sum over coordinates of x_i times u_i over 2.

What this establishes is that the discrete model is not an approximation that drifts as it is refined. It has a well-defined continuous target, and that target is a cosine moment with a quadratic phase. This is the kind of result that makes a discrete theory credible: the continuum limit exists, is unique, and is computable. The library proves it for all real mode directions and all bucket amplitudes, with no hidden regularity assumptions beyond the standard ones.

In Recognition Science, this continuum limit is one step in a larger chain that connects discrete recognition events to continuous physical laws. The framework models gravity as a lattice of buckets, each recording a phase, and this theorem shows that the macroscopic limit of that lattice is a smooth cosine law. It is a bridge between the discrete ledger of recognition events and the continuous geometry of spacetime, and it is a proved bridge, not a heuristic one.

THEOREM canonicalFiniteH_div_momentumNormSq_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
canonicalFiniteH_div_momentumNormSq_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:275 
/-- FINAL P1.1a HEADLINE: for every fixed nonzero integer mode, the actual
finite reduced Regge symbol, divided by `momentumNormSq`, converges to exactly
the raw Regge TT moment at the normalized real mode direction.  The literal
phase remains `(sum_i x_i * (u_i / 2))^2`. -/
theorem canonicalFiniteH_div_momentumNormSq_tendsto (E : Fin 3 → Fin 3 → ℝ)
    (m : Fin 3 → ℤ) (hm : ∃ i : Fin 3, m i ≠ 0) :
    Filter.Tendsto
      (fun j : ℕ =>
        @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m /
          momentumNormSq (j + 3) m)
      Filter.atTop
      (nhds
        (reggeTTMoment rawCosineSupport
          (rawPhaseQuadratic (normalizedRealMode m))
          (rawBucketAmplitude E))) := by
  let x : Fin 3 → ℝ := fun i => (m i : ℝ)
  let s : ℝ := realModeNormSq x
  have hs : 0 < s := realModeNormSq_intCast_pos m hm
  have hq0 :
      Filter.Tendsto (fun j : ℕ => sideScale (j + 3))
        Filter.atTop (nhds 0) := by
    have h :=
      (tendsto_const_div_atTop_nhds_zero_nat (2 * Real.pi)).comp
        (Filter.tendsto_add_atTop_nat 3)
    exact h.congr fun j => rfl
  have hqmem :
      ∀ᶠ j : ℕ in Filter.atTop,
        sideScale (j + 3) ∈ ({0}ᶜ : Set ℝ) := by
    filter_upwards with j
    have hden : ((j + 3 : ℕ) : ℝ) ≠ 0 := by positivity
    have hnum : (2 * Real.pi : ℝ) ≠ 0 := mul_ne_zero two_ne_zero Real.pi_ne_zero
    simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
    exact div_ne_zero hnum hden
  have hq :
      Filter.Tendsto (fun j : ℕ => sideScale (j + 3))
        Filter.atTop (nhdsWithin 0 {(0 : ℝ)}ᶜ) :=
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hq0 hqmem
  have hscale :=
    (rawCosineFold_scale_tendsto x E).comp hq
  have hdiv := hscale.div_const s
  have hlimit :
      Filter.Tendsto
        (fun j : ℕ =>
          rawCosineFoldAtScale (sideScale (j + 3)) x E /
              sideScale (j + 3) ^ (2 : ℕ) / s)
        Filter.atTop
        (nhds
          (reggeTTMoment rawCosineSupport
            (rawPhaseQuadratic (normalizedRealMode m))
            (rawBucketAmplitude E))) := by
    rw [show normalizedRealMode m =
        fun i => x i / Real.sqrt (realModeNormSq x) by
      funext i
      rfl]
    rw [reggeTTMoment_normalized x hs E]
    simpa [s] using hdiv
  have hshift : Filter.Tendsto (fun j : ℕ => j + 3)
      Filter.atTop Filter.atTop := Filter.tendsto_add_atTop_nat 3
  have hassembly :=
    hshift.eventually
      (eventually_canonicalFiniteH_eq_rawCosineBlochFold E m hm)
  refine hlimit.congr' ?_
  filter_upwards [hassembly] with j hj
  specialize hj (instNeZeroAddThree j)
  rw [hj, momentumNormSq_eq_scale_sq]
  unfold rawCosineFoldAtScale reggeTTBlochFold
  rw [div_div]
  have hsum_eq :
      (∑ b ∈ rawCosineSupport,
          rawCosineEvaluatorAtScale (sideScale (j + 3)) x b *
            rawBucketAmplitude E b) =
        ∑ b ∈ rawCosineSupport,
          rawCosineEvaluator (j + 3) m b * rawBucketAmplitude E b := by
    refine Finset.sum_congr rfl fun b _ => ?_
    rw [rawCosineEvaluator_eq_scale]
  rw [hsum_eq]
THEOREM cos_sub_one_div_sq_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
cos_sub_one_div_sq_tendsto · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:119 
/-- Local cosine two-jet obtained from the reusable centered-second-difference
theorem of the finite-symbol existence stage. -/
theorem cos_sub_one_div_sq_tendsto (a : ℝ) :
    Filter.Tendsto
      (fun q : ℝ => (Real.cos (q * a) - 1) / q ^ (2 : ℕ))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds (-(a ^ (2 : ℕ)) / 2)) := by
  have hC2 : ContDiffAt ℝ 2 (fun q : ℝ => Real.cos (a * q)) 0 :=
    (Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)).contDiffAt
  have hcenter :=
    ReggeTTLocalSymbolExistence.tendsto_centeredSecondDifference_of_contDiffAt
      (fun q : ℝ => Real.cos (a * q)) hC2
  rw [iteratedDeriv_two_cos_mul a] at hcenter
  have hhalf := hcenter.const_mul (1 / 2 : ℝ)
  have heq :
      (fun q : ℝ => (Real.cos (q * a) - 1) / q ^ (2 : ℕ)) =
        fun t : ℝ =>
          1 / 2 *
            (((fun q : ℝ => Real.cos (a * q)) t -
                2 * (fun q : ℝ => Real.cos (a * q)) 0 +
                (fun q : ℝ => Real.cos (a * q)) (-t)) / t ^ (2 : ℕ)) := by
    funext t
    simp only [mul_zero, Real.cos_zero, mul_neg, Real.cos_neg, mul_comm t a]
    ring
  rw [heq, show -(a ^ (2 : ℕ)) / 2 = 1 / 2 * -(a ^ (2 : ℕ)) by ring]
  exact hhalf
THEOREM rawCosineFoldAtScale_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
rawCosineFoldAtScale_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:63 
/-- The scale-zero raw cosine fold is the assembled constant block and hence
vanishes.  This consumes the hinge-aware assembled zero-mode theorem, not a
stencil-only cancellation. -/
theorem rawCosineFoldAtScale_zero (x : Fin 3 → ℝ)
    (E : Fin 3 → Fin 3 → ℝ) :
    rawCosineFoldAtScale 0 x E = 0 := by
  have hfold :=
    rawCosineFold_eq_rawTripleSum (N := 1) E (fun _ => (0 : ℤ))
  have heval :
      rawCosineFoldAtScale 0 x E =
        reggeTTBlochFold rawCosineSupport
          (@rawCosineEvaluator 1 (by infer_instance) (fun _ => (0 : ℤ)))
          (rawBucketAmplitude E) := by
    unfold rawCosineFoldAtScale reggeTTBlochFold
    refine Finset.sum_congr rfl fun b _ => ?_
    simp [rawCosineEvaluatorAtScale, rawPhaseLinear, rawCosineEvaluator,
      commensurateMomentum]
  rw [heval, hfold]
  have hone : ∀ p : Fin 6 × Fin 6 × Fin 6,
      rawCosineEvaluator 1 (fun _ => (0 : ℤ)) (bucketKeyOf p) = 1 := by
    intro p
    unfold rawCosineEvaluator commensurateMomentum
    norm_num
  have hsum :
      (∑ p : Fin 6 × Fin 6 × Fin 6,
        rawCosineEvaluator 1 (fun _ => (0 : ℤ)) (bucketKeyOf p) *
          rawTripleWeight E p) = assembledConstantBlock E := by
    unfold assembledConstantBlock rawTripleWeight
    rw [Fintype.sum_prod_type]
    simp_rw [Fintype.sum_prod_type, hone, one_mul, Finset.sum_neg_distrib]
  rw [hsum]
  exact assembledConstantBlock_eq_zero E

What this page does not claim

This module does not prove that gravity itself is continuous in the physical world. The continuum limit here is a mathematical convergence result, not a derivation of Einstein's field equations. The theorem does not apply to zero modes, which are excluded by the nonzero condition.

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