pith. sign in
module module high

IndisputableMonolith.Information.Thermodynamics

show as:
view Lean formalization →

The Information.Thermodynamics module supplies the minimal LedgerState and associated cost functions needed to formulate the information-theoretic Landauer bound inside Recognition Science. Information theorists and statistical mechanicians cite it when mapping J-cost dissipation to thermodynamic limits. The module consists of definitions for LedgerState, RecognitionCost, ledger_entropy and thermal_cost together with theorems establishing landauer_bound_holds, total_dissipation_bound and eight_tick_dissipation_limit.

claimLedgerState is the minimal local ledger state such that the Landauer bound holds: dissipation cost $\geq k_B T \ln 2$ per erased bit, expressed via RecognitionCost and ledger_entropy in RS-native units with $\tau_0=1$ tick.

background

The module sits in the Information domain and imports the RS time quantum $\tau_0=1$ tick from Constants together with cost primitives from the Cost module. Its central object is LedgerState, introduced explicitly as the minimal local ledger state for the information-theoretic Landauer bound.

Sibling definitions include RecognitionCost, reciprocity_skew, admissible predicates, RecognitionOperator, ledger_entropy and thermal_cost. These support the three explicit bounds landauer_bound_holds, total_dissipation_bound and eight_tick_dissipation_limit.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the parent Information aggregator, whose doc-comment states it aggregates the information-theoretic and thermodynamic foundation of Recognition Science, including CompressionPrior (MDL grounded in J-cost) and EMLFromRecognition (oriented exp-log compiler gate from ledger coordinates). It therefore supplies the thermodynamic half of the information bridge.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)