`actualize_valid`

proved

show as: view math explainer →

module: IndisputableMonolith.Modal.Possibility
domain: Modal
line: 296 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Modal.Possibility on GitHub at line 296.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 293  identity_config (c.time + 8)
 294
 295/-- Actualization always produces a valid configuration. -/
 296lemma actualize_valid (c : Config) : (Actualize c).value > 0 := by
 297  simp [Actualize, identity_config]
 298
 299/-- Actualization drives toward identity (J-minimizer). -/
 300theorem actualize_decreases_cost (c : Config) (hne : c.value ≠ 1) :
 301    J (Actualize c).value < J c.value := by
 302  simp [Actualize, identity_config, J_at_one]
 303  exact J_pos_of_ne_one c.pos hne
 304
 305/-! ## Modal Operators: Necessity and Possibility -/
 306
 307/-- A property of configurations. -/
 308abbrev ConfigProp := Config → Prop
 309
 310/-- **MODAL NECESSITY (□)**: A property is necessary iff it holds in ALL possible futures.
 311
 312    □p at c ⟺ ∀ y ∈ P(c), p(y)
 313
 314    In RS, necessity means "forced by cost minimization." -/
 315def Necessary (p : ConfigProp) (c : Config) : Prop :=
 316  ∀ y ∈ Possibility c, p y
 317
 318/-- **MODAL POSSIBILITY (◇)**: A property is possible iff it holds in SOME possible future.
 319
 320    ◇p at c ⟺ ∃ y ∈ P(c), p(y)
 321
 322    In RS, possibility means "reachable at finite cost." -/
 323def Possible (p : ConfigProp) (c : Config) : Prop :=
 324  ∃ y ∈ Possibility c, p y
 325
 326/-- Modal notation -/

papers checked against this theorem

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