ArithmeticApproximant
plain-language theorem explainer
The ArithmeticApproximant structure supplies an interface for a truncated arithmetic function J_N from the complex plane to itself, equipped with placeholder conditions on holomorphy, boundary modulus, and zero-pole alignment with the xi function. Analytic number theorists working on explicit prime-sum estimates for error budgets would cite it when discharging PrimeTailBound for N at least 17 and sigma_0 greater than 1/2. The declaration is a bare structure with no computational body or lemmas applied.
Claim. For a natural number $N$, an arithmetic approximant consists of a map $J_N : ℂ → ℂ$ that is holomorphic on the half-plane Re $s > 1/2$, satisfies $|J_N(s)| = 1$ almost everywhere on the critical line Re $s = 1/2$, and shares the zero and pole structure of the Riemann xi function without cancellation.
background
The module supplies explicit upper bounds on prime reciprocal sums for the attachment-with-margin error budget in a Riemann-hypothesis argument. It records that the sum over primes of $p^{-α}$ converges for $α > 1$, derives tail bounds via partial summation, and instantiates the PrimeTailBound predicate from the ErrorBudget file. The ArithmeticApproximant structure is introduced as the abstract carrier for the truncated arithmetic function $J_N$ that enters the deformation-identification step. Upstream results on modular realizations and empirical programs supply only generic interface patterns; the concrete number-theoretic content is drawn from the cited Rosser–Schoenfeld and Dusart estimates.
proof idea
The declaration is a structure definition with an empty proof body. Its three property fields are set to the placeholder True, leaving concrete verification to later constructions that instantiate the structure.
why it matters
ArithmeticApproximant is the type parameter in ArithmeticDeformationIdentification, which feeds directly into the theorem attachmentWithMargin_of_bossLemma. That theorem closes the boss-lemma route to AttachmentWithMargin on a region to the right of sigma_0. The construction therefore supplies the arithmetic side of the explicit tail-bound instantiation primeTailBound_of_explicit, supporting the Christmas-route error budget decomposition referenced in Riemann-Christmas.tex. It touches the open question of producing a concrete holomorphic J_N that meets the three placeholder conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.