sensor_carrier_compatible

formal source

 883    a neighborhood of any hypothetical zero.
 884    Specifically: if Re(ρ) = σ₀ > 1/2, then D(ρ, σ₀ − 1/2) ⊂ {Re(s) > 1/2}
 885    and the carrier is holomorphic nonvanishing on this disk. -/
 886theorem sensor_carrier_compatible (sensor : DefectSensor) :
 887    ∃ (carrier : RegularCarrier),
 888      carrier.radius = sensor.realPart - 1/2 ∧
 889      0 < carrier.radius := by
 890  exact ⟨eulerRegularCarrier sensor.realPart sensor.in_strip.1,
 891         euler_regular_carrier_covers_strip sensor.realPart sensor.in_strip.1,
 892         by
 893           change 0 < sensor.realPart - 1 / 2
 894           linarith [sensor.in_strip.1]⟩
 895
 896/-! ### §9. The full instantiation certificate -/
 897
 898/-- **Euler Instantiation Certificate.**
 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 σ) ∧