zeroFreeCriterion_of_vectorC

formal source

 273
 274/-- A successful Vector C bridge upgrades the proved Euler-carrier and honest
 275phase-family infrastructure into a complete `ZeroFreeCriterion`. -/
 276noncomputable def zeroFreeCriterion_of_vectorC
 277    (vc : VectorCChargeZeroBridge) :
 278    ZeroFreeCriterion where
 279  logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
 280  carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
 281  honest_phase_family := honest_argument_principle_phase_family
 282  charge_zero_of_honest_phase := charge_zero_of_honest_phase_of_vectorC vc
 283
 284/-- Therefore any successful Vector C bridge proves RH via the existing
 285analytic route. -/
 286theorem direct_rh_from_vectorC_bridge (vc : VectorCChargeZeroBridge) :
 287    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 288  rh_from_zero_free_criterion (zeroFreeCriterion_of_vectorC vc)
 289
 290/-! ### §5. Full RH from complex-analysis axioms (legacy path)
 291
 292**WARNING**: The theorems below depend on the deprecated axiom
 293`defect_annular_cost_bounded` which is logically inconsistent with proved
 294results. They are retained only as the legacy reference path. The preferred
 295routes are:
 296- Ontology: `UnifiedRH.unified_rh` (external bridge hypothesis)
 297- Analytic: `ZeroFreeCriterion` via honest ζ⁻¹ phase data (§4 above) -/
 298
 299/-- **The Riemann Hypothesis (legacy analytic route).**
 300
 301⚠ DEPRECATED: depends on `defect_annular_cost_bounded`.
 302For the preferred route, see `UnifiedRH.unified_rh` (ontology) or
 303`direct_rh_from_zero_free_criterion` (analytic). -/
 304theorem analytic_rh (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
 305    (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) :
 306    False :=