nuclear_cost_nonneg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not claim that nuclearCost vanishes for any specific nucleus.
- Does not supply the explicit algebraic form of Jcost.
- Does not address the existence or length of transmutation paths.
- Does not constrain the rate of cost reduction along a path.
formal statement (Lean)
59theorem nuclear_cost_nonneg (cfg : NuclearConfig) : 0 ≤ nuclearCost cfg :=
proof body
Term-mode proof.
60 Jcost_nonneg cfg.ratio_pos
61
62/-- **THEOREM EN-006.2**: Nuclear cost is zero iff the nucleus is in the ground state
63 (doubly-magic, x = 1). -/