Encyclopedia Gravity Gravity Analysis Regge Ttcontinuum Limit Canonical Finite H Div Momentum Norm Sq

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttcontinuum Limit Canonical Finite H Div Momentum Norm Sq

A finite approximation to a gravity amplitude converges to a clean continuous formula as the grid refines, and the proof is machine-checked.

Verify this page

The continuum limit

In numerical work on gravity, one often replaces continuous space with a fine grid. The question is whether a quantity computed on the grid settles down to a definite value as the grid spacing shrinks to zero. The declaration canonicalFiniteH_div_momentumNormSq_tendsto answers this for a specific object: a reduced Regge symbol, which is a discrete building block used in Regge calculus, a lattice approach to general relativity. The theorem states that when you take the finite symbol, divide by the squared norm of the momentum, and let the grid size grow, the result converges to a particular continuous limit.

The limit is not an arbitrary number. It is exactly the Regge TT moment, a continuous expression, evaluated at the normalized real mode direction. The direction is obtained by taking an integer momentum mode and scaling it to unit Euclidean length. The theorem holds for every fixed nonzero integer mode, meaning the mode must have at least one nonzero component. The convergence is in the standard topological sense: the sequence of finite values approaches the limit arbitrarily closely as the grid size tends to infinity.

The proof is notable for its structure. It works in stages. First, it shows that the raw cosine fold, a finite sum over grid cells, divided by the square of a continuous scale parameter, tends to the Regge TT moment. This is the reusable continuous-variable headline. Then it connects the discrete grid scale to this continuous parameter, showing that the commensurate momentum evaluator is exactly the free-scale evaluator at the specific scale 2π/N. Finally, it factors the momentum normalization into the scale squared times the integer-mode norm squared, which allows the division to be moved to the right place. The whole chain is formalized in a machine-checked library of formal theorems, so the result is verified by computer, not just argued informally.

What the theorem does not claim is equally important. It does not assert that the finite Regge symbol itself converges to the continuous moment. It only claims convergence after division by the squared momentum norm. Without that normalization, the finite quantity may diverge or behave differently as the grid refines. The theorem also does not address the physical interpretation of the limit, such as whether it corresponds to a classical gravitational observable. It is a mathematical statement about a specific sequence of finite approximations, not a physical claim about the nature of spacetime.

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 reggeTTMoment_normalized · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
reggeTTMoment_normalized · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:223 
/-- `reggeTTMoment` is homogeneous under direction normalization with the
expected inverse squared-norm factor. -/
theorem reggeTTMoment_normalized (x : Fin 3 → ℝ)
    (hx : 0 < realModeNormSq x) (E : Fin 3 → Fin 3 → ℝ) :
    reggeTTMoment rawCosineSupport
        (rawPhaseQuadratic
          (fun i => x i / Real.sqrt (realModeNormSq x)))
        (rawBucketAmplitude E) =
      reggeTTMoment rawCosineSupport (rawPhaseQuadratic x)
        (rawBucketAmplitude E) / realModeNormSq x := by
  unfold reggeTTMoment reggeTTBlochFold
  rw [Finset.sum_div]
  refine Finset.sum_congr rfl fun b _ => ?_
  show
    -rawPhaseQuadratic (fun i => x i / Real.sqrt (realModeNormSq x)) b / 2 *
        rawBucketAmplitude E b =
      -rawPhaseQuadratic x b / 2 * rawBucketAmplitude E b / realModeNormSq x
  rw [rawPhaseQuadratic_normalized x hx b]
  field_simp [hx.ne']
THEOREM realModeNormSq_intCast_pos · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
realModeNormSq_intCast_pos · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:243 
/-- A nonzero integer mode has positive real squared norm. -/
theorem realModeNormSq_intCast_pos (m : Fin 3 → ℤ)
    (hm : ∃ i : Fin 3, m i ≠ 0) :
    0 < realModeNormSq (fun i => (m i : ℝ)) := by
  obtain ⟨i, hi⟩ := hm
  unfold realModeNormSq
  have hi' : (m i : ℝ) ≠ 0 := by exact_mod_cast hi
  exact Finset.sum_pos' (fun j _ => sq_nonneg (m j : ℝ))
    ⟨i, Finset.mem_univ i, sq_pos_of_ne_zero hi'⟩
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 the finite Regge symbol converges without the momentum norm division. It does not claim any physical interpretation of the limit as a classical gravitational observable. It does not claim convergence for modes with zero norm.

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