nonzero_charge_cost_divergent
plain-language theorem explainer
Nonzero charge on a defect sensor forces its annular cost to diverge without bound under uniform-charge sampling. Researchers establishing cost-finiteness equivalences to the Riemann hypothesis cite this result to separate divergent from admissible sensors. The proof is a one-line wrapper applying the defect_cost_unbounded lemma.
Claim. Let $s$ be a defect sensor with charge $m$. If $m ≠ 0$, then for every real bound $B$ there exists a refinement depth $N$ such that every annular mesh of depth $N$ whose rings have winding number $m$ satisfies annular cost $> B$.
background
The Unified RH module organizes T1-bounded realizability into four components: CostDivergent (annular cost unbounded for nonzero charge), EulerTraceAdmissible (Euler carrier convergent and nonvanishing), PhysicallyRealizableLedger (scalar proxy with bounded T1 defect), and DivergenceWitnessesBoundary (external bridge hypothesis). CostDivergent is defined precisely as the statement that the topological floor of annular cost grows as Θ(m² log N) for charge m ≠ 0, forcing the total past any finite bound at large N. The module replaces earlier total-cost boundedness claims with this architecture, drawing on LawOfExistence for defect sensors and EulerInstantiation for carrier data.
proof idea
The proof is a one-line wrapper that applies the defect_cost_unbounded lemma directly to the sensor and the hypothesis that its charge is nonzero.
why it matters
This supplies the forward direction of costDivergent_iff_charge_ne_zero, which is invoked by cost_finiteness_iff_rh and rh_from_cost_finiteness to equate cost finiteness with the absence of nonzero-charge sensors. It supports ontological_exclusion by showing divergence is forced whenever charge is nonzero, consistent with T1 boundary exclusion. The result closes the cost-divergence half of the RS physical thesis decomposition while leaving the external bridge hypothesis open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.