euler_rh_conditional

formal source

 933
 934    This theorem connects the concrete number theory (this file)
 935    to the abstract conditional RH (CostCoveringBridge.lean). -/
 936theorem euler_rh_conditional (pkg : CostCoveringPackage)
 937    (hcover : ∀ sensor : DefectSensor, DefectTopologicalFloorCovered pkg sensor)
 938    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) : False :=
 939  rh_from_cost_covering pkg sensor hm (hcover sensor)
 940
 941/-- The complete RH conditional on RS, given an explicit cost-covering package
 942    and topological-floor coverage. -/
 943theorem riemann_hypothesis_euler_conditional (pkg : CostCoveringPackage)
 944    (hcover : ∀ sensor : DefectSensor, DefectTopologicalFloorCovered pkg sensor) :
 945    ∀ (σ₀ : ℝ) (hσ : 1/2 < σ₀) (hσ1 : σ₀ < 1) (m : ℤ) (hm : m ≠ 0),
 946    let sensor : DefectSensor := ⟨m, σ₀, ⟨hσ, hσ1⟩⟩
 947    False :=
 948  fun σ₀ hσ hσ1 m hm => euler_rh_conditional pkg hcover ⟨m, σ₀, ⟨hσ, hσ1⟩⟩ hm
 949
 950/-! ### §11. Sampled-trace Euler carrier (axiom-free) -/
 951
 952/-- The Euler carrier packaged as a `BudgetedCarrier` using the sampled-trace
 953infrastructure from `SampledTrace.lean`. This uses the zero-winding certificate
 954from `EulerCarrierComplex.lean` instead of a synthetic zero-charge trace.
 955
 956The key difference from `eulerBudgetedCarrier` is that the zero-winding
 957property is derived from the carrier's holomorphy and nonvanishing
 958(via `eulerZeroWindingCert`), not assumed. -/
 959noncomputable def eulerSampledBudgetedCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 960    BudgetedCarrier :=
 961  SampledTrace.sampledBudgetedCarrier
 962    (EulerCarrierComplex.eulerZeroWindingCert σ₀ hσ)
 963    (carrierDerivBound σ₀)
 964    (carrierDerivBound_pos hσ)
 965    (σ₀ - 1/2)
 966    (by linarith)