zetaDefectSensor_charge_ne_zero

formal source

  55  simp [zetaDefectSensor]
  56
  57/-- A sensor with charge 1 has nonzero charge. -/
  58theorem zetaDefectSensor_charge_ne_zero (σ : ℝ)
  59    (hstrip : 1/2 < σ ∧ σ < 1) :
  60    (zetaDefectSensor σ hstrip 1).charge ≠ 0 := by
  61  simp [zetaDefectSensor]
  62
  63/-- **Core unconditional result.** Any `DefectSensor` with nonzero
  64charge fails the `PhysicallyExists` predicate.  Direct corollary of
  65`ontological_dichotomy`. No custom axioms. -/
  66theorem nonzero_charge_not_physical (sensor : DefectSensor)
  67    (hm : sensor.charge ≠ 0) :
  68    ¬ PhysicallyExists sensor := by
  69  intro hphys
  70  exact hm ((ontological_dichotomy sensor).mpr hphys)
  71
  72/-- For any point in the strip (1/2, 1), the unit-charge sensor
  73is not physically realizable.  This is the dichotomy applied to a
  74concrete sensor. -/
  75theorem unit_sensor_not_physical (σ : ℝ) (hstrip : 1/2 < σ ∧ σ < 1) :
  76    ¬ PhysicallyExists (zetaDefectSensor σ hstrip 1) :=
  77  nonzero_charge_not_physical _ (zetaDefectSensor_charge_ne_zero σ hstrip)
  78
  79/-- **If** there is a zero of `riemannZeta` at a point with real part in
  80(1/2, 1), **then** there exists a DefectSensor that:
  81- has nonzero charge,
  82- is centered at that real part,
  83- is NOT physically realizable.
  84
  85The existence of the zero is the hypothesis; the non-physicality is
  86proved from the dichotomy. -/
  87theorem strip_zero_gives_nonphysical_sensor (ρ : ℂ)
  88    (_hzero : riemannZeta ρ = 0)