perfect_transmutation_efficiency
plain-language theorem explainer
Recognition Science assigns J-cost to nuclear configurations via their stability ratio, with the stable state at zero cost. The theorem asserts that transmutation from any unstable configuration to the stable state achieves exactly unit efficiency in this metric. Nuclear engineers applying the Recognition framework to fission waste would cite the result when certifying optimal pathways. The tactic proof unfolds the efficiency definition, invokes the cost-zero equivalence to obtain a nonzero premise, and simplifies using the stable state's zero,
Claim. Let $cfg$ be a nuclear configuration whose stability ratio $x$ satisfies $x ≠ 1$. The transmutation efficiency of $cfg$ to the stable configuration (ratio exactly 1) equals 1.
background
NuclearConfig is the structure carrying a positive real ratio $x$, with $x=1$ marking doubly-magic (stable) nuclei and $x≠1$ marking unstable ones. The associated J-cost is defined by nuclearCost(cfg) := Jcost(cfg.ratio). The constant stable_config is the NuclearConfig with ratio 1; its cost vanishes by stable_config_zero_cost, which rests on Jcost_unit0. The module derives transmutation properties from the Recognition Composition Law and the J-cost barrier structure, treating fission products as high-cost states whose descent to the nearest zero-cost attractor models optimal waste transmutation.
proof idea
The tactic proof first unfolds transmutation_efficiency. It then constructs the auxiliary fact that nuclearCost cfg ≠ 0 by applying the equivalence nuclear_cost_zero_iff_stable to the instability hypothesis h_unstable. Finally it invokes simp with the two facts h0 and stable_config_zero_cost to obtain the unit-efficiency conclusion.
why it matters
The result supplies EN-006.14, the final efficiency statement in the fission-transmutation suite, and is referenced by the en006_certificate that records the complete derivation. It closes the chain that begins with nuclear_cost_zero_iff_stable and stable_config_zero_cost, confirming that the J-cost geodesic to the stable state is 100 % efficient. Within the broader framework this supplies the engineering counterpart to the T5 J-uniqueness and T6 phi fixed-point steps, showing that cost descent reaches the zero-cost attractor with no loss.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.