Pith. sign in
module module high

IndisputableMonolith.Information.Thermodynamics

show as:
view Lean formalization →

The module supplies the minimal local ledger state needed to state the information-theoretic Landauer bound inside Recognition Science. Researchers deriving thermodynamic limits on recognition or computation from J-cost would cite the module. It assembles the state via imports from Constants and Cost, then exposes supporting definitions and bounds without internal proof bodies.

claimMinimal local ledger state $\mathcal{L}$ for the Landauer bound, with entropy and thermal cost expressed in RS-native units where $\tau_0=1$ tick.

background

The module belongs to the Information domain and rests on the Recognition Science framework that derives all physics from a single functional equation. It imports the fundamental time quantum $\tau_0=1$ tick from Constants and the cost structure from Cost. The module DOC_COMMENT identifies its core object as the minimal local ledger state required for the information-theoretic Landauer bound; sibling definitions such as LedgerState, ledger_entropy and thermal_cost supply the concrete ledger quantities.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Information aggregator, which combines it with CompressionPrior and EMLFromRecognition to assemble the information-theoretic and thermodynamic foundation of Recognition Science. It supplies the local ledger needed for downstream bounds such as landauer_bound_holds and eight_tick_dissipation_limit, linking J-cost to entropy production inside the eight-tick octave.

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)