  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
  49

papers checked against this theorem

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