IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
ErrorBudget packages the three error terms (determinant continuity, prime tail truncation, window leakage) for the attachment-with-margin inequality in the Christmas-route approach to the Riemann hypothesis. It requires their sum to be at most m/4 for margin m > 0. Number theorists assembling explicit zero-free regions cite this decomposition when bounding the far-field gap. The module supplies the predicate and its nonnegativity properties through direct definitions.
claimThe module defines an error budget structure $E = (e_2, e_t, e_w)$ such that $e_2 + e_t + e_w ≤ m/4$ for margin $m > 0$, where the terms bound the decomposition of $sup_{s ∈ R} |J_N(s) - J_{cert,N}(s)|$ arising from the attachment-with-margin inequality.
background
The upstream AttachmentWithMargin module formalizes the attachment-with-margin inequality: $sup_{s ∈ R} |J_N(s) - J_{cert,N}(s)| ≤ m_R / 4$ with $m_R := inf_{s ∈ R} Re(2 J_{cert,N}(s))$. This module decomposes the left-hand side into three contributions: det2Err from Hilbert–Schmidt determinant continuity, tailErr from prime tail truncation, and winErr from window localization leakage. The local setting is the purely algebraic consequence of the Christmas-paper decomposition for the Riemann hypothesis.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the ErrorBudget predicate that PrimeTailBounds discharges via explicit prime tail estimates. It completes the three-way decomposition required by the attachment-with-margin inequality (eq:attachment) in the Christmas route. Downstream work on PrimeTailBounds instantiates the PrimeTailBound component of this budget.
scope and limits
- Does not derive numerical values for the individual error terms.
- Does not establish convergence of the prime sums.
- Does not connect to the J-function or phi-ladder from the core Recognition framework.
- Does not address the full Riemann hypothesis, only the error budget for one route.
used by (1)
depends on (1)
declarations in this module (14)
-
structure
ErrorBudget -
def
total -
theorem
total_nonneg -
def
Admissible -
theorem
admissible_of_components_bound -
theorem
attachmentWithMargin_of_threeBudgets -
def
Det2Lipschitz -
def
PrimeTailBound -
def
WindowLeakageBound -
theorem
prime_tail_bound_rosser_schoenfeld -
theorem
integer_tail_bound -
def
christmasBudget -
theorem
christmas_attachment_of_explicit_budgets -
theorem
christmas_RH_of_budgets