206theorem identity_prefers_stasis : prefers_stasis 1 one_pos := by
proof body
Term-mode proof.
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 -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.