defect_cost_unbounded
plain-language theorem explainer
Any defect sensor with nonzero charge forces annular costs on uniform-winding meshes to exceed every finite bound B at large enough refinement depth N. Recognition Science cites this as the core contradiction engine in its cost-covering argument for the Riemann hypothesis. The proof scales the divergent harmonic series by a positive constant C built from the squared charge, then applies annular coercivity to obtain the strict lower bound on annularCost.
Claim. Let $S$ be a defect sensor with nonzero charge $m$. For every real number $B$ there exists a natural number $N$ such that every annular mesh of depth $N$ whose rings all carry winding number $m$ has annular cost strictly larger than $B$.
background
A DefectSensor is the structure that records a hypothetical zero of zeta inside the critical strip: its charge field is the multiplicity $m$ of the zero (equivalently the order of the pole of zeta inverse), while realPart and in_strip locate the zero with Re > 1/2. AnnularMesh N is a concentric-ring discretization at refinement depth N; annularCost integrates the RS defect functional J over the mesh, weighted by the constant kappa from zero-parameter gravity. The module packages the three-layer cost-covering architecture: unconditional annular bounds, an explicit carrier package, and the conditional RH statement that follows once the topological floor is shown to be covered.
proof idea
Fix arbitrary B. Define the positive constant C = pi squared times kappa over 4 times charge squared, using sq_pos_iff and kappa_pos for positivity. Invoke the atTop filter property of the divergent harmonic series to extract N0 such that the partial sum up to N0+1 exceeds B/C + 1. Set N = N0 + 1. For any mesh obeying the uniform winding hypothesis, equate its total charge to the sensor charge, then apply annular_coercivity to obtain annularCost at least C times the partial sum. Chain the scaled inequality with this lower bound to conclude B < annularCost.
why it matters
The lemma supplies the unconditional divergence statement that is repackaged as CostDivergent and nonzero_charge_cost_divergent in UnifiedRH; it is invoked directly by defect_topological_floor_unbounded and by the realized-family excess bounds in DefectSampledTrace. The doc-comment identifies it as the key contradiction lemma: a zero with Re > 1/2 produces a pole whose topological floor grows as m squared log N and therefore violates any finite carrier scale. This closes the unconditional analysis layer before the realized-carrier budget is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.