A_well_defined

formal source

 254def A : Config → Config := Actualize
 255
 256/-- A is well-defined (always produces valid config). -/
 257lemma A_well_defined (c : Config) : (A c).value > 0 := actualize_valid c
 258
 259/-- A drives toward identity. -/
 260theorem A_toward_identity (c : Config) (hne : c.value ≠ 1) :
 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) :