pith. sign in
module module moderate

IndisputableMonolith.Crystallography.SelectionRules

show as:
view Lean formalization →

This module introduces selection rules for crystallographic triads in the Recognition Science framework. It defines Triad structures, legalTriad predicates, neutral8 objects, and countLegal functions to enforce constraints from the eight-tick octave. Researchers deriving lattice symmetries from the J-functional equation would cite these definitions. The module consists entirely of definitions with no theorems or proofs.

claimThe module defines objects $T$ (Triad), the predicate legalTriad$(T)$, the structure neutral8, and the function countLegal that tallies valid configurations under the Recognition Composition Law.

background

Recognition Science derives spatial structure from the J-cost functional and the eight-tick octave (T7). This module sits in the crystallography domain and supplies the basic combinatorial objects needed to select admissible triads. The sibling definitions Triad, legalTriad, neutral8, and countLegal encode the local rules that later connect to D = 3 and the phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the combinatorial primitives that parent theorems on crystal symmetry and defect counting will invoke. It fills the gap between the abstract forcing chain (T5–T8) and concrete lattice models, preparing the ground for downstream results that apply the Recognition Composition Law to periodic structures.

scope and limits

declarations in this module (4)