stable_config_zero_cost

formal source

 129def stable_config : NuclearConfig := ⟨1, one_pos⟩
 130
 131/-- **THEOREM EN-006.7**: The stable configuration has zero cost. -/
 132theorem stable_config_zero_cost : nuclearCost stable_config = 0 := by
 133  unfold nuclearCost stable_config
 134  exact Jcost_unit0
 135
 136/-- **THEOREM EN-006.8**: Stable configuration is optimal (minimal cost). -/
 137theorem stable_is_optimal (cfg : NuclearConfig) :
 138    nuclearCost stable_config ≤ nuclearCost cfg := by
 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. -/
 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⟩