nothing_unbounded_defect

formal source

 101
 102/-- For any threshold, sufficiently small positive values have defect exceeding it.
 103    This means "approaching nothing" has unbounded cost. -/
 104theorem nothing_unbounded_defect :
 105    ∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x :=
 106  nothing_cannot_exist
 107
 108/-- No value near zero is RSExistent.
 109    This is the operational content of "Nothing cannot recognize itself". -/
 110theorem nothing_not_rs_exists :
 111    ∃ ε > 0, ∀ x, 0 < x → x < ε → ¬RSExists x := by
 112  obtain ⟨ε, hε_pos, hε⟩ := nothing_unbounded_defect 1
 113  use ε, hε_pos
 114  intro x hx_pos hx_small ⟨_, hdef⟩
 115  have hC : 1 < defect x := hε x hx_pos hx_small
 116  rw [hdef] at hC
 117  linarith
 118
 119/-! ## RSTrue: Truth as Stabilized Recognition -/
 120
 121/-- A configuration-to-cost bridge: maps a configuration to the scalar
 122    cost-input via observable and scale maps relative to a reference. -/
 123structure CostBridge (C : Type*) where
 124  χ : C → ℝ
 125  χ_pos : ∀ c, 0 < χ c
 126
 127/-- A predicate stabilizes along the orbit of `B` from seed `c₀` to the
 128    value it takes at `c_star`, meaning the orbit eventually agrees with
 129    `c_star` on `P`. -/
 130def Stabilizes {C : Type*} (B : C → C) (P : C → Bool) (c₀ c_star : C) : Prop :=
 131  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → P (B^[n] c₀) = P c_star
 132
 133/-- Configuration-level existence: `c` exists iff its cost-bridge
 134    image has zero defect, i.e. `χ(c) = 1`. -/