 899    Packages the complete chain:
 900    Euler product → carrier convergent → nonvanishing → derivative bounded
 901    → abstract interface satisfied → cost-covering applicable. -/
 902structure EulerInstantiationCert where
 903  /-- The carrier converges on Re(s) > 1/2. -/
 904  carrier_convergent : ∀ σ, 1/2 < σ → Summable (fun (p : Nat.Primes) => det2LogFactor p σ)
 905  /-- The carrier is nonvanishing. -/
 906  carrier_nonzero : ∀ σ, 1/2 < σ → carrierValue σ ≠ 0
 907  /-- The logarithmic derivative is bounded. -/
 908  deriv_bounded : ∀ σ, 1/2 < σ → 0 < carrierDerivBound σ
 909  /-- For any hypothetical zero, a compatible RegularCarrier exists. -/
 910  compatible : ∀ (sensor : DefectSensor),
 911    ∃ (carrier : RegularCarrier), carrier.radius = sensor.realPart - 1/2
 912
 913/-- The Euler instantiation certificate is verified. -/
 914@[simp] def EulerInstantiationCert.verified (cert : EulerInstantiationCert) : Prop :=
 915  (∀ σ, 1/2 < σ → carrierValue σ ≠ 0) ∧
 916  (∀ σ, 1/2 < σ → 0 < carrierDerivBound σ) ∧
 917  (∀ (sensor : DefectSensor),
 918    ∃ (carrier : RegularCarrier), carrier.radius = sensor.realPart - 1/2)
 919
 920/-- Construct the verified certificate from the proved results. -/
 921noncomputable def mkEulerInstantiationCert : EulerInstantiationCert where
 922  carrier_convergent := fun σ hσ => det2_product_convergent hσ
 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.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.