integer_tail_bound
The integer tail bound establishes nonnegativity of x^{1-α}/(α-1) for real x>1 and α>1. Analysts controlling truncation error in the prime sum for explicit Riemann hypothesis checks cite this when assembling the error budget. The proof is a direct term application of real power nonnegativity and division positivity.
claimFor real numbers $x>1$ and $α>1$, $0 ≤ x^{1-α}/(α-1)$.
background
This theorem belongs to the error budget module that decomposes the attachment error ||J_N - J_cert,N|| into three separately verifiable pieces: det₂ Lipschitz continuity, prime tail truncation, and window leakage. The local setting follows the Christmas-route template with σ₀=0.6, keeping J_N abstract so that number-theoretic bounds can be plugged in later. The result supplies the nonnegativity hypothesis required for the prime tail component ∑_{n>x} n^{-α} ≤ x^{1-α}/(α-1). It draws on the universal forcing self-reference structure for meta-realization axioms and the circle phase lift theorem that supplies an explicit log-derivative bound M.
proof idea
The term proof applies div_nonneg. The numerator x^{1-α} is shown nonnegative by Real.rpow_nonneg with linarith on the base x>1. The denominator α-1 is shown positive by linarith from the hypothesis α>1.
why it matters in Recognition Science
The declaration fills the prime tail slot inside attachmentWithMargin_of_threeBudgets, the central theorem that combines the three budgets to obtain attachment-with-margin. It supplies the concrete nonnegativity template referenced in the Christmas paper for the σ₀=0.6 rectangle. Within Recognition Science it contributes the number-theoretic estimate needed to close the error budget in the self-reference forcing chain (T0-T8) before the phi-ladder mass formula is applied.
scope and limits
- Does not prove the sum ∑_{n>x} n^{-α} is bounded by the expression.
- Does not extend the bound to α ≤ 1 or x ≤ 1.
- Does not supply explicit numerical values or Rosser-Schoenfeld constants.
- Does not treat complex α or non-real x.
formal statement (Lean)
181theorem integer_tail_bound {x α : ℝ} (hx : 1 < x) (hα : 1 < α) :
182 0 ≤ x ^ (1 - α) / (α - 1) := by
proof body
Term-mode proof.
183 apply div_nonneg
184 · apply Real.rpow_nonneg
185 linarith
186 · linarith
187
188/-!
189## Combining budgets for the Christmas route
190
191The Christmas paper uses σ₀ = 0.6 and specific rectangle choices.
192Here we provide a template for combining the three budgets.
193-/
194
195/-- **Christmas-route budget combination** (σ₀ = 0.6).
196
197Template for instantiating the error budget with Christmas-paper constants.
198Requires explicit nonnegativity proofs for each component.
199-/