transmutation_cost_pos
plain-language theorem explainer
Nuclear configurations with stability ratio different from one carry strictly positive J-cost. Researchers modeling RS-derived transmutation pathways cite this to confirm that fission products sit above the zero-cost ground state. The argument obtains non-negativity from an upstream lemma, derives a contradiction to zero via the zero-cost characterization of stable nuclei, and concludes strict positivity with lt_of_le_of_ne.
Claim. For every nuclear configuration with stability ratio $x ≠ 1$, the associated J-cost satisfies $0 < J(x)$.
background
Module EN-006 derives conditions for nuclear waste transmutation from the J-cost barrier structure. NuclearConfig is a structure carrying a positive real ratio x, where x = 1 marks perfectly stable doubly-magic nuclei. nuclearCost maps each configuration to its J-cost J(x), the measure of deviation from stability. Upstream nuclear_cost_nonneg establishes that J-cost is always non-negative. Upstream nuclear_cost_zero_iff_stable establishes that J-cost equals zero if and only if the ratio equals one.
proof idea
The proof invokes nuclear_cost_nonneg to obtain J-cost ≥ 0. It applies nuclear_cost_zero_iff_stable to show that J-cost = 0 would force the ratio to equal one, contradicting the hypothesis. lt_of_le_of_ne then yields the strict inequality.
why it matters
This theorem supplies the positivity half of fission_transmutation_from_ledger and is invoked by strict_transmutation_progress to guarantee cost descent along transmutation paths. It occupies the third position in the EN-006 sequence and reinforces that only the ground state (doubly-magic nuclei) achieves zero defect cost, consistent with the J-cost attractor structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.