defect_topological_floor_unbounded
plain-language theorem explainer
For any DefectSensor with nonzero charge the annular topological floor diverges with mesh depth. Workers on the cost-covering route to the Riemann hypothesis cite the result to separate finite carrier budgets from defect costs. The proof obtains an N from the unbounded-cost lemma, builds the uniform-charge mesh, confirms zero excess, and equates cost to floor.
Claim. Let $s$ be a DefectSensor whose charge $m$ satisfies $m ≠ 0$. Then for every real $B$ there exists a natural number $N$ such that $B < $ annularTopologicalFloor $N$ $m$.
background
DefectSensor is the structure recording a pole of order $m$ (the charge) of $ζ(s)^{-1}$ at a point with real part strictly between 1/2 and 1. annularTopologicalFloor $N$ $m$ is the minimal annular cost realized by any mesh of depth $N$ carrying total charge $m$; it is defined in the AnnularCost layer via the excess-adjusted phi-cost functional. The CostCoveringBridge module supplies the explicit carrier package and the conditional RH statement that assumes the floor is covered by a finite carrier scale. Upstream lemmas defect_cost_unbounded and uniformChargeMesh_excess_zero supply the cost divergence and the zero-excess identity used here.
proof idea
The tactic proof opens with intro B, obtains N from defect_cost_unbounded, constructs the uniformChargeMesh of that depth, shows B is below its annularCost, records that the mesh excess is identically zero, deduces that annularCost equals annularTopologicalFloor, and closes the existential.
why it matters
The theorem is invoked directly by carrier_defect_budget_contradiction, defect_floor_exceeds_any_bound, not_DefectTopologicalFloorCovered and rh_from_cost_covering. It supplies the divergence step that forces any supposed zero of multiplicity ≥1 to violate the finite carrier budget, thereby completing the RS cost-covering argument for the absence of zeros with real part >1/2. The result sits inside the unconditional annular analysis layer of the CostCoveringBridge architecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.