Holography Landauer Identity

The posted-record identity

Landauer's principle, proposed by Rolf Landauer in 1961, states 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 principle connects information theory to thermodynamics: logical irreversibility has a physical price. In the Recognition Science framework, this price appears as an exact identity, not just a lower bound, when heat is identified with changes in a posted record.

The framework models a ledger, a discrete record of events, where each step of a process posts a signed flux to a cell's potential. The core theorem, books_balance, proves that the total posted flux equals the change in the cell's potential. The Landauer identity module builds on this by defining a physical heat observable that reads the posted flux, scaled by a conversion quantum q. Under that single named premise, the theorem physical_landauer_identity proves that dissipated heat equals q times the net erased bits, exactly, for any finite trajectory.

The identity is unconditional as an accounting statement. The physical reading requires three named MODEL premises: heat reads posted flux, the proved deficit-free period is identified with inverse temperature, and logical erasure posts the same endpoint debit. With these, the classical Landauer lower bound follows as a corollary. At the forced period, the per-bit quantum takes the surface-rate form kappa * log 2 / (2 * pi), where kappa is the period's rate constant.

The module also names a falsifier. If a measurement ever finds erasure strictly cheaper than the posted debit, the theorem cheaper_erasure_falsifies_posting_rule proves the heat-carrier premise is false. The identity itself is not at risk; only the physical identification is. This keeps the framework honest: the accounting is proved, the physics is conditional, and the condition is testable.

What this establishes in plain language: in this model, you cannot erase information for free. The cost is not an accident of implementation but a consequence of how the ledger balances. The framework's machine-checked library of formal theorems proves the exact identity, and the physical interpretation stands or falls on three explicit, named assumptions.

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

/-- Classical Landauer lower bound, conditional on all three physical
identifications: heat reads posted flux, the deficit-free period is inverse
temperature, and logical erasure posts the endpoint debit. Equality in the
record ledger implies the classical inequality. -/
theorem classical_landauer_bound_of_posted_logical_erasure
    (q kappa : ℝ) (heat : PhysicalStepHeat)
    (hk : 0 < kappa)
    (hcarrier : HeatIsPostedRecordFlux q heat)
    (hthermal : ThermalBitCalibration q (euclideanPeriod kappa))
    (erasedBits : ℕ) (c : CellCfg) (p : List CellCfg)
    (hlogical : LogicalErasurePostsDebit erasedBits c p) :
    0 ≤ thermalBitHeat (euclideanPeriod kappa) * (erasedBits : ℝ)
      ∧ thermalBitHeat (euclideanPeriod kappa) * (erasedBits : ℝ)
        ≤ dissipatedHeat heat c p := by
  have hperiod : 0 < euclideanPeriod kappa := by
    unfold euclideanPeriod
    exact div_pos (by positivity) hk
  have hquantum : 0 < thermalBitHeat (euclideanPeriod kappa) := by
    unfold thermalBitHeat
    exact div_pos (Real.log_pos (by norm_num)) hperiod
  have hbits :
      (netErasedBits c p : ℝ) = (erasedBits : ℝ) := by
    exact_mod_cast hlogical
  constructor
  · exact mul_nonneg hquantum.le (Nat.cast_nonneg erasedBits)
  · rw [physical_landauer_identity q heat hcarrier c p,
      hthermal, hbits]

/-- At the proved deficit-free period, the calibrated per-bit quantum has the
surface-rate form `kappa * log 2 / (2 * pi)`. The only physical input is the
named thermal calibration; the period itself is forced by closure. -/
theorem thermalBitHeat_at_forced_period
    (q kappa : ℝ) (hk : 0 < kappa)
    (hthermal : ThermalBitCalibration q (euclideanPeriod kappa)) :
    q = kappa * Real.log 2 / (2 * Real.pi) := by
  unfold ThermalBitCalibration thermalBitHeat euclideanPeriod at hthermal
  rw [hthermal]
  field_simp [ne_of_gt hk, Real.pi_ne_zero]

/-- 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 physical interpretation is not proved; it depends on three named MODEL premises. The identity does not by itself identify posted weight loss with logical entropy erasure. No SI value for the conversion quantum q is derived in this module.

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: