rh_from_cost_finiteness
plain-language theorem explainer
Universal cost finiteness over defect sensors forces every sensor to carry zero charge. Researchers modeling the Riemann hypothesis inside Recognition Science would cite this as the direct implication from bounded annular cost to the absence of nonzero charges. The proof is a one-line wrapper that invokes the nonzero-charge divergence lemma to reach an immediate contradiction.
Claim. If no defect sensor has divergent annular cost, then every defect sensor has charge zero: if $hcf : ∀ sensor : DefectSensor, ¬CostDivergent(sensor)$, then $∀ sensor : DefectSensor, sensor.charge ≠ 0 → ⊥$.
background
CostDivergent(sensor) holds when the annular cost of a defect sensor grows without bound under uniform-charge sampling; the topological floor scales as Θ(m² log N) for charge m ≠ 0, forcing the total cost past any finite bound at large refinement depth N. PhysicalSensor is the subtype of DefectSensor whose T1 defect remains bounded, corresponding to physically realized recognition events on the ledger. The module replaces an earlier global bounded-cost assertion with a three-component architecture: cost divergence (proved for nonzero charge), Euler trace admissibility (proved from instantiation data), and physically realizable ledgers whose scalar proxies stay T1-bounded.
proof idea
The proof is a one-line wrapper. Given a sensor with nonzero charge, nonzero_charge_cost_divergent sensor hm immediately yields CostDivergent sensor; this contradicts the hypothesis hcf that no sensor is cost-divergent, producing False.
why it matters
The declaration supplies one direction of the claimed equivalence between cost finiteness and the Riemann hypothesis inside the Unified RH architecture. It supports the construction of PhysicalSensor as the subtype of realizable sensors, all of which must carry zero charge. The result sits inside the T1-bounded realizability chain and relies on the unconditional divergence lemma for nonzero charges; the converse direction and the boundary-transport hypothesis remain external.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.