perfect_transmutation_efficiency
plain-language theorem explainer
Perfect transmutation from an unstable nuclear configuration (ledger ratio not equal to 1) to the stable state reaches unit efficiency. Recognition Science modelers of nuclear waste reduction cite this result. The proof unfolds the efficiency definition, derives nonzero cost from the instability hypothesis via the zero-cost equivalence, and simplifies directly using the stable configuration's zero cost.
Claim. Let $cfg$ be a nuclear configuration with stability ratio $x ≠ 1$. The efficiency of transmuting $cfg$ to the stable configuration (ratio 1) equals 1.
background
In the FissionTransmutationStructure module a NuclearConfig consists of a positive real ratio $x$, with $x=1$ marking a perfectly stable doubly-magic nucleus and $x≠1$ marking an unstable nucleus. Its J-cost is nuclearCost $cfg$ := Jcost($cfg$.ratio), the instability measure drawn from the Recognition Composition Law. The stable_config is the canonical NuclearConfig with ratio 1. The upstream theorem nuclear_cost_zero_iff_stable states that nuclearCost $cfg$ = 0 if and only if $cfg$.ratio = 1. The companion result stable_config_zero_cost asserts nuclearCost stable_config = 0.
proof idea
The tactic proof first unfolds transmutation_efficiency. It then applies nuclear_cost_zero_iff_stable to the hypothesis $cfg$.ratio ≠ 1, obtaining nuclearCost $cfg$ ≠ 0. The final simp step reduces the expression using this nonzero fact together with stable_config_zero_cost.
why it matters
This theorem supplies EN-006.14, the final efficiency statement in the fission transmutation derivation. It is referenced by the en006_certificate that aggregates all derived J-cost properties for the module. The result closes the chain that begins from the J-cost barrier structure and the equivalence of zero cost with stability, confirming that cost descent to the stable attractor yields perfect efficiency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.