Information Information

The recognition cost of a channel

Information theory, in the classical sense founded by Claude Shannon in 1948, measures how much a communication channel can carry and how much noise corrupts it. A channel takes an input message and produces an output, and the central question is how faithfully the output can represent the input. Shannon's noisy-channel coding theorem gives the maximum rate at which information can be sent reliably, a quantity called the channel capacity.

Recognition Science starts from a different question: what does it cost to recognize one thing as another? The framework keeps a discrete record of recognition events, a ledger, and forces a specific cost function on the ratio of the two things being compared. The cost is J(x) = (x + 1/x)/2 - 1, which is zero when the two are equal, grows as they diverge, and is always nonnegative. The framework applies this same cost to a communication channel by taking the ratio of the message sent to the message received, and calls the result the recognition cost of the channel.

The framework's machine-checked library of formal theorems proves three general facts about this cost. First, when the message and the received signal are equal, the cost is exactly zero. Second, for any positive message and positive received signal, the cost is never negative. Third, the framework's canonical threshold, the golden ratio minus 1.5, is positive. These are simple consequences of the cost function's defining properties, and they hold for any channel whatsoever.

What the framework does not do is make these facts specific to information theory. The cost is defined as J(m/e) without any reference to what m and e mean in a communication context. The docstring records a research note that the intended target was quantum channel capacity, where the framework conjectures a relation between the recognition cost and classical capacity, but that relation is not proved here. The framework proves the general cost facts once, universally quantified, and shares that body verbatim with 2383 sibling modules.

What the framework establishes, in plain language, is that the recognition cost is a well-behaved measure of channel fidelity: it is zero exactly when nothing is lost, and it is never negative. The threshold positivity is a small but real fact: the golden ratio, about 1.618, is more than 1.5, so the threshold is a positive number. These facts give the framework a consistent way to price any channel, but they do not yet connect that price to Shannon's capacity or to any specific physical channel. That connection remains open.

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]

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

What this page does not claim

The framework does not prove any connection between the recognition cost and Shannon's channel capacity. The framework does not establish the research note about quantum channel capacity. The recognition cost being zero at equality does not imply that a channel with zero cost is noiseless in the Shannon sense.

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