zeta_zero_gives_charged_sensor

formal source

  17
  18/-- A zero of zeta in the right half of the critical strip gives a nonphysical
  19nonzero-charge sensor by the already-proved ontological dichotomy. -/
  20theorem zeta_zero_gives_charged_sensor
  21    (ρ : ℂ) (_hzero : riemannZeta ρ = 0)
  22    (hlo : 1 / 2 < ρ.re) (hhi : ρ.re < 1) :
  23    ∃ sensor : DefectSensor, sensor.charge ≠ 0 ∧ sensor.realPart = ρ.re :=
  24  ⟨zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1,
  25    zetaDefectSensor_charge_ne_zero ρ.re ⟨hlo, hhi⟩,
  26    rfl⟩
  27
  28/-- Argument-principle data: a witnessed defect sensor carries genuine
  29zeta-derived phase-family data. -/
  30structure ArgumentPrincipleSensorCert where
  31  witnessed_phase_family :
  32    ∀ sensor : WitnessedDefectSensor, sensor.charge ≠ 0 →
  33      ∃ zfd : ZetaPhaseFamilyData,
  34        zfd.sensor = sensor.toDefectSensor ∧
  35          zfd.phaseFamily.sensor = sensor.toDefectSensor
  36  zero_gives_charged_sensor :
  37    ∀ ρ : ℂ, riemannZeta ρ = 0 → 1 / 2 < ρ.re → ρ.re < 1 →
  38      ∃ sensor : DefectSensor, sensor.charge ≠ 0 ∧ sensor.realPart = ρ.re
  39
  40/-- The current argument-principle sensor certificate. -/
  41def argumentPrincipleSensorCert : ArgumentPrincipleSensorCert where
  42  witnessed_phase_family := fun sensor hm =>
  43    honest_argument_principle_phase_family sensor hm
  44  zero_gives_charged_sensor := zeta_zero_gives_charged_sensor
  45
  46end NumberTheory
  47end IndisputableMonolith