pith. machine review for the scientific record. sign in
theorem proved term proof

EBBA_iff_rh

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 736theorem EBBA_iff_rh :
 737    EulerBoundaryBridgeAssumption ↔
 738      (∀ sensor : DefectSensor, sensor.charge ≠ 0 → False) :=

proof body

Term-mode proof.

 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:
 767**when the arithmetic is physical, infinite costs become impossible.**
 768
 769In the two-scalar framing this appears as a bridge between distinct scalars.
 770In the one-scalar framing it is a direct consequence of T1: the physical
 771ledger scalar IS the cost scalar, and T1 forbids its defect from diverging. -/
 772
 773/-- `CostDivergent` is equivalent to nonzero charge.  Forward direction is
 774`nonzero_charge_cost_divergent`; backward is `costDivergent_charge_ne_zero`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more