Admissible
plain-language theorem explainer
The declaration defines when a three-way error budget for the Riemann attachment inequality is admissible under a given margin. Number theorists working on the Christmas decomposition of the J-function error would invoke this predicate to certify that the summed contributions stay inside the allowed tolerance. It is realized as a direct inequality check on the aggregated total field of the ErrorBudget structure.
Claim. Let $E$ be a three-way error budget whose components are the determinant-continuity error, prime-tail truncation error, and window-leakage error. The budget $E$ is admissible for margin $m$ precisely when the sum of its components satisfies $E. total ≤ m/4$.
background
The module formalizes the Christmas-paper decomposition of the attachment error norm into three separately verifiable contributions: determinant continuity from the Hilbert-Schmidt to det₂ Lipschitz interface, prime-sum truncation at finite N, and localization leakage inside a rectangular window. The ErrorBudget structure packages these as det2Err, tailErr, and winErr together with their non-negativity proofs; the total projection aggregates them. The module doc states that this separation lets algebraic and topological reasoning proceed independently of explicit number-theoretic estimates, referencing Riemann-Christmas.tex equation eq:attachment and Lemma attachment-error-decomp.
proof idea
One-line definition that directly encodes the predicate as the inequality on the total error component of the supplied ErrorBudget record.
why it matters
The predicate supplies the central gate condition for the attachmentWithMargin_of_threeBudgets theorem that concludes the full attachment inequality once the three budgets are admissible. It is the concrete realization of the Christmas-paper error-decomposition lemma and is reused as a uniform admissibility pattern in downstream ethics cost models and SAT encodings. Within the Recognition framework it closes the error-budget step of the RH route by converting the abstract margin requirement into a checkable numerical predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.