TransmutationPath
plain-language theorem explainer
TransmutationPath is a structure that records an initial fission product configuration, its stable end state, the number of steps taken, and a net reduction in J-cost. Researchers deriving nuclear waste transmutation pathways from the Recognition Science cost function would cite this definition. It is introduced as a direct packaging of four fields with the cost inequality included as a field.
Claim. A transmutation path is given by an initial nuclear configuration $c_i$, a final nuclear configuration $c_f$, a natural number $n$ of steps, and the inequality $J(c_f) ≤ J(c_i)$, where $J$ is the J-cost of the nuclear ratio.
background
NuclearConfig is a structure holding a positive real ratio $x$, where $x=1$ denotes a stable doubly-magic nucleus and $x≠1$ an unstable fission product. The function nuclearCost(cfg) returns the J-cost of cfg.ratio, which quantifies instability as the deviation from the ideal ratio of 1. In the local setting of EN-006, transmutation is modeled as a sequence of recognition events that reduce total J-cost, with doubly-magic nuclei acting as zero-cost attractors. Upstream results include the definition of J-cost from the multiplicative recognizer and the non-negativity of nuclear costs. TransmutationPath formalizes a pathway from high-cost fission products to a stable endpoint.
proof idea
The declaration is a plain structure definition. The four fields are start and finish of type NuclearConfig, n_steps of type ℕ, and net_reduction carrying the inequality nuclearCost finish ≤ nuclearCost start.
why it matters
This structure supplies the data type underlying the EN-006 theorems on fission transmutation. It is invoked in the proofs of path_reduces_total_cost, which extracts the net reduction, and stable_end_state_exists, which constructs a path to a zero-cost configuration. The definition thereby supports the claim that Recognition Science predicts optimal transmutation paths as monotonic descents in J-cost toward doubly-magic nuclei.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.