rh_from_complex_analysis_axioms
plain-language theorem explainer
The result records that assuming uniform boundedness of annular costs for any nonzero-charge defect sensor in the Euler product setting produces a contradiction. Analytic number theorists tracing legacy routes to the Riemann Hypothesis cite it to mark the failure of the bounded-cost axiom. The proof is a direct one-line application of the dedicated inconsistency lemma.
Claim. Let $S$ be a defect sensor with nonzero charge $m$. Suppose there exists $K$ such that the annular cost of every mesh in the canonical sampled family generated by $S$ is at most $K$. Then a contradiction follows.
background
The EulerInstantiation module embeds the Euler product of the zeta function into the abstract RS carrier/sensor framework of AnnularCost and CostCoveringBridge. A DefectSensor at a prospective zero records the multiplicity (charge) of the pole of zeta inverse together with the real part of its location. The hypothesis DeprecatedDefectAnnularCostBounded asserts existence of a uniform bound K on the annular costs of the canonical defect sampled family for that sensor.
proof idea
The proof is a one-line wrapper that applies defect_annular_cost_bounded_inconsistent to the supplied sensor, nonzero-charge hypothesis, and boundedness assumption.
why it matters
It closes the deprecated bounded-cost path inside the analytic route to RH. The declaration is invoked directly by analytic_rh in AnalyticTrace and by rh_from_single_axiom in ArgumentPrincipleProved; both are flagged as legacy in favor of UnifiedRH.unified_rh or AnalyticTrace.ZeroFreeCriterion. The module architecture note records the instantiation chain primes to Hilbert-Schmidt norm to holomorphic nonvanishing carrier to cost-covering axiom, which this result shows cannot be satisfied under the bounded-cost hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.