Gravity Analysis Regge Bloch M2 Tendsto4 D Fold Along M2 Tendsto Axis Ttplus Hol

The closing of a limit

In the framework's discrete model of gravity, space is built from flat building blocks hinged along edges. A recognition event, a discrete record of geometric comparison, assigns a number to each hinge. The quantity foldAlong sums these numbers over all hinges for a given configuration. The declaration FoldAlongM2Tendsto_axisTTPlus_holds proves a limit statement: as a scale parameter μ approaches zero, the ratio foldAlong divided by μ² tends to a finite value, for a specific configuration called axisTTPlus.

The proof works through a cosine two-jet expansion. Each hinge contribution is a cosine of μ times a phase. The theorem tendsto_foldAlong_div_sq shows that if the zeroth-order term of the deficit kernel vanishes for every hinge, then the ratio converges. For axisTTPlus, the kernel vanishing is already proved as kerAlong_axis_zero. The declaration assembles these pieces: it applies the general limit theorem to the axisTTPlus configuration, using the established vanishing to satisfy the hypothesis. The result is a closed, punctured limit statement for that configuration.

The declaration does not claim the limit for arbitrary configurations. It specifically closes the limit for two polarizations: axisTTPlus and decoyGauge, the latter proved separately. A general configuration H remains an open named proposition, not a proved theorem. The statement also does not interpret the finite limit value physically; it establishes the mathematical convergence, not what the limit means for the discrete gravity model.

theorem FoldAlongM2Tendsto_axisTTPlus_holds :
    FoldAlongM2Tendsto_axisTTPlus :=
  (FoldAlongM2Tendsto_axis_iff).mp FoldAlongM2Tendsto_of_axisTTPlus

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

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)

What this page does not claim

The limit is not proved for arbitrary configurations, only for axisTTPlus and decoyGauge. The declaration does not assign physical meaning to the finite limit value. No claim is made about the behavior of the ratio for configurations where the kernel does not vanish at zero scale.

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: