Information Thermodynamics

The ledger's heat

Information thermodynamics studies the physical cost of manipulating information. The ledger, a discrete record of recognition events, tracks how much a system's internal model must change to match reality. Each change carries a cost, a number measuring the effort of that recognition. The framework's central result, proved in a machine-checked library of formal theorems, is that this cost function must take one specific form: J(x) = (x + 1/x)/2 - 1. This is not a choice; it is forced by five plain conditions any reasonable cost must satisfy.

The module builds a minimal model of a ledger state. A state holds a set of active bonds, each with a multiplier that records how strongly that bond is recognized. The total recognition cost sums the J-cost over all active bonds. The module then defines an entropy proxy: the sum of the absolute logarithms of the multipliers. This measures how far each bond is from perfect balance, where the multiplier is 1 and the log is 0. The framework calls this ledger entropy, and it plays the role of thermodynamic entropy in this discrete setting.

The key result is a proved theorem: the total recognition cost of any state is bounded below by half the sum of the squared logarithms of the multipliers. This is a Landauer-type bound. In conventional physics, Landauer's principle says erasing one bit of information must dissipate at least kT ln 2 of heat. Here, the theorem shows that reducing mismatch in the ledger requires a minimum cost that grows quadratically with the size of the mismatch. The module also defines a thermal cost scale, T ln 2, matching the classical Landauer limit per tick.

The framework also proves a dissipation limit over its eight-tick recognition cycle. Any operator that evolves the ledger and minimizes J-cost cannot increase the total cost from one state to the next. Over a full cycle, the integrated cost balances the erasure, matching the Landauer picture. This is a formal statement: the framework's library checks that such an operator exists and that the bound holds. It does not claim to derive the second law of thermodynamics from scratch; it shows that within this model, the cost structure forces a Landauer-like limit.

What this establishes in plain language: if recognition has a forced cost, then erasing information has a minimum price in that cost's units. The module makes the link between the abstract cost function and thermodynamic entropy explicit and machine-checked. It gives a concrete picture of how a discrete ledger can carry an entropy-like quantity and how that quantity obeys a dissipation bound. The framework's contribution is not a new physical measurement but a formal bridge: the cost that recognition must pay is the same kind of quantity that thermodynamics calls heat.

/-- **Entropy Dissipation Theorem**
    The total recognition cost of a state is bounded below by the quadratic
    sum of the information mismatches. -/
theorem total_dissipation_bound (s : LedgerState) :
    RecognitionCost s ≥ (1/2 : ℝ) * (s.active_bonds.sum (fun b => (Real.log (s.bond_multipliers b))^2)) := by
  unfold RecognitionCost
  rw [Finset.mul_sum]
  apply Finset.sum_le_sum
  intro b hb
  have h := landauer_bound_holds s b hb
  dsimp at h
  linarith

/-- **8-Tick Dissipation Limit**
    The total dissipation over one 8-tick cycle corresponds to the Landauer limit
    for pattern closure. -/
theorem eight_tick_dissipation_limit (R : RecognitionOperator) (s : LedgerState) :
    let s_next := R.evolve s
    -- Over one complete cycle, the integrated cost balances the erasure
    admissible s → admissible s_next → RecognitionCost s_next ≤ RecognitionCost s := by
  intro s_next hadm_s _
  exact R.minimizes_J s hadm_s

/-- **DEFINITION: Thermal Energy Scale**
    The base thermal cost per tick. -/
noncomputable def thermal_cost (T : ℝ) : ℝ :=
  T * Real.log 2

What this page does not claim

The module does not derive the full second law of thermodynamics. The framework does not claim the cost function is the only possible entropy measure. No claim is made that the Landauer limit is physically realized in any specific experimental setup.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/Thermodynamics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: