Pith. sign in
module module high

IndisputableMonolith.Physics.ThermodynamicLawsFromRS

show as:
view Lean formalization →

The module defines thermodynamic laws and processes derived from Recognition Science, with the 0th law as the condition J equals zero for thermal equilibrium. Physicists deriving classical thermodynamics from a single functional equation would cite it as the entry point for equilibrium concepts. The module consists of type definitions, counts, and basic predicates with no embedded proofs.

claimThermal equilibrium holds when the J-cost vanishes: $J=0$. Thermodynamic laws are predicates on processes satisfying this condition, with counts for laws and processes defined over the phi-ladder.

background

The module imports the Cost module, which supplies the J-cost function satisfying the Recognition Composition Law. It introduces sibling definitions for ThermodynamicLaw, ThermodynamicProcess, ThermodynamicCert, and associated counts. The local setting is the derivation of physics from the forcing chain, where T5 fixes J-uniqueness as $J(x)=(x+x^{-1})/2-1$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the base case for thermodynamic laws in the Recognition Science framework, directly encoding the 0th law as J=0 from the doc-comment. It connects to the T5 J-uniqueness step in the forcing chain and prepares ground for later laws via the phi-ladder mass formula.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)