CostMonotonic

formal source

 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
 295    conclude p (A c) from p y when J y > J (A c).
 296
 297    This is the correct characterization: adjointness is conditional on
 298    the property type. -/
 299theorem H_adjoint_non_minimal (p : ConfigProp) (c : Config)
 300    (_h_unique : ∀ y ∈ Possibility c, J y.value = J (Actualize c).value → y = Actualize c)
 301    (y : Config) (_hy : y ∈ Possibility c) (hp : p y) (_h_cost_pos : J y.value ≠ 0)
 302    (hcm : CostMonotonic p) (hA_pos : (A c).value > 0) :
 303    p (A c) := by
 304  -- y has positive cost, A c has zero cost (identity), so J y > J (A c)
 305  have hJ_y_pos : J y.value > 0 := by
 306    cases' (lt_or_eq_of_le (J_nonneg y.pos)) with h h
 307    · exact h
 308    · exact absurd h.symm _h_cost_pos
 309  have hJ_A : J (A c).value = 0 := by simp only [A, Actualize, identity_config, J_at_one]
 310  have h_gt : J y.value > J (A c).value := by rw [hJ_A]; exact hJ_y_pos