CostCoveringCert
plain-language theorem explainer
CostCoveringCert bundles an explicit CostCoveringPackage (a realized BudgetedCarrier witness) with the universal assertion that every DefectSensor has its topological floor bounded by the carrier scale. Number theorists studying conditional routes to the Riemann hypothesis cite this structure to certify that the RS cost-covering argument is assembled without naked axioms. The definition is a direct record bundling the package field and the floor-covered quantification over sensors.
Claim. A certificate consists of a budgeted carrier package $P$ together with the property that for every defect sensor $S$ (a point with real part in $(1/2,1)$ at which the inverse zeta function has a pole of order $m = S.charge$), the annular topological floor satisfies $annularTopologicalFloor(N,m) ≤ carrierBudgetScale(P.carrier)$ for all natural numbers $N$.
background
The module assembles the RS cost-covering bridge after the budget interface is made realizable. Its three layers are unconditional annular bounds from AnnularCost.lean, an explicit carrier package, and the conditional theorem that the defect topological floor is controlled by the same carrier scale. CostCoveringPackage is the structure holding a single BudgetedCarrier field; DefectSensor records charge (multiplicity), realPart, and the in-strip predicate; DefectTopologicalFloorCovered is the predicate asserting that the annular topological floor at that charge never exceeds the carrier budget scale. The carrier $C(s) = det_2(I-A(s))^2$ is holomorphic and nonvanishing on Re(s) > 1/2, with annular excess O(R²) along realized zero-charge traces.
proof idea
The declaration is a plain structure definition that directly records the two fields: the package and the universal quantification over sensors of the DefectTopologicalFloorCovered predicate. No tactics or lemmas are applied inside the structure itself; the surrounding rh theorem then applies rh_from_cost_covering to discharge the verified property.
why it matters
CostCoveringCert packages the full conditional RH result for the Recognition Science cost-covering bridge, replacing any prior naked axiom with an explicit BudgetedCarrier witness. It sits at the end of the three-layer architecture described in the module documentation and supplies the hypothesis interface that any downstream consumer must instantiate. The construction closes the topological step in which a zero of zeta with Re(ρ) > 1/2 would force the defect floor to diverge faster than the finite carrier budget, thereby forcing multiplicity zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.