crystalSymmetries
plain-language theorem explainer
The definition assigns the count of crystal symmetry operations to 2 raised to the spatial dimension D. Semiconductor physicists working in Recognition Science cite it when connecting the eight-tick octave to zincblende lattice properties and device certification. It is realized as an immediate numerical assignment that evaluates directly to 8.
Claim. The number of crystal symmetry operations is given by $2^D$, where $D=3$ is the spatial dimension fixed by the forcing chain.
background
The module derives semiconductor relations from Recognition Science, with five device types equal to configDim D = 5 and two carrier types equal to D-1. Crystal symmetries are linked to the eight-tick octave of period 2^3, producing eight operations for zincblende crystals. Band gaps are placed on the phi-ladder, with silicon near phi^{-3} in RS units where c=1 and hbar=phi^{-5}.
proof idea
The declaration is a direct definition that sets the symmetry count to the exponential 2^3. No lemmas or tactics are applied; the value is assigned explicitly to instantiate the dimension D=3 from the upstream forcing chain.
why it matters
This supplies the eight_syms field inside SemiconductorPhysicsCert, which bundles the five-device count, two-carrier relation, and symmetry count into a single certificate. It fills the T8 step of the forcing chain where D=3 produces the eight-tick octave. The downstream theorem crystalSymmetries_8 confirms the numerical value equals 8, anchoring the zincblende observation to the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.