eightTickCode
The definition supplies the natural 8-tick code as an error-correcting code with parameters n=8, k=1, d=8. Researchers deriving error correction bounds in Recognition Science cite it as the basic object realizing phase redundancy from the eight-tick structure. The construction is a direct structure instance with no further proof obligations.
claimThe natural 8-tick code is the error-correcting code with codeword length $n=8$, message length $k=1$, and minimum distance $d=8$.
background
The module derives error correction bounds from the 8-tick structure of Recognition Science. The ErrorCode structure defines an (n, k, d) code, where n denotes codeword length, k message length, and d minimum distance; such codes correct up to floor((d-1)/2) errors. The 8-tick phases provide natural redundancy by encoding each bit across eight phases, with majority-vote decoding.
proof idea
The definition constructs the code directly by supplying the triple of natural numbers to the ErrorCode structure.
why it matters in Recognition Science
The definition is used by the theorems detect_vs_correct, eight_tick_corrects_3, and threshold_majority_voting to establish detection of up to 7 errors and correction of up to 3 errors, along with the majority-voting threshold below 3/8. It instantiates the eight-tick octave from the foundation as a concrete error-correcting code, providing the base case for bounds derived from phase correlations in the Recognition Science framework.
scope and limits
- Does not establish the Hamming bound for the code.
- Does not treat quantum error correction.
- Does not compute channel capacity.
- Does not derive the error threshold from noise models.
Lean usage
theorem corrects_three : ((eightTickCode.d - 1) / 2) = 3 := by rflformal statement (Lean)
121def eightTickCode : ErrorCode := ⟨8, 1, 8⟩
proof body
Definition body.
122