Encyclopedia Gravity Gravity Analysis Regge Ttcontinuum Limit Momentum Norm Sq Eq Scale Sq

ARTICLE 2 claims 2 theorems

Gravity Analysis Regge Ttcontinuum Limit Momentum Norm Sq Eq Scale Sq

A formal theorem in the Recognition Science library factors the squared momentum of a lattice mode into a scale factor and the mode's squared length, a step toward showing how discrete structures recover continuous gravity.

Verify this page

Momentum normalization

In lattice gravity, a mode is a pattern of displacements on a discrete grid, and its momentum is a measure of how rapidly that pattern oscillates. The declaration momentumNormSq_eq_scale_sq establishes an exact algebraic identity: the squared momentum of any integer-valued mode equals the square of a scale factor times the squared Euclidean norm of the mode's real direction. The scale factor is 2π/N, where N is the side length of the lattice, and the norm is the ordinary sum of squares of the mode's three components. This is a theorem in the framework's machine-checked library of formal theorems, proved for every nonzero side length N and every integer mode.

The identity is the algebraic hinge that lets the framework pass from a finite lattice to a continuous limit. Dividing the finite Regge symbol by this momentum normalization, and letting N grow, the theorem canonicalFiniteH_div_momentumNormSq_tendsto shows the quotient converges to a continuous object: the raw Regge transverse-traceless moment evaluated at the normalized real mode direction. The proof combines the exact factorization with a cosine two-jet limit, where the cosine's second derivative at zero supplies the quadratic phase. The result is that the discrete lattice's momentum normalization exactly matches the continuous scale squared, so the continuum limit is not an approximation but an identity in the limit.

What the declaration does not claim is that this momentum normalization is the physical momentum of a graviton or any observed particle. It is a formal statement about a specific lattice construction in the framework's gravity analysis, not a measurement or a prediction. The theorem also does not assert that the continuum limit exists for all modes; it requires the mode to be nonzero, and it concerns the normalized quotient, not the raw symbol itself. The declaration is a step in a longer derivation, not a standalone physical law.

THEOREM momentumNormSq_eq_scale_sq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean
momentumNormSq_eq_scale_sq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean:265 
/-- Exact factorization of the momentum normalization into scale squared
times the integer-mode norm squared. -/
theorem momentumNormSq_eq_scale_sq (N : ℕ) [NeZero N]
    (m : Fin 3 → ℤ) :
    momentumNormSq N m =
      sideScale N ^ (2 : ℕ) * realModeNormSq (fun i => (m i : ℝ)) := by
  unfold momentumNormSq commensurateMomentum sideScale realModeNormSq
  simp only [Fin.sum_univ_three]
  ring
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]

What this page does not claim

This momentum normalization is the physical momentum of a graviton or any observed particle. The continuum limit exists for all modes without the nonzero condition. The theorem establishes the existence of gravity as a physical force.

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