crystalSymmetries_8
plain-language theorem explainer
The theorem asserts that the RS-derived count of crystal symmetry operations equals eight. Researchers modeling zincblende semiconductors would cite this equality when connecting lattice symmetries to the three-dimensional spatial structure. The proof proceeds by direct evaluation of the preceding definition via the decide tactic.
Claim. The number of symmetry operations in the zincblende crystal lattice equals eight, satisfying $2^{D}=8$ for spatial dimension $D=3$.
background
The Semiconductor Physics from RS module derives device properties from the phi-ladder and dimensional constraints of the Recognition Science framework. The sibling definition crystalSymmetries sets the symmetry count to $2^{D}$, with the upstream forcing chain fixing $D=3$ and yielding the eight-tick octave structure. The module doc states that five device types equal configDim $D=5$ and two carrier types equal $D-1$, with the symmetry count of eight following as $2^{D}$.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to confirm the numerical equality after unfolding the definition of crystalSymmetries as two raised to the third power.
why it matters
This result supplies the eight_syms field in the semiconductorPhysicsCert definition, which aggregates the key RS-derived semiconductor properties including five devices and two carriers. It instantiates the T8 step of the forcing chain by confirming that $D=3$ yields the observed eight symmetries in zincblende crystals, matching the module doc's $2^{D}$ relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.