Centering
plain-language theorem explainer
Centering enumerates the seven lattice centering modes that combine with the seven crystal systems to produce the fourteen Bravais lattices. Crystallographers and Recognition Science modelers cite it when counting periodic space-filling structures in three dimensions. The declaration is a direct inductive enumeration whose only derived structure is decidable equality.
Claim. The inductive type of Bravais-lattice centering modes consists of the seven constructors primitive ($P$), body-centered ($I$), face-centered ($F$), A-face-centered ($A$), B-face-centered ($B$), C-face-centered ($C$), and rhombohedral ($R$).
background
Recognition Science obtains three spatial dimensions from the eight-tick octave (T7-T8). Any periodic filling of this space must obey the crystallographic restriction: only rotation orders 1, 2, 3, 4, and 6 are compatible with lattice translations. Centering modes classify the additional lattice vectors that preserve this periodicity while still tiling space without gaps.
proof idea
The declaration is an inductive type definition that directly lists the seven centering modes. Decidable equality and Repr are obtained automatically by the deriving clause; no lemmas or tactics are invoked.
why it matters
The definition supplies the centering options required by the module's derivation of exactly fourteen Bravais lattices. It is used by the downstream theorem point_groups_sum and supports the module claim that seven crystal systems plus centering options yield fourteen lattices. In the broader framework it instantiates the space-filling constraint that follows from D = 3 and the eight-tick structure, contributing to the predicted counts of 32 point groups and 230 space groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.