DoublyMagicAttractor
plain-language theorem explainer
A structure packaging a nuclear configuration whose J-cost satisfies an upper bound of 1, identifying it as a nearby local minimum on the stability ladder. Nuclear transmutation modelers in Recognition Science cite this when building descent arguments for waste reduction. The definition arises directly from combining the configuration type with the cost bound.
Claim. A doubly-magic attractor is a nuclear configuration $c$ (parameterized by stability ratio $x$) such that its J-cost satisfies $J(c) ≤ 1$.
background
NuclearConfig parameterizes each nucleus by its ledger ratio $x$, with $x=1$ for stable doubly-magic nuclei and $x≠1$ for unstable ones. The associated J-cost is defined as nuclearCost cfg = Jcost cfg.ratio, serving as the instability measure derived from the ledger factorization of positive reals under multiplication.
proof idea
Direct structure definition that packages NuclearConfig with the inequality nuclearCost config ≤ 1. No lemmas or tactics are invoked.
why it matters
Supports the theorem stable_is_attractor showing the zero-cost stable configuration itself meets the bound. It operationalizes the EN-006 claim that doubly-magic nuclei act as J-cost minima and optimal endpoints for transmutation paths. In the module setting, this closes the local-minimum step in cost-descent sequences toward shell closures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.