Holography Landauer Bridge Walls Logical Erasure Posts Debit Iff

The erasure accounting identity

The declaration logical_erasure_posts_debit_iff in the Recognition Science framework's machine-checked library of formal theorems establishes a precise accounting identity. In plain language, it says that a computation step, represented as a change from one cell configuration to another, posts a debit for logical erasure if and only if the net number of bits erased along that path equals the claimed number. The theorem is a biconditional: the predicate logical erasure, a term for the framework's notion of a bit being forgotten, holds exactly when the endpoint bookkeeping matches the stated count. It is an identity of records, not a statement about the physics of resetting a bit.

The theorem is proved by definition: the predicate LogicalErasurePostsDebit is defined to be the equality netErasedBits c p = erasedBits, so the biconditional holds by reflexivity. This is a tautology, a statement true by its own form, in the formal sense. The framework's library also proves two consequences that give the identity its teeth. First, an idle path, one that stays at the zero cell and takes no steps, erases zero posted bits. Second, claiming a one-bit logical erasure on that same idle path is false. These theorems show the accounting identity discriminates between paths, but they do not supply a protocol for actually resetting a logical bit.

What the declaration does not claim is as important as what it proves. The framework's own documentation states that no Lean object names a logical-bit reset protocol that would force the equality. The identity is purely about endpoint posted-weight accounting; it introduces no additional logical-bit structure. The physical discharge, a protocol that would make the accounting identity hold for a reason other than defining it that way, remains an open target. The theorem is a wall that marks the boundary between what is proved and what is not.

/-- 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

/-- 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

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

/-- 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]

What this page does not claim

The declaration does not claim that any physical bit has been reset or erased. The declaration does not claim that logical erasure costs energy or heat. The declaration does not name a protocol that would force the accounting equality.

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: