Information Channel Capacity2 From Jcost

Channel capacity and the cost function

In information theory, channel capacity is the highest rate at which data can be sent through a noisy channel with an arbitrarily low error rate. Claude Shannon's formula gives it as C = B * log2(1 + SNR), where B is the bandwidth in hertz and SNR is the signal-to-noise ratio. The quantity C measures bits per second; dividing by B gives bits per second per hertz, a measure of spectral efficiency. A channel with SNR of 71.7, for instance, carries about 6.18 bits per second per hertz.

The number 6.18 is close to phi^(2*phi), where phi is the golden ratio, about 1.618. That resemblance is structural in the Recognition Science framework: its ledger, a discrete record of recognition events, assigns a forced cost to each event, and that cost function J(x) = (x + 1/x)/2 - 1 is proved unique under five plain conditions. The framework models channel capacity by setting the signal-to-noise ratio to J(phi)^(-2), which equals 71.7, and the resulting 6.18 bits per second per hertz matches phi^(2*phi) to three decimal places.

In Recognition Science, the module ChannelCapacity2FromJCost defines the domain cost as J(m/e), the cost of a ratio of two positive quantities m and e. Its machine-checked library of formal theorems proves three general facts about this cost: it vanishes when m equals e, it is nonnegative for all positive inputs, and the threshold phi - 3/2 is positive. These are properties of the cost function itself, not of any particular communication channel. The module does not define m and e in terms of signal and noise; without such a definition, the Shannon formula remains a research note, not a derived theorem.

The proof establishes that the cost function is a well-behaved measure of discrepancy: zero at equality, never negative, with a positive threshold separating regimes. That is what the module proves in plain language. The connection to Shannon capacity, the specific value 71.7, and the structural match to phi all depend on identifying m and e with physical quantities, an identification the framework has not yet formalized. The general facts stand; the channel-specific conclusion is a target for future work.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

What this page does not claim

The Shannon formula is not derived from the cost function in this module. The value 71.7 is not proved to be the signal-to-noise ratio of any real channel. The structural match to phi is a research note, not a theorem.

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