transmutation_efficiency
Transmutation efficiency measures the fractional J-cost reduction when a nuclear configuration moves from initial to final state. Nuclear engineers analyzing waste transmutation pathways under Recognition Science would cite this quantity to bound performance or confirm unit efficiency at stable endpoints. The definition is a direct conditional that returns 1 on zero initial cost and otherwise the normalized difference of nuclearCost values.
claimFor nuclear configurations with stability ratios, let $J$ denote the J-cost function. The efficiency is $1$ if $J(initial)=0$, and otherwise $(J(initial)-J(final))/J(initial)$.
background
NuclearConfig is a structure holding a positive real stability ratio $x$, with $x=1$ marking perfectly stable doubly-magic nuclei. The companion definition nuclearCost maps each configuration to its J-cost via Jcost of the ratio, serving as the instability measure in the EN-006 module. The module derives fission-product transmutation from the J-cost barrier structure, treating high-J fission products as far from stability and transmutation paths as cost-reducing sequences that terminate at local J-cost minima.
proof idea
Direct definition. It branches on whether nuclearCost initial equals zero and returns 1 in that case; otherwise it returns the ratio of the cost difference to the initial cost.
why it matters in Recognition Science
The definition supplies the efficiency metric invoked by efficiency_bounded (EN-006.13) and perfect_transmutation_efficiency (EN-006.14). It operationalizes the module claim that transmutation efficiency is the ratio of cost reduction to initial cost, linking directly to the Recognition Science picture of J-cost descent toward doubly-magic attractors.
scope and limits
- Does not specify any concrete sequence of nuclear reactions or neutron captures.
- Does not incorporate measured cross sections or energy barriers.
- Does not address multi-step paths or branching probabilities.
- Does not compute numerical efficiencies for named isotopes.
Lean usage
theorem efficiency_nonneg (initial final : NuclearConfig) (h : nuclearCost final ≤ nuclearCost initial) : 0 ≤ transmutation_efficiency initial final := (efficiency_bounded initial final h).1formal statement (Lean)
195def transmutation_efficiency (initial final : NuclearConfig) : ℝ :=
proof body
Definition body.
196 if nuclearCost initial = 0 then 1
197 else (nuclearCost initial - nuclearCost final) / nuclearCost initial
198
199/-- **THEOREM EN-006.13**: Transmutation efficiency is in [0, 1]. -/