charge_zero_cost_scalar_t1_bounded

formal source

 856
 857/-- For charge `0`, the Euler ledger scalar `1` has T1 defect `0` — perfectly
 858bounded.  The charge-`0` sector IS physically realizable. -/
 859theorem charge_zero_cost_scalar_t1_bounded (sensor : DefectSensor)
 860    (hzero : sensor.charge = 0) :
 861    ∃ K : ℝ, ∀ N : ℕ,
 862      IndisputableMonolith.Foundation.LawOfExistence.defect
 863        (eulerLedgerScalarState sensor N) ≤ K := by
 864  refine ⟨0, fun N => ?_⟩
 865  simp [eulerLedgerScalarState, hzero,
 866        IndisputableMonolith.Foundation.LawOfExistence.defect_at_one]
 867
 868/-- The full ontological dichotomy: the cost scalar is T1-bounded iff
 869charge `= 0`.  This IS the RS ontological argument for RH:
 870
 871* Charge `0` ↔ bounded T1 defect ↔ physically realizable ↔ exists
 872* Charge `≠ 0` ↔ unbounded T1 defect ↔ not realizable ↔ does not exist -/
 873theorem ontological_dichotomy (sensor : DefectSensor) :
 874    (sensor.charge = 0) ↔
 875      ∃ K : ℝ, ∀ N : ℕ,
 876        IndisputableMonolith.Foundation.LawOfExistence.defect
 877          (eulerLedgerScalarState sensor N) ≤ K := by
 878  constructor
 879  · exact charge_zero_cost_scalar_t1_bounded sensor
 880  · intro ⟨K, hK⟩
 881    by_contra hm
 882    have : ∀ N, eulerLedgerScalarState sensor N =
 883        realizedDefectCollapseScalar sensor hm N := by
 884      intro N; exact eulerLedgerScalarState_eq_collapse sensor hm N
 885    have hK' : ∀ N,
 886        IndisputableMonolith.Foundation.LawOfExistence.defect
 887          (realizedDefectCollapseScalar sensor hm N) ≤ K := by
 888      intro N; rw [← this N]; exact hK N
 889    exact direct_t1_exclusion sensor hm ⟨K, hK'⟩