`isMagic`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Nuclear.Octave on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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.