Gravity Analysis Regge Exact Flat Hessian Bloch Tendsto4 D Centered Trig Poly M2

The cosine two-jet

In classical analysis, the second derivative of a function measures its curvature at a point. For a sum of cosine terms, the second derivative at zero is a weighted sum of negative squared frequencies. The declaration centeredTrigPolyM2 packages that fact as a finite sum: for a finite set of indices, each with a weight and a frequency, it forms the sum of weight times negative frequency squared over two.

The mathematical content is a limit, proved in the framework's machine-checked library of formal theorems. Take a finite weighted sum of terms of the form cos(t times frequency) minus 1, divide by t squared, and let t approach zero from either side, but never equal zero. The quotient converges to the two-jet sum. This is the classical Taylor expansion of cosine at zero, stated as a limit rather than as a derivative. The proof uses the standard identity cos(2θ) − 1 = −2 sin²θ and the fact that sin θ over θ tends to 1.

The result matters because it lets a later step replace a trigonometric expression by its quadratic approximation near zero, with the error vanishing as t squared. It is a reusable lemma, not a physical claim. It does not assert anything about gravity, the Bloch symbol, or the Regge action. It does not prove the second derivative exists in a new sense; it proves the limit equals the expected quadratic form for these finite sums.

In Recognition Science, this lemma serves the exact midpoint Bloch symbol route, a path in the framework's gravity analysis that avoids a large coupling table. The library keeps the lemma separate from that table, so the limit result stands on its own. What the declaration establishes is a clean analytical fact: the centered trigonometric polynomial divided by t squared tends to its cosine two-jet. What it does not claim is any physical interpretation of that limit.

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

def centeredTrigPolyM2 {ι : Type*} (w θ : ι → ℝ) (s : Finset ι) : ℝ :=
  ∑ i ∈ s, w i * (-(θ i) ^ 2 / 2)

What this page does not claim

The declaration does not claim any physical meaning for the limit. It does not prove the second derivative exists in a new sense. It does not assert anything about the Regge action or gravity.

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: