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

The limit theorem

The theorem tendsto_foldAlong_div_sq is a statement about a quantity called foldAlong, which is a discrete record of how a geometric structure, a Regge spacetime, responds to a small deformation. The theorem says that if you take this quantity, divide it by the square of the deformation size, and let the deformation size shrink to zero, the result approaches a specific finite number. That number is called m2Symbol, and it is the second-order coefficient of the deformation, the part that tells you how the structure bends at the smallest scale.

The proof is not a numerical experiment. It is a formal argument checked by a machine, which means every step follows from the rules of logic. The argument uses a known fact about the cosine function, which describes how the deformation oscillates, and a separate fact that the deformation's effect vanishes at zero size for two special directions. The theorem is stated for any deformation that satisfies a certain condition: the effect must vanish at zero size. It then applies to two particular cases, one called axisTTPlus and one called decoyGauge, which are two specific choices of the deformation direction.

The theorem does not claim that the limit exists for every possible deformation. It only covers the two named directions, and for those it shows the limit is finite and equal to the second-order coefficient. It also does not say that the second-order coefficient is zero or nonzero; it only says that the ratio approaches it. The theorem is a precise statement about a mathematical limit, not a physical law about gravity itself. It is a step in a larger program that aims to show how gravity emerges from a discrete structure, but this particular theorem only establishes a technical fact about the limit of a ratio.

In plain terms, the theorem is a guarantee: if you measure the response of the structure to a tiny deformation, and you scale that response by the square of the deformation size, you will get a well-defined answer, and that answer is the second-order coefficient. This is useful because it means the second-order behavior is stable and can be computed reliably. The theorem does not tell you what the second-order coefficient is for any specific case, only that the limit exists and equals it. It is a foundational piece, not a final result.

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 FoldAlongM2Tendsto_of_axisTTPlus :
    FoldAlongM2Tendsto axisTTPlus := by
  unfold FoldAlongM2Tendsto
  exact tendsto_foldAlong_div_sq axisTTPlus fun s t => kerAlong_axis_zero s t

theorem FoldAlongM2Tendsto_of_decoyGauge :
    FoldAlongM2Tendsto decoyGauge := by
  unfold FoldAlongM2Tendsto
  exact tendsto_foldAlong_div_sq decoyGauge fun s t => kerAlong_gauge_zero s t

What this page does not claim

The theorem does not claim that the limit exists for all possible deformations. The theorem does not state the value of the second-order coefficient for any specific case. The theorem does not establish a physical law of gravity; it only proves a mathematical limit.

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: