strict_transmutation_progress
plain-language theorem explainer
Any nuclear configuration whose ratio differs from 1 admits a transmutation step to the stable configuration that strictly lowers J-cost. Nuclear engineers modeling waste reduction would cite the result to guarantee descent to a zero-cost endpoint. The proof constructs the required step record directly from the positivity of cost on unstable nuclei and the zero cost of the stable configuration, then discharges the inequality by linear arithmetic.
Claim. For any nuclear configuration $cfg$ with ratio $x ≠ 1$, there exists a transmutation step from $cfg$ to the stable configuration such that the J-cost of the final configuration is strictly less than the J-cost of $cfg$.
background
A NuclearConfig is a structure carrying a positive real ratio $x$, with $x=1$ marking a stable doubly-magic nucleus. nuclearCost(cfg) is defined as Jcost of that ratio and serves as the instability measure. A TransmutationStep packages an initial and final NuclearConfig together with a proof that cost does not increase. The module derives optimal transmutation paths from the J-cost barrier structure of Recognition Science. Upstream lemmas establish that unstable configurations carry positive cost (transmutation_cost_pos) and that the stable configuration carries zero cost (stable_config_zero_cost).
proof idea
The term proof first obtains a positive lower bound on nuclearCost(cfg) via transmutation_cost_pos and the zero value for the target via stable_config_zero_cost. It then builds the TransmutationStep record with initial cfg and final stable_config, using linarith on the two inequalities to confirm the strict descent.
why it matters
EN-006.12 supplies the strict descent step required by the EN-006 certificate on fission-product transmutation. It instantiates the cost-monotone descent property for nuclear configurations and closes the argument that every unstable nucleus reaches a doubly-magic attractor. The result sits inside the Recognition Science derivation of transmutation efficiency from the J-cost geodesic to stability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.