twofold_from_8
plain-language theorem explainer
An eight-tick periodic ledger produces a twofold rotation axis by the division 8/4 = 2. A crystallographer deriving allowed symmetries from Recognition Science would cite this step when linking the fundamental octave to the monoclinic and orthorhombic systems. The proof is a one-line reflexivity that confirms the arithmetic identity holds definitionally.
Claim. In the eight-tick octave, the twofold symmetry axis satisfies $8/4 = 2$.
background
The module derives the 32 crystallographic point groups and 7 crystal systems from the 8-tick structure that forces three spatial dimensions. Periodic filling of 3D space restricts rotations to orders 1, 2, 3, 4, and 6; the twofold axis appears as an essential element in the monoclinic (one 2-fold or mirror) and orthorhombic (three perpendicular 2-folds) systems. The local setting is the space-filling constraint that follows from the Recognition Science ledger geometry.
proof idea
The proof is a one-line reflexivity that directly verifies the arithmetic identity 8/4 = 2.
why it matters
This declaration anchors the twofold symmetry as fundamental within the crystal symmetry derivation, connecting directly to the T7 eight-tick octave in the unified forcing chain. It supplies the basic 2-fold element required for the classification into 7 crystal systems and 32 point groups. No downstream theorems are recorded, so the step remains a local arithmetic anchor for the space-filling rules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.