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

Centered trigonometric sums

A trigonometric polynomial is a sum of cosine and sine terms. The object here, centeredTrigPoly, is a special one: it takes a finite list of angles, weights each cosine by a chosen coefficient, subtracts 1 from each cosine, and adds the results. Subtracting 1 centers each term so that at angle zero every term vanishes. The whole sum is a function of a real parameter t, and the question is what happens to the sum divided by t squared as t approaches zero.

The answer is a clean limit. For each angle a, the quotient (cos(t a) - 1) / t squared tends to -a squared / 2. This is the classical cosine two-jet: the constant term is 1, the linear term is 0, and the quadratic coefficient is -1/2. Summing over the finite index set with weights gives the limit of the whole centered sum divided by t squared: it is the weighted sum of -a squared / 2. The declaration centeredTrigPolyM2 records exactly that limiting expression, and the theorem tendsto_centeredTrigPoly_div_sq states the convergence. A second theorem handles division by an extra nonzero constant n, so the same limit holds for the sum divided by t squared times n.

The proof is short and uses only standard real analysis. The identity cos(2θ) - 1 = -2 sin² θ converts each cosine difference into a squared sine. Then the known limit sin θ / θ → 1 gives the quadratic behavior. The library file that contains these results is a reusable collection of lemmas for the exact midpoint Bloch symbol route in gravity analysis; it deliberately does not import a large coupling table, so the proof stays lightweight.

In Recognition Science, this lemma is a technical tool. It provides the leading quadratic behavior of a centered trigonometric sum near zero, which is the kind of estimate needed when analyzing the Hessian of a gravitational action in the exact flat regime. The framework's machine-checked library of formal theorems records this as a proved statement about real functions, not as a physical claim. The limit is a fact about calculus; what physical use the framework makes of it is a separate question.

What the declaration does not claim is just as important. It does not assert that any particular physical system obeys this limit; it only states a property of the defined sum. It does not claim the sum converges for all t, only that the quotient has a limit as t tends to zero through nonzero values. It does not say anything about the 1208-row coupling table that the file avoids importing. Those are separate matters.

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

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

private theorem cos_sub_one_eq_neg_two_sin_sq (θ : ℝ) :
    Real.cos (2 * θ) - 1 = -(2 * Real.sin θ ^ 2) := by
  have h : Real.cos (2 * θ) = 2 * Real.cos θ ^ 2 - 1 := Real.cos_two_mul (x := θ)
  have hs : Real.sin θ ^ 2 + Real.cos θ ^ 2 = 1 := Real.sin_sq_add_cos_sq θ
  nlinarith [sq_nonneg (Real.sin θ), sq_nonneg (Real.cos θ)]

What this page does not claim

The declaration does not assert that any physical system obeys this limit. The limit is only as t tends to zero through nonzero values, not for all t. The file does not import or use the 1208-row coupling table.

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: