nuclear_cost_zero_iff_stable
plain-language theorem explainer
For any nuclear configuration with positive stability ratio x, the associated J-cost vanishes if and only if x equals 1. Nuclear engineers modeling transmutation pathways cite the equivalence to certify that a fission product has reached a stable, zero-cost endpoint. The proof reduces the squared-ratio expression for J-cost to zero by division and positivity, then invokes the unit case for the converse direction.
Claim. Let $x > 0$ be the stability ratio of a nuclear configuration. Then the J-cost satisfies $J(x) = 0$ if and only if $x = 1$.
background
In the EN-006 module, a NuclearConfig is a structure carrying a positive real stability ratio x together with the proof that x > 0; x = 1 marks doubly-magic ground states while x ≠ 1 marks unstable fission products. The nuclearCost of such a configuration is defined to be the J-cost J(x) of its ratio. Upstream lemmas from the Cost module give the explicit squared form J(x) = (x-1)^2 / (2x) for x ≠ 0 and the unit evaluation J(1) = 0.
proof idea
The tactic proof unfolds nuclearCost to Jcost, then splits the biconditional. Forward: Jcost_eq_sq rewrites the cost as a quotient; positivity of the denominator forces the numerator (x-1)^2 to vanish, hence x = 1. Reverse: direct substitution of x = 1 followed by Jcost_unit0 yields zero cost.
why it matters
The result is invoked inside the EN-006 certificate, the perfect transmutation efficiency theorem, and the positive-cost theorem for unstable configurations. It supplies the EN-006.2 link in the fission transmutation chain, confirming that only ground-state nuclei achieve zero J-cost and thereby anchoring the cost-descent model to doubly-magic attractors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.