thermalPhysicsCert
plain-language theorem explainer
This definition assembles a certificate confirming five distinct heat transfer mechanisms in the Recognition Science framework and that equilibrium corresponds to zero J-cost. Physicists modeling thermal processes from first principles would reference it to ground the count of mechanisms at D=5. The construction is a direct field assignment drawing on prior cardinality and equilibrium results.
Claim. The definition supplies an instance of the structure asserting that the cardinality of heat transfer mechanisms equals 5 and that the J-cost at unit scale vanishes: $Fintype.card(HeatTransferMechanism)=5$ and $Jcost(1)=0$.
background
In the Recognition Science treatment of thermal physics the J-cost function measures the recognition penalty of temperature gradients, vanishing precisely when temperature is uniform. The structure ThermalPhysicsCert packages two facts: exactly five heat transfer mechanisms (conduction, convection, radiation, phase change, thermoelectric) matching configDim D=5, together with the equilibrium condition Jcost 1 = 0. Upstream results supply the equilibrium theorem Jcost 1 = 0 via Jcost_unit0 and the mechanism count via direct enumeration.
proof idea
The definition is a one-line wrapper that populates the five_mechanisms field from heatTransferMechanismCount and the equilibrium field from thermal_equilibrium.
why it matters
This certificate closes the thermal physics module by supplying the concrete instance required for downstream use of the five-mechanism structure. It directly implements the module claim that five mechanisms equal configDim D=5 and ties thermal equilibrium to J=0, consistent with the 0th law in the Recognition framework. No open questions are addressed here; it serves as a foundational definition for thermal derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.