five_not_crystallographic
plain-language theorem explainer
Five-fold rotational symmetry cannot tile three-dimensional space periodically. Solid-state physicists and crystallographers cite this result when enumerating the allowed point groups under space-filling constraints. The proof is a one-line wrapper that unfolds the membership predicate and decides the negation against the explicit list of permitted orders.
Claim. Five-fold rotational symmetry is not crystallographic: a rotation by $2π/5$ cannot map any periodic lattice in three dimensions onto itself.
background
Crystal symmetry emerges in Recognition Science from the 8-tick structure that forces three spatial dimensions. Any periodic arrangement must respect the underlying ledger geometry, so rotational symmetries are restricted to those that permit space-filling without gaps or overlaps. The module states that only orders 1, 2, 3, 4, and 6 satisfy this constraint. allowedRotationOrders is defined as the list [1, 2, 3, 4, 6]. isCrystallographic n holds precisely when n belongs to that list, which encodes the classical crystallographic restriction in RS-native terms.
proof idea
The proof is a one-line wrapper. Simplification unfolds isCrystallographic to membership in allowedRotationOrders, after which the decide tactic verifies that 5 lies outside [1, 2, 3, 4, 6].
why it matters
This theorem supplies one concrete instance of the crystallographic restriction inside the Recognition Science derivation of crystal symmetry. It directly supports the module claim that exactly five rotation orders are allowed, which then determines the 32 point groups and 7 crystal systems. The result rests on the 8-tick octave forcing D = 3, ensuring that only these orders permit periodic tiling of three-dimensional space. No scaffolding remains; the statement is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.