zetaDefectSensor_charge_one

formal source

  49
  50/-- A sensor constructed via `zetaDefectSensor` with multiplicity 1 has
  51charge 1. -/
  52theorem zetaDefectSensor_charge_one (σ : ℝ)
  53    (hstrip : 1/2 < σ ∧ σ < 1) :
  54    (zetaDefectSensor σ hstrip 1).charge = 1 := by
  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,