TransmutationStep
plain-language theorem explainer
TransmutationStep records a nuclear configuration change from initial to final ratio that satisfies nuclearCost final ≤ nuclearCost initial. Engineers modeling fission waste reduction cite the structure to enforce monotonic J-cost descent toward stable nuclei. The definition is a direct record type whose reduces_cost field supplies the inequality used by all downstream cost theorems.
Claim. A transmutation step consists of nuclear configurations $C_i$ and $C_f$ (each with positive stability ratio) such that the J-cost satisfies $J(C_f) ≤ J(C_i)$.
background
NuclearConfig is the structure holding a positive real ratio $x$, with $x=1$ marking stable doubly-magic nuclei. nuclearCost is the derived J-cost function Jcost applied to that ratio. The module EN-006 derives transmutation conditions from the J-cost barrier structure, where fission products sit at high cost and valid paths descend toward zero-cost attractors at shell closures.
proof idea
The structure is introduced directly by its three fields; the reduces_cost field simply records the required inequality. No tactic or lemma application occurs inside the definition itself.
why it matters
TransmutationStep supplies the atomic object for the EN-006 series, directly feeding transmutation_reduces_cost (EN-006.4), cost_reduction_bounded (EN-006.5), and strict_transmutation_progress (EN-006.12). It instantiates the Recognition Science cost-descent principle on nuclear ratios, consistent with the J-uniqueness and phi-ladder landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.