heatTransferMechanismCount
plain-language theorem explainer
The theorem establishes that Recognition Science admits exactly five heat transfer mechanisms, matching the configuration dimension D=5. Researchers deriving thermal nonequilibrium from the J-cost functional would cite this enumeration of conduction, convection, radiation, phase change, and thermoelectric effects. The proof is a direct decision on the finite inductive type that lists the mechanisms.
Claim. $|C| = 5$ where $C = $ {conduction, convection, radiation, phase change, thermoelectric}.
background
The Thermal Physics from RS module sets thermal equilibrium to J = 0, the uniform recognition state, while temperature gradients carry positive J-cost. The upstream equilibrium result states that Jcost 1 = 0. HeatTransferMechanism is the inductive type whose five constructors are conduction, convection, radiation, phaseChange, and thermoelectric, each carrying DecidableEq and Fintype instances.
proof idea
One-line wrapper that applies the decide tactic to the decidable Fintype.card computation on the inductive HeatTransferMechanism type.
why it matters
Supplies the five_mechanisms field inside the thermalPhysicsCert definition. It confirms the canonical count equals configDim D=5 in the Recognition Science framework, consistent with the forcing chain that fixes spatial D=3 at T8 while allowing five thermal channels. No open scaffolding questions are closed by this result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.