unit_sensor_not_physical
Any real σ strictly between 1/2 and 1 produces a unit-charge defect sensor from the Riemann zeta function that fails to be physically realizable. Number theorists connecting analytic zeros to the Recognition Science ledger framework cite this to convert a hypothetical strip zero into a concrete non-physical object. The proof is a direct one-line application of the nonzero-charge non-physicality lemma to the pre-proved charge fact for this sensor.
claimFor any real number $σ$ with $1/2 < σ < 1$, the defect sensor constructed from the Riemann zeta function with unit charge at real part $σ$ is not physically realizable.
background
The module bridges the abstract DefectSensor and PhysicallyExists framework from UnifiedRH to Mathlib's riemannZeta. UnifiedRH establishes the ontological dichotomy: a sensor is physically realizable if and only if its charge is zero. EulerInstantiation supplies zetaDefectSensor, which builds a concrete DefectSensor from strip data (real part σ in (1/2,1)) together with a chosen charge. The present theorem applies the dichotomy to the unit-charge case of this construction.
proof idea
The proof is a one-line wrapper that applies nonzero_charge_not_physical to the fact zetaDefectSensor_charge_ne_zero σ hstrip. No further tactics or reductions are required.
why it matters in Recognition Science
This theorem supplies the key step for no_strip_zeros_from_rs, which shows that the RS Physical Thesis (every strip zero is a physical ledger event) contradicts the existence of any zero in (1/2,1). It thereby enables the derivation of Mathlib's RiemannHypothesis from the RS thesis. The result closes the formalization gap by instantiating the abstract ontological dichotomy on the concrete zeta sensor.
scope and limits
- Does not prove or disprove the existence of zeros in the open strip.
- Does not invoke the Riemann hypothesis as a premise.
- Applies only to unit-charge sensors; other charges require separate arguments.
- Does not address zeros on the critical line Re = 1/2.
Lean usage
unit_sensor_not_physical ρ.re ⟨hlo, hhi⟩ (hrs ρ hzero hlo hhi)formal statement (Lean)
75theorem unit_sensor_not_physical (σ : ℝ) (hstrip : 1/2 < σ ∧ σ < 1) :
76 ¬ PhysicallyExists (zetaDefectSensor σ hstrip 1) :=
proof body
Term-mode proof.
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. -/