thermodynamicProcessCount
plain-language theorem explainer
The declaration establishes that exactly five canonical thermodynamic processes exist within the Recognition Science mapping of the laws. Researchers deriving thermodynamic structure from the J-cost and equilibrium conditions would cite the count to confirm the process space dimension matches D=3. The proof is a direct one-line decision procedure that exhausts the finite inductive enumeration of the process constructors.
Claim. The set of thermodynamic processes has cardinality five: $|$isothermal, adiabatic, isobaric, isochoric, Carnot$| = 5$.
background
ThermodynamicProcess is the inductive type whose five constructors enumerate the canonical processes: isothermal, adiabatic, isobaric, isochoric, and Carnot. The module sets the local context by mapping the four thermodynamic laws onto RS primitives, with the zeroeth law identified as J=0 at equilibrium and the total process count fixed at configDim D=5. This rests on the upstream equilibrium result that Jcost 1 = 0, which supplies the recognition-equilibrium anchor for the zeroeth law.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance automatically derived from the inductive definition of ThermodynamicProcess.
why it matters
The result populates the five_processes field inside the ThermodynamicCert definition that certifies the full law-to-RS correspondence. It directly realizes the module claim that five processes equal configDim D=5, consistent with the four laws equaling 2^(D-1) at D=3 and the upstream equilibrium theorem. No open scaffolding remains for this enumeration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.