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

stable_is_attractor

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)

 152theorem stable_is_attractor : ∃ a : DoublyMagicAttractor, a.config = stable_config :=

proof body

Term-mode proof.

 153  ⟨⟨stable_config, by rw [stable_config_zero_cost]; norm_num⟩, rfl⟩
 154
 155/-- **THEOREM EN-006.10**: For any fission product, there exists a transmutation path
 156    to a stable end state (the global minimum). -/

depends on (3)

Lean names referenced from this declaration's body.