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

rh_right_half_certificate

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)

 258theorem rh_right_half_certificate (hrs : RSPhysicalThesis) :
 259    ∀ (s : ℂ), riemannZeta s = 0 → s.re > 1/2 → s.re = 1/2 :=

proof body

Term-mode proof.

 260  rh_right_half_from_rs hrs
 261
 262/-! ### §7. Connecting WitnessedDefectSensor (detailed version)
 263
 264The above proof uses a unit-charge sensor for simplicity.  For a
 265stronger result that tracks the actual multiplicity, the
 266`WitnessedDefectSensor` from `EulerInstantiation.lean` provides:
 267
 268- `order_witness : meromorphicOrderAt zetaReciprocal rho = ↑(-charge)`
 269- `toDefectSensor` projects to a `DefectSensor`
 270- The dichotomy then gives `charge = 0 ↔ PhysicallyExists`
 271
 272This connects the actual analytic structure (meromorphic order of ζ⁻¹)
 273to the RS existence criterion, but requires more Mathlib integration
 274(extracting the integer order from `meromorphicOrderAt`). -/
 275
 276/-- Any `WitnessedDefectSensor` with nonzero charge produces a
 277`DefectSensor` that fails `PhysicallyExists`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.