ErrorBudget
plain-language theorem explainer
ErrorBudget packages the three nonnegative real components of the attachment error for the Riemann hypothesis along the Christmas route: Hilbert-Schmidt determinant continuity, prime-tail truncation, and window leakage. A number theorist working on explicit RH bounds would cite it to separate the algebraic attachment condition from concrete prime-sum estimates. The declaration is a plain structure definition that records the three fields together with their nonnegativity proofs and supplies the total-error accessor used downstream.
Claim. An error budget consists of three nonnegative real numbers $E = (e_2, e_t, e_w)$ where $e_2$ bounds the Hilbert-Schmidt-to-determinant continuity error, $e_t$ bounds the truncation error after finitely many primes, and $e_w$ bounds the localization leakage outside a rectangle $R$, together with the constraints $e_2, e_t, e_w ≥ 0$.
background
The module decomposes the attachment error $‖J_N - J_{cert,N}‖$ into three separately verifiable budgets so that the algebraic part of the Christmas-paper argument can be isolated from number-theoretic estimates. The attachment inequality itself requires that the total error be at most $m/4$ for a positive margin $m$ on the rectangle $R$. Upstream results supply the abstract interface for the determinant continuity (LedgerFactorization) and the general forcing framework (PhiForcingDerived), while the module keeps $J$ and $J_{cert}$ as arbitrary functions $ℂ → ℂ$.
proof idea
This is a structure definition; it directly assembles the three real fields and their nonnegativity hypotheses with no lemmas or tactics applied.
why it matters
ErrorBudget supplies the data type consumed by Admissible and by the three-budget attachment theorem attachmentWithMargin_of_threeBudgets, which together close the algebraic step of the Christmas-route argument for the Riemann hypothesis. It appears in the explicit instantiation christmasBudget and in the prime-tail bound prime_tail_tsum_bound. The construction touches the open question of obtaining sufficiently small concrete values for the three components from prime-number estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.