eightTickCode
plain-language theorem explainer
The eightTickCode definition supplies the concrete (8,1,8) code that encodes one bit across eight phases with minimum distance 8. Researchers deriving majority-vote thresholds from Recognition Science phase structure cite this object when bounding correction performance. The definition is a direct record constructor that instantiates the ErrorCode structure with the triple (8,1,8).
Claim. The 8-tick code is the $(n,k,d)$ code with $n=8$, $k=1$, $d=8$, where $n$ is codeword length, $k$ is message length, and $d$ is minimum distance.
background
The module INFO-005 derives error correction bounds from 8-tick structure. The ErrorCode structure records an $(n,k,d)$ code, where $n$ is codeword length, $k$ message length, and $d$ minimum distance; such a code corrects up to floor((d-1)/2) errors. The 8-tick phases supply natural redundancy for encoding bits across phases, with decoding by majority vote.
proof idea
The definition is a direct record constructor that builds the ErrorCode structure with the triple (8,1,8).
why it matters
This definition supplies the concrete code object used by detect_vs_correct, eight_tick_corrects_3, and threshold_majority_voting. It realizes the natural redundancy from the eight-tick octave (T7) in the forcing chain, enabling derivation of error correction bounds. The parent theorems establish detection of up to 7 errors and correction of up to 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.