pith. machine review for the scientific record. sign in
theorem proved term proof

modal_completeness

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 237theorem modal_completeness (c : Config) :
 238    ∃ path : List Config, path.head? = some c ∧
 239    path.getLast? = some (identity_config (c.time + 8)) := by

proof body

Term-mode proof.

 240  use [c, identity_config (c.time + 8)]
 241  simp only [List.head?_cons, List.getLast?_cons_cons, List.getLast?_singleton, and_self]
 242
 243/-! ## Boundaries of Possibility -/
 244
 245/-- **IMPOSSIBLE REGION**: Where J → ∞.
 246
 247    As x → 0⁺, J(x) → ∞, making these configurations unreachable at finite cost.
 248    This is the "boundary of possibility." -/

depends on (17)

Lean names referenced from this declaration's body.