TransmutationStep
plain-language theorem explainer
TransmutationStep packages an initial NuclearConfig, a final NuclearConfig, and a certificate that nuclearCost of the final is at most that of the initial. Physicists modeling J-cost descent for nuclear waste transmutation cite this structure when building pathways to stable nuclei. The definition is a direct packaging of the two configurations together with the inequality nuclearCost final ≤ nuclearCost initial.
Claim. A transmutation step consists of an initial nuclear configuration with ledger ratio $x$, a final configuration with ratio $y$, and the inequality $J(y) ≤ J(x)$, where $J$ is the J-cost measuring defect from the stable point $x=1$.
background
NuclearConfig is a structure holding a positive real ratio, with ratio equal to 1 marking perfectly stable doubly-magic nuclei and other values marking unstable fission products. nuclearCost extracts the J-cost of a configuration by applying the Jcost function to its ratio, serving as the instability measure in the EN-006 module. This draws on the cost definitions from ObserverForcing and MultiplicativeRecognizerL4, both of which equate recognition cost to J-cost on positive ratios.
proof idea
The declaration is a structure definition with three fields that directly records the initial and final configurations and the reduces_cost inequality. No lemmas or tactics are invoked; it functions as a typed container for later use in cost-reduction statements.
why it matters
TransmutationStep supplies the data type for the parent results cost_reduction_bounded, strict_transmutation_progress, and transmutation_reduces_cost. It realizes the EN-006.4 claim that any valid transmutation step reduces or maintains J-cost, linking the fission-product module to the broader J-cost barrier structure and the stability valley at ratio 1. It leaves open the construction of explicit optimal paths to doubly-magic attractors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.