ArithmeticDeformationIdentification
plain-language theorem explainer
Arithmetic deformation identification requires that the truncated arithmetic function and the passive certificate transfer function differ in norm by at most one quarter of the given margin throughout the region R. Researchers deriving explicit prime tail bounds for the Riemann hypothesis attachment error budget cite this predicate to close the boss lemma. The definition consists of a direct universal quantification over points in R of the complex norm inequality between the two functions.
Claim. Let $N$ be a natural number, $σ_0$ a real number, $J_N$ the truncated arithmetic function from an approximant for $N$, $J_{cert}$ the transfer function from a passive certificate for $N$ and $σ_0$ with positive margin $m$, and $R$ a set of complex numbers. The predicate holds precisely when $∀ s ∈ R$, $‖J_N(s) - J_{cert}(s)‖ ≤ m/4$.
background
In the module on prime tail bounds for the attachment-with-margin error budget, explicit estimates on sums over primes are developed to discharge the PrimeTailBound predicate using convergence for exponents greater than 1 and partial summation. The ArithmeticApproximant structure supplies a truncated arithmetic function $J_N$ that is holomorphic for Re $s > 1/2$. The PassiveCertificate structure supplies a rational transfer function $J_{cert}$ that is passive, meaning Re$(2 J_{cert} s) ≥ 0$ for Re $s > σ_0$, together with a positive margin $m$ defined as the infimum of that real part on the relevant half-plane.
proof idea
The predicate is introduced directly as the universal quantification of the norm inequality between the approximant function $J_N$ and the certificate function $J_{cert}$ on the set $R$. No lemmas are applied; the definition is the statement itself.
why it matters
This predicate serves as the boss lemma condition in the prime tail bounds module. It is invoked by the theorem attachmentWithMargin_of_bossLemma to conclude that attachment-with-margin holds on $R$ whenever the identification is satisfied. The construction supports the explicit error budget for the Riemann hypothesis by ensuring the arithmetic deformation stays controlled within the passive margin, advancing from prime tail estimates to the full attachment condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.