ThermalConductivityRegime
plain-language theorem explainer
Five thermal conductivity regimes are enumerated inductively as ballistic, diffusive, phonon-dominated, electron-dominated, and interface-limited. Materials physicists working on heat transport in the Recognition Science φ-ladder model cite this enumeration when classifying conductivity across scales. The definition is a bare inductive type that automatically derives Fintype, DecidableEq, Repr, and BEq instances.
Claim. The set of thermal conductivity regimes is the finite collection consisting of ballistic transport, diffusive transport, phonon-dominated conduction, electron-dominated conduction, and interface-limited conduction.
background
The module defines thermal conductivity regimes as five canonical categories that correspond to configDim D = 5 on the φ-ladder. These regimes classify distinct heat-transport mechanisms, with the adjacent-regime conductivity ratio fixed by the golden ratio φ. The local theoretical setting is the B9 Materials Depth section, which derives material properties directly from the self-similar φ-ladder.
proof idea
The declaration is a direct inductive definition of the five regimes. Automatic derivation of DecidableEq, Repr, BEq, and Fintype instances follows from the finite inductive structure, enabling the cardinality result to be obtained by decide.
why it matters
This enumeration supplies the domain for the ThermalConductivityCert structure, which asserts exactly five regimes together with the φ-ratio between successive kappa values and positivity of kappa. It fills the materials depth of the Recognition framework by providing the discrete set on which the φ-ladder acts for thermal properties, aligning with configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.