ThermodynamicProcess
plain-language theorem explainer
The inductive type enumerates the five canonical thermodynamic processes as distinct constructors. Researchers mapping the laws of thermodynamics onto the Recognition Science J-cost functional cite this when establishing that process count equals configDim at D=3. The declaration is a direct inductive definition with five cases plus automatic derivation of Fintype, Repr, and related instances.
Claim. The set of thermodynamic processes consists of the five types isothermal, adiabatic, isobaric, isochoric, and Carnot.
background
The module maps the four laws of thermodynamics to Recognition Science: the 0th law to J=0 at recognition equilibrium, the 1st law to sigma-conservation, the 2nd law to J-cost increase toward equilibrium, and the 3rd law to J approaching zero as recognition becomes perfect. Four laws total 4, which equals 2^(D-1) for D=3. Five canonical processes are identified as isothermal, adiabatic, isobaric, isochoric, and Carnot, corresponding to configDim D=5.
proof idea
This is an inductive definition that introduces five constructors for the listed processes. It derives DecidableEq, Repr, BEq, and Fintype automatically. No proof body or tactics are required.
why it matters
This definition supplies the five processes required by the ThermodynamicCert structure to assert Fintype.card ThermodynamicProcess =5, matching configDim at D=3. It supports the module claim that five processes equal configDim D=5 and enables the downstream cardinality theorem proved by decide. It contributes to the foundation for deriving all thermodynamic laws from the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.