prime_tail_bound_rosser_schoenfeld
plain-language theorem explainer
The theorem proves non-negativity of the explicit upper-bound expression (1.25506 α)/((α-1) log x) * x^(1-α) for x ≥ 17 and α > 1. Researchers formalizing the prime-tail component of the attachment error budget in the Christmas-route Riemann Hypothesis decomposition would cite it. The proof is a short tactic sequence that chains Real.log_pos, mul_pos, div_nonneg, and rpow_nonneg to establish the sign.
Claim. For real numbers $x$ and $α$ with $x ≥ 17$ and $α > 1$, $0 ≤ (1.25506 α)/((α-1) log x) · x^{1-α}$.
background
The module decomposes the attachment error ‖J_N - J_cert,N‖ into three separately verifiable budgets: det₂ Lipschitz continuity, prime-tail truncation error from cutting the prime sum at finite N, and window leakage. This theorem supplies the concrete non-negativity check for the prime-tail budget using a Rosser–Schoenfeld-style estimate. The local theoretical setting is the Christmas-paper decomposition (Riemann-Christmas.tex eq:attachment and Lemma attachment-error-decomp) that feeds the main theorem attachmentWithMargin_of_threeBudgets.
proof idea
Tactic proof. First apply Real.log_pos and linarith to obtain 0 < log x. Then use mul_pos to obtain positivity of the denominator (α-1) log x. Finally apply mul_nonneg, div_nonneg, and Real.rpow_nonneg (with linarith) to conclude the whole expression is non-negative.
why it matters
Supplies the prime-tail budget required by attachmentWithMargin_of_threeBudgets in the error-budget decomposition for the attachment-with-margin statement. Implements the number-theoretic estimate referenced in the Christmas route for the Riemann Hypothesis. The constant 1.25506 is the classical Rosser–Schoenfeld factor; the theorem remains a placeholder pending formalization of the actual prime-sum inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.