fundamentalBitRate
plain-language theorem explainer
Defines the universe's fundamental bit rate as the reciprocal of the RS tick duration τ₀, in bits per second per ledger entry. Anyone deriving Shannon capacity or ledger bandwidth in Recognition Science cites this constant. The body is a one-line assignment R_max := 1/τ₀; no proof obligations.
Claim. The fundamental bit rate is the real number $R_{\max} = 1/\tau_0$, where $\tau_0$ is the fundamental tick duration (one ledger update). Units are bits per second per ledger entry.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger structure. Capacity is the usual $C = \max_{p(x)} I(X;Y)$ bits per use; in RS it is read as the ledger's bandwidth, the rate at which the ledger can record and transmit information.
The constant $\tau_0$ is the fundamental time unit: duration of one tick in RS-native units (also available via a CODATA-style derivation $\sqrt{\hbar G/(\pi c^3)}/c$). The reciprocal $1/\tau_0$ is therefore the natural clock rate of ledger updates.
Sibling material in the module treats mutual information, channel capacity as a supremum over input distributions, nonnegativity and symmetry of $I(X;Y)$, and a Shannon theorem stub. The shifted cost $H(x) = J(x)+1$ appears in the import graph but is not used in this definition.
proof idea
Pure definition: assign the real 1 / tau0. No tactics, no lemmas, no hypotheses. The value inherits whatever meaning and units tau0 carries from Constants (and the Compat/Derivation aliases).
why it matters
Anchors the ledger-bandwidth story in INFO-002: once capacity is phrased as a rate, the natural RS unit is one bit per tick per entry, so $R_{\max} = 1/\tau_0$. The doc-comment flags the scale (~$10^{27}$ bits/s per entry), tying the information layer to the same tick that appears in the eight-tick octave (T7) and the forcing chain.
No downstream consumers are wired yet (used_by empty). Intended landing sites are capacity-from-ledger arguments and any bound that converts mutual information per use into a physical bit rate. It does not itself close Shannon's theorem or the Gaussian-channel formula; those remain sibling scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.