path_reduces_total_cost

formal source

 121  net_reduction : nuclearCost finish ≤ nuclearCost start
 122
 123/-- **THEOREM EN-006.6**: Any transmutation path reduces total cost. -/
 124theorem path_reduces_total_cost (path : TransmutationPath) :
 125    nuclearCost path.finish ≤ nuclearCost path.start :=
 126  path.net_reduction
 127
 128/-- A stable configuration: J-cost = 0 (doubly-magic nucleus). -/
 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