Gravity Analysis Regge Exact Flat Hessian Bloch Tendsto4 D Cos Sub One Eq Neg Tw

A trigonometric identity

The declaration cos_sub_one_eq_neg_two_sin_sq establishes a familiar trigonometric identity: for any real number θ, the cosine of twice that number minus one equals negative two times the square of the sine of that number. In symbols, cos(2θ) − 1 = −2 sin²(θ). This is not a new physical claim; it is a standard consequence of the double-angle formula for cosine, which states cos(2θ) = 2cos²(θ) − 1, combined with the Pythagorean identity sin²(θ) + cos²(θ) = 1. The declaration is a theorem, meaning it is a proved statement in the framework's machine-checked library of formal theorems.

The identity's role in the framework is as a stepping stone. The library uses it to prove a limit: as a variable q approaches zero (but is never equal to zero), the expression (cos(q·a) − 1) / q² tends to −a²/2. This limit is the second-order Taylor approximation of the cosine function near zero, scaled by a². The framework then applies this limit to a sum of weighted cosine terms, called a centered trigonometric polynomial, showing that such a sum divided by t² tends to a specific constant. This constant, the sum of weights times −θᵢ²/2, is the cosine two-jet of the polynomial. This chain of limits is part of a larger calculation related to a curvature quantity in a gravity analysis, specifically the Hessian of a flat metric.

What the declaration does not claim is just as important. It does not assert anything about gravity, spacetime, or the physical meaning of the variables θ, a, or q. The identity is purely mathematical, holding for any real numbers. It does not claim that the limit converges for all values of q; the limit is explicitly on the punctured neighborhood of zero, meaning q is never zero. The declaration does not prove the limit itself; that is a separate theorem, cos_sub_one_div_sq_tendsto. And the identity does not depend on any physical constants or the framework's specific axioms; it is a general result about real numbers, provable from standard library facts.

In the context of the framework's gravity analysis, this identity is a tool, not a conclusion. It provides the precise limiting behavior of a cosine term that appears in a curvature expression. The framework's library builds on this to show that a certain sum of such terms, when scaled, approaches a well-defined limit. This limit is what allows the framework to connect a discrete, ledger-like structure to a continuous geometric quantity. The identity itself, however, remains a standard piece of trigonometry, and its proof does not rely on any framework-specific assumptions.

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 θ)]

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

The declaration does not make any physical claim about gravity or spacetime. The identity does not prove the limit (cos(q·a) − 1) / q² → −a²/2; that is a separate theorem. The identity does not depend on any framework-specific axioms 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: