triclinicConstraint
plain-language theorem explainer
The triclinicConstraint definition asserts that a lattice satisfies the triclinic system precisely when its three edge lengths are positive. Researchers deriving the seven crystal systems from the 8-tick octave and space-filling rules would cite this when classifying lattices that carry no essential symmetry elements. The definition is realized as a direct one-line alias to the validLengths predicate.
Claim. For lattice parameters $p = (a, b, c, α, β, γ)$, the triclinic constraint holds precisely when $a > 0$, $b > 0$, and $c > 0$.
background
LatticeParams is the structure that records the three edge lengths a, b, c together with the three inter-edge angles α, β, γ of a unit cell. validLengths is the predicate requiring each of those lengths to be strictly positive. The module derives crystal symmetry from the 8-tick structure that forces three spatial dimensions, then restricts rotational symmetries to orders 1, 2, 3, 4, 6 so that identical units tile space periodically; the triclinic case is the one with no further angle or length restrictions beyond positivity.
proof idea
The definition is a one-line wrapper that directly applies the validLengths predicate to the supplied LatticeParams structure.
why it matters
This definition supplies the minimal constraint set for the triclinic system, the first of the seven crystal systems enumerated in the module. It participates in the RS derivation that obtains exactly seven systems from the combination rules of the 32 crystallographic point groups and the 14 Bravais lattices. No downstream uses are recorded, leaving open its explicit integration into the full count of 230 space groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.