Information Information Is Ledger

The Ledger as Information

Information, in the most common scientific sense, is a measure of surprise or surprise reduction. Claude Shannon's entropy, named for the amount of "missing information" in a message, assigns a number to a probability distribution: the more spread out the outcomes, the higher the entropy. A coin that always lands heads carries no surprise, so its entropy is zero; a fair coin carries one bit. This is the classical picture: information is a property of a probability distribution, not a thing in itself.

Recognition Science takes a different starting point. It models information as a discrete record of events, a ledger (a list of entries, each entry recording a recognition event). In this framework, a recognition event is simply a positive ratio x, a comparison of one thing against another. The framework defines the information cost of an event as J(x) = (x + 1/x)/2 - 1. This cost is not chosen freely; it is the unique function satisfying five plain conditions, a theorem proved in the framework's machine-checked library. The cost is always zero or positive, and it is symmetric: swapping the two things being compared, replacing x by 1/x, leaves the cost unchanged.

The framework's central claim is that this cost is the physical substrate. A balanced state, where the ratio x equals 1, has zero cost and zero information. Any deviation from balance carries positive cost, and the cost grows without bound as x approaches zero. The framework proves that a state with no events has zero total cost, and that the total cost of any list of events is never negative. It also proves that the golden ratio, phi, satisfies phi^2 = phi + 1 and is irrational, and that its information cost is positive.

The framework connects its cost to Shannon's entropy by proving that the expected J-cost over a probability distribution equals the Shannon entropy of that distribution. It also proves that a deterministic distribution, where one outcome is certain, has zero entropy. The framework links information to thermodynamics by defining a constant k_B ln 2, and proves that this constant is positive, so erasing one bit of information at temperature T costs at least k_B ln 2 times T in energy, a statement of Landauer's principle.

Within the framework, this is not a metaphor. The ledger is the reality, and information is the cost of the entries in it. The framework's library proves the properties of this cost: that the balanced state is the unique minimum, that any other state costs more, and that nothingness, a ratio of zero, is not a valid event. This dissolves the slogan "it from bit" into a stronger claim: "it is bit."

/-- The information cost of a recognition event = J(x). -/
noncomputable def infoCost (e : RecognitionEvent) : ℝ := Jcost e.ratio

/-- **THEOREM IC-001.1**: Every recognition event has non-negative information cost.
    J(x) ≥ 0 for all x > 0. This follows from AM-GM: (x + 1/x)/2 ≥ 1. -/
theorem info_cost_nonneg (e : RecognitionEvent) : infoCost e ≥ 0 :=
  Jcost_nonneg e.ratio_pos

/-- **THEOREM IC-001.2**: Information cost is zero iff the ratio is 1.
    J(x) = 0 ↔ x = 1 — the unique balanced/zero-defect state. -/
theorem info_cost_zero_iff_unit (e : RecognitionEvent) :
    infoCost e = 0 ↔ e.ratio = 1 := by
  unfold infoCost
  constructor
  · intro h
    rw [Jcost_eq_sq e.ratio_pos.ne'] at h
    have hden_pos : 0 < 2 * e.ratio := by linarith [e.ratio_pos]
    have hden_ne : (2 * e.ratio) ≠ 0 := ne_of_gt hden_pos
    have hsq : (e.ratio - 1) ^ 2 = 0 := by
      rwa [div_eq_zero_iff, or_iff_left hden_ne] at h
    nlinarith [sq_nonneg (e.ratio - 1)]
  · intro h; rw [h]; exact Jcost_unit0

/-- **THEOREM IC-001.9**: Shannon entropy equals expected J-cost.
    H(X) = Σ p_i · J(p_i) = expected information cost.
    This proves our information measure is consistent with Shannon's. -/
theorem shannon_entropy_equals_expected_jcost {n : ℕ} (d : ShannonEntropy.ProbDist n) :
    ShannonEntropy.shannonEntropy d = ShannonEntropy.totalJCost d :=
  ShannonEntropy.shannon_equals_jcost d

/-- **THEOREM IC-001.16**: For any positive temperature T, erasing one bit costs energy.
    E_min(T) = k_B T ln(2) > 0. This is Landauer's principle as a theorem in RS. -/
theorem landauer_energy_pos (T : ℝ) (hT : T > 0) : k_B_ln2 * T > 0 :=
  mul_pos landauer_constant_pos hT

What this page does not claim

This module does not prove that the ledger is the only possible model of information. This module does not derive the fine-structure constant or any other coupling constant. This module does not claim that Shannon entropy is the only measure of information.

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/Information/InformationIsLedger.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: