zetaDefectSensor_charge_ne_zero
plain-language theorem explainer
The theorem shows that a unit-charge DefectSensor at real part σ in (1/2, 1) has nonzero charge. Researchers bridging Mathlib's riemannZeta to the Recognition Science ledger framework cite it when proving that hypothetical strip zeros yield non-physical sensors. The proof is a one-line simplification that unfolds the definition of zetaDefectSensor.
Claim. Let $σ ∈ ℝ$ satisfy $1/2 < σ < 1$. The charge of the defect sensor at $σ$ with multiplicity 1 is nonzero.
background
DefectSensor is the structure from CostCoveringBridge that records the multiplicity (charge) of a zero of riemannZeta, its real part, and the condition that the real part lies in the right half of the critical strip. zetaDefectSensor, defined in EulerInstantiation, builds such a sensor from a real part σ in (1/2, 1) together with a positive integer multiplicity. The ZetaLedgerBridge module closes the formal gap between this concrete construction and the abstract PhysicallyExists predicate, whose equivalence to zero charge is given by the ontological_dichotomy theorem in UnifiedRH.
proof idea
The proof is a one-line wrapper that applies simp on the definition of zetaDefectSensor, which directly sets the charge field to 1.
why it matters
This lemma supplies the nonzero-charge fact required by downstream results such as strip_zero_gives_nonphysical_sensor and unit_sensor_not_physical, which then invoke ontological_dichotomy to conclude non-physicality. It supports the RSPhysicalThesis by showing that any strip zero produces a sensor that fails the physical-existence predicate, and it is invoked in no_strip_zeros_of_decomposed_data and zeroInducedBridge_iff_no_strip_zeros to derive the absence of such zeros under the RS thesis. The result sits at the interface between the phi-forcing chain and the concrete zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.