HeatTransferMechanism
plain-language theorem explainer
The declaration defines an inductive type enumerating the five canonical heat transfer mechanisms. A researcher deriving thermal equilibrium from the Recognition Science J-cost equation would cite this enumeration to set the configuration dimension at five. The definition proceeds by direct listing of the five cases with automatic derivation of finite type structure.
Claim. Define the inductive type $H$ whose constructors are conduction, convection, radiation, phase change, and thermoelectric effect, equipped with decidable equality and finite cardinality.
background
In Recognition Science, the J-cost function $J(x) = (x + x^{-1})/2 - 1$ quantifies the recognition cost of a configuration $x$. Thermal equilibrium holds when $J = 0$, corresponding to uniform temperature as uniform recognition, while a temperature gradient produces $J > 0$. The module ThermalPhysicsFromRS fixes the configuration dimension at five by enumerating the standard heat transfer mechanisms.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
This definition supplies the finite set required by the downstream theorem heatTransferMechanismCount, which proves the cardinality equals five, and by the structure ThermalPhysicsCert, which pairs that cardinality with the equilibrium condition Jcost 1 = 0. It realizes the module claim that five mechanisms equal configDim D = 5 in the thermal physics derivation from Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.