efficiency_bounded
plain-language theorem explainer
Under the hypothesis that a transmutation step does not increase J-cost, the derived efficiency ratio lies between zero and one. Nuclear engineers applying Recognition Science to fission product management would cite this bound when certifying transmutation pathways. The proof proceeds by unfolding the efficiency definition, case-splitting on whether the initial configuration is already stable, and applying non-negativity of nuclear costs together with basic inequalities on the reals.
Claim. Let $x$ and $y$ be nuclear configurations with J-costs $C(x)$ and $C(y)$. If $C(y) ≤ C(x)$, then the transmutation efficiency satisfies $0 ≤ η(x,y) ≤ 1$, where $η(x,y) = 1$ if $C(x) = 0$ and $η(x,y) = (C(x) - C(y))/C(x)$ otherwise.
background
In the EN-006 module, nuclear configurations are modeled as structures NuclearConfig carrying a positive real ratio that equals 1 precisely for stable doubly-magic nuclei. The associated J-cost is defined by nuclearCost cfg := Jcost cfg.ratio, which is shown non-negative by nuclear_cost_nonneg via Jcost_nonneg. The module derives transmutation pathways as sequences that reduce total J-cost, with efficiency defined as the relative cost reduction (or 1 for already-stable initial states). This sits inside the broader claim that Recognition Science yields optimal transmutation paths to J-cost minima at doubly-magic nuclei. Upstream, the non-negativity theorem nuclear_cost_nonneg states: THEOREM EN-006.1: Nuclear cost is non-negative.
proof idea
The term-mode proof unfolds the definition of transmutation_efficiency. It performs case analysis on whether nuclearCost initial equals zero. When true, the efficiency is defined as 1 and the bounds hold by norm_num. When false, it applies div_nonneg to the numerator and denominator using nuclear_cost_nonneg on both configurations, then invokes div_le_one (after confirming the denominator is positive) and linarith with the hypothesis nuclearCost final ≤ nuclearCost initial together with non-negativity.
why it matters
This result supplies the upper and lower bounds required for the EN-006 certificate, which lists it among the derived properties of fission product transmutation. It directly supports the module's claim that transmutation efficiency is in [0,1] under cost reduction, closing one of the enumerated theorems in the EN-006 derivation from J-cost barriers. No open questions are flagged in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.