carrierTypes
plain-language theorem explainer
The declaration sets the number of semiconductor carrier types to 2, matching D-1 for spatial dimension D=3. Researchers deriving device physics from Recognition Science cite it when confirming electrons and holes plus crystal symmetries. It is implemented as a direct constant assignment with no computation.
Claim. The number of carrier types is defined as $2$, satisfying the relation $2 = D - 1$ where $D = 3$ is the spatial dimension.
background
The module derives semiconductor properties from the phi-ladder and forcing chain. Five device types equal configuration dimension 5, while carrier types equal D-1. The upstream result T8 fixes D=3 spatial dimensions, yielding two carriers (electrons and holes) and eight symmetries equal to 2^D.
proof idea
Direct definition assigning the natural number 2. No lemmas or tactics are applied; the assignment matches the doc-comment relation to D-1.
why it matters
This definition supplies the carrier count required by the SemiconductorPhysicsCert structure and the equality theorem proving carrierTypes = 3-1. It realizes the T8 landmark D=3 from the eight-tick octave and connects to zincblende symmetries of 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.