Gravity Analysis Regge Exact Flat Hessian Bloch Tendsto4 D Tendsto Centered Trig

A limit for trig polynomials

In classical analysis, a Taylor expansion describes how a smooth function behaves near a point. For the cosine function, the expansion around zero is cos(x) = 1 - x²/2 + higher-order terms. The theorem in question is a precise, formalized version of this idea applied to a finite sum of such cosine terms.

The object under study is a finite sum of the form Σ wᵢ(cos(t·θᵢ) - 1), where wᵢ and θᵢ are real numbers and t is a real parameter. This is called a centered trig polynomial because each term is shifted so that it vanishes at t = 0. The theorem states that as t approaches zero (but is never equal to zero), this sum divided by t² tends to a specific finite limit: Σ wᵢ(-θᵢ²/2). In words, after dividing by t², the leading quadratic behavior of each cosine term is isolated and summed.

This result is proved in the framework's machine-checked library of formal theorems. The proof uses standard facts about cosine and sine, such as the double-angle identity, and does not rely on any framework-specific axioms. It is a statement about real analysis, not about physics or geometry directly.

In Recognition Science, this limit is a technical lemma, not a physical law. It appears in a route toward studying a certain Hessian, but the theorem itself only establishes a limit of a mathematical expression. It does not claim anything about gravity, spacetime, or the framework's cost function. The theorem's value is that it provides a clean, verified analytical step that can be used in larger arguments.

The practical consequence is that any argument needing this limit can cite it as a proved fact, rather than re-deriving it. It is a small but solid piece of the framework's analytical foundation. What it does not do is say anything about the physical meaning of the weights wᵢ or the angles θᵢ; those are left to other parts of the framework.

/-- **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

The theorem does not claim any physical law about gravity or spacetime. It does not establish the value of any framework constant or cost function. It does not assert that the limit exists for all real numbers, only on a punctured neighborhood of zero.

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: