stable_config
plain-language theorem explainer
stable_config supplies the NuclearConfig with ratio exactly 1 as the zero J-cost endpoint. Transmutation theorists cite it to witness existence of stable attractors in cost-descent paths. The definition is a direct structure constructor using the standard positivity witness for 1.
Claim. The stable configuration is the element of NuclearConfig whose ratio field equals $1$ (with witness $0<1$).
background
Module Engineering.FissionTransmutationStructure models nuclear transmutation via J-cost barriers. NuclearConfig is the structure whose ratio field is a positive real; ratio = 1 marks doubly-magic nuclei at local J-cost zero. J-cost itself is the derivedCost of a multiplicative recognizer (MultiplicativeRecognizerL4.cost) or the Jcost of a RecognitionEvent (ObserverForcing.cost). The module doc states that fission products lie at high J-cost and that optimal paths descend to the nearest zero-cost point.
proof idea
One-line definition that applies the NuclearConfig structure constructor to the pair (1, one_pos). No lemmas or tactics are invoked.
why it matters
This definition supplies the zero-cost witness required by fission_transmutation_from_ledger, stable_end_state_exists, and perfect_transmutation_efficiency. It realizes the EN-006 claim that doubly-magic nuclei are J-cost minima, closing the existence half of the transmutation theorem and feeding the cost-monotone-descent termination result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.