LatticeParams
plain-language theorem explainer
LatticeParams records the three edge lengths and three angles that parametrize a crystal unit cell. Crystallographers working inside the Recognition Science derivation of the seven crystal systems cite this record when stating the input type for system-specific constraints. It is introduced by a plain structure definition with six real fields and no attached propositions.
Claim. A lattice is given by real numbers $a,b,c$ (edge lengths) and real numbers $α,β,γ$ (angles between the pairs of edges).
background
The module derives the 32 crystallographic point groups and 7 crystal systems from the Recognition Science 8-tick octave that forces three spatial dimensions and the consequent space-filling restriction to rotation orders 1, 2, 3, 4, 6. LatticeParams supplies the common data type on which the seven system predicates are defined. Upstream results supply the constants α and γ together with unrelated list enumerations; none alter the geometric meaning of the six fields.
proof idea
Record definition that directly introduces the six real fields; no lemmas or tactics are applied.
why it matters
It is the shared input type for the downstream constraint predicates (cubicConstraint, hexagonalConstraint, orthorhombicConstraint, etc.) that partition lattices into the seven crystal systems. The construction therefore sits inside the module-level claim that exactly seven systems arise from the 8-tick geometry and the crystallographic restriction. No open scaffolding is closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.