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

stable_is_optimal

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)

 137theorem stable_is_optimal (cfg : NuclearConfig) :
 138    nuclearCost stable_config ≤ nuclearCost cfg := by

proof body

Term-mode proof.

 139  rw [stable_config_zero_cost]
 140  exact nuclear_cost_nonneg cfg
 141
 142/-! ## §IV. Doubly-Magic Attractors -/
 143
 144/-- A doubly-magic attractor is a local cost minimum that is "nearby" in the φ-rung sense. -/

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.