countLegal
plain-language theorem explainer
countLegal tallies the number of triads satisfying the even-sum and non-zero condition in a supplied list. Researchers testing space-group frequency biases against LNAL-derived selection rules would invoke it to quantify motif compliance. The definition is a direct one-line application of List.countP to the legalTriad predicate.
Claim. For a list $ts$ of integer triples $(h,k,l)$, the function returns the number of triples whose coordinate sum is even and which are not the zero triple.
background
The module supplies predicates for LNAL-inspired selection rules that translate eight-window neutrality and legal SU(3) triads into reciprocal-space constraints usable for empirical bias tests. A Triad is the structure holding three integers $h,k,l$. The predicate legalTriad returns true precisely when the sum $h+k+l$ is even and at least one coordinate is nonzero, serving as the eight-window neutrality diagnostic over motif weights.
proof idea
One-line wrapper that applies List.countP to the legalTriad predicate on the input list.
why it matters
The definition supplies a concrete counter for motif compliance checks inside the crystallography selection rules scaffold. It directly supports the eight-window neutrality diagnostic required by the Recognition framework's T7 octave and T8 dimensional constraints. No downstream theorems yet reference it, leaving open its integration into larger space-group frequency statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.