dopantType_count
plain-language theorem explainer
The theorem states that the finite type enumerating dopant categories for silicon semiconductors has cardinality exactly five, matching the configDim D=5 convention. Materials physicists building dopant models or certification structures would cite this result to confirm the classification is complete and finite. The proof is a one-line decision procedure that evaluates the cardinality from the derived Fintype instance on the five-constructor inductive type.
Claim. The set of five canonical dopant categories for silicon-type semiconductors has cardinality $|DopantType| = 5$, where the categories are group-V donor, group-III acceptor, deep-level impurity, compensating impurity, and transition-metal scattering center.
background
The module introduces five canonical dopant categories for silicon-type semiconductors tied to configDim D = 5: group-V donor (P, As, Sb), group-III acceptor (B, Al, Ga), deep-level impurity, compensating, and transition-metal scattering center. DopantType is the inductive type with exactly these five constructors, deriving DecidableEq, Repr, BEq, and Fintype instances. This places the result in the Materials domain, where configDim fixes the number of categories in solid-state models.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes Fintype.card directly from the Fintype instance derived for the inductive DopantType type, which enumerates precisely five cases.
why it matters
This theorem supplies the five_types field inside the semiconductorDopantCert definition, anchoring the dopant classification to the configDim = 5 convention. It closes the enumeration step for downstream certification in the Materials section. No open questions or scaffolding remain; the result is fully discharged by the decision procedure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.