rh_no_zeros_in_strip
plain-language theorem explainer
The theorem shows that assuming bounded annular cost for every nonzero-charge defect sensor forces all such charges to vanish, exposing an inconsistency in the legacy analytic route. Researchers auditing the Euler product instantiation of the RS cost framework would cite it to confirm the contradiction with prior unboundedness results. The proof is a direct term application of the complex-analysis zero-free criterion to the supplied bounded-cost witness.
Claim. If for every defect sensor with nonzero charge there exists a constant $K$ such that the annular cost of the canonical sampled family mesh is at most $K$ for all mesh sizes, then no defect sensor has nonzero charge.
background
The EulerInstantiation module shows how the Euler product of the zeta function supplies a concrete carrier satisfying the abstract sensor and cost interfaces from AnnularCost and CostCoveringBridge. DeprecatedDefectAnnularCostBounded asserts that the annular cost remains uniformly bounded over the canonical defect sampled family for any nonzero charge. The defect functional is the J-cost of the multiplicative recognizer, and upstream results supply the canonical arithmetic object together with the cost of recognition events as the derived J-cost. This setting derives a conditional zero-free region via the cost-covering axiom but marks the bounded-cost hypothesis as inconsistent with the already-established unboundedness theorem.
proof idea
The proof is a one-line term wrapper that applies rh_from_complex_analysis_axioms to the bounded-cost hypothesis for each sensor and charge witness.
why it matters
This result closes the deprecated bounded-cost path to RH by deriving a contradiction, directing attention to the preferred UnifiedRH.unified_rh or AnalyticTrace.ZeroFreeCriterion. It fills the inconsistency step flagged in the module architecture after the Euler product is shown to satisfy EulerCarrier and RegularCarrier. The declaration touches the open question of which cost-covering axiom remains consistent with the full RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.