Gravity Analysis Regge Exact Flat Hessian Bloch Tendsto4 D Cos Sub One Div Sq Te

A cosine limit

The declaration cos_sub_one_div_sq_tendsto is a theorem about a standard trigonometric limit. For any real number a, it states that as q approaches zero (but never equals zero), the expression (cos(q a) - 1) / q² approaches -a²/2. This is a classical result from real analysis, closely related to the second-order Taylor expansion of cosine: cos(x) ≈ 1 - x²/2 for small x. The theorem formalizes this approximation as a precise limit statement, using the standard Tendsto predicate from the Mathlib library.

The proof is short and self-contained. It first rewrites cos(2θ) - 1 as -2 sin²(θ) using the double-angle identity, then applies the Pythagorean identity sin²+cos²=1, and finishes with a nonlinear arithmetic step. The result is a clean, reusable lemma that does not depend on any framework-specific axioms; it is pure mathematics about real numbers and limits.

In the context of the Recognition Science framework's gravity analysis, this lemma is a building block. The file it lives in also defines a centered trigonometric polynomial, a finite sum of terms w_i * (cos(t θ_i) - 1), and proves that dividing this polynomial by t² tends to a limit as t approaches zero. That limit is the sum of w_i * (-θ_i²/2), which is the quadratic term of the polynomial's Taylor expansion. A further lemma handles division by a nonzero constant n. Together, these results form what the file's docstring calls an "exact midpoint Bloch symbol route" toward analyzing a flat Hessian in four dimensions.

What the declaration does not claim is equally important. It does not prove anything about gravity, curvature, or the physical meaning of the Bloch symbol. It is a purely analytic statement about real-valued functions. The connection to the Regge exact flat Hessian is a research direction that this lemma supports, not a conclusion it establishes. The theorem itself says nothing about the framework's core cost function, the golden ratio, or any physical constant.

For a reader encountering this in an encyclopedia, the practical takeaway is simple: this is a rigorously verified limit from undergraduate calculus, packaged for reuse in a larger formal development. Its value lies in being a reliable, machine-checked step that later arguments can build upon without re-deriving the trigonometry each time.

/-- `(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 theorem does not establish any physical claim about gravity or curvature. It does not prove the existence or properties of the Bloch symbol itself. It makes no statement about the framework's cost function or physical constants.

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: