transmutation_reduces_cost
plain-language theorem explainer
Any valid transmutation step between nuclear configurations satisfies that the J-cost of the final state is at most the J-cost of the initial state. Researchers modeling nuclear waste transmutation pathways would invoke this result to establish monotonic cost descent along admissible sequences. The proof consists of a direct one-line reference to the reduction property embedded in the definition of a valid transmutation step.
Claim. For any transmutation step connecting an initial nuclear configuration to a final one, the nuclear cost satisfies $nuclearCost(final) ≤ nuclearCost(initial)$.
background
In the EN-006 module, each nuclear configuration carries a J-cost that quantifies its instability as the deviation of its ratio from the stability valley, with the definition nuclearCost(cfg) := Jcost(cfg.ratio). A TransmutationStep is the structure consisting of an initial and final NuclearConfig together with an explicit witness that the step reduces this cost. The construction rests on the cost functions imported from ObserverForcing and MultiplicativeRecognizerL4, both of which return the J-cost of a recognition event or comparator output.
proof idea
The proof is a one-line term that directly returns the reduces_cost field of the supplied TransmutationStep structure.
why it matters
The declaration supplies the monotonicity step required by the EN-006 certificate, which aggregates it with nuclear_cost_nonneg and nuclear_cost_zero_iff_stable to certify the full transmutation derivation. It realizes the Recognition Science claim that valid fission-product sequences descend in J-cost toward doubly-magic attractors, consistent with the J-uniqueness fixed point and the phi-ladder mass formula from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.