A_advances_time

formal source

 261    J (A c).value < J c.value := actualize_decreases_cost c hne
 262
 263/-- A preserves time advancement. -/
 264theorem A_advances_time (c : Config) : (A c).time = c.time + 8 := by
 265  simp [A, Actualize, identity_config]
 266
 267/-! ## The Adjointness of P and A -/
 268
 269/-- **HYPOTHESIS**: For cost-monotonic properties, the actualized element inherits properties.
 270
 271    A property p is **cost-monotonic** if:
 272      p y ∧ J y.value > J y'.value → p y'
 273    i.e., the property propagates down the cost gradient.
 274
 275    Under this assumption, if p holds at any y ∈ Possibility c, then p holds at A c
 276    (the cost-minimizing element).
 277
 278    **STATUS**: HYPOTHESIS - This captures a specific class of properties for which
 279    adjointness holds. Not all properties are cost-monotonic. -/
 280def CostMonotonic (p : ConfigProp) : Prop :=
 281  ∀ y y' : Config, p y → J y.value > J y'.value → y'.value > 0 → p y'
 282
 283/-- For cost-monotonic properties, adjointness holds from any higher-cost element. -/
 284theorem adjoint_from_cost_monotonic (p : ConfigProp) (c : Config)
 285    (hcm : CostMonotonic p)
 286    (y : Config) (hy : y ∈ Possibility c) (hp : p y)
 287    (hA_pos : (A c).value > 0) :
 288    J y.value > J (A c).value → p (A c) := by
 289  intro h_cost_gt
 290  exact hcm y (A c) hp h_cost_gt hA_pos
 291
 292/-- **HYPOTHESIS**: Non-cost-monotonic properties may not transfer.
 293
 294    For properties that don't propagate down the cost gradient, we cannot