stable_config_zero_cost
plain-language theorem explainer
The ratio-1 stable nuclear configuration has zero J-cost. Modelers of transmutation pathways cite this to fix the global minimum of the cost landscape. The proof is a one-line wrapper that unfolds the nuclear cost definition and applies the base lemma Jcost(1) = 0.
Claim. Let $J$ be the J-cost function on positive ratios. For the stable nuclear configuration with ratio 1, $J(1) = 0$.
background
J-cost is defined as $J(x) = (x-1)^2/(2x)$ and vanishes exactly at the fixed point $x=1$. In this module nuclearCost maps a NuclearConfig to Jcost of its ratio, while stable_config is the NuclearConfig carrying ratio 1. The module derives fission-transmutation conditions from the J-cost barrier structure, treating doubly-magic nuclei as local zero-cost attractors and transmutation paths as cost-decreasing sequences toward them. Upstream, Jcost_unit0 states Jcost 1 = 0 by direct simplification of the Jcost definition.
proof idea
One-line wrapper that unfolds nuclearCost and stable_config then applies the lemma Jcost_unit0.
why it matters
This anchors the zero-cost endpoint required by the fission transmutation theorem and the stable-end-state existence theorem. It fills EN-006.7 in the module's registry of results and corresponds to the T5 J-uniqueness fixed point of the Recognition Science forcing chain. Downstream theorems quote it to certify that every transmutation path reaches a global minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.