Gravity Analysis Spectral Convergence Sub Cube Le Sin

A global bound on sine

The sine function, written sin t, is one of the most familiar objects in mathematics. For small positive t, sin t is very close to t. The standard Taylor approximation says sin t is roughly t minus t cubed over six. The declaration sub_cube_le_sin in the framework's machine-checked library of formal theorems proves a global version of this approximation: for every t greater than or equal to zero, t minus t cubed over six is less than or equal to sin t. The word global is the point. The usual textbook bound only works when t is small, typically when the absolute value of t is at most one. This theorem has no such smallness hypothesis; it holds for all nonnegative t, no matter how large.

The proof is a short monotonicity argument. Define a function g of s as sin s minus s plus s cubed over six. Its derivative is cos s minus one plus s squared over two. A standard inequality, one minus s squared over two is less than or equal to cos s, shows this derivative is never negative for s at least zero. So g is nondecreasing, and since g of zero is zero, g of t is at least zero for every nonnegative t. That is exactly the claimed inequality. The same argument also yields the companion bound, the absolute value of sin t minus t is at most t cubed over six, again for all nonnegative t.

Why does a bound on sine matter for gravity analysis? The framework's spectral convergence toolkit uses it to measure how a discrete model of space approaches a continuous one. In the flat torus model, a lattice with N points per side has eigenvalues that involve the sine function. The relevant quantity is four N squared times sine squared of pi k over N, where k is a wavenumber. As N grows, this expression should approach the continuous eigenvalue, two pi k squared. The global sine bound supplies the error rate: the difference is at most a constant depending on k, divided by N squared. This explicit rate upgrades a qualitative convergence statement to a quantitative one, and it is what later curved perturbation bounds consume.

In Recognition Science, this theorem is a proved result, not a model or a hypothesis. It is part of a toolkit whose lemmas are all axiom-clean, meaning the machine-checked library certifies them without extra assumptions. The declaration does not claim anything about curved spaces, about the physical interpretation of the eigenvalues, or about the rate being optimal. It only establishes a numerical inequality about sine, and the toolkit then uses that inequality to control a specific discrete-to-continuous limit.

/-- THEOREM (global cubic sine lower bound). For `t ≥ 0`,
`t - t³/6 ≤ sin t`. Proof: `g(s) = sin s - s + s³/6` has derivative
`cos s - 1 + s²/2 ≥ 0` (by `Real.one_sub_sq_div_two_le_cos`), so `g` is
monotone and `g(t) ≥ g(0) = 0`. No smallness hypothesis on `t`. -/
theorem sub_cube_le_sin (t : ℝ) (ht : 0 ≤ t) :
    t - t ^ 3 / 6 ≤ Real.sin t := by
  have hderiv : ∀ s : ℝ,
      HasDerivAt (fun x : ℝ => Real.sin x - x + x ^ 3 / 6)
        (Real.cos s - 1 + (3 : ℝ) * s ^ 2 / 6) s := by
    intro s
    have hp : HasDerivAt (fun x : ℝ => x ^ 3) ((3 : ℝ) * s ^ 2) s := by
      have h := hasDerivAt_pow 3 s
      norm_num at h
      exact h
    exact ((Real.hasDerivAt_sin s).sub (hasDerivAt_id s)).add (hp.div_const 6)
  have hmono : Monotone (fun x : ℝ => Real.sin x - x + x ^ 3 / 6) := by
    refine monotone_of_hasDerivAt_nonneg hderiv ?_
    rw [Pi.le_def]
    intro s
    simp only [Pi.zero_apply]
    have hc := Real.one_sub_sq_div_two_le_cos (x := s)
    linarith
  have h0 : (fun x : ℝ => Real.sin x - x + x ^ 3 / 6) 0 = 0 := by
    simp
  have h := hmono ht
  rw [h0] at h
  simp only at h
  linarith

/-- THEOREM (global cubic Taylor bound for sine). For `t ≥ 0`,
`|sin t - t| ≤ t³/6`. Combines `Real.sin_le` (upper) with
`sub_cube_le_sin` (lower). Unlike Mathlib's `Real.sin_bound`, no `|t| ≤ 1`
hypothesis is needed. -/
theorem abs_sin_sub_le_cube (t : ℝ) (ht : 0 ≤ t) :
    |Real.sin t - t| ≤ t ^ 3 / 6 := by
  have h1 : Real.sin t ≤ t := Real.sin_le ht
  have h2 : t - t ^ 3 / 6 ≤ Real.sin t := sub_cube_le_sin t ht
  have h3 : 0 ≤ t ^ 3 / 6 := by positivity
  rw [abs_le]
  constructor <;> linarith

/-- THEOREM (rated limit, composing the toolkit). The flat discrete TT
eigenvalue `4N² sin²(πk/N)` converges to `(2πk)²`, obtained by feeding the
quantitative expansion into `eigenvalue_limit_of_uniform_bound` with
`C = (2πk)⁴/12`. Re-derives
`DiscreteLichnerowicz.discreteEigenvalue_tendsto` with an explicit rate. -/
theorem discrete_sine_eigenvalue_tendsto (k : ℕ) :
    Filter.Tendsto
      (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)
      Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) :=
  eigenvalue_limit_of_uniform_bound _ _ ((2 * Real.pi * (k : ℝ)) ^ 4 / 12) 1
    (fun N hN => discrete_sine_eigenvalue_expansion k N hN)

What this page does not claim

The theorem says nothing about curved spaces or the physical interpretation of the eigenvalues. The bound is not claimed to be optimal; it is a sufficient error rate for the toolkit's purpose. The declaration does not establish the min-max perturbation result, which remains future work.

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/SpectralConvergence.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: