CostDivergent
plain-language theorem explainer
A defect sensor is cost-divergent when its annular cost exceeds every finite bound under uniform winding sampling. Researchers proving the Recognition Science equivalence between cost finiteness and the Riemann Hypothesis cite this definition to isolate the nonzero charge case. The definition encodes the growth of the topological floor as Θ(m² log N) for charge m.
Claim. A defect sensor $s$ is cost-divergent if for every real bound $B$ there exists a mesh depth $N$ such that every annular mesh of depth $N$ with all rings having winding number equal to the charge of $s$ has annular cost strictly larger than $B$.
background
The Unified RH module replaces the prior bounded-total-cost ledger with a three-component architecture: cost divergence for nonzero-charge sensors, Euler trace admissibility, and boundary transport. CostDivergent is the first component and states that nonzero charge forces annular cost to diverge unconditionally from annular coercivity. DefectSensor carries an integer charge. AnnularMesh N is a depth-N refinement whose rings carry winding numbers. annularCost sums the J-costs over the mesh, where J-cost is the derived cost of the multiplicative recognizer comparator.
proof idea
This is a direct definition. It encodes the unboundedness condition on annularCost for meshes whose rings all match the fixed sensor charge, using the cost function induced by MultiplicativeRecognizerL4.cost and ObserverForcing.cost.
why it matters
CostDivergent is the base of the cost-finiteness principle. It feeds costDivergent_iff_charge_ne_zero and cost_finiteness_iff_rh, which equate universal cost finiteness with the Riemann Hypothesis. The definition aligns with the T1 defect boundary in the forcing chain and supplies the divergence half of the unified RH equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.