`Possibility`

definition

show as: view math explainer →

module: IndisputableMonolith.Modal.Possibility
domain: Modal
line: 230 · 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 230.

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

 227    3. The change would be cost-advantageous or neutral
 228
 229    P : Config → Set Config -/
 230def Possibility (c : Config) : Set Config :=
 231  {y : Config |
 232    -- Within one octave step
 233    y.time = c.time + 8 ∧
 234    -- Cost-respecting (change doesn't increase total cost)
 235    J c.value + J_transition c.value y.value c.pos y.pos + J y.value ≤
 236      J c.value + J_stasis c.value
 237  }
 238
 239/-- The identity is always possible from any configuration.
 240
 241    The boundedness constraint is now part of the Config structure,
 242    ensuring all physical configurations can reach identity in one step. -/
 243lemma identity_always_possible (c : Config) :
 244    identity_config (c.time + 8) ∈ Possibility c := by
 245  simp only [Possibility, Set.mem_setOf_eq, identity_config]
 246  constructor
 247  · -- Time advances by 8
 248    trivial
 249  · -- Cost respecting: we need to show
 250    -- J c.value + J_transition c.value 1 c.pos one_pos + J 1 ≤ J c.value + J_stasis c.value
 251    have hJ1 : J 1 = 0 := J_at_one
 252    have hStasis : J_stasis c.value = 8 * J c.value := rfl
 253    have hJ_nonneg : 0 ≤ J c.value := J_nonneg c.pos
 254    simp only [hJ1, add_zero, hStasis]
 255    -- Goal: J c.value + J_transition c.value 1 c.pos one_pos ≤ J c.value + 8 * J c.value
 256    -- Sufficient: J_transition c.value 1 c.pos one_pos ≤ 8 * J c.value
 257    have h_trans_bound : J_transition c.value 1 c.pos one_pos ≤ 8 * J c.value := by
 258      unfold J_transition
 259      simp only [one_div, hJ1, add_zero]
 260      -- Goal: |log c.value⁻¹| * (J c.value / 2) ≤ 8 * J c.value

papers checked against this theorem

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