NuclearConfig
plain-language theorem explainer
NuclearConfig records a nuclear state via its ledger ratio x > 0, where x = 1 marks the stable point at which J-cost vanishes. Transmutation engineers cite the structure to index sequences of recognition events that descend J-cost toward doubly-magic attractors. The declaration is a plain record with a single positivity field.
Claim. A nuclear configuration is a pair $(x, p)$ where $x > 0$ is the ledger ratio (with $x = 1$ the stable fixed point) and $p$ is a witness that $x > 0$. The associated J-cost is the value of the derived cost function at $x$.
background
J-cost is the instability measure induced by the multiplicative recognizer comparator on positive ratios, as defined in MultiplicativeRecognizerL4.cost and lifted to recognition events in ObserverForcing.cost. LedgerFactorization.of supplies the underlying factorization of positive reals under multiplication that calibrates the J function. The module EN-006 treats fission products as high-J-cost states far from the x = 1 valley and seeks cost-reducing paths to local minima at doubly-magic nuclei.
proof idea
Structure definition. Two fields are declared: the ratio real and the explicit positivity hypothesis. No further computation or tactic steps occur.
why it matters
NuclearConfig supplies the carrier type for every subsequent result in the module, including nuclearCost, transmutation_cost_pos, cost_monotone_descent_terminates, and fission_transmutation_from_ledger. It directly implements the EN-006 claim that transmutation efficiency follows from J-cost descent on the ledger ratio. The structure therefore anchors the engineering application of the Recognition Composition Law and the phi-ladder minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.