thermalConductivityRegime_count
plain-language theorem explainer
The theorem establishes that the inductive type of thermal conductivity regimes has cardinality exactly five, matching the five regimes listed in the module. Materials researchers modeling conductivity on the phi-ladder would cite this result when assembling regime certificates. The proof is a one-line decision procedure that enumerates the five constructors of the inductive definition.
Claim. The finite cardinality of the set of thermal conductivity regimes equals five, where the regimes are ballistic, diffusive, phonon-dominated, electron-dominated, and interface-limited.
background
The module ThermalConductivityRegimesFromPhiLadder defines five canonical regimes via an inductive type whose constructors are ballistic, diffusive, phononDominated, electronDominated, and interfaceLimited. This set is identified with configDim D = 5 in the Recognition Science treatment of materials. The upstream inductive definition supplies the derived Fintype instance that the cardinality statement relies on.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic computes the cardinality directly from the Fintype instance automatically derived from the five-constructor inductive type.
why it matters
This cardinality populates the five_regimes field inside the downstream thermalConductivityCert definition, which also records the phi ratio and positivity properties. It completes the B9 Materials Depth section of the Recognition Science framework, where the phi-ladder supplies exactly five regimes for thermal conductivity. The result closes the enumeration step required for the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.