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

collapse_automatic

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)

 236theorem collapse_automatic (c : Config) (_ : J c.value ≥ collapse_threshold) :
 237    has_definite_pointer (Actualize c) ∨ J (Actualize c).value < collapse_threshold := by

proof body

Term-mode proof.

 238  right
 239  simp only [Actualize, identity_config, J_at_one, collapse_threshold]
 240  norm_num
 241
 242/-! ## The Actualization Operator -/
 243
 244/-- **THE ACTUALIZATION OPERATOR A**: Maps current to actualized configuration.
 245
 246    A : Config → Config
 247    A(c) = argmin_{y ∈ P(c)} J(y)
 248
 249    This is dual to the Possibility operator P:
 250    - P gives what COULD happen
 251    - A gives what DOES happen
 252
 253    Together, P and A completely characterize RS modal dynamics. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.