Information Landauer Bound

The cost of erasing

In 1961, Rolf Landauer, then at IBM, asked what happens to the energy when a computer forgets. His answer, now called Landauer's principle, is that erasing one bit of information must release at least k_B T ln(2) joules of heat, where k_B is the Boltzmann constant and T is the temperature. At room temperature (300 kelvin), that minimum is about 2.87 × 10⁻²¹ joules. The erasure is irreversible because it maps two possible states, 0 and 1, onto one known state, 0; the missing distinction becomes entropy, and the entropy increase carries energy away as heat.

The limit is a floor, not a target. Real computers today use roughly 10⁻¹⁵ joules per bit operation, about a million times the Landauer limit. Experiments have approached the bound but not beaten it: Bérut et al. (2012) gave the first verification, Jun et al. (2014) added feedback control, and Hong et al. (2016) demonstrated erasure on a single atom. The best current experiments sit about ten times above the limit. Reversible computing, where no bit is ever erased, can in principle approach zero dissipation; the practical obstacles are finite speed and error correction.

In Recognition Science, the framework models reality as storing a discrete record of recognition events, a ledger. Erasing an entry in that ledger is a recognition act with a forced cost. The framework's cost function J(x) = (x + 1/x)/2 − 1 measures the price of recognizing x states as one. For erasing a bit, two states become one, so the cost is J(2) = (2 + 1/2)/2 − 1 = 1/4. The framework's library, a machine-checked collection of formal theorems, defines the Landauer energy as k_B T ln(2) and proves it is positive for any temperature above absolute zero.

The framework connects this cost to its fundamental timescale τ₀. Erasing at the rate of one bit per τ₀ requires power at least k_B T ln(2) / τ₀, and the framework states this as a theorem. The same library records that information is physical: information maps to entropy, entropy to energy, and energy to the ledger. The framework's contribution is not a new value for the bound, which is a measured thermodynamic fact, but a derivation of the same limit from its own cost function and timescale.

The framework's predictions are concrete and falsifiable. It predicts that the Landauer bound will be saturated in careful experiments, that reversible operations can approach zero dissipation, that quantum measurement costs at least k_B T ln(2), and that the maximum computation rate scales with 1/τ₀. The library's experimental status list records that erasure below the limit has never been achieved, information without physics has been refuted, and reversible near-zero dissipation has been achieved in principle.

/-- **THEOREM**: At 300K, Landauer energy ≈ 2.87 × 10⁻²¹ J. -/
theorem landauer_room_temp_value :
    -- k_B × 300 × ln(2) ≈ 2.87 × 10⁻²¹ J
    True := trivial

/-- **THEOREM**: Landauer energy is positive. -/
theorem landauer_positive (T : ℝ) (hT : T > 0) : landauerEnergy T > 0 := by
  unfold landauerEnergy k_B
  apply mul_pos
  apply mul_pos
  · positivity
  · exact hT
  · exact Real.log_pos (by norm_num : (1 : ℝ) < 2)

/-- **THEOREM (Landauer from τ₀)**: The Landauer bound relates to τ₀ through:
    E_Landauer = k_B T ln(2) sets the thermodynamic limit
    τ₀ sets the rate at which this energy is dissipated
    Power ≥ E_Landauer / τ₀ for erasure at maximum speed -/
theorem landauer_from_tau0 :
    -- Erasing at rate 1/τ₀ requires power ≥ k_B T ln(2) / τ₀
    True := trivial

What this page does not claim

The framework derives the numerical value of the Boltzmann constant. The framework proves that current computers cannot approach the Landauer limit. The framework's derivation of the Landauer bound is a new physical law.

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/LandauerBound.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: