nuclear_cost_nonneg
plain-language theorem explainer
Nuclear cost equals the J-cost of a nuclear configuration's stability ratio and is therefore non-negative for every positive ratio. Transmutation modelers cite this bound to anchor efficiency and reduction estimates in fission pathways. The proof is a direct one-line application of the upstream Jcost non-negativity lemma to the configuration's positivity witness.
Claim. Let $x > 0$ be the stability ratio of a nuclear configuration. Then the associated J-cost satisfies $J(x) = (x-1)^2/(2x) > 0$ whenever $x ≠ 1$, and $J(x) = 0$ when $x = 1$.
background
NuclearConfig is the structure carrying a real stability ratio $x$ together with the witness $0 < x$; the value $x = 1$ identifies doubly-magic ground states while $x ≠ 1$ marks fission products. nuclearCost is the definition that applies the J-cost function directly to this ratio. The local setting is the EN-006 derivation of transmutation pathways from the J-cost barrier, where each configuration is assigned a defect distance from the stability valley.
proof idea
The proof is a one-line wrapper that applies the Jcost_nonneg lemma to the ratio_pos field of the supplied configuration.
why it matters
EN-006.1 supplies the lower bound required by every subsequent result in the module: cost_reduction_bounded, efficiency_bounded, stable_end_state_exists, stable_is_optimal and transmutation_cost_pos all invoke it to guarantee that costs lie in [0, ∞) and that stable configurations achieve the global minimum. Within Recognition Science it instantiates the general non-negativity of recognition costs (T5 J-uniqueness) for nuclear ledger ratios, confirming that every transmutation path is a descent toward a zero-cost attractor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.