ErrorBudget
plain-language theorem explainer
ErrorBudget packages three nonnegative real numbers that bound the Hilbert-Schmidt determinant continuity error, the prime-tail truncation error, and the window-leakage error in the decomposition of the attachment error for the Riemann Hypothesis certificate. Analytic number theorists working on explicit versions of the Christmas decomposition would cite this structure when verifying that the summed error stays below m/4. The declaration is a record type that directly encodes the three components together with their nonnegativity proofs.
Claim. An error budget consists of three nonnegative real numbers $(e_d, e_t, e_w)$ where $e_d$ bounds the Hilbert-Schmidt to determinant-2 continuity error, $e_t$ bounds the truncation error from a finite prime sum, and $e_w$ bounds the localization error from restricting to a rectangular window.
background
The module decomposes the attachment error norm of an approximant J minus a certificate Jcert into three separately bounded contributions on a region R. The det2 component controls continuity of the determinant map from Hilbert-Schmidt operators, the tail component arises from cutting the prime sum at finite N, and the win component measures leakage from localizing the analysis to a finite rectangle. This separation lets algebraic reasoning about the attachment inequality proceed independently of the concrete number-theoretic estimates required for each term. The structure is imported from AttachmentWithMargin and supplies the input type for the admissibility predicate that checks whether the total error is at most m/4.
proof idea
The declaration is a structure definition with no proof body. It directly records the three error fields and the three nonnegativity hypotheses as structure fields.
why it matters
This structure supplies the error packaging required by attachmentWithMargin_of_threeBudgets, which concludes that an admissible total error implies the attachment inequality holds. It implements the Christmas-paper decomposition of the attachment error into det2, tail, and win contributions. In the Recognition Science framework it supports the separation of topological and arithmetic estimates that feed the zero-free region arguments connected to the phi-ladder and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.