EBBA_of_cost_finiteness

formal source

 817    exact hrh sensor (costDivergent_charge_ne_zero sensor hdiv)
 818
 819/-- The RS Cost Finiteness Principle implies `EulerBoundaryBridgeAssumption`. -/
 820theorem EBBA_of_cost_finiteness
 821    (hcf : ∀ sensor : DefectSensor, ¬CostDivergent sensor) :
 822    EulerBoundaryBridgeAssumption :=
 823  EBBA_of_rh (cost_finiteness_iff_rh.mp hcf)
 824
 825/-- `EulerBoundaryBridgeAssumption` implies cost finiteness. -/
 826theorem cost_finiteness_of_EBBA
 827    (bridge : EulerBoundaryBridgeAssumption) :
 828    ∀ sensor : DefectSensor, ¬CostDivergent sensor :=
 829  cost_finiteness_iff_rh.mpr (unified_rh bridge)
 830
 831/-! ### §11b. Direct T1 Defect Route — One Scalar
 832
 833The strongest version of the ontological argument uses a single scalar
 834and no proxy at all.  The cost scalar `1/(1 + annularCost)` is both:
 835
 836* **The physical ledger entry** (in RS, the ledger records `1/(1 + cost)`)
 837* **The T1-testable observable** (its defect IS the cost)
 838
 839For charge `0`: cost is bounded, cost scalar stays away from `0`, T1 defect
 840is bounded.  The sensor has a physically realizable ledger.
 841
 842For charge `≠ 0`: cost diverges, cost scalar → `0`, T1 defect → `∞`.
 843The sensor **cannot** have a physically realizable ledger.
 844
 845T1 says: only sensors with physically realizable ledgers exist.
 846Therefore only charge-`0` sensors exist.  That is RH. -/
 847
 848/-- **Direct T1 exclusion**: if the cost scalar's T1 defect were bounded for
 849a nonzero-charge sensor, that contradicts the proved divergence.  This is the
 850one-scalar core of the RS ontological argument. -/