argument_principle_sampling
plain-language theorem explainer
Argument principle sampling asserts that any defect sensor admits, for each natural number N, an annular mesh of that resolution whose total charge equals the sensor charge. Researchers instantiating the Euler product of zeta into the Recognition Science carrier framework would cite this when translating zero orders into mesh windings for cost calculations. The proof is a one-line term construction that directly builds the uniform-charge mesh and confirms the equality by reflexivity.
Claim. Let $s$ be a defect sensor. Then for every natural number $N$, there exists an annular mesh $m$ of resolution $N$ such that the charge of $m$ equals the charge of $s$.
background
The Euler Product Instantiation module shows how the Euler product of zeta instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. The instantiation chain runs from primes through Hilbert-Schmidt norms and det2 factors to a holomorphic nonvanishing C(s) on Re(s) > 1/2, enabling the cost-covering axiom and conditional RH. Core objects include PrimeSum sigma, HilbertSchmidtNorm sigma, carrierLogSeries sigma, and carrierDerivBound sigma. Upstream results supply the Defect definition as a toy defect functional that is zero when checks pass, together with cost functions induced by multiplicative recognizers and observer forcing events.
proof idea
The proof is a term-mode lambda abstraction over N that applies the uniformChargeMesh constructor to the given resolution and the sensor charge, then uses reflexivity to witness the charge equality. No further lemmas or tactics are required beyond the mesh constructor itself.
why it matters
This supplies the sampling step labeled Axiom 1 in the module documentation, allowing zero orders of zeta to be represented as mesh charges within the Euler carrier interface. It supports the path from concrete Euler product to abstract cost-covering and conditional RH. The declaration touches the open question of adding contour integration to Mathlib, which the doc comment identifies as still unavailable for the full argument principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.