cost_reduction_bounded
Any valid transmutation step from an initial nuclear configuration to a final one satisfies nuclearCost(initial) minus nuclearCost(final) at most equal to nuclearCost(initial). Nuclear engineers optimizing waste transmutation sequences would cite the bound when verifying feasible descent toward stable nuclei. The proof is a one-line linear arithmetic reduction that invokes non-negativity of the final cost.
claimLet $J$ denote the nuclear J-cost function. For any transmutation step from initial configuration $x$ to final configuration $y$ satisfying $J(y) ≤ J(x)$, the inequality $J(x) - J(y) ≤ J(x)$ holds.
background
In the FissionTransmutationStructure module, nuclearCost maps a NuclearConfig (with ratio $x$) to its J-cost $J(x)$, the instability measure from the ideal stable state $x ≈ 1$. A TransmutationStep records an initial configuration, a final configuration, and the explicit condition that nuclearCost(final) ≤ nuclearCost(initial), encoding a valid cost-reducing recognition event toward stability.
proof idea
The term-mode proof applies the linarith tactic directly to the hypothesis nuclear_cost_nonneg step.final. This non-negativity rearranges algebraically to the target difference bound without further lemmas.
why it matters in Recognition Science
As THEOREM EN-006.5 it supplies the upper bound on cost reduction that complements transmutation_reduces_cost and nuclear_cost_nonneg within the same module. The result supports the module's derivation of J-cost geodesics to doubly-magic nuclei and aligns with the Recognition Composition Law and T5 J-uniqueness in the forcing chain. No downstream uses are recorded, leaving its role in optimal_path_exists open for later closure.
scope and limits
- Does not claim the reduction is strictly positive.
- Does not bound the length of any transmutation path.
- Does not incorporate reaction rates or cross sections.
- Does not address experimental realizability of steps.
formal statement (Lean)
106theorem cost_reduction_bounded (step : TransmutationStep) :
107 nuclearCost step.initial - nuclearCost step.final ≤ nuclearCost step.initial := by
proof body
Term-mode proof.
108 linarith [nuclear_cost_nonneg step.final]
109
110/-! ## §III. Transmutation Pathways -/
111
112/-- A transmutation pathway: sequence of steps from fission product to stable end. -/