 203    For x ≠ 1: There exists y closer to 1 with J_change(x,y) < J_stasis(x).
 204
 205    This proves: **Existence (x = 1) is the unique stable state.** -/
 206theorem identity_prefers_stasis : prefers_stasis 1 one_pos := by
 207  intro y hy _
 208  -- J_stasis(1) = 0, and J_change(1,y) ≥ 0 for all y > 0
 209  have hJ1 : J_stasis 1 = 0 := J_stasis_at_one
 210  rw [hJ1]
 211  unfold J_change
 212  apply add_nonneg
 213  · unfold J_transition
 214    apply mul_nonneg (abs_nonneg _)
 215    apply div_nonneg
 216    · apply add_nonneg J_at_one.ge (J_nonneg hy)
 217    · norm_num
 218  · exact J_stasis_nonneg hy
 219
 220/-! ## Possibility: What Could Follow -/
 221
 222/-- **POSSIBILITY OPERATOR**: P(c) is the set of configurations reachable from c.
 223
 224    A configuration y is possible from x iff:
 225    1. y has positive value (exists in RS)
 226    2. The transition cost is finite
 227    3. The change would be cost-advantageous or neutral
 228
 229    P : Config → Set Config -/
 230def Possibility (c : Config) : Set Config :=
 231  {y : Config |
 232    -- Within one octave step
 233    y.time = c.time + 8 ∧
 234    -- Cost-respecting (change doesn't increase total cost)
 235    J c.value + J_transition c.value y.value c.pos y.pos + J y.value ≤
 236      J c.value + J_stasis c.value

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.