Holography Landauer Identity Physical Landauer Identity

The erasure identity

Landauer's principle, proposed by Rolf Landauer in 1961, says that erasing one bit of information must dissipate at least kT ln 2 of heat, where k is Boltzmann's constant and T is the temperature. The familiar statement is an inequality: erasure costs at least that much. The Recognition Science framework contains a machine-checked derivation that turns this lower bound into an exact equality, but only inside a specific formal model and only after three named physical identifications are accepted as premises.

The declaration physical_landauer_identity proves that, on a discrete record of cell states, the heat dissipated during a process equals a fixed quantum q multiplied by the net number of erased bits. The proof is a short chain: it first shows that any heat observable matching the posted-record flux is exactly q times that flux on every path, then applies a previously proved accounting identity called books_balance, and finishes by ring simplification. The result is an equality, not an inequality, and it is unconditional about the accounting. The classical lower bound appears as a corollary, saturated because the stronger identity holds.

The equality does not stand alone as a physical law. It requires three MODEL premises, each a definitional choice rather than a proved fact. HeatIsPostedRecordFlux identifies measured boundary heat with the posted flux times q. ThermalBitCalibration identifies the proved deficit-free period with inverse temperature, making q equal to ln 2 divided by beta. LogicalErasurePostsDebit identifies a logical reset of n bits with the same endpoint record debit. With all three in place, the framework derives the classical Landauer bound as a theorem. Without them, the identity is pure accounting about a formal ledger, with no Joules or kelvins attached.

The framework is explicit about what would falsify the physical reading. A process that erases bits while dissipating strictly less heat than q times the net debit is named CheaperThanPostedDebit, and a proved theorem says any such measurement refutes the heat-carrier identification. This is a concrete, testable consequence: if a real erasure came in under the posted cost, the premise HeatIsPostedRecordFlux would be false, and the physical reading would fall while the accounting identity would remain intact.

In Recognition Science, the identity is therefore a bridge with a precise load rating. The accounting side is proved. The physical side is conditional on named premises, each of which is a modeling choice with a stated falsifier. The framework's contribution is not a new experimental fact about erasure, but a demonstration that if heat reads as posted flux, then Landauer's bound is not merely a floor but an exact bookkeeping identity.

/-- The RS Landauer identity on the forced cell. Given the explicit carrier
identification, dissipated heat equals the per-bit quantum times the net
posted-record debit, exactly. -/
theorem physical_landauer_identity
    (q : ℝ) (heat : PhysicalStepHeat)
    (hcarrier : HeatIsPostedRecordFlux q heat)
    (c : CellCfg) (p : List CellCfg) :
    dissipatedHeat heat c p = q * (netErasedBits c p : ℝ) := by
  unfold dissipatedHeat netErasedBits
  rw [physicalPathHeat_eq_scaled_recordFlux q heat hcarrier (c :: p)]
  rw [books_balance]
  push_cast
  ring

/-- Posted-debit lower-bound form. For a record-decreasing process and a
nonnegative heat quantum, the posted debit is nonnegative and dissipated heat
is at least `q` times that debit. The inequality is saturated because the
stronger exact identity holds. This theorem alone does not identify posted
weight loss with logical entropy erasure. -/
theorem posted_debit_lower_bound
    (q : ℝ) (heat : PhysicalStepHeat)
    (hcarrier : HeatIsPostedRecordFlux q heat)
    (c : CellCfg) (p : List CellCfg)
    (hq : 0 ≤ q) (herase : 0 ≤ netErasedBits c p) :
    0 ≤ q * (netErasedBits c p : ℝ)
      ∧ q * (netErasedBits c p : ℝ) ≤ dissipatedHeat heat c p := by
  have hbits : 0 ≤ (netErasedBits c p : ℝ) := by
    exact_mod_cast herase
  constructor
  · exact mul_nonneg hq hbits
  · exact le_of_eq (physical_landauer_identity q heat hcarrier c p).symm

/-- Any physical erasure measured strictly cheaper than its posted debit
refutes the heat-carrier identification used by the physical reading. -/
theorem cheaper_erasure_falsifies_posting_rule
    (q : ℝ) (heat : PhysicalStepHeat) (c : CellCfg)
    (p : List CellCfg)
    (hcheap : CheaperThanPostedDebit q heat c p) :
    ¬ HeatIsPostedRecordFlux q heat := by
  intro hcarrier
  have hlt := hcheap.2.2
  rw [physical_landauer_identity q heat hcarrier c p] at hlt
  exact (lt_irrefl _ hlt)

What this page does not claim

The identity does not prove that real physical heat obeys the posted-flux rule; that requires the named MODEL premise HeatIsPostedRecordFlux. The identity does not assign a numerical value in Joules or kelvins to the quantum q; SI units remain outside the certificate. The identity does not by itself identify posted weight loss with logical entropy erasure; that requires the LogicalErasurePostsDebit premise.

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