strict_transmutation_progress
plain-language theorem explainer
For any nuclear configuration with ratio not equal to 1, a transmutation step exists that reaches the stable configuration while strictly lowering J-cost. Nuclear engineers working on waste reduction pathways would cite the result to establish guaranteed descent. The term-mode proof constructs the step explicitly from the positivity of non-stable cost and the zero cost of the stable state, then verifies the inequality by linear arithmetic.
Claim. For any nuclear configuration whose stability ratio $x$ satisfies $x ≠ 1$, there exists a transmutation step whose initial state is that configuration and whose final state is the stable configuration (ratio 1) such that the J-cost of the final state is strictly less than the J-cost of the initial state.
background
NuclearConfig is a structure holding a positive real ratio $x$, with $x=1$ marking doubly-magic stable nuclei. nuclearCost maps each configuration to its J-cost via the function Jcost applied to the ratio. TransmutationStep records an ordered pair of configurations together with a proof that the final J-cost is at most the initial J-cost. stable_config is the canonical ratio-1 object whose J-cost is identically zero. The module derives fission-product transmutation from the J-cost barrier structure, treating sequences of recognition events as cost-reducing paths toward local minima at shell closures.
proof idea
The term proof first obtains the positivity of nuclearCost for the given unstable configuration via transmutation_cost_pos. It then recalls that nuclearCost of stable_config equals zero via stable_config_zero_cost. The step is built by pairing the input configuration with stable_config and supplying the two inequalities (final cost zero is less than or equal to initial cost, and strictly less) which linarith discharges from the two facts.
why it matters
This is theorem EN-006.12 inside the fission-product transmutation development. It supplies the strict-progress guarantee required by the EN-006 certificate, which records the full set of derived statements for the module. The result closes the existence half of the cost-monotone-descent claim listed in the module header and sits downstream of the zero-cost property of doubly-magic nuclei.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.