regimeCount
plain-language theorem explainer
The theorem asserts that the set of thermoelectric regimes has cardinality five. Material physicists classifying thermoelectric materials under Recognition Science would reference this count. The proof proceeds by a single decision tactic that computes the cardinality from the five explicit constructors of the inductive type.
Claim. Let $R$ be the finite set whose elements are the five thermoelectric regimes (insulator, semiconductor, semimetal, metal, superconductor). Then the cardinality of $R$ equals 5.
background
Thermoelectric regimes are classified into five categories: insulator, semiconductor, semimetal, metal, and superconductor. This classification arises in the context of the thermoelectric figure of merit ZT derived from J-cost minimization in Recognition Science. The module establishes that this count matches the configuration dimension D = 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic succeeds because the inductive type is equipped with a Fintype instance derived from its five constructors, allowing direct computation of the cardinality.
why it matters
This declaration supplies the regime count used in the thermoelectricCert definition, which certifies the thermoelectric figure of merit. It parallels the heatTransferCert in the thermodynamics module. In the Recognition Science framework, the five regimes correspond to configDim D = 5, consistent with the eight-tick octave and spatial dimensions derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.