mkEulerInstantiationCert
plain-language theorem explainer
mkEulerInstantiationCert assembles Euler product convergence, nonvanishing of C(s), positive derivative bound, and regular-carrier compatibility into one certificate structure. Number theorists working on conditional Riemann hypothesis statements would cite it to instantiate the abstract RS carrier inside the cost-covering bridge. The definition is a direct record constructor that applies four prior theorems to fill the fields.
Claim. The definition produces a certificate $C$ such that for every real $σ > 1/2$ the series of $det_2$ log factors over primes is summable, the carrier value is nonzero, the logarithmic derivative bound is positive, and for every defect sensor there exists a regular carrier whose radius equals the sensor real part minus $1/2$.
background
The Euler Product Instantiation module shows that the zeta Euler product supplies a concrete carrier for the abstract RS framework of AnnularCost and CostCoveringBridge. Core objects are PrimeSum $σ = ∑_p p^{-σ}$, HilbertSchmidtNorm $σ = ∑_p p^{-2σ}$, carrierLogSeries, and carrierDerivBound $σ = 2∑_p (log p) p^{-2σ}/(1-p^{-σ})$. The module proves that $C(s) = det_2(I-A(s))^2$ is holomorphic and nonvanishing for Re(s) > 1/2 with bounded logarithmic derivative, satisfying the EulerCarrier and RegularCarrier interfaces.
proof idea
Direct record construction. carrier_convergent is filled by det2_product_convergent, carrier_nonzero by carrier_nonvanishing, deriv_bounded by carrierDerivBound_pos, and compatible by the pair (eulerRegularCarrier, euler_regular_carrier_covers_strip).
why it matters
The definition completes Layer 3 of the module architecture: primes to Hilbert-Schmidt operator to convergent det₂ product to holomorphic nonvanishing C(s) on Re(s) > 1/2. It supplies the concrete carrier required by the cost-covering axiom in CostCoveringBridge, yielding the conditional statement that no zeros exist with Re(s) > 1/2. The construction touches the open question of whether the same RS cost structure can be made unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.