not_DefectTopologicalFloorCovered
plain-language theorem explainer
A finite carrier scale cannot cover the defect topological floor for any sensor with nonzero charge across all mesh depths. Researchers bridging Recognition Science cost-covering to the Riemann Hypothesis cite this result to separate the uniform bound from the required carrier-defect relation. The proof assumes coverage and invokes the unboundedness of the floor under nonzero charge to reach an immediate contradiction via comparison of growth rates.
Claim. Let $P$ be a cost-covering package and let $S$ be a defect sensor whose charge (pole order) is nonzero. Then the defect topological floor of $S$ is not bounded above by the carrier budget scale of $P$ for every mesh depth $N$.
background
CostCoveringPackage supplies an explicit BudgetedCarrier witness together with its annular excess budget; DefectSensor records a pole of order $m$ (the charge) at a point with real part strictly between $1/2$ and $1$; DefectTopologicalFloorCovered asserts that the annular topological floor at every depth $N$ stays below the carrier scale. The module sets the local setting as the third layer of the RS cost-covering architecture: after unconditional annular bounds are established in AnnularCost, an explicit package is supplied so that the conditional statement (no zeros of zeta with real part exceeding $1/2$) can be stated without a naked axiom.
proof idea
One-line wrapper that applies the upstream lemma defect_topological_floor_unbounded. Assume coverage; extract a depth $N$ at which the floor exceeds the carrier scale; obtain the contradiction by not_lt_of_ge.
why it matters
The result feeds directly into carrier_side_obstruction (which shows the sampled Euler package cannot cover nonzero charge) and into eulerSampledFloorCovered_iff_charge_zero (which equates coverage with charge zero). It isolates the genuinely nontrivial step quoted in the doc-comment: relating the carrier witness to the defect by more than a uniform scalar bound. Within the Recognition framework this closes the conditional RH bridge once a concrete package is exhibited, advancing the T5-T8 chain by converting the cost-covering axiom into a concrete obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.