stable_end_state_exists
plain-language theorem explainer
For any nuclear configuration there exists a transmutation path ending at a zero J-cost stable state. Nuclear engineers modeling fission-product management would cite the existence result. The term-mode proof directly assembles a one-step path to the predefined stable configuration by invoking its zero-cost property together with non-negativity of nuclear cost.
Claim. For every nuclear configuration $cfg$ there exists a transmutation path $path$ such that $path.start = cfg$ and the J-cost of $path.finish$ equals zero.
background
NuclearConfig is a structure carrying a positive real ratio $x$, with $x=1$ marking doubly-magic nuclei. The associated J-cost is given by nuclearCost(cfg) := Jcost(cfg.ratio); nuclear_cost_nonneg states that this quantity is always nonnegative, while stable_config_zero_cost states that it vanishes exactly when the ratio equals 1. TransmutationPath records a start configuration, a finish configuration, a step count, and a net-reduction inequality between their J-costs. The module derives optimal transmutation routes from the J-cost barrier structure, treating fission products as high-cost points and doubly-magic nuclei as zero-cost attractors.
proof idea
The proof is a direct term construction. It supplies a TransmutationPath whose start field is the input cfg, whose finish field is stable_config, whose step count is 1, and whose net-reduction field is obtained by rewriting stable_config_zero_cost and applying nuclear_cost_nonneg. The second line then matches the two required equalities by reflexivity and the zero-cost property.
why it matters
EN-006.10 supplies the existence half of the fission-transmutation statement. It is invoked inside fission_transmutation_from_ledger and appears in the EN-006 certificate. The result closes the cost-descent argument for nuclear engineering, showing that every configuration reaches the global J-cost minimum at the stability valley.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.