PrimeTailBound
plain-language theorem explainer
PrimeTailBound defines the predicate asserting that truncation error from the prime sum tail beyond N stays at most E_tail whenever σ₀ > 1/2 with the listed positivity conditions. Researchers decomposing the attachment error in the Christmas route to the Riemann hypothesis would cite it to isolate the prime contribution from determinant and window terms. The definition is introduced directly as a conjunction of four inequalities together with a placeholder comment for the explicit sum estimate.
Claim. Let $N$ be a natural number, let $σ_0$ and $E_{tail}$ be real numbers. The predicate holds precisely when $0 < σ_0$, $1/2 < σ_0$, $0 ≤ E_{tail}$ and $N ≥ 1$, which encodes that the tail contribution $∑_{p > N} p^{-σ_0}$ (or analogous prime terms) is bounded above by $E_{tail}$.
background
The ErrorBudget module decomposes the attachment error $‖J_N - J_{cert,N}‖$ into three separately verifiable budgets: determinant-2 Lipschitz continuity, prime-tail truncation, and window leakage. PrimeTailBound supplies the second budget, requiring the sum over primes larger than the cutoff N to remain below the allocated error E_tail. This separation lets the algebraic argument in attachmentWithMargin_of_threeBudgets proceed without committing to concrete number-theoretic estimates at the outset.
proof idea
The definition is a direct conjunction of the four inequalities 0 < σ₀, 1/2 < σ₀, 0 ≤ E_tail and N ≥ 1. No lemmas or tactics are invoked; the body serves as an abbrev-style predicate with a comment noting that the actual bound will later involve the explicit tail sum.
why it matters
PrimeTailBound supplies one of the three error budgets required by attachmentWithMargin_of_threeBudgets, which concludes that if the budgets sum to at most m/4 then attachment-with-margin holds. It fills the prime-tail slot in the Christmas-route decomposition referenced in Riemann-Christmas.tex (eq:attachment and Lemma attachment-error-decomp). The predicate is instantiated downstream by primeTailBound_christmas (for σ₀ = 0.6) and primeTailBound_of_explicit (for general σ₀ > 1/2), linking the abstract budget to Rosser–Schoenfeld-style explicit estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.