eulerZeroTrace
plain-language theorem explainer
eulerZeroTrace defines the zero-charge AnnularTrace for the Euler product instantiation in Recognition Science. It supplies the concrete carrier with identically zero annular excess for use in budgeted carrier constructions. Researchers bridging the Euler product to the cost-covering axiom cite this object. The definition sets the charge to zero and verifies the mesh specification via direct simplification of uniformChargeMesh.
Claim. The zero-charge Euler trace is the AnnularTrace with charge field equal to $0$ and mesh function sending each refinement level $N$ to uniformChargeMesh $N$ $0$, satisfying the charge specification identically.
background
The EulerInstantiation module shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework from AnnularCost.lean and CostCoveringBridge.lean. AnnularTrace is the structure with a charge value and a mesh function assigning charge distributions to refinement rings; the zero-charge instance has excess identically zero. In the local setting the module proceeds from PrimeSum and HilbertSchmidtNorm through carrierLogSeries and carrierDerivBound to concrete carriers satisfying the EulerCarrier interface.
proof idea
The definition is a direct record construction: charge is set to zero, mesh is defined via uniformChargeMesh, and the charge_spec field is discharged by simp on the uniformChargeMesh definition.
why it matters
This definition supplies the trace field for eulerBudgetedCarrier, realizing the BudgetedCarrier witness for the Euler product with budget constant zero. It completes the concrete instantiation step in the chain from primes to EulerCarrier to RegularCarrier to the cost-covering axiom, enabling conditional results on the Riemann hypothesis. The zero-excess property closes the uniform bound required by the annular cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.