DopantType
plain-language theorem explainer
The declaration introduces an inductive type that enumerates five dopant categories for silicon semiconductors under configDim equal to five. Materials physicists classifying impurity effects on carrier density cite this enumeration when building device models. It is realized as a direct inductive construction that derives decidable equality, representation, boolean equality, and finite type structure automatically.
Claim. The set of canonical dopant types in silicon semiconductors consists of group-V donors, group-III acceptors, deep-level impurities, compensating impurities, and transition-metal scattering centers.
background
The module treats semiconductor modeling when the configuration dimension equals five, corresponding to silicon-type systems. It enumerates five categories: group-V donors (P, As, Sb), group-III acceptors (B, Al, Ga), deep-level impurities, compensating impurities, and transition-metal scattering centers. These categories classify how impurities modify electrical behavior in the Recognition Science materials layer.
proof idea
The declaration is an inductive definition with five constructors and derives the instances DecidableEq, Repr, BEq, and Fintype automatically with no proof body or lemmas applied.
why it matters
This definition supplies the type whose cardinality is fixed at five in the downstream theorem dopantType_count and the structure SemiconductorDopantCert. It anchors the materials section to the configDim = 5 case, consistent with the framework's assignment of D = 3 spatial dimensions to material classification. No open questions or scaffolding are indicated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.