ErrorCode
plain-language theorem explainer
The structure for error-correcting codes packages the parameters of a binary code as codeword length, message length, and minimum distance. Researchers deriving bounds for phase-based transmission in Recognition Science cite this when instantiating the 8-tick encoding. It is introduced as a direct structure definition that matches the classical triple notation without added constraints.
Claim. An $(n, k, d)$ error-correcting code is specified by a codeword length $n$, a message length $k$, and a minimum distance $d$. Such a code corrects up to $⌊(d-1)/2⌋$ errors and achieves rate $R = k/n$.
background
The module targets derivation of error correction bounds from the 8-tick structure. In Recognition Science, 8-tick phases supply natural redundancy: each bit is encoded across phases and recovered via phase correlations. This setting rests on the fundamental tick as the RS time quantum and draws from upstream structures on nuclear densities and ledger factorization.
proof idea
The declaration is a structure definition that directly introduces the three fields for codeword length, message length, and minimum distance, together with inline comments on their classical roles.
why it matters
This definition supplies the type instantiated downstream by the natural 8-tick code with parameters (8, 1, 8). It supports Hamming-bound calculations for the eight-tick octave and connects the information module to the T7 period in the unified forcing chain. The structure closes the interface needed to apply classical coding bounds inside RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.