EBBA_iff_rh

formal source

 733This theorem makes machine-checkable the observation documented in §9:
 734the bridge hypothesis is not weaker than RH — it IS RH expressed through
 735the T1-bounded realizability architecture. -/
 736theorem EBBA_iff_rh :
 737    EulerBoundaryBridgeAssumption ↔
 738      (∀ sensor : DefectSensor, sensor.charge ≠ 0 → False) :=
 739  ⟨unified_rh, EBBA_of_rh⟩
 740
 741/-! ## §11. RS Ontological Route — Direct T1 Exclusion
 742
 743The two-scalar architecture (§§1–10) introduced a carrier proxy and a cost-
 744tracking collapse scalar, then bridged them with `EulerBoundaryBridgeAssumption`.
 745That bridge is logically equivalent to RH (`EBBA_iff_rh`).
 746
 747This section presents the **direct RS ontological route**, which bypasses the
 748proxy entirely.  The argument is:
 749
 7501. **T1 (Law of Existence):**  `J(0⁺) = ∞`.  Near-zero scalars have unbounded
 751   cost.  Proved: `nothing_cannot_exist`.
 752
 7532. **Cost divergence:**  Charge `m ≠ 0` forces annular cost to grow as
 754   `Θ(m² log N)`.  Proved: `nonzero_charge_cost_divergent`.
 755
 7563. **Cost scalar collapses:**  The cost scalar `1/(1 + annularCost)` is forced
 757   toward zero.  Proved: `realizedDefectCollapseBoundaryApproaching_of_nonzero_charge`.
 758
 7594. **T1 defect diverges:**  The T1 defect of the cost scalar diverges.
 760   Proved: `realizedDefectCollapseScalar_defect_unbounded`.
 761
 7625. **Physical realizability requires bounded T1 defect.**  A sensor whose
 763   physical ledger scalar has unbounded T1 defect violates the Law of
 764   Existence and cannot be physically instantiated.
 765
 766The chain 1–4 is unconditional.  Step 5 is the RS ontological principle: