total
plain-language theorem explainer
The total definition aggregates the three error components of an ErrorBudget into a single real number for the attachment inequality. Researchers formalizing the Christmas-paper decomposition of the J_N to J_cert,N discrepancy would cite this when checking the overall margin bound m/4. It is realized as a direct sum of the det2 continuity, prime tail, and window leakage fields.
Claim. For an error budget $E$, the total error is $E._{det2Err} + E._{tailErr} + E._{winErr}$, where $det2Err$ is the Hilbert-Schmidt determinant continuity error, $tailErr$ the prime tail truncation error, and $winErr$ the window leakage error.
background
This module formalizes the Christmas-paper decomposition of the attachment error into three separately checkable budgets for the Riemann Hypothesis. The ErrorBudget structure packages det2Err (HS to det2 Lipschitz), tailErr (truncation at N primes), and winErr (localization to rectangle R), with the key requirement that their sum is at most m/4 for margin m > 0. The module doc notes that J_N and J_cert,N remain abstract functions from C to C so algebraic reasoning separates from number-theoretic estimates.
proof idea
This is a one-line definition that sums the three error fields det2Err, tailErr, and winErr directly from the ErrorBudget record.
why it matters
This sum feeds the attachmentWithMargin_of_threeBudgets theorem that closes the decomposition argument. It is referenced by downstream results including applied (time-translation symmetry), energyConservationCert, hamilton_equations_from_EL, and totalEnergy in the Action module, as well as spaceTranslationFlow and space_translation_invariance_implies_momentum_conservation in Noether. It supports the framework's separation of topological and arithmetic error controls in the RH setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.