pith. sign in
module module high

IndisputableMonolith.Physics.ThermodynamicLawsFromRS

show as:
view Lean formalization →

This module defines the thermodynamic laws extracted from Recognition Science, opening with the 0th law as vanishing J-cost at equilibrium. Foundational physicists deriving classical thermodynamics from a single functional equation would cite it. The module supplies type definitions, counts, and a certificate structure rather than executable proofs.

claimThe module introduces the 0th law as $J=0$ for thermal equilibrium, together with a predicate on processes, a count of four laws, a process structure, and a certificate type that records compliance.

background

Recognition Science obtains all physics from the J-cost functional defined in the Cost module, where $J(x)=(x+x^{-1})/2-1$ measures departure from self-similarity. The present module applies this cost to thermodynamics by declaring equilibrium precisely when the cost vanishes. It imports Mathlib for basic algebraic structures and Cost for the J primitive, then assembles sibling declarations that enumerate laws, classify processes, and certify equilibrium states.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the interface that lets the Recognition framework recover the 0th law directly from J-uniqueness (T5 of the forcing chain). It feeds parent derivations of the remaining thermodynamic laws in the broader physics layer, closing the link between the Recognition Composition Law and classical equilibrium thermodynamics.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)