defect_floor_exceeds_any_bound
plain-language theorem explainer
This theorem shows that for a defect sensor with nonzero charge the annular topological floor grows without bound in the refinement depth N. Researchers closing the Riemann hypothesis via carrier-defect budget comparisons cite it to force divergence on shared circles. The proof is a one-line wrapper applying the defect topological floor unboundedness lemma.
Claim. Let $m$ be the nonzero charge of a defect sensor. For any real number $K$, there exists a natural number $N$ such that $K$ is strictly less than the annular topological floor evaluated at refinement depth $N$ and charge $m$.
background
The module develops the carrier-defect budget comparison strategy (Phase 4a of the RH closure plan). On identical circles around a hypothetical zero of zeta, the carrier family is holomorphic and nonvanishing with charge zero, so its topological floor is identically zero and its sampled cost equals its excess. The defect family is the reciprocal of zeta, carrying charge $m$ nonzero, so its topological floor grows as Theta of m squared log N. A DefectSensor packages the charge datum; annularTopologicalFloor N m returns the corresponding floor value. Upstream cost definitions from multiplicative recognizers and observer forcing supply the J-cost background used in the surrounding budget decomposition.
proof idea
The proof is a one-line wrapper that applies the lemma defect_topological_floor_unbounded to the sensor, the nonzero-charge hypothesis, and the bound K.
why it matters
It supplies the divergence half of the key result carrier_defect_budget_contradiction named in the module documentation. That result yields the contradiction for any nonzero charge by showing the defect floor eventually exceeds any finite carrier budget on the shared circles. The construction aligns with the module's three-step architecture of carrier family, defect family, and budget transfer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.