carrierTypes_eq_Dminus1
plain-language theorem explainer
The theorem equates the number of semiconductor carrier types to two, confirming it matches three spatial dimensions minus one. Device physicists working within the Recognition Science derivation of material properties would cite this when linking carrier count to dimensionality. The proof proceeds by direct numerical evaluation using the decide tactic on the unfolded definition.
Claim. The number of charge carrier types satisfies $2 = 3 - 1$, where the left side counts electrons and holes and the right side follows from spatial dimension $D = 3$.
background
In the Semiconductor Physics from RS module, five canonical device types equal configuration dimension five, while the band gap arises from the phi-ladder. The sibling definition sets carrier types to the constant two, accompanied by the note that this count equals D minus one. This rests on the upstream definition that directly assigns the value two and ties into the eight crystal symmetries equaling two to the power D.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the numerical equality after unfolding the definition of carrier types to the constant two.
why it matters
This supplies the two_carriers field inside the SemiconductorPhysicsCert definition, which aggregates five device types, two carriers, and eight symmetries to certify the RS-derived semiconductor physics. It instantiates the framework landmark that spatial dimension D equals three from the forcing chain T8, closing the link from abstract forcing to concrete material counts. No open questions remain, as the equality is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.