MaxwellsDemon

Difficulty: hard — 3 definitions, 0 abbreviations, 1 lemmas, 7 theorems.

definition lemma theorem
legend

This file models a control mechanism, in the spirit of a well known thought experiment: a device that inspects two systems and only lets a proposed change happen when it moves information in one chosen direction — shrinking what one side holds while growing what the other holds.

One honest limitation: the device’s own yes/no decision is given size zero in this file’s model — its own record of what it just decided is treated as free. That looks like it lets information move from one side to the other for nothing. The resolution, well known for this exact problem, is that the device’s memory of its past decisions must eventually be cleared out again, and clearing memory out has an unavoidable cost that this file’s model does not yet charge for. gatedFlow’s own conserves field is exactly where that extra cost would have to be added, so this file leaves it as a natural next step rather than claiming to have resolved the paradox.

A gated flow between two information systems: Bool picks a direction (true for A→B, false for B→A), and transferAB/transferBA propose how the two states would change. The gate only lets the transfer actually happen when it grows the receiver and shrinks the sender — otherwise the states are left untouched. hAB/hBA require the proposed transfers to only redistribute size between the two sides (never create or destroy it), so the whole gate still satisfies InformationSystem’s own conservation law regardless of which side wins.

information-systems
noncomputable def InformationSystem.gatedFlow
    (transferAB : StateA → StateB → StateA × StateB) (hAB : ∀ a b, ‖transferAB a b‖ = ‖a‖ + ‖b‖)
    (transferBA : StateA → StateB → StateA × StateB) (hBA : ∀ a b, ‖transferBA a b‖ = ‖a‖ + ‖b‖) :
    InformationSystem (StateA × StateB) Bool Bool where
  step p dir :=
    if dir then
      if ‖(transferAB p.1 p.2).2‖ > ‖p.2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖
      then (transferAB p.1 p.2, true) else (p, false)
    else
      if ‖(transferBA p.1 p.2).1‖ > ‖p.1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖
      then (transferBA p.1 p.2, true) else (p, false)
  conserves p dir := by
    have hd : ‖dir‖ = 0 := by cases dir <;> rfl
    have hPairS : ∀ (x : StateA × StateB) (b : Bool), ‖(x, b)‖ = ‖x‖ + ‖b‖ := fun _ _ => rfl
    have hPairP : ∀ (x : StateA) (y : StateB), ‖((x, y) : StateA × StateB)‖ = ‖x‖ + ‖y‖ :=
      fun _ _ => rfl
    have hTrue : ‖(true : Bool)‖ = 0 := rfl
    have hFalse : ‖(false : Bool)‖ = 0 := rfl
    change ‖p.1‖ + ‖p.2‖ + ‖dir‖ = _
    split <;> split <;> simp only [hAB, hBA, hd, hPairS, hPairP, hTrue, hFalse]

Outer dependencies: InformationSystem, instNormBool_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Bool, Decidable, Eq, Eq.mpr, Eq.symm, Eq.trans, GT.gt, Nonempty, Not, Prod, True, congr, congrArg, eq_self, id, if_neg, if_pos, ite, of_eq_true, rfl

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

The gate lets an A→B transfer through exactly when it would grow StateB and shrink StateA: the demon only ever moves information in the direction that makes one side fuller and the other emptier.

theorem InformationSystem.gatedFlow_success_AB
    (transferAB : StateA → StateB → StateA × StateB) (hAB : ∀ a b, ‖transferAB a b‖ = ‖a‖ + ‖b‖)
    (transferBA : StateA → StateB → StateA × StateB) (hBA : ∀ a b, ‖transferBA a b‖ = ‖a‖ + ‖b‖)
    (p : StateA × StateB) :
    ((InformationSystem.gatedFlow transferAB hAB transferBA hBA).step p true).2 = true ↔
      ‖(transferAB p.1 p.2).2‖ > ‖p.2‖ ∧ ‖(transferAB p.1 p.2).1‖ < ‖p.1‖ := by

Dependencies: InformationSystem.gatedFlow, instNormBool_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Bool, Bool.false_eq_true, Decidable, Eq, Eq.mp, Eq.mpr, Eq.trans, False, GT.gt, Iff, Nonempty, Not, Prod, True, and_self, congr, congrArg, congrFun', eq_self, eq_true, false_iff, id, if_neg, if_pos, iff_self, implies_congr_ctx, implies_true, ite, of_eq_true

Used by: (none)

The gate lets a B→A transfer through exactly when it would grow StateA and shrink StateB: the demon only ever moves information in the direction that makes one side fuller and the other emptier.

theorem InformationSystem.gatedFlow_success_BA
    (transferAB : StateA → StateB → StateA × StateB) (hAB : ∀ a b, ‖transferAB a b‖ = ‖a‖ + ‖b‖)
    (transferBA : StateA → StateB → StateA × StateB) (hBA : ∀ a b, ‖transferBA a b‖ = ‖a‖ + ‖b‖)
    (p : StateA × StateB) :
    ((InformationSystem.gatedFlow transferAB hAB transferBA hBA).step p false).2 = true ↔
      ‖(transferBA p.1 p.2).1‖ > ‖p.1‖ ∧ ‖(transferBA p.1 p.2).2‖ < ‖p.2‖ := by

Dependencies: InformationSystem.gatedFlow, instNormBool_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: And, Bool, Bool.false_eq_true, Decidable, Eq, Eq.mp, Eq.mpr, Eq.trans, False, GT.gt, Iff, Nonempty, Not, Prod, True, and_self, congr, congrArg, congrFun', eq_self, eq_true, false_iff, id, if_neg, if_pos, iff_self, implies_congr_ctx, implies_true, ite, of_eq_true

Used by: (none)

Landauer’s principle, illustrated on a two-bit memory cell

Cell below is a concrete two-bit memory. Its measure is the constant 2 — its fixed storage capacity, the natural way to size a memory cell, regardless of what it currently holds. eraseSecondBit clears the second bit while consuming and producing nothing (Unit, size 0). conserves holds trivially: capacity never changes, so InformationSystem’s size-ledger sees nothing wrong here at all — no gain, no loss, ever.

Yet the operation cannot be undone: (true, true) and (true, false) both erase to (true, false), so no function can exist that recovers which of the two a given result came from. Because Cell only has finitely many possible values, this loss is not just a coincidence about these two particular values: any function on a finite type that ever collapses two different values together must also fail to reach some other value at all (Finite.injective_iff_surjective) — so cells of the form (_, true) become permanently unreachable once erasure happens. The space of states actually still in use shrinks, a real, countable loss that the constant ‖·‖ := 2 bookkeeping never sees.

This is the formal content of Landauer’s principle: erasing information is not free, even though this file’s size-based bookkeeping stays silent about it. A bookkeeping rule that does register the erasure would have to let the erased side’s measure grow past the fixed 2-bit capacity — for example by letting the output carry the erased bit away, or by allowing some further, unbounded measure (heat, in the original physical story) to absorb it — rather than the fixed, bounded measure used here.

A concrete two-bit memory cell.

def Cell := Bool × Bool

Outer dependencies: (none)

Lean core dependencies: Bool, Prod

Used by: Cell.erase_not_injective, Cell.erase_not_surjective, eraseSecondBit, instDecidableEqCell, instFintypeCell, instNonemptyCell, instNormCell, instNormNonnegCell

instance : Fintype Cell := inferInstanceAs (Fintype (Bool × Bool))

Outer dependencies: Cell

Mathlib dependencies: Finset, Finset.univ, Fintype

Lean core dependencies: Bool, Prod

Used by: Cell.erase_not_surjective

instance : DecidableEq Cell := inferInstanceAs (DecidableEq (Bool × Bool))

Outer dependencies: Cell

Lean core dependencies: Bool, DecidableEq, Prod

Used by: Cell.erase_not_injective

instance : Nonempty Cell := ⟨(false, false)⟩

Outer dependencies: Cell

Lean core dependencies: Bool, Nonempty

Used by: Cell.erase_not_injective, Cell.erase_not_surjective, eraseSecondBit

A cell’s size is its fixed 2-bit storage capacity, regardless of content.

instance : Norm Cell where
  norm _ := 2

Outer dependencies: Cell

Mathlib dependencies: Norm, Real

Lean core dependencies: Nat

Used by: Cell.erase_not_injective, Cell.erase_not_surjective, eraseSecondBit, instNormNonnegCell

Technical — you can skip this.

instance : NormNonneg Cell := ⟨fun _ => by change (0:ℝ) ≤ 2; norm_num⟩

Outer dependencies: Cell, NormNonneg, instNormCell

Mathlib dependencies: Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Real

Lean core dependencies: Bool, Nat, id

Used by: (none)

Clear the second bit, consuming and producing nothing (Unit).

def eraseSecondBit : InformationSystem Cell Unit Unit where
  step c _ := ((c.1, false), ())
  conserves c _ := by simp [Norm.norm]

Outer dependencies: Cell, InformationSystem, instNonemptyCell, instNormCell, instNormUnit_computerNetworks

Inner dependencies: instNormProd_computerNetworks

Mathlib dependencies: Real, add_zero

Lean core dependencies: Bool, Eq, Eq.trans, Prod, True, Unit, Unit.unit, congr, congrArg, eq_self, of_eq_true

Used by: Cell.erase_not_injective, Cell.erase_not_surjective

Clearing the second bit collides two distinct cells onto the same result.

theorem Cell.erase_not_injective :
    ¬ Function.Injective (fun c : Cell => (eraseSecondBit.step c ()).1) := by

Dependencies: Cell, eraseSecondBit, instNonemptyCell, instNormCell, instNormUnit_computerNetworks

Proof dependencies: instDecidableEqCell

Lean core dependencies: Bool, Decidable.decide, Eq, False, Function.Injective, Not, Unit, Unit.unit, absurd, id, of_decide_eq_true, rfl

Used by: Cell.erase_not_surjective

Because Cell is finite, non-injectivity forces non-surjectivity: cells with a true second bit are never reached as a result of erasing. The reachable state space has genuinely shrunk — the erased bit really is gone, a fact the constant-capacity measure never registers.

theorem Cell.erase_not_surjective :
    ¬ Function.Surjective (fun c : Cell => (eraseSecondBit.step c ()).1) := by

Dependencies: Cell, eraseSecondBit, instNonemptyCell, instNormCell, instNormUnit_computerNetworks

Proof dependencies: Cell.erase_not_injective, instFintypeCell

Mathlib dependencies: Finite.injective_iff_surjective

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Function.Injective, Function.Surjective, Not, Unit, Unit.unit, congrArg, id

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend