Encyclopedia Gravity Gravity Analysis Regge Bloch M2 Tendsto4 D

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Bloch M2 Tendsto4 D

A machine-checked proof that two special polarizations of a lattice gravity model have a well-defined small-momentum limit, a technical step toward a physical continuum.

Verify this page

The second-order limit

Regge calculus is a discrete approach to general relativity in which spacetime is built from flat triangular pieces, and curvature lives only along the hinges where those pieces meet. The module ReggeBlochM2Tendsto4D studies a four-dimensional version of this setup, but with an important twist: the geometry is probed by a wave of momentum μ (a small oscillation parameter) along a fixed direction. The question is whether the discrete gravitational action has a sensible limit as that momentum goes to zero, the limit that would define a continuum theory.

The answer is yes, but only for two special configurations. The module proves that for the polarization called axisTTPlus (a traceless, transverse metric fluctuation) and for the pure gauge mode decoyGauge (a deformation that does not change the physical geometry), the ratio of the discrete action to the square of the momentum converges to a finite number as the momentum vanishes. The machine-checked library of formal theorems establishes this limit by showing that the leading term in the action is quadratic in momentum, with a coefficient that is a sum over the 15 independent components of the metric perturbation.

The proof works by isolating the part of the action that vanishes at zero momentum, then showing that this part is proportional to the square of momentum, so dividing by that square leaves a finite remainder. The key lemma, tendsto_foldAlong_div_sq, states that the total action along the momentum direction, divided by μ², tends to a specific constant m2Symbol. The module then verifies this for the two named configurations by checking that their deficit kernels, the objects measuring curvature, vanish at zero momentum, which is the condition needed for the limit to exist.

In Recognition Science, this is a step in a larger program: the framework derives physics from a discrete ledger of recognition events, and Regge calculus is one candidate for how that discrete structure becomes the smooth geometry of general relativity. The module does not claim that the full theory has a continuum limit for all configurations; that remains an open problem. It establishes the limit only for the two special polarizations, and the general case is left as a named proposition in the source code.

The practical consequence is that these two modes are the ones that can be consistently extended to small momenta, which is a necessary condition for them to describe physical gravitons or gauge degrees of freedom in a continuum approximation. The proof is a formal, machine-checked result, meaning it does not rely on hand-waving or numerical approximation. It is a theorem in the framework's library, with the full chain of reasoning verified by a computer.

THEOREM FoldAlongM2Tendsto_of_axisTTPlus · FoldAlongM2Tendsto_of_decoyGauge · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean
FoldAlongM2Tendsto_of_axisTTPlus · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:246 
theorem FoldAlongM2Tendsto_of_axisTTPlus :
    FoldAlongM2Tendsto axisTTPlus := by
  unfold FoldAlongM2Tendsto
  exact tendsto_foldAlong_div_sq axisTTPlus fun s t => kerAlong_axis_zero s t
FoldAlongM2Tendsto_of_decoyGauge · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:251 
theorem FoldAlongM2Tendsto_of_decoyGauge :
    FoldAlongM2Tendsto decoyGauge := by
  unfold FoldAlongM2Tendsto
  exact tendsto_foldAlong_div_sq decoyGauge fun s t => kerAlong_gauge_zero s t
THEOREM tendsto_foldAlong_div_sq · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean
tendsto_foldAlong_div_sq · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:217 
theorem tendsto_foldAlong_div_sq (H : Mat4)
    (h0 : ∀ s t, kerAlong H s t 0 = 0) :
    Tendsto (fun μ : ℝ => foldAlong H μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
      (𝓝 (m2Symbol H)) := by
  have hsum :
      Tendsto
        (fun μ : ℝ =>
          ∑ s : Fin 24, ∑ t : Fin 10,
            transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2)
        (𝓝[≠] (0 : ℝ))
        (𝓝 (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCoeff H s t)) := by
    apply tendsto_finset_sum
    intro s _
    apply tendsto_finset_sum
    intro t _
    exact tendsto_transportedSlotTerm_div_sq H s t (h0 s t)
  have hcongr :
      (fun μ : ℝ => foldAlong H μ / μ ^ 2) =ᶠ[𝓝[≠] (0 : ℝ)]
        fun μ : ℝ =>
          ∑ s : Fin 24, ∑ t : Fin 10,
            transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2 := by
    filter_upwards [self_mem_nhdsWithin] with μ hμ
    have hne : μ ≠ 0 := hμ
    unfold foldAlong blochFold11
    rw [Finset.sum_div]
    refine Finset.sum_congr rfl fun s _ => ?_
    rw [Finset.sum_div]
  exact (tendsto_congr' hcongr).mpr (by simpa [m2Symbol] using hsum)
THEOREM tendsto_kerAlong_div_sq · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean
tendsto_kerAlong_div_sq · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:81 
theorem tendsto_kerAlong_div_sq (H : Mat4) (s : Fin 24) (t : Fin 10)
    (h0 : kerAlong H s t 0 = 0) :
    Tendsto (fun μ : ℝ => kerAlong H s t μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
      (𝓝 (kerM2Coeff H s t)) := by
  have hcongr :
      (fun μ : ℝ => kerAlong H s t μ / μ ^ 2) =ᶠ[𝓝[≠] (0 : ℝ)]
        fun μ : ℝ =>
          ∑ d : Fin 15,
            (slotDeficitKer s t d * classCoeff H d) *
              ((Real.cos (μ * phaseScale (hingeBase s t) d) - 1) / μ ^ 2) := by
    filter_upwards [self_mem_nhdsWithin] with μ hμ
    have hne : μ ≠ 0 := hμ
    have hK := kerAlong_eq H s t μ
    have hsum0 : kerAlong H s t 0 = 0 := h0
    rw [kerAlong_zero] at hsum0
    have hrewrite :
        kerAlong H s t μ / μ ^ 2 =
          (∑ d : Fin 15,
              slotDeficitKer s t d * classCoeff H d *
                (Real.cos (μ * phaseScale (hingeBase s t) d) - 1)) / μ ^ 2 := by
      rw [hK]
      have hsub :
          (∑ d : Fin 15,
              slotDeficitKer s t d * classCoeff H d *
                Real.cos (μ * phaseScale (hingeBase s t) d)) -
            (∑ d : Fin 15, slotDeficitKer s t d * classCoeff H d) =
          ∑ d : Fin 15,
            slotDeficitKer s t d * classCoeff H d *
              (Real.cos (μ * phaseScale (hingeBase s t) d) - 1) := by
        simp [Finset.sum_sub_distrib, mul_sub]
      calc
        (∑ d : Fin 15,
              slotDeficitKer s t d * classCoeff H d *
                Real.cos (μ * phaseScale (hingeBase s t) d)) / μ ^ 2
            =
          ((∑ d : Fin 15,
                slotDeficitKer s t d * classCoeff H d *
                  Real.cos (μ * phaseScale (hingeBase s t) d)) -
              (∑ d : Fin 15, slotDeficitKer s t d * classCoeff H d)) /
            μ ^ 2 := by rw [hsum0, sub_zero]
        _ = (∑ d : Fin 15,
                slotDeficitKer s t d * classCoeff H d *
                  (Real.cos (μ * phaseScale (hingeBase s t) d) - 1)) /
            μ ^ 2 := by rw [hsub]
    rw [hrewrite, Finset.sum_div]
    refine Finset.sum_congr rfl fun d _ => ?_
    field_simp [hne]
  have hsum :
      Tendsto
        (fun μ : ℝ =>
          ∑ d : Fin 15,
            (slotDeficitKer s t d * classCoeff H d) *
              ((Real.cos (μ * phaseScale (hingeBase s t) d) - 1) / μ ^ 2))
        (𝓝[≠] (0 : ℝ))
        (𝓝
          (∑ d : Fin 15,
            (slotDeficitKer s t d * classCoeff H d) *
              (-(phaseScale (hingeBase s t) d) ^ 2 / 2))) := by
    apply tendsto_finset_sum
    intro d _
    exact
      (cos_sub_one_div_sq_tendsto (phaseScale (hingeBase s t) d)).const_mul _
  have htarget :
      (∑ d : Fin 15,
          (slotDeficitKer s t d * classCoeff H d) *
            (-(phaseScale (hingeBase s t) d) ^ 2 / 2)) =
        kerM2Coeff H s t := by
    unfold kerM2Coeff
    simp [div_eq_mul_inv, Finset.mul_sum, mul_left_comm, mul_assoc, mul_comm]
  rw [← htarget]
  exact (tendsto_congr' hcongr).mpr hsum

What this page does not claim

The module does not prove a continuum limit for general metric perturbations, only for the two named polarizations. The module does not derive the fine-structure constant or any other specific physical constant. The module does not claim that Regge calculus is the unique discrete approach to gravity within Recognition Science.

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/ReggeBlochM2Tendsto4D.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