Gravity Analysis Regge Exact Flat Hessian Bloch Tendsto4 D

The flat-space limit

In general relativity, gravity is not a force but the curvature of spacetime. A key test of any theory of gravity is that it reproduces the simpler physics of flat space when you look at a small enough region. The mathematical tool for this is the Taylor expansion: near any point, a smooth curved surface can be approximated by its tangent plane, and the error shrinks quadratically as you zoom in. This result proves a precise version of that fact for a special family of trigonometric functions used in the framework's analysis of the Regge action, a discretized form of the Einstein-Hilbert action.

The central result is a limit statement. For any real number a, the expression (cos(q a) - 1) / q² approaches -a²/2 as q tends to zero. This is exactly the second-order Taylor coefficient of the cosine function: cos(x) ≈ 1 - x²/2 for small x. The proof uses only standard real analysis: the double-angle identity for cosine, the Pythagorean identity, and the fact that squares are nonnegative. It is a small, self-contained lemma in the machine-checked library of formal theorems.

The result then generalizes this scalar statement to a finite sum of such terms, each weighted by a coefficient w_i and evaluated at a frequency θ_i. The object centeredTrigPoly is a sum over a finite index set of w_i times (cos(t θ_i) - 1). The theorem tendsto_centeredTrigPoly_div_sq states that this sum, divided by t², tends to the sum of w_i times (-θ_i²/2) as t approaches zero. This is the cosine two-jet: the quadratic part of the Taylor expansion of a trigonometric polynomial, extracted cleanly by a limit.

In Recognition Science, this lemma serves the exact midpoint Bloch symbol route, a technique for analyzing the Regge action in a flat-space limit. The framework models gravity through a discrete ledger of recognition events, and this result provides the analytic bridge that connects the discrete cosine structure to the continuous quadratic form of flat spacetime. The outcome is a formal proof, checked by the kernel, that the leading correction to flatness is indeed quadratic in the deviation parameter, with the correct coefficient -a²/2.

What this establishes in plain language: when you zoom in on curved spacetime, the curvature term vanishes quadratically, and the coefficient of that quadratic term is exactly what the Taylor expansion predicts. This is the mathematical guarantee that the discrete model's flat-space limit is the correct one, not an approximation but an exact statement about limits.

/-- `(cos(q a) - 1) / q² → -a²/2` on the punctured neighborhood of `0`. -/
theorem cos_sub_one_div_sq_tendsto (a : ℝ) :
    Tendsto (fun q : ℝ => (Real.cos (q * a) - 1) / q ^ 2)
      (𝓝[≠] (0 : ℝ)) (nhds (-(a ^ 2) / 2)) := by
  by_cases ha : a = 0
  · subst ha
    refine tendsto_const_nhds.congr' ?_
    filter_upwards [self_mem_nhdsWithin] with q hq
    have hq0 : q ≠ 0 := hq
    simp [Real.cos_zero, hq0]
  · have hcongr :
        (fun q : ℝ => (Real.cos (q * a) - 1) / q ^ 2) =ᶠ[𝓝[≠] (0 : ℝ)]
          fun q : ℝ => -(a ^ 2 / 2) * (Real.sinc (q * a / 2)) ^ 2 := by
      filter_upwards [self_mem_nhdsWithin] with q hq
      have hθ : (2 : ℝ) * (q * a / 2) = q * a := by ring
      have htrig := cos_sub_one_eq_neg_two_sin_sq (q * a / 2)
      rw [hθ] at htrig
      have hqa2 : q * a / 2 ≠ 0 :=
        div_ne_zero (mul_ne_zero hq ha) two_ne_zero
      have hstep :
          (-(2 * Real.sin (q * a / 2) ^ 2)) / q ^ 2 =
            -(a ^ 2 / 2) * (Real.sin (q * a / 2) / (q * a / 2)) ^ 2 := by
        field_simp [hq, ha, hqa2]
      calc
        (Real.cos (q * a) - 1) / q ^ 2
            = (-(2 * Real.sin (q * a / 2) ^ 2)) / q ^ 2 := by rw [htrig]
        _ = -(a ^ 2 / 2) * (Real.sin (q * a / 2) / (q * a / 2)) ^ 2 := hstep
        _ = -(a ^ 2 / 2) * (Real.sinc (q * a / 2)) ^ 2 := by
          rw [Real.sinc_of_ne_zero hqa2]

    let f : ℝ → ℝ := fun q => -(a ^ 2 / 2) * (Real.sinc ((a / 2) * q)) ^ 2
    have hfun :
        (fun q : ℝ => -(a ^ 2 / 2) * (Real.sinc (q * a / 2)) ^ 2) = f := by
      funext q; simp only [f]; ring_nf
    have hcont : Continuous f :=
      continuous_const.mul
        ((Real.continuous_sinc.comp (continuous_const.mul continuous_id)).pow 2)
    have hlim0 : Tendsto f (𝓝 (0 : ℝ)) (nhds (f 0)) := hcont.continuousAt.tendsto
    have hf0 : f 0 = -(a ^ 2 / 2) := by simp [f, Real.sinc_zero]
    have hlim :
        Tendsto (fun q : ℝ => -(a ^ 2 / 2) * (Real.sinc (q * a / 2)) ^ 2)
          (𝓝[≠] (0 : ℝ)) (nhds (-(a ^ 2 / 2))) := by
      rw [hfun, ← hf0]
      exact hlim0.mono_left nhdsWithin_le_nhds
    have htarget : (-(a ^ 2) / 2) = -(a ^ 2 / 2) := by ring
    rw [htarget]
    exact (tendsto_congr' hcongr).mpr hlim

/-- **THEOREM:** centered Finset trig poly `/ t²` tends to its cosine two-jet. -/
theorem tendsto_centeredTrigPoly_div_sq
    {ι : Type*} (w θ : ι → ℝ) (s : Finset ι) :
    Tendsto (fun t : ℝ => centeredTrigPoly w θ s t / t ^ 2)
      (𝓝[≠] (0 : ℝ)) (nhds (centeredTrigPolyM2 w θ s)) := by
  have hsum :
      Tendsto
        (fun t : ℝ =>
          ∑ i ∈ s, w i * ((Real.cos (t * θ i) - 1) / t ^ 2))
        (𝓝[≠] (0 : ℝ))
        (nhds (∑ i ∈ s, w i * (-(θ i) ^ 2 / 2))) := by
    refine tendsto_finset_sum s fun i _ =>
      (cos_sub_one_div_sq_tendsto (θ i)).const_mul (w i)
  have hcongr :
      (fun t : ℝ => centeredTrigPoly w θ s t / t ^ 2) =ᶠ[𝓝[≠] (0 : ℝ)]
        fun t : ℝ =>
          ∑ i ∈ s, w i * ((Real.cos (t * θ i) - 1) / t ^ 2) := by
    filter_upwards [self_mem_nhdsWithin] with t ht
    unfold centeredTrigPoly
    rw [Finset.sum_div]
    refine Finset.sum_congr rfl fun i _ => ?_
    field_simp [ht]
  exact (tendsto_congr' hcongr).mpr hsum

What this page does not claim

This result does not prove any property of the full Regge action or its dynamics. This result does not establish the physical connection between the discrete ledger and continuous spacetime. This result does not derive the Einstein field equations.

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/ReggeExactFlatHessianBlochTendsto4D.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: