not_costDivergent_of_charge_zero
plain-language theorem explainer
A defect sensor with zero charge cannot have divergent annular cost. Researchers working on the T1-bounded realizability architecture cite this to separate the cost-divergence component from Euler-trace admissibility. The proof assumes divergence at bound 1, constructs a uniform zero-charge annular mesh, shows excess cost vanishes while total cost exceeds 1, and reaches a numerical contradiction via the topological floor.
Claim. Let $S$ be a defect sensor. If the charge of $S$ equals zero, then the annular cost of $S$ does not diverge: there exists a real bound $B$ such that for every refinement depth $N$ and every annular mesh with uniform winding zero the annular cost is at most $B$.
background
In the Unified RH module the architecture separates cost divergence from Euler trace admissibility. CostDivergent holds for a sensor when its annular cost exceeds every bound under uniform-charge sampling at increasing refinement depths $N$. AnnularCost sums the ring costs over an AnnularMesh of $N$ rings, while annularExcess subtracts the topological floor given by annularTopologicalFloor. Upstream, annularCost is shown to diverge as Θ(m² log N) for nonzero charge m via Jensen coercivity.
proof idea
The proof proceeds by contradiction. Assume CostDivergent sensor. Specialize to bound 1 to obtain N and a mesh with uniform charge zero. The excess cost is zero by uniformChargeMesh_excess_zero. The topological floor is zero by annularTopologicalFloor_zero. Unfolding annularExcess and applying linarith yields annularCost equal to zero. This contradicts the assumption that annularCost exceeds 1.
why it matters
This theorem supplies the contrapositive direction for costDivergent_charge_ne_zero, which states that any cost-divergent sensor must have nonzero charge. It fills the cost-divergence component in the Unified RH proof chain: euler_trace_admissible leads to PhysicallyRealizableLedger, and divergence would force boundary approach forbidden by T1. It relies on the annular coercivity result that nonzero charge forces divergence as Θ(m² log N).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.