nonzero_charge_impossible

formal source

  61
  62/-- No sensor with nonzero charge can physically exist.
  63Contrapositive of the dichotomy. -/
  64theorem nonzero_charge_impossible (sensor : DefectSensor)
  65    (hm : sensor.charge ≠ 0) :
  66    ¬PhysicallyExists sensor :=
  67  nonzero_charge_not_physical sensor hm
  68
  69/-- For any point in the strip (1/2, 1), the unit-charge sensor is
  70not physically realizable.  Pure consequence of the dichotomy. -/
  71theorem unit_sensor_not_physical_cert (σ : ℝ) (hstrip : 1/2 < σ ∧ σ < 1) :
  72    ¬PhysicallyExists (zetaDefectSensor σ hstrip 1) :=
  73  unit_sensor_not_physical σ hstrip
  74
  75/-! ### The RS-conditional result -/
  76
  77/-- **The Riemann Hypothesis, conditional on the RS Physical Thesis.**
  78
  79`RSPhysicalThesis` states that every nontrivial zeta zero in the strip
  80is a physical recognition event.  Given this, no strip zeros can exist
  81(because physical sensors have charge 0, but zeros have positive
  82multiplicity).  Combined with the classical zero-free region
  83(`Re(s) ≥ 1`), this gives Mathlib's `RiemannHypothesis`.
  84
  85To inspect the axiom footprint:
  86```
  87#print axioms riemann_hypothesis_from_rs
  88```
  89-/
  90theorem riemann_hypothesis_from_rs :
  91    RSPhysicalThesis → RiemannHypothesis :=
  92  rh_certificate
  93
  94/-! ### The full certificate (zero sorry) -/