rh_from_cost_covering
plain-language theorem explainer
The theorem shows that a cost-covering package together with a defect sensor of nonzero multiplicity whose annular topological floor stays below the carrier budget scale produces a contradiction. Researchers deriving conditional forms of the Riemann hypothesis cite it as the explicit bridge from the RS cost-covering condition to the exclusion of zeros with real part larger than one half. The proof is a direct term extraction of an unbounded floor value followed by an immediate comparison to the covering bound.
Claim. Let $P$ be a cost-covering package and let $S$ be a defect sensor with nonzero multiplicity whose real part lies strictly between $1/2$ and $1$. If the annular topological floor generated by the multiplicity of $S$ is bounded above by the carrier budget scale of $P$ for every natural number $N$, then a contradiction follows.
background
In the CostCoveringBridge module the carrier is the holomorphic nonvanishing function $C(s) = det_2(I-A(s))^2 = prod_p (1-p^{-s})^2 exp(2p^{-s})$ on Re(s) > 1/2. A CostCoveringPackage is a structure containing an explicit BudgetedCarrier witness for the realized carrier trace and its annular excess budget. A DefectSensor records the multiplicity (charge) of a zero of zeta, its real part, and the fact that the real part lies inside the critical strip. The predicate DefectTopologicalFloorCovered asserts that for all N the annular topological floor produced by the sensor charge is at most the carrier budget scale.
proof idea
The term proof first invokes the lemma defect_topological_floor_unbounded on the given sensor, its nonzero charge, and the carrier budget scale to obtain an N at which the floor strictly exceeds the budget. It then applies not_lt_of_ge to the covering hypothesis evaluated at that N and the extracted lower bound, yielding falsehood.
why it matters
This is the central theorem of the CostCoveringBridge module and feeds directly into the certificate CostCoveringCert as well as the corollaries riemann_hypothesis_conditional and euler_rh_conditional. It supplies the conditional step in the Recognition Science framework: the cost-covering axiom implies zeta has no zeros with real part exceeding 1/2. Combined with the functional equation symmetry, the full Riemann hypothesis follows. It leaves open the concrete construction of a carrier package that would discharge the covering hypothesis without assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.