`sum8`

definition

show as: view math explainer →

module: IndisputableMonolith.Nuclear.Octave
domain: Nuclear
line: 26 · 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 26.

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

  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.