`Triad`

definition

show as: view math explainer →

module: IndisputableMonolith.Crystallography.SelectionRules
domain: Crystallography
line: 19 · 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 19.

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

  16open scoped BigOperators
  17
  18/‑ A reciprocal-space motif encoded as a triple of Miller-like integers. -/
  19structure Triad where
  20  h : ℤ
  21  k : ℤ
  22  l : ℤ
  23  deriving Repr, DecidableEq
  24
  25/‑ Legal triad proxy: parity and sum constraints (scaffold). -/
  26def legalTriad (t : Triad) : Bool :=
  27  let s := t.h + t.k + t.l
  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.