cost_reduction_bounded
plain-language theorem explainer
The theorem shows that for any valid transmutation step the drop in J-cost is at most the starting cost, which follows immediately once the final cost is known to be nonnegative. Nuclear engineers working on J-cost descent models for fission-product pathways would cite the bound when estimating maximum possible savings per step. The proof is a one-line linear-arithmetic wrapper that invokes non-negativity of the terminal configuration.
Claim. Let $x$ and $y$ be nuclear configurations connected by a valid transmutation step, so that the J-cost satisfies $J(y) ≤ J(x)$. Then $J(x) - J(y) ≤ J(x)$.
background
In the FissionTransmutationStructure module, nuclearCost(cfg) is defined as Jcost(cfg.ratio) and measures the instability of a nuclear ratio relative to the stability valley. A TransmutationStep is a pair of configurations together with the hypothesis that nuclearCost(final) ≤ nuclearCost(initial), enforcing that each step moves toward lower J-cost. The module derives transmutation pathways from the Recognition Science claim that fission products sit at high J-cost and that sequences of recognition events descend the J-cost geodesic to the nearest doubly-magic nucleus (J = 0). Upstream, nuclear_cost_nonneg supplies the fact that every configuration satisfies 0 ≤ nuclearCost(cfg), obtained from Jcost_nonneg on the positive ratio.
proof idea
One-line wrapper that applies linear arithmetic to the non-negativity of the final configuration's nuclear cost (nuclear_cost_nonneg step.final).
why it matters
The result is labeled EN-006.5 and supplies an elementary upper bound on per-step savings inside the transmutation pathway analysis of the module. It sits between the positivity theorem nuclear_cost_nonneg and the later statements on monotone descent and existence of stable endpoints listed in the module documentation. Within the Recognition Science framework it instantiates the general J-cost reduction property (T5 J-uniqueness and the Recognition Composition Law) for the concrete engineering setting of nuclear ratios, confirming that cost descent cannot overshoot the initial defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.