pith. machine review for the scientific record. sign in
structure definition def or abbrev high

NuclearConfig

show as:
view Lean formalization →

The nuclear configuration structure parameterizes states by a positive real stability ratio, with equality to one marking stable doubly-magic nuclei. Nuclear engineers modeling transmutation cite it to represent J-cost descent from unstable fission products. The declaration consists of a direct structure introduction with a positivity hypothesis on the ratio.

claimA nuclear configuration is given by a positive real number $x > 0$ (the stability ratio), where $x = 1$ identifies stable nuclei.

background

The module derives fission product transmutation conditions from the J-cost barrier structure in Recognition Science. Each nuclear configuration carries a J-cost measuring its defect from the ideal stable state at ratio one; fission products occupy high J-cost positions far from the stability valley, while transmutation follows sequences of recognition events that reduce total J-cost toward doubly-magic local minima. Upstream results supply the cost definition from the multiplicative recognizer as derivedCost on the comparator and the observer forcing statement that the cost of any recognition event equals its J-cost; the ledger factorization calibrates J on the positive reals under multiplication.

proof idea

The declaration is a structure definition with fields for the ratio and its positivity proof. No tactics or lemmas are applied; it directly introduces the data type used by nuclearCost and transmutation path theorems.

why it matters in Recognition Science

It forms the base type for the EN-006 theorems on transmutation, including the main result asserting paths from any configuration to a zero-cost stable state. This realizes the framework claim that transmutation efficiency follows from J-cost descent, linking to the phi-forcing and spectral emergence structures that fix the underlying constants and dimensions.

scope and limits

formal statement (Lean)

  50structure NuclearConfig where
  51  /-- The stability ratio: x = 1 for perfectly stable. -/
  52  ratio : ℝ
  53  ratio_pos : 0 < ratio
  54
  55/-- The J-cost (instability measure) of a nuclear configuration. -/

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.