capacity_from_ledger
plain-language theorem explainer
Documents the intended claim that Recognition Science channel capacity is fixed by ledger bandwidth (temporal, spatial, and energy cutoffs), but the formal statement is only True. Anyone citing INFO-002 should treat this as a proved placeholder, not a capacity formula. The proof is the one-line term trivial.
Claim. The proposition $\mathrm{True}$ holds. Informally (from the surrounding documentation only): ledger channel capacity is $C_{\mathrm{ledger}} = (\text{ledger transitions per second}) \times (\text{bits per transition})$, with temporal scale set by $\tau_0$, spatial scale by voxel size, and energy scale by $E_{\mathrm{coh}}$.
background
Module INFO-002 aims to derive Shannon channel capacity from the Recognition Science ledger. Classically, $C = \max_{p(x)} I(X;Y)$ bits per use, and for a Gaussian channel $C = \tfrac12 \log_2(1+S/N)$. Here the intended source of $C$ is ledger bandwidth rather than an abstract noise model.
The doc-comment decomposes that bandwidth into three cutoffs: minimum time per bit $\tau_0$, minimum spatial resolution (voxel size), and minimum energy per bit $E_{\mathrm{coh}}$. The product form $C_{\mathrm{ledger}} = (\text{transitions/s}) \times (\text{bits/transition})$ is the stated organizing identity. Sibling definitions in the module (Channel, mutualInformation, channelCapacity, shannons_theorem) sketch the Shannon side; this declaration is the ledger-side marker.
Named import edges attached to the declaration (has, bit, the) are incidental identifier collisions and do not supply the capacity argument.
proof idea
Term-mode proof of True by trivial. No lemmas about mutual information, ledger transition rates, or $\tau_0$ are applied. The nearby comment stating $R_{\max} = 1/\tau_0$ bits per second per ledger entry is documentation only and is not part of the proof term.
why it matters
Sits in the Information domain as the named hook for "capacity from ledger bandwidth" under INFO-002. Downstream use count is zero, so nothing in the mirror currently depends on it. Framework-wise it points at the claim that reliable bit rate is set by discrete ledger ticks (related in spirit to the eight-tick octave and the recognition clock), not at a derived constant such as $\alpha$ or a mass-ladder rung.
Because the formal statement is only True, it does not yet close Shannon's theorem against RS structure, nor does it pin $C$ to $\phi$-ladder or $J$-cost identities. It records the target slogan until a real inequality or equality about $I(X;Y)$ and ledger rates is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.