eulerCarrierInstance
plain-language theorem explainer
The definition supplies a concrete instance of the EulerCarrier structure using the Euler product of the zeta function, with the half-plane fixed at Re(s) > 1. Researchers deriving conditional Riemann hypothesis statements from cost-covering axioms would reference this instantiation to close the bridge from analytic number theory to the RS framework. The construction proceeds by direct record filling, invoking norm_num for the half-plane inequality and a prior carrierDerivBound lemma for the logarithmic derivative estimate.
Claim. The Euler product of the zeta function supplies a carrier $C(s)$ on the half-plane Re$(s)>1$ such that $|C'/C|$ is bounded by the convergent series $2 sum_p (log p) p^{-2 sigma}/(1-p^{-sigma})$, $C(s)$ is nonvanishing, and the finite bound on the derivative holds for any sigma > 1.
background
In the Recognition Science cost structure the abstract EulerCarrier interface from CostCoveringBridge requires a holomorphic nonvanishing function on a half-plane Re(s) > sigma_0 together with a bound on |C'/C|. The module EulerInstantiation constructs this from the Euler product of zeta(s) via the prime zeta function PrimeSum sigma := sum_p p^{-sigma} and the Hilbert-Schmidt norm squared HilbertSchmidtNorm sigma := sum_p p^{-2 sigma}. The carrierLogSeries and carrierDerivBound are the explicit series for the log and its derivative. Upstream, the RegularCarrier from AnnularCost provides the regularity condition on disks.
proof idea
The definition is a direct record construction for the EulerCarrier structure. It sets halfPlane to 1, proves halfPlane_gt by norm_num, assigns logDerivBound to the carrierDerivBound lemma, discharges the finite bound case by trivial, and sets nonvanishing to True.
why it matters
This definition closes the concrete-to-abstract bridge in the Euler product instantiation, allowing the cost-covering axiom from CostCoveringBridge to apply and yield a conditional Riemann hypothesis. It sits at the end of the chain primes to Hilbert-Schmidt convergence to carrier nonvanishing to EulerCarrier. The framework landmark is the conditional RH step in the T0-T8 forcing chain via the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.