costDivergent_iff_charge_ne_zero
plain-language theorem explainer
CostDivergent for a defect sensor holds exactly when its charge is nonzero. Researchers formalizing the physical Riemann hypothesis via recognition cost would cite the equivalence to enforce charge neutrality under T1 bounds. The proof is a term-mode construction that pairs the forward lemma nonzero_charge_cost_divergent with the reverse costDivergent_charge_ne_zero.
Claim. For any defect sensor $s$, the annular cost diverges under uniform-charge sampling if and only if the charge of $s$ is nonzero.
background
The Unified RH module replaces a prior global bounded-cost claim with a three-component architecture: cost divergence, Euler trace admissibility, and physically realizable ledger. CostDivergent is defined so that for every real bound B there exists mesh depth N such that any annular mesh whose rings carry winding equal to the sensor charge has annular cost exceeding B; this encodes the quadratic-logarithmic growth for nonzero charge. The setting draws on upstream defect from LawOfExistence and the T1 defect bound that forbids unbounded annular cost for realizable events.
proof idea
The proof is a one-line term wrapper that applies the two directional lemmas: the forward direction from nonzero_charge_cost_divergent and the reverse direction from costDivergent_charge_ne_zero.
why it matters
The equivalence anchors the cost finiteness principle in the Recognition Science framework, where T1 defect bounds prohibit divergent annular cost for physical recognition events. It feeds the PhysicallyRealizableLedger construction and the argument that zeta zeros, treated as ledger events, must carry zero charge. The module note records that physical restriction occurs via the PhysicalSensor subtype rather than a global axiom, closing one link in the chain from annular coercivity to RH realizability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.