legalTriad
plain-language theorem explainer
legalTriad defines a boolean predicate on integer triads (h,k,l) that returns true precisely when their sum is even and they are not all zero. Researchers testing empirical bias in space-group frequencies against LNAL-inspired selection rules would cite this predicate. The definition is a direct arithmetic check on the three components with no external lemmas.
Claim. A triad $(h,k,l)inmathbb{Z}^3$ satisfies the legal predicate if $h+k+l$ is even and $(h,k,l)neq(0,0,0)$.
background
The module supplies simple predicates for LNAL-inspired crystallography selection rules, translating eight-window neutrality and legal SU(3) triads into reciprocal-space motif constraints usable for empirical bias tests against space-group frequencies. A Triad is the structure of three integers (h,k,l) serving as Miller indices. Upstream results include SpectralEmergence.of, which forces SU(3) times SU(2) times U(1) gauge content together with exactly three particle generations, and PhiForcingDerived.of, which structures J-cost minimization as a convex problem with unique minimum at unity.
proof idea
The definition computes the integer sum s = h + k + l and returns the conjunction of (s even) and (at least one index nonzero). It is a direct one-line arithmetic predicate with no lemmas or tactics applied.
why it matters
This predicate is invoked by countLegal to tally legal triads over a list, supporting the empirical tests scaffolded in the crystallography module. It realizes the legal SU(3) triad proxy described in the module documentation and connects directly to the SU(3) sector dimension forced by SpectralEmergence.of. The definition closes one concrete piece of the selection-rules scaffold within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.