`railFactor`

definition

show as: view math explainer →

module: IndisputableMonolith.Nuclear.Octave
domain: Nuclear
line: 18 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Nuclear.Octave on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  15open scoped BigOperators Real
  16
  17/‑ Rail factor for nuclear levels (dimensionless). -/
  18def railFactor (n : ℤ) : ℝ :=
  19  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ))
  20
  21/‑ Level energy proxy on rail n with sub‑rail offset δ (integer). -/
  22def levelEnergy (n δ : ℤ) : ℝ :=
  23  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ) + (δ : ℝ))
  24
  25/‑ Sliding 8‑window sum over an occupancy/cost proxy `x`. -/
  26def sum8 (x : ℕ → ℝ) (i0 : ℕ) : ℝ :=
  27  (Finset.range 8).sum (fun k => x (i0 + k))
  28
  29/‑ Eight‑window neutrality predicate for closures. -/
  30def isClosure (x : ℕ → ℝ) (i0 : ℕ) : Prop :=
  31  sum8 x i0 = 0
  32
  33/‑ Magic‑number predicate (display‑level): index `Z` is magic if some aligned
  34   8‑window around it is neutral. In practice, this will be evaluated on a
  35   fit‑free valence‑cost proxy assembled from `levelEnergy`. -/
  36def isMagic (x : ℕ → ℝ) (Z : ℕ) : Prop :=
  37  ∃ s : ℕ, s ≤ Z ∧ isClosure x s
  38
  39end Octave
  40end Nuclear
  41end IndisputableMonolith
  42
  43
  44
  45
  46
  47
  48

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.