`LedgerState`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.Thermodynamics
domain: Information
line: 21 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.Thermodynamics on GitHub at line 21.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  18open Real
  19
  20/-- Minimal local ledger state for the information-theoretic Landauer bound. -/
  21structure LedgerState where
  22  active_bonds : Finset ℕ
  23  bond_multipliers : ℕ → ℝ
  24  bond_pos : ∀ b ∈ active_bonds, 0 < bond_multipliers b
  25
  26/-- Total recognition cost over active bonds. -/
  27noncomputable def RecognitionCost (s : LedgerState) : ℝ :=
  28  s.active_bonds.sum (fun b => Cost.Jcost (s.bond_multipliers b))
  29
  30/-- Entropy proxy: sum of absolute log-imbalances over active bonds. -/
  31noncomputable def reciprocity_skew (s : LedgerState) : ℝ :=
  32  s.active_bonds.sum (fun b => |Real.log (s.bond_multipliers b)|)
  33
  34/-- Admissibility predicate for the local information ledger. -/
  35def admissible (_s : LedgerState) : Prop := True
  36
  37/-- A local dissipative recognition operator for information thermodynamics. -/
  38structure RecognitionOperator where
  39  evolve : LedgerState → LedgerState
  40  minimizes_J : ∀ s, admissible s → RecognitionCost (evolve s) ≤ RecognitionCost s
  41
  42/-- **DEFINITION: Ledger Entropy**
  43    Entropy defined as the absolute log-imbalance of the ledger. -/
  44noncomputable def ledger_entropy (s : LedgerState) : ℝ :=
  45  reciprocity_skew s
  46
  47/-- **DEFINITION: Thermal Energy Scale**
  48    The base thermal cost per tick. -/
  49noncomputable def thermal_cost (T : ℝ) : ℝ :=
  50  T * Real.log 2
  51

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.