Encyclopedia Gravity Gravity Analysis Regge Bloch M2 Tendsto4 D Tendsto Ker Along Div Sq

ARTICLE 3 claims 2 theorems 1 model

Gravity Analysis Regge Bloch M2 Tendsto4 D Tendsto Ker Along Div Sq

A machine-checked theorem shows how a discrete gravitational defect kernel vanishes at zero momentum, and names the exact coefficient of its leading quadratic behavior.

Verify this page

The second-order limit

In the study of discrete gravity, a ledger (a discrete record of geometric events) assigns to each small region a number measuring how much the local geometry fails to close flat. The declaration tendsto_kerAlong_div_sq concerns the behavior of this deficit kernel as a momentum parameter μ approaches zero. It proves that if the kernel vanishes at μ = 0, then the ratio of the kernel to μ² converges to a specific constant, called kerM2Coeff, as μ tends to zero.

This is a second-order Taylor expansion result. The kernel is a smooth function of μ built from cosine terms, and the theorem states that its leading quadratic coefficient is exactly kerM2Coeff, a sum over 15 components of the product of the deficit kernel slot, the class coefficient, and the squared phase scale. The proof uses the cosine two-jet expansion and the already-established zero-momentum vanishing on two special polarizations: the axis TT plus state and the decoy gauge state.

In Recognition Science, this result closes the punctured limit for those two polarizations, meaning the behavior of the kernel near zero momentum is fully characterized to second order. The theorem is part of a chain that analyzes how the deficit kernel behaves under a Bloch momentum ansatz, a periodic wave-like modulation. It does not claim that the kernel vanishes for all polarizations, nor does it establish anything about the full symbol H, which remains a named proposition in the framework's library.

The practical consequence is that for these two specific polarizations, the second-order behavior of the deficit kernel is exactly known and machine-checked, providing a rigorous foundation for further analysis of the gravitational action's small-momentum limit. The general case, where the kernel does not vanish at zero, remains an open target.

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
THEOREM kerAlong_axis_zero · kerAlong_gauge_zero · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean
kerAlong_axis_zero · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:64 
theorem kerAlong_axis_zero (s : Fin 24) (t : Fin 10) :
    kerAlong axisTTPlus s t 0 = 0 := by
  rw [kerAlong_zero]
  simpa [classDot] using classDot_slotDeficitKer_axis s t
kerAlong_gauge_zero · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:69 
theorem kerAlong_gauge_zero (s : Fin 24) (t : Fin 10) :
    kerAlong decoyGauge s t 0 = 0 := by
  rw [kerAlong_zero]
  simpa [classDot] using classDot_slotDeficitKer_gauge s t
MODEL kerM2Coeff · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean
kerM2Coeff · IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean:74 
/-- Formal second-jet coefficient of `kerAlong` after using `K(0)=0`. -/
def kerM2Coeff (H : Mat4) (s : Fin 24) (t : Fin 10) : ℝ :=
  -(1 / 2 : ℝ) *
    ∑ d : Fin 15,
      slotDeficitKer s t d * classCoeff H d *
        (phaseScale (hingeBase s t) d) ^ 2

What this page does not claim

The theorem does not claim the deficit kernel vanishes for all polarizations. The theorem does not establish the behavior of the full symbol H, which remains an open proposition. The theorem does not provide a physical interpretation of the constant kerM2Coeff.

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