Landauer's principle

Forgetting costs heat, at a rate set by temperature alone. This is where information stops being an abstraction.

proved in corpus · proved here, no imported axiomsLean landauer_bound

In plain terms

Here is the problem, and it starts with a demon. Maxwell imagined a tiny being that sorts fast molecules from slow ones, apparently creating a temperature difference for free and breaking the second law of thermodynamics. For a century the demon dodged every exorcism -- each proposed fix turned out to have a loophole.

Landauer found the real answer, and it is about memory. The demon must record what it learns, and its memory is finite, so eventually it must erase. Erasing is the step that cannot be free: resetting a memory to a blank state compresses many possible configurations into one, and that compression must be paid for in heat dumped to the surroundings.

The price is universal. It depends on the temperature and on nothing else -- not the technology, not the cleverness of the engineering. Forgetting one bit costs, at minimum, a fixed tempest-in-a-teacup amount of heat, and the demon's books balance exactly.

In CSD

Thermodynamics is not bolted onto this programme; it grows out of the same soil as the Born rule. The substrate is measure-preserving, so at the finest grain nothing is ever lost and entropy is conserved. Irreversibility appears only when a record is coarse- grained -- which is Boltzmann's picture, reversible microdynamics with irreversibility living in the description, not the dynamics.

Given that setup, an erasure bound is not an import from another field. It is what the record layer owes and pays: the corpus derives temperature and free energy first, from a variational principle, and then proves the Landauer bound in those earned terms. It is the tightest link the development has between information and physical cost.

Mathematically

The entropy removed from a system is bounded by beta times the heat delivered to the bath. Proof route: unitary evolution on an initially product state conserves total entropy; subadditivity bounds the system's entropy drop by the bath's entropy rise; the bath's Clausius inequality converts entropy rise into heat.

Stated in the Reeb-Wolf form, which forces the assumptions into the open -- the bath starts in a Gibbs state, everything is finite-dimensional, the initial system state is positive-definite, and BOTH final marginals are full-rank. Those last two are not decoration: they are what the subadditivity step consumes, and that step is proved only at positive-definite marginal scope. Naming them is the point, because several informal derivations of the principle are known to smuggle assumptions at exactly the step this version makes visible.

The name

Rolf Landauer (1927-1999) was born in Stuttgart; his family fled to New York in 1938 after his father's death. Harvard degrees, then IBM from 1952, where he spent his whole career at the Watson Research Center in Yorktown Heights -- corporate research at its mid-century best, where a physicist could spend decades on why computing costs energy.

The principle appeared in 1961 in the IBM Journal of Research and Development, a house journal, under the resolutely unglamorous title of a paper about heat generation. His slogan -- information is physical -- was a deliberate provocation. His colleague Charles Bennett drew the astonishing corollary a decade later: computation itself can be free; only forgetting costs. Experimental confirmation came in 2012, thirteen years after Landauer died.

Module
CsdLean4/Thermo/Landauer.lean
Related
von neumann entropy
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy