costDivergent_charge_ne_zero
plain-language theorem explainer
Any defect sensor whose annular cost diverges under uniform-charge sampling must carry nonzero charge. Workers on the T1-bounded realizability architecture cite this to close the equivalence between cost divergence and nonzero charge. The argument reduces directly to the contrapositive that zero charge implies bounded cost.
Claim. Let $s$ be a defect sensor. If the annular cost of $s$ diverges, then the charge of $s$ is nonzero.
background
In the Unified RH module the architecture replaces earlier total-cost boundedness claims with three components. CostDivergent(sensor) asserts that for every real bound B there exists a refinement depth N such that every annular mesh whose rings have winding number equal to the sensor charge has annular cost exceeding B. This encodes the growth Θ(m² log N) for charge m ≠ 0. The defect functional is defined by defect(x) = J(x).
proof idea
The proof assumes for contradiction that the charge is zero and invokes the lemma not_costDivergent_of_charge_zero to obtain an immediate contradiction with the divergence hypothesis.
why it matters
This supplies the backward direction of the equivalence CostDivergent(s) ↔ s.charge ≠ 0. It is invoked directly in costDivergent_iff_charge_ne_zero, cost_finiteness_iff_rh, and euler_divergence_witnesses_boundary. The result supports the RS Cost Finiteness Principle and the claim that divergence forces approach to the T1 boundary x = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.