Encyclopedia Holography Holography Landauer Identity Classical Landauer Bound Of Posted Logical Erasure

ARTICLE 4 claims 4 theorems

Holography Landauer Identity Classical Landauer Bound Of Posted Logical Erasure

Landauer's principle says erasing a bit of information must dissipate at least kT ln 2 of heat; Recognition Science derives this bound from a ledger of posted records.

Verify this page

The classical bound

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. This is not about the energy of the information itself, but about the physical cost of resetting a memory to a known state. The principle sets a fundamental lower limit on the energy computers must spend to forget.

The Recognition Science framework derives this bound from a more basic accounting identity. In this framework, the ledger, a discrete record of every transition a system makes, tracks a quantity called posted flux. A theorem in the framework's machine-checked library of formal theorems proves that, for any process that decreases the number of posted bits, the dissipated heat is at least the per-bit quantum times the number of bits erased. This is the classical Landauer bound, and it holds exactly when three named physical identifications are made: heat reads the posted flux, the system's natural period is the inverse temperature, and logical erasure posts the same debit as the record accounting.

The theorem itself is an exact identity, not an inequality. The framework proves that dissipated heat equals the per-bit quantum times the net erased bits, and the inequality follows directly from that equality when the quantum is nonnegative. The per-bit quantum, at the framework's forced period, takes the form kappa * log 2 / (2 * pi), which mirrors the classical kT ln 2 once the period is identified with inverse temperature.

What the declaration does not claim is equally important. It does not prove that the physical identifications are true; those are named premises, not theorems. The inverse temperature is not derived, and no SI value for the quantum is fixed. The framework does not claim that this bound applies to all physical systems, only to those satisfying the three named conditions. A measured erasure cheaper than the posted debit would refute the heat-reading premise, and the framework names this as its falsifier.

For the reader, the consequence is concrete: within Recognition Science, the Landauer bound is not an assumption but a consequence of a more basic ledger identity. The bound is exact under the named physical bridge, and the framework provides a clear experimental test that would break that bridge.

THEOREM physical_landauer_identity · posted_debit_lower_bound · IndisputableMonolith/Holography/LandauerIdentity.lean
physical_landauer_identity · IndisputableMonolith/Holography/LandauerIdentity.lean:87 
/-- 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 · IndisputableMonolith/Holography/LandauerIdentity.lean:101 
/-- 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
THEOREM classical_landauer_bound_of_posted_logical_erasure · IndisputableMonolith/Holography/LandauerIdentity.lean
classical_landauer_bound_of_posted_logical_erasure · IndisputableMonolith/Holography/LandauerIdentity.lean:154 
/-- 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]
THEOREM thermalBitHeat_at_forced_period · IndisputableMonolith/Holography/LandauerIdentity.lean
thermalBitHeat_at_forced_period · IndisputableMonolith/Holography/LandauerIdentity.lean:182 
/-- 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]
THEOREM cheaper_erasure_falsifies_posting_rule · IndisputableMonolith/Holography/LandauerIdentity.lean
cheaper_erasure_falsifies_posting_rule · IndisputableMonolith/Holography/LandauerIdentity.lean:202 
/-- 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 identifications (heat reads posted flux, period is inverse temperature, logical erasure posts debit) are proved, not assumed. The inverse temperature or an SI value for the quantum is derived within the framework. The bound applies to all physical erasure processes, only those satisfying the named conditions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND