mkEulerInstantiationCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove convergence of the product for σ ≤ 1/2.
- Does not supply explicit numerical constants for the derivative bound.
- Does not address zeros on the critical line Re(s) = 1/2.
- Does not establish the unconditional Riemann hypothesis.
formal statement (Lean)
921noncomputable def mkEulerInstantiationCert : EulerInstantiationCert where
922 carrier_convergent := fun σ hσ => det2_product_convergent hσ
proof body
Definition body.
923 carrier_nonzero := fun σ hσ => carrier_nonvanishing hσ
924 deriv_bounded := fun σ hσ => carrierDerivBound_pos hσ
925 compatible := fun sensor =>
926 ⟨eulerRegularCarrier sensor.realPart sensor.in_strip.1,
927 euler_regular_carrier_covers_strip sensor.realPart sensor.in_strip.1⟩
928
929/-! ### §10. Connecting to the conditional RH -/
930
931/-- The full chain: Euler product instantiation + explicit cost-covering package
932 implies no zeros with Re(s) > 1/2.
933
934 This theorem connects the concrete number theory (this file)
935 to the abstract conditional RH (CostCoveringBridge.lean). -/