Information Channel Capacity Mutual Information Symmetric

Symmetry of mutual information

In information theory, mutual information I(X; Y) quantifies how much knowing the value of one random variable reduces uncertainty about another. It is defined as the Kullback-Leibler divergence between the joint distribution P(X, Y) and the product of the marginals P(X)P(Y). A fundamental property is its symmetry: I(X; Y) = I(Y; X). This is not an assumption but a theorem, first proved by Claude Shannon in his 1948 paper "A Mathematical Theory of Communication." The symmetry reflects that information is a relationship, not a one-way flow: if a noisy channel's input tells you about its output, the output equally tells you about the input.

The symmetry of mutual information is a key part of channel capacity. The capacity C of a channel is the maximum of I(X; Y) over all input distributions p(x), written C = max_p(x) I(X; Y). Shannon's noisy-channel coding theorem states that for any rate R below C, there exists an error-correcting code achieving arbitrarily small error probability, while for R above C, reliable communication is impossible. The symmetry property ensures that this capacity is well-defined: the maximum over inputs is the same whether you view the channel from the transmitter's or the receiver's side.

In Recognition Science, the framework's machine-checked library of formal theorems includes a declaration named mutual_information_symmetric. Its statement is simply True, proved by the trivial tactic. This is not a derivation of Shannon's theorem from first principles; it is a placeholder, a formal acknowledgment that the property holds. The library also contains a definition of mutual information as a supremum over achievable rates, a proof that it is non-negative, and a bound showing it cannot exceed log(inputSize * outputSize). These are genuine formal results, but they are scaffolding for a larger project.

The larger project is to derive Shannon's channel capacity from the ledger, the framework's discrete record of recognition events. The library defines a fundamental bit rate as the reciprocal of a constant tau0, and states a theorem capacity_from_ledger asserting that the ledger's finite capacity determines the channel capacity. However, this theorem is also stated as True, with no proof. The connection between the ledger's bandwidth and Shannon's capacity is an open target, not an established result.

What the declaration does not claim is as important as what it states. It does not prove the symmetry of mutual information from the ledger structure, nor does it establish any new information-theoretic result. It is a formal placeholder, a commitment that the property is true and will be derived. The real content of the library lies in the definitions and the few proved lemmas about non-negativity and boundedness. The derivation of Shannon's theorem from the ledger remains an open problem, and the falsifier structure in the library names the conditions under which the framework's approach would fail: if a channel could exceed its capacity, if there were no bandwidth limit, or if the constant tau0 were irrelevant.

/-- **THEOREM**: Mutual information is symmetric: I(X;Y) = I(Y;X). -/
theorem mutual_information_symmetric :
    True := trivial

/-- **THEOREM**: Mutual information is non-negative. -/
theorem mutual_information_nonneg (ch : Channel) (p : InputDistribution ch.inputSize) :
    mutualInformation ch p ≥ 0 := by
  unfold mutualInformation
  exact le_max_left 0 _

/-- Mutual information is bounded above by log of alphabet sizes.

    **Information-theoretic result**: The sum computed in `mutualInformation` is
    Σ p(x,y) log(p(x,y)/p(y)), which equals Σ p(x,y) log(p(x|y)) = -H(X|Y).

    Since conditional entropy H(X|Y) ≥ 0, we have -H(X|Y) ≤ 0.
    Therefore max(0, -H(X|Y)) ≤ max(0, 0) = 0 ≤ log(nm) for n,m ≥ 1. -/
private theorem mutual_info_bounded (ch : Channel) (p : InputDistribution ch.inputSize) :
    mutualInformation ch p ≤ Real.log (ch.inputSize * ch.outputSize) := by
  unfold mutualInformation
  apply max_le
  · -- 0 ≤ log(nm) for n,m ≥ 1
    have hn : (ch.inputSize : ℝ) ≥ 1 := Nat.one_le_cast.mpr ch.input_nonempty
    have hm : (ch.outputSize : ℝ) ≥ 1 := Nat.one_le_cast.mpr ch.output_nonempty
    exact Real.log_nonneg (by nlinarith : (ch.inputSize : ℝ) * ch.outputSize ≥ 1)
  · -- The sum is -H(X|Y) ≤ 0 ≤ log(nm)
    have h_log_bound : Real.log (↑ch.inputSize * ↑ch.outputSize) ≥ 0 := by
      have hn : (ch.inputSize : ℝ) ≥ 1 := Nat.one_le_cast.mpr ch.input_nonempty
      have hm : (ch.outputSize : ℝ) ≥ 1 := Nat.one_le_cast.mpr ch.output_nonempty
      exact Real.log_nonneg (by nlinarith)
    -- Show the sum is ≤ 0, then use transitivity to log(nm)
    have h_sum_nonpos : (Finset.univ.sum fun x : Fin ch.inputSize =>
        Finset.univ.sum fun y : Fin ch.outputSize =>
          let pxy := p.probs x * ch.transition x y
          let py := Finset.univ.sum fun x' => p.probs x' * ch.transition x' y
          if h : pxy > 0 ∧ py > 0 then pxy * (Real.log pxy - Real.log py)
          else 0) ≤ 0 := by
      apply Finset.sum_nonpos; intro x _
      apply Finset.sum_nonpos; intro y _
      simp only
      split_ifs with h
      · -- pxy > 0 and py > 0
        -- pxy ≤ py (since pxy is one term in the sum defining py)
        -- so pxy/py ≤ 1, log(pxy/py) ≤ 0, pxy * log(pxy/py) ≤ 0
        have h_pxy_le_py : p.probs x * ch.transition x y ≤
            Finset.univ.sum fun x' => p.probs x' * ch.transition x' y :=
          Finset.single_le_sum (fun i _ => mul_nonneg (p.nonneg i) (ch.trans_nonneg i y))
            (Finset.mem_univ x)
        have h_ratio_le : (p.probs x * ch.transition x y) /
            (Finset.univ.sum fun x' => p.probs x' * ch.transition x' y) ≤ 1 := by
          rw [div_le_one h.2]
          exact h_pxy_le_py
        have h_log_diff_nonpos : Real.log (p.probs x * ch.transition x y) -
            Real.log (Finset.univ.sum fun x' => p.probs x' * ch.transition x' y) ≤ 0 := by
          rw [← Real.log_div (ne_of_gt h.1) (ne_of_gt h.2)]
          exact Real.log_nonpos (le_of_lt (div_pos h.1 h.2)) h_ratio_le
        exact mul_nonpos_of_nonneg_of_nonpos (le_of_lt h.1) h_log_diff_nonpos
      · rfl
    linarith

/-- In Recognition Science, channel capacity comes from the ledger's bandwidth:

    1. **Temporal bandwidth**: τ₀ sets the minimum time per bit
    2. **Spatial bandwidth**: Voxel size sets minimum spatial resolution
    3. **Energy bandwidth**: E_coh sets minimum energy per bit

    C_ledger = (ledger transitions per second) × (bits per transition) -/
theorem capacity_from_ledger :
    -- The ledger has finite capacity
    -- This determines the channel capacity
    True := trivial

What this page does not claim

The declaration does not derive Shannon's channel capacity from the ledger structure. The symmetry of mutual information is not proved from the ledger's axioms. The library does not establish that the ledger's bandwidth limits information transmission.

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/ChannelCapacity.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: