validLengths
plain-language theorem explainer
validLengths encodes the requirement that the three lattice edge lengths a, b, and c are all strictly positive. Workers classifying crystal systems under Recognition Science constraints cite this predicate as the starting point for all seven systems. The implementation is a direct definition consisting of the conjunction of three inequalities drawn from the LatticeParams record.
Claim. A lattice with edge lengths $a$, $b$, $c$ satisfies the validity condition precisely when $a > 0$, $b > 0$, and $c > 0$.
background
LatticeParams is the structure that records the six geometric parameters of a crystal unit cell: the three lengths a, b, c together with the three angles alpha, beta, gamma. The module derives the 32 crystallographic point groups and 7 crystal systems from the 8-tick octave structure that forces three spatial dimensions and restricts rotations to orders 1, 2, 3, 4, and 6 only. This positivity condition on lengths is the minimal requirement that precedes any angle constraints for each crystal system.
proof idea
The definition is a direct conjunction asserting positivity of the three length components of the input LatticeParams structure.
why it matters
This predicate serves as the base constraint for the triclinic system, which imposes no further restrictions. It anchors the classification of all crystal systems in the module's derivation from the 8-tick structure and the space-filling requirement in three dimensions. The definition closes the minimal geometric setup needed before enumerating the allowed symmetries that produce exactly 32 point groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.