Information Information Is Ledger Deterministic Has Zero Entropy

The deterministic state

In the mathematics of information, a deterministic probability distribution is one where a single outcome happens with certainty: the coin always lands heads, the die always shows six. Its Shannon entropy, the standard measure of surprise or information content, is zero, because nothing about the outcome is uncertain. This is a classical fact, known since Claude Shannon's 1948 founding of information theory, and it holds for any distribution that assigns probability 1 to one event and 0 to all others.

The Recognition Science framework, which models physical reality as a discrete record of recognition events, proves this classical fact inside its machine-checked library of formal theorems. The declaration deterministic_has_zero_entropy states that if a distribution assigns probability 1 to one outcome and 0 to every other, its Shannon entropy equals 0. The proof is not a numerical approximation or a physical assumption; it is a formal derivation from the definition of Shannon entropy, checked step by step by the library's kernel.

The framework's larger claim is that information is not abstract but is the ledger itself: each physical fact corresponds to a recognition event with a positive ratio, and the information cost of that event is J(x) = (x + 1/x)/2 - 1. In this vocabulary, the deterministic state has zero entropy because it is perfectly balanced: the ratio is 1, the cost is 0, and no information is stored. The empty ledger, with no events at all, also has total information cost 0, and any deviation from the balanced ratio carries strictly positive cost.

What the theorem does not claim is that a deterministic physical system is unphysical or trivial. It claims only that the probability distribution carries no surprise. A deterministic process can still be complex in other senses, for example in the sequence of states it visits over time. The theorem also does not claim that Shannon entropy is the only measure of information; it proves that Shannon entropy equals the expected J-cost for the framework's probability distributions, but other information measures remain outside its scope.

The practical consequence is a clean bridge between the framework's cost function and classical information theory. When a reader encounters a deterministic distribution in the framework, they know immediately: its entropy is zero, its information content is zero, and it sits at the balanced point of the cost function. This unifies the ledger picture with Shannon's measure, giving a single scale on which certainty, balance, and zero information all coincide.

/-- **THEOREM IC-001.11**: The deterministic distribution (one outcome certain) has zero entropy.
    Perfect knowledge = zero information cost = balanced ledger. -/
theorem deterministic_has_zero_entropy {n : ℕ} (d : ShannonEntropy.ProbDist n) (i : Fin n)
    (hdet : d.probs i = 1) (hother : ∀ j ≠ i, d.probs j = 0) :
    ShannonEntropy.shannonEntropy d = 0 :=
  ShannonEntropy.zero_entropy_deterministic d i hdet hother

/-- **THEOREM IC-001.11**: The deterministic distribution (one outcome certain) has zero entropy.
    Perfect knowledge = zero information cost = balanced ledger. -/
theorem deterministic_has_zero_entropy {n : ℕ} (d : ShannonEntropy.ProbDist n) (i : Fin n)
    (hdet : d.probs i = 1) (hother : ∀ j ≠ i, d.probs j = 0) :
    ShannonEntropy.shannonEntropy d = 0 :=
  ShannonEntropy.zero_entropy_deterministic d i hdet hother

/-- **THEOREM IC-001.14**: The empty ledger state has zero information cost.
    Consistent with: no recognition events = no information. -/
theorem empty_state_zero_cost : totalInfoCost ⟨[]⟩ = 0 := by
  unfold totalInfoCost
  simp

/-- **THEOREM IC-001.3**: Any ratio x ≠ 1 carries strictly positive information cost.
    J(x) > 0 for all x > 0, x ≠ 1. -/
theorem info_cost_pos_of_ne_one (e : RecognitionEvent) (hne : e.ratio ≠ 1) :
    infoCost e > 0 := by
  have hzero := (info_cost_zero_iff_unit e).not.mpr hne
  have hnn := info_cost_nonneg e
  exact lt_of_le_of_ne hnn (Ne.symm hzero)

What this page does not claim

The theorem does not claim that deterministic physical systems are simple or trivial in their dynamics. It does not claim that Shannon entropy is the only valid measure of information. It does not claim that the framework's ledger model is the only way to derive the zero-entropy result.

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: