Holography Landauer Bridge Walls One Bit Erasure Fails On Idle

The idle path test

Landauer's principle says that erasing one bit of information must dissipate at least a certain minimum amount of heat. The recognition science framework formalizes a version of this idea in a machine-checked library of formal theorems. The declaration one_bit_erasure_fails_on_idle is a precise test of one part of that formalization: it proves that a path which does nothing, an idle path, cannot be credited with erasing one bit.

The proof works by looking at the accounting rule for logical erasure. In the framework, the predicate LogicalErasurePostsDebit is defined as an exact equality: the number of bits erased equals the net change in a posted weight. On the idle path, the starting cell is the zero cell and nothing happens, so the net change is zero. The theorem proves that the predicate for one bit erased is false on this path, because zero is not equal to one. This is a theorem, not a definitional choice: the proof is a direct simplification of the definitions.

The theorem does not claim that erasure is impossible. It does not claim that a one-bit erasure can never occur on a non-idle path. It only shows that the accounting premise, as stated, distinguishes between paths: it correctly refuses to grant a one-bit erasure to a path that does no work. The framework also proves a companion result, zero_bits_erasure_on_idle, which shows that the same premise correctly grants zero bits erased on the idle path.

What the declaration does not do is supply a protocol for actually resetting a logical bit. The theorem is a negative result about a specific path, not a positive construction of a reset operation. The framework explicitly leaves open the question of whether a real physical reset protocol can force the accounting equality. The theorem is a wall that blocks a false claim, not a bridge that completes the argument.

/-- Claiming a one-bit logical erasure on the idle path is false. This shows
the premise discriminates paths, but still does not supply a reset protocol. -/
theorem one_bit_erasure_fails_on_idle :
    ¬ LogicalErasurePostsDebit 1 cell0 [] := by
  simp [LogicalErasurePostsDebit, netErasedBits]

/-- The logical-erasure premise is exactly endpoint posted-weight accounting.
There is no additional logical-bit structure in the statement. -/
theorem logical_erasure_posts_debit_iff
    (erasedBits : ℕ) (c : CellCfg) (p : List CellCfg) :
    LogicalErasurePostsDebit erasedBits c p ↔
      netErasedBits c p = (erasedBits : ℤ) :=
  Iff.rfl

/-- Claiming a one-bit logical erasure on the idle path is false. This shows
the premise discriminates paths, but still does not supply a reset protocol. -/
theorem one_bit_erasure_fails_on_idle :
    ¬ LogicalErasurePostsDebit 1 cell0 [] := by
  simp [LogicalErasurePostsDebit, netErasedBits]

/-- Quiet path: staying at the zero cell erases zero posted bits. -/
theorem zero_bits_erasure_on_idle :
    LogicalErasurePostsDebit 0 cell0 [] := by
  simp [LogicalErasurePostsDebit, netErasedBits]

What this page does not claim

This theorem does not claim that one-bit erasure is impossible on any path. This theorem does not supply a protocol for actually resetting a logical bit. This theorem does not identify an independent calorimeter with the ledger.

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/Holography/LandauerBridgeWalls.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: