Triad
plain-language theorem explainer
Triad defines an integer triple for reciprocal-space vectors under crystallography selection rules. Researchers testing motif frequencies in space groups would cite it when constructing lists for parity-based filters. The declaration is a direct structure with three integer fields plus derived Repr and DecidableEq instances.
Claim. A triad is an ordered triple of integers $(h, k, l) ∈ ℤ³$ equipped with decidable equality.
background
The module supplies simple predicates for LNAL-inspired selection rules that map eight-window neutrality and legal SU(3) triads onto reciprocal-space motif constraints. These predicates enable empirical bias checks against observed space-group frequencies. The structure declaration sits inside that scaffold and draws on upstream parity patterns and phase-lift bounds.
proof idea
The declaration is a structure definition that introduces the three integer fields and derives Repr and DecidableEq. No lemmas or tactics are invoked.
why it matters
Triad supplies the input type for legalTriad (even sum and non-zero check) and countLegal (tally of valid entries). It therefore anchors the scaffold for SU(3) triad constraints inside the eight-tick neutrality framework. The module remains disconnected from the forcing chain T0-T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.