IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
This module packages a three-way error budget for the attachment-with-margin inequality arising in the Christmas-route approach to the Riemann Hypothesis. It decomposes the total discrepancy into determinant continuity error, prime tail truncation error, and window leakage error, with the constraint that their sum is at most m/4. Researchers formalizing explicit bounds on the zeta function cite this structure to organize the quantitative estimates. The module is a definition module that introduces the relevant predicates and basic non-negativty
claimThe module introduces the predicate asserting that the sum of the determinant continuity error, prime tail truncation error, and window leakage error is at most $m/4$ for margin $m>0$, together with the total error function and the admissibility condition on the three components.
background
In the Christmas-route formalization the attachment-with-margin inequality requires that the supremum over the region of the absolute difference between the truncated J-function and its certified version is bounded by one quarter of the infimum of the real part of the certified function. This module decomposes the left-hand side into three contributions drawn from the Christmas-paper analysis: the Hilbert-Schmidt determinant continuity error, the prime tail truncation error, and the window or localization leakage error. The upstream AttachmentWithMargin module isolates the purely algebraic consequence of the far-field remaining gap.
proof idea
This is a definition module, no proofs. It introduces the error budget predicate, the total error sum, non-negativity statements, and component-wise admissibility lemmas that are later instantiated by downstream modules.
why it matters in Recognition Science
This module supplies the error budget decomposition instantiated by the PrimeTailBounds module to discharge the tail error component. It directly supports the quantitative attachment inequality needed for the Christmas-route proof of the Riemann Hypothesis, as described in the upstream attachment-with-margin doc-comment.
scope and limits
- Does not compute explicit numerical values for any error term.
- Does not prove convergence of prime sums.
- Does not address the full Riemann Hypothesis argument.
- Does not supply bounds for the determinant or window components.
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