`neutral8`

definition

show as: view math explainer →

module: IndisputableMonolith.Crystallography.SelectionRules
domain: Crystallography
line: 31 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Crystallography.SelectionRules on GitHub at line 31.

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

  28  (s % 2 = 0) && (t.h ≠ 0 ∨ t.k ≠ 0 ∨ t.l ≠ 0)
  29
  30/‑ Eight-window neutrality diagnostic over a sequence of motif weights. -/
  31def neutral8 (w : ℕ → ℝ) (i0 : ℕ) : ℝ :=
  32  (Finset.range 8).sum (fun i => w (i0 + i))
  33
  34/‑ Count legal triads in a finite list. -/
  35def countLegal (ts : List Triad) : ℕ :=
  36  ts.countP (fun t => legalTriad t)
  37
  38end SelectionRules
  39end Crystallography
  40end IndisputableMonolith

papers checked against this theorem

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