SemiconductorDopantCert
plain-language theorem explainer
The SemiconductorDopantCert structure records that the inductive type of dopant categories has exactly five elements. Solid-state physicists modeling silicon doping would cite it when fixing the number of impurity classes to match configDim equal to 5. It is introduced as a bare structure definition whose single field asserts the Fintype cardinality equality.
Claim. Let DopantType be the finite inductive type whose five constructors are group-V donor, group-III acceptor, deep-level impurity, compensating center, and transition-metal scattering center. The structure SemiconductorDopantCert consists of the single field five_types witnessing that the cardinality of DopantType equals 5.
background
The module treats semiconductor dopant types in the B15 Solid-State Depth layer of Recognition Science, where configDim is fixed at D = 5 for silicon-type materials. DopantType is the inductive type with exactly the five constructors groupVDonor, groupIIIAcceptor, deepLevel, compensating, and transitionMetal, each carrying the standard Fintype instance. This enumeration directly encodes the five canonical categories: group-V donors (P, As, Sb), group-III acceptors (B, Al, Ga), deep-level impurities, compensating centers, and transition-metal scattering centers.
proof idea
The declaration is a structure definition containing one field. No lemmas or tactics are invoked; the field simply records the equality Fintype.card DopantType = 5, which follows immediately from the derived Fintype instance on the five-constructor inductive type.
why it matters
SemiconductorDopantCert supplies the type for the downstream definition semiconductorDopantCert, which constructs the witness using dopantType_count. It anchors the material-parameter count to the Recognition framework's configDim, consistent with the forcing chain that produces discrete cardinalities from the self-similar fixed point phi. The definition closes the enumeration step for solid-state applications without adding axioms or hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.