trigonalConstraint
plain-language theorem explainer
TrigonalConstraint encodes the lattice parameters for the trigonal (rhombohedral) crystal system as equal edges a = b = c with angles α = β = γ ≠ 90°. Modelers classifying the seven crystal systems under Recognition Science space-filling rules would cite it. The definition is a direct predicate built from conjunctions on the fields of LatticeParams.
Claim. For lattice parameters $p$, the trigonal constraint requires $a = b = c$, $α = β = γ ≠ 90^∘$.
background
LatticeParams is the structure holding three edge lengths a, b, c and three inter-edge angles α (between b and c), β (between a and c), γ (between a and b). The module derives crystal symmetry from the 8-tick structure that forces three spatial dimensions together with the restriction that only 1-, 2-, 3-, 4-, and 6-fold rotations permit periodic tiling of 3D space. Upstream, LatticeParams supplies the raw parameters on which every crystal-system predicate is written.
proof idea
The definition is a direct conjunction of equalities on the six fields of LatticeParams together with the single inequality on the angle.
why it matters
This definition supplies the trigonal case inside the enumeration of seven crystal systems listed in the module doc-comment. It participates in the derivation that exactly seven systems arise once the eight-tick octave (T7) and D = 3 are imposed. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.