Gravity Analysis Regge Bloch M2 Tendsto4 D Fold Along M2 Tendsto Of Decoy Gauge

A limit for a special gauge

In a discrete model of gravity, space is built from flat building blocks hinged along shared faces, and curvature shows up as a deficit angle where blocks meet. The Recognition Science framework studies a four-dimensional version of this setup. A key quantity, the fold, measures how the geometry responds when you look along a particular direction at ever finer scales. The theorem FoldAlongM2Tendsto_of_decoyGauge proves that for one specific choice of coordinates, called the decoy gauge, this fold divided by the square of the scale parameter has a well-defined limit as the scale goes to zero.

The proof rests on two ingredients. First, a general lemma shows that if the deficit kernel vanishes at zero scale, then the fold divided by the square of the scale does converge. Second, for the decoy gauge, that vanishing condition holds by a separate proved fact. The same argument also works for another special case, the axis TT polarization. Both are closed cases of a broader statement, FoldAlongM2Tendsto, which asks for the limit to exist for any choice of coordinates. That general property remains an open target in the library, not a proved theorem.

What the theorem does not claim is just as important. It does not say the limit exists for all configurations, only for these two named polarizations. It does not compute the value of the limit, only that it exists. And it does not assert anything about the physical meaning of the decoy gauge or the axis TT polarization beyond their role in this formal limit. The theorem is a technical result about convergence, not a statement about the nature of gravity.

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 (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

What this page does not claim

The limit exists for all coordinate choices, only for the two named polarizations. The theorem computes the numerical value of the limit. The theorem makes any statement about the physical meaning of the decoy gauge.

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: