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

levelEnergy

show as:
view Lean formalization →

levelEnergy supplies the nuclear level position on the phi-ladder as the golden ratio raised to the power 2n plus delta offset. Nuclear modelers assembling valence-cost proxies for magic-number checks would cite this definition. It is realized as a direct real exponentiation of the phi constant taken from the CPM Constants bundle.

claimThe nuclear level energy indexed by integers $n$ and $δ$ equals $φ^{2n + δ}$, where $φ$ is the golden ratio.

background

The Nuclear.Octave module places nuclear levels inside the eight-tick octave of Recognition Science. levelEnergy returns the rung height on the phi-ladder used to build occupancy or cost proxies. The upstream Constants structure from CPM.LawOfExistence bundles the golden ratio together with Knet, Cproj, Ceng and Cdisp. The cost definitions in MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost of recognition events, which levelEnergy helps populate for later closure tests.

proof idea

The definition is a one-line wrapper that applies Real.rpow to the phi constant from Constants with the exponent formed by casting 2*n + δ to reals.

why it matters in Recognition Science

levelEnergy is used by the isClosure predicate that declares an 8-window sum neutral when it equals zero, thereby identifying magic numbers on a fit-free valence-cost proxy. It fills the phi-ladder step required by the mass formula yardstick * phi^(rung - 8 + gap(Z)) and aligns with the T7 eight-tick octave and T8 D = 3 forcing-chain landmarks. The definition closes the scaffolding path from abstract cost to concrete nuclear octave sums.

scope and limits

formal statement (Lean)

  22def levelEnergy (n δ : ℤ) : ℝ :=

proof body

Definition body.

  23  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ) + (δ : ℝ))
  24
  25/‑ Sliding 8‑window sum over an occupancy/cost proxy `x`. -/

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.