IndisputableMonolith.Crystallography.SelectionRules

   1import Mathlib
   2
   3/-!
   4# Crystallography Selection Rules (scaffold)
   5
   6LNAL-inspired selection: eight-window neutrality and legal SU(3) triads
   7translated into reciprocal-space motif constraints. This module provides simple
   8predicates and counters usable for empirical bias tests against space-group
   9frequencies.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Crystallography
  14namespace SelectionRules
  15
  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
  41