path_reduces_total_cost
plain-language theorem explainer
Any transmutation path from a fission product to a stable nucleus reduces total J-cost. Nuclear engineers modeling waste stabilization and RS theorists studying cost descent cite this monotonicity result. The proof is a one-line term that extracts the net_reduction inequality already stored in the path structure.
Claim. For any transmutation path $p$, the J-cost of the final configuration satisfies $J(p_0) ≤ J(p_1)$ where $p_0$ is the starting fission product and $p_1$ the stable end state.
background
The module derives nuclear transmutation from the J-cost barrier. nuclearCost(cfg) is defined as Jcost(cfg.ratio), the instability measure of a nuclear configuration. A TransmutationPath is a structure carrying a start configuration, a finish configuration, step count, and an explicit net_reduction field asserting nuclearCost(finish) ≤ nuclearCost(start). Upstream, cost is the J-cost of a recognition event and nuclearCost inherits non-negativity from the foundational cost function.
proof idea
The proof is a one-line term wrapper that returns the net_reduction field of the supplied TransmutationPath.
why it matters
This result (EN-006.6) closes the cost-reduction chain in the fission module and supports downstream claims that stable endpoints exist and optimal paths are cost-monotone. It illustrates how sequences of recognition events drive configurations toward J=0 minima at doubly-magic nuclei, consistent with the phi-ladder descent and the Recognition Composition Law. The theorem remains an application layer result rather than a foundational forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.