efficiency_bounded
plain-language theorem explainer
The theorem shows that transmutation efficiency, the relative J-cost reduction between two nuclear configurations, lies in the closed interval [0,1] whenever the final configuration has J-cost no larger than the initial one. Nuclear engineers modeling waste reduction pathways would cite the bound to certify that any cost-decreasing step yields a valid efficiency fraction. The proof is a direct term-mode case split on the zero-cost guard in the efficiency definition, followed by non-negativity and division lemmas.
Claim. Let $C$ be the J-cost of a nuclear configuration (with $C(x) = J(x)$ for stability ratio $x$). For configurations $i$ and $f$ satisfying $C(f) ≤ C(i)$, the efficiency defined by $η(i,f) = 1$ if $C(i)=0$ and $η(i,f) = (C(i)-C(f))/C(i)$ otherwise obeys $0 ≤ η(i,f) ≤ 1$.
background
NuclearConfig is the structure of a nuclear state carrying a positive real stability ratio $x$, with $x=1$ the doubly-magic ground state. nuclearCost extracts the J-cost via nuclearCost(cfg) := Jcost(cfg.ratio). transmutation_efficiency(initial,final) returns 1 when the initial cost vanishes and otherwise the normalized reduction (initial cost minus final cost) divided by initial cost. The module EN-006 derives fission-product transmutation from the J-cost barrier structure, where each step is a recognition event that lowers total defect from the stability valley. Upstream nuclear_cost_nonneg states that J-cost is nonnegative for every configuration.
proof idea
The term proof first unfolds the definition of transmutation_efficiency. It then splits on the if-guard that tests whether nuclearCost initial equals zero. In the zero case the two inequalities are immediate by norm_num. In the positive case the lower bound follows from div_nonneg applied to the two nonnegativity facts, while the upper bound follows from rewriting the division inequality and applying linarith to the hypothesis nuclearCost final ≤ nuclearCost initial.
why it matters
This result is EN-006.13 and supplies the final numerical bound required by the EN-006 certificate, which lists it among the derived statements confirming that J-cost descent produces feasible efficiencies. It closes the local theory of cost-monotone transmutation paths inside the Recognition framework, where J-cost reduction is the sole driver of optimal neutron-capture sequences toward doubly-magic attractors. No open scaffolding remains for this bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.