hamming_bound_8tick
plain-language theorem explainer
The Hamming sphere-packing bound holds for the 8-tick binary code with k=1 information bit and t=3 error correction: the total volume of radius-3 balls around the two codewords is at most 2^8. Information theorists working on phase-based redundancy in Recognition Science cite this when confirming perfect codes from the eight-tick octave. The verification is a direct numerical check via native_decide on the binomial sum.
Claim. $2^{1} (1 + 8 + 28 + 56) = 186 < 256 = 2^{8}$, confirming that the Hamming balls of radius 3 around the codewords fit inside the ambient space of length 8.
background
Recognition Science uses the eight-tick octave as the fundamental period for encoding, with each information bit spread across eight phases to generate redundancy. The upstream definition tick sets the RS-native time quantum τ₀ = 1, so one octave equals exactly eight ticks. The module INFO-005 derives combinatorial error-correction bounds from this phase structure, treating the 8-tick block as a binary code of length n=8.
proof idea
The proof is a one-line term that applies native_decide to evaluate the concrete numerical inequality directly.
why it matters
This anchors the error-correction analysis inside the eight-tick octave (T7) and shows the phase-based code meets the sphere-packing limit for t=3. It supports the derivation of information bounds from the forcing chain by confirming the 8-tick structure yields a perfect code. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.