ChannelCapacityFalsifier
plain-language theorem explainer
Packages three observational failure modes that would defeat the ledger-bandwidth derivation of Shannon capacity: transmission above C, unbounded ledger bandwidth, or irrelevance of the fundamental tick τ₀. Anyone auditing INFO-002 cites this as the explicit falsification interface. It is a pure structure definition with a single implication field asserting that any of those modes yields False.
Claim. A falsifier record for the ledger-derived channel capacity consists of three propositions: (i) information can be transmitted faster than capacity $C$; (ii) the ledger has no bandwidth bound; (iii) the fundamental tick $\tau_0$ does not set the rate. The record requires that the disjunction of (i)--(iii) implies falsehood.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger structure. Classically, $C = \max_{p(x)} I(X;Y)$ bits per use is the supremum reliable rate; for a Gaussian channel this is $\tfrac12\log_2(1+S/N)$. In RS the same quantity is read off the ledger's bandwidth: the maximum rate at which the ledger can record and transmit distinctions.
Sibling material in the module defines channels, input distributions, mutual information $I(X;Y)$, nonnegativity and symmetry of $I$, the capacity functional, and a Shannon-style coding bound. Constants and the J-cost infrastructure are imported so that rates can eventually be tied to $\tau_0$ and the phi-ladder.
The present declaration does not prove capacity. It only names the three concrete ways the derivation would fail, so that later theorems can discharge or refute them.
proof idea
No proof body: this is a structure (definition). Four fields are declared. Three are bare propositions standing for the failure modes named in the doc-comment. The fourth is the implication that their disjunction is absurd. Downstream work is expected to inhabit or refute those propositions; nothing is proved here.
why it matters
Gives INFO-002 an explicit, referee-checkable falsification interface rather than an open-ended claim that "ledger bandwidth yields Shannon capacity." Aligns with the RS pattern of packaging what would break a forcing or derivation step (compare forcing-chain landmarks T0--T8, where each step has a clear negation). With no current downstream users, it is scaffolding for later theorems such as capacity-from-ledger and the Shannon bound in this module: those results should show that none of the three modes can hold once the ledger bandwidth and $\tau_0$ rate are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.