pith. machine review for the scientific record. sign in
theorem proved term proof

strip_zero_gives_nonphysical_sensor

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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 :=

proof body

Term-mode proof.

  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
 106Within the RS framework, this follows from:
 107- The Euler product `ζ(s) = ∏_p (1 − p^{−s})⁻¹` is the ledger balance
 108  equation (each prime `p` is a debit/credit pair on the arithmetic ledger).
 109- A zero of ζ is a point where the ledger fails to balance — a defect.
 110- The Law of Existence (T₁) requires every physical event to have
 111  bounded defect cost.
 112
 113**In ZFC alone, this is an additional postulate.**
 114**Within the RS framework (T₀–T₈), it is derivable.** -/

depends on (27)

Lean names referenced from this declaration's body.