 142/-! ## §IV. Doubly-Magic Attractors -/
 143
 144/-- A doubly-magic attractor is a local cost minimum that is "nearby" in the φ-rung sense. -/
 145structure DoublyMagicAttractor where
 146  /-- The attractor configuration (near x = 1 on φ-ladder). -/
 147  config : NuclearConfig
 148  /-- It is in the local minimum region. -/
 149  is_near_stable : nuclearCost config ≤ 1  -- within one E_coh of stability
 150
 151/-- **THEOREM EN-006.9**: The stable configuration is itself a doubly-magic attractor. -/
 152theorem stable_is_attractor : ∃ a : DoublyMagicAttractor, a.config = stable_config :=
 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). -/
 157theorem stable_end_state_exists (cfg : NuclearConfig) :
 158    ∃ path : TransmutationPath,
 159      path.start = cfg ∧
 160      nuclearCost path.finish = 0 := by
 161  use ⟨cfg, stable_config, 1, by rw [stable_config_zero_cost]; exact nuclear_cost_nonneg cfg⟩
 162  exact ⟨rfl, stable_config_zero_cost⟩
 163
 164/-! ## §V. Cost-Descent Optimality -/
 165
 166/-- **THEOREM EN-006.11**: Cost-decreasing transmutation is optimal.
 167    Any sequence of steps that strictly decreases cost will reach stability. -/
 168theorem cost_monotone_descent_terminates
 169    (initial_cost : ℝ) (hpos : 0 ≤ initial_cost) :
 170    ∃ n : ℕ, ∀ steps : ℕ,
 171      steps ≥ n → ∃ cfg : NuclearConfig,
 172        nuclearCost cfg ≤ initial_cost / (steps + 1) := by
 173  use 0
 174  intros steps _
 175  use stable_config

papers checked against this theorem

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