cost_finiteness_iff_rh
plain-language theorem explainer
Cost finiteness for every defect sensor is equivalent to the nonexistence of any defect sensor with nonzero charge. Researchers deriving the Riemann hypothesis from Recognition Science cost bounds would cite this biconditional when connecting annular cost limits to the absence of off-critical zeros. The proof constructs the equivalence in two directions by invoking the established implications between nonzero charge and cost divergence.
Claim. The annular cost remains finite for every defect sensor if and only if no defect sensor carries nonzero charge: $ (∀ sensor, ¬ cost-divergent(sensor)) ↔ (∀ sensor, charge(sensor) = 0) $.
background
The module presents a three-component architecture replacing earlier total-cost bounds with structured realizability. A defect sensor models a potential zeta zero, carrying an integer charge (multiplicity) and real-part location. CostDivergent states that the annular cost of a sensor exceeds every finite bound under uniform-charge mesh refinement, growing as Θ(m² log N) for nonzero m.
proof idea
The term-mode proof opens the biconditional with constructor. The forward direction applies the lemma that nonzero charge forces cost divergence. The reverse direction applies the lemma that cost divergence forces nonzero charge.
why it matters
This equivalence anchors the Unified RH module and supplies the two directions used by cost_finiteness_of_EBBA and EBBA_of_cost_finiteness. It realizes the Recognition Science claim that the Riemann hypothesis is equivalent to the cost-finiteness principle within the T1-bounded ledger. The result closes the loop between the eight-tick octave and the Euler-boundary bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.