binarySymmetricCapacity
plain-language theorem explainer
The definition of binary symmetric channel capacity supplies the Shannon capacity C(p) = 1 minus binary entropy of p. Modelers of information transmission under Recognition Science's 8-tick structure cite this when bounding reliable rates supported by phase redundancy. The implementation is a direct one-line expression of the binary entropy formula using real logarithms.
Claim. The capacity of a binary symmetric channel with crossover probability $p$ is $C(p) = 1 - H_2(p)$, where the binary entropy is $H_2(p) = -p log_2 p - (1-p) log_2 (1-p)$, equivalently $1 + p (ln p / ln 2) + (1-p) (ln (1-p) / ln 2)$.
background
The module INFO-005 derives error correction bounds from the 8-tick structure. It recalls Shannon's channel capacity theorem as the maximum reliable transmission rate for a noisy channel, with the RS mechanism using 8-tick phases to supply natural redundancy via phase correlations. Upstream results include the shifted cost H(x) = J(x) + 1 from CostAlgebra, which converts the Recognition Composition Law into the d'Alembert equation, together with structures from PhiForcingDerived and SpectralEmergence that fix the phi-ladder and gauge content.
proof idea
This is a definition implemented as the direct algebraic expression for binary entropy subtracted from unity; no lemmas or tactics are applied.
why it matters
It feeds the ten-percent capacity example that illustrates reliable transmission at 53 percent capacity for p equal to 0.1. This supports the error correction mechanism from 8-tick phases, linking to the eight-tick octave (T7) and the overall forcing chain. It addresses how phase correlations provide natural redundancy within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.