nuclearCost
plain-language theorem explainer
nuclearCost assigns to each nuclear configuration the J-cost of its stability ratio. Modelers of transmutation pathways cite this definition when establishing cost bounds for sequences of fission steps. The definition is realized as a direct wrapper around the Jcost function on the ratio field.
Claim. For a nuclear configuration with stability ratio $x > 0$, the nuclear cost is $J(x)$, where $J$ is the J-cost function.
background
NuclearConfig is a structure with a positive real ratio field, where the value 1 corresponds to perfectly stable doubly-magic nuclei and other values to unstable configurations. The J-cost serves as the instability measure for any such configuration. The module derives transmutation conditions from the J-cost barrier structure, treating paths as sequences of recognition events that reduce total cost toward local minima at doubly-magic nuclei.
proof idea
One-line wrapper that applies Jcost to the ratio field of the input configuration.
why it matters
This definition supplies the cost measure used throughout the EN-006 theorems, including fission_transmutation_from_ledger which asserts positive cost for non-stable states, existence of zero-cost stable states, and paths reaching them. It supports downstream results such as cost_monotone_descent_terminates and cost_reduction_bounded. The construction connects directly to the J-cost structure in the Recognition framework, where doubly-magic nuclei act as zero-cost attractors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.