CostBridge

formal source

 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`. -/
 135def RSExists_cfg {C : Type*} (bridge : CostBridge C) (c : C) : Prop :=
 136  RSExists (bridge.χ c)
 137
 138/-- **RSTrue**: A predicate `P` is RS-true at `c_star` under dynamics `B`
 139    from seed `c₀` if:
 140    1. `c_star` exists (its cost-bridge value has zero defect),
 141    2. `P` holds at `c_star`,
 142    3. `P` stabilizes along the orbit to the value at `c_star`.
 143
 144    This replaces the placeholder `def RSTrue (P : Prop) : Prop := P`. -/
 145def RSTrue {C : Type*}
 146    (bridge : CostBridge C) (B : C → C) (c₀ c_star : C) (P : C → Bool) : Prop :=
 147  RSExists_cfg bridge c_star ∧ P c_star = true ∧ Stabilizes B P c₀ c_star
 148
 149/-! ## RS-Decidability and Boolean Laws -/
 150
 151/-- A predicate is **RS-decidable** at `(c_star, B, c₀)` when the background
 152    conditions for Boolean reasoning hold: existence and stabilization. -/
 153def RSDecidable {C : Type*}