pith. sign in
module module high

IndisputableMonolith.Information.Thermodynamics

show as:
view Lean formalization →

The Information.Thermodynamics module supplies the minimal ledger state and cost structures needed to formulate the information-theoretic Landauer bound in Recognition Science. Researchers deriving thermodynamic limits from recognition costs would cite it when bridging information theory to dissipation. The module consists of type definitions and bound statements built on J-cost and the fundamental time quantum.

claimThe module introduces LedgerState as the minimal local ledger for the Landauer bound, together with RecognitionCost, ledger_entropy, thermal_cost, and the statements landauer_bound_holds, total_dissipation_bound, eight_tick_dissipation_limit.

background

Recognition Science quantifies recognition effort via the J-cost function imported from the Cost module. Constants supplies the RS-native time quantum τ₀ = 1 tick. The module defines LedgerState as the minimal structure that tracks local information for thermodynamic accounting, enabling derived notions such as reciprocity_skew, admissible states, RecognitionOperator, and entropy measures.

proof idea

This is a definition module, no proofs. It declares the core type LedgerState, auxiliary functions RecognitionCost, ledger_entropy and thermal_cost, and states the three main bounds landauer_bound_holds, total_dissipation_bound and eight_tick_dissipation_limit.

why it matters in Recognition Science

The module feeds IndisputableMonolith.Information, the aggregator that unites compression priors and recognition foundations with thermodynamic constraints. It supplies the local ledger machinery required to state the Landauer bound inside the RS framework and connects to the eight-tick dissipation limit.

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)