stable_is_optimal
plain-language theorem explainer
The theorem asserts that the stable nuclear configuration (ratio 1) achieves minimal J-cost among all NuclearConfig instances. Engineers deriving transmutation sequences would cite it to confirm cost descent terminates at a global minimum. The proof is a term-mode one-liner that rewrites the stable cost to zero and applies non-negativity.
Claim. For every nuclear configuration $cfg$ with positive ratio $x$, the J-cost of the stable configuration satisfies $J(1) ≤ J(x)$.
background
In the EN-006 module, a NuclearConfig is a structure carrying a positive real ratio $x$, where $x=1$ marks doubly-magic nuclei. The function nuclearCost cfg is defined as Jcost cfg.ratio and serves as the instability measure. The module derives transmutation pathways as sequences that reduce total J-cost toward local minima at shell closures. Upstream, nuclear_cost_nonneg states that nuclearCost is nonnegative for any cfg, while stable_config is the constant configuration with ratio 1.
proof idea
Term-mode proof applies the rewrite rule stable_config_zero_cost to replace the left-hand side with zero, then invokes the exact tactic on nuclear_cost_nonneg cfg.
why it matters
The result is EN-006.8 and feeds directly into the en006_certificate that lists all derived statements for fission-product transmutation. It closes the optimality half of the cost-monotone-descent claim in the module, consistent with the Recognition Science view that doubly-magic nuclei are J(x)=0 attractors. The declaration touches the J-uniqueness step (T5) and the cost barrier structure used for optimal pathways.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.