`A`

definition

show as: view math explainer →

module: IndisputableMonolith.Modal.Actualization
domain: Modal
line: 254 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Modal.Actualization on GitHub at line 254.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 251    - A gives what DOES happen
 252
 253    Together, P and A completely characterize RS modal dynamics. -/
 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)

papers checked against this theorem

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