unit_sensor_not_physical

formal source

  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)
  89    (hlo : 1/2 < ρ.re) (hhi : ρ.re < 1) :
  90    ∃ sensor : DefectSensor,
  91      sensor.charge ≠ 0 ∧ ¬ PhysicallyExists sensor :=
  92  ⟨zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1,
  93   zetaDefectSensor_charge_ne_zero ρ.re ⟨hlo, hhi⟩,
  94   unit_sensor_not_physical ρ.re ⟨hlo, hhi⟩⟩
  95
  96/-! ### §2. The RS Physical Thesis -/
  97
  98/-- **The RS Physical Thesis (for arithmetic).**
  99
 100This is the single non-mechanical ingredient of the RS argument for RH.
 101It asserts that every nontrivial zero of `riemannZeta` in the critical
 102strip corresponds to a physical recognition event on the arithmetic
 103ledger, and therefore its associated DefectSensor must satisfy
 104`PhysicallyExists`.
 105