threshold_majority_voting
plain-language theorem explainer
The theorem verifies that the majority-voting decoder for the 8-tick code tolerates exactly three errors per block of eight, placing the per-phase error threshold below 3/8. Information theorists analyzing phase-redundant encodings would cite this bound when establishing reliable recovery in periodic structures. The proof is a one-line term that unfolds the code definition and normalizes the arithmetic.
Claim. For the 8-tick code with block length $n=8$ and minimum distance $d=7$, the majority-voting threshold satisfies $t < n$ and $t = 3$ where $t = (d-1)/2$.
background
The module INFO-005 derives error correction bounds from the 8-tick structure. The eightTickCode definition encodes one bit across eight phases as the all-zero or all-one pattern and decodes by majority vote, supplying natural redundancy from phase correlations. Upstream, the eightTickCode parameters are given as length 8, dimension 1, distance 8, while the correction factor from the phi-ladder supplies a positive finite-N adjustment to channel capacity.
proof idea
The proof is a one-line wrapper that unfolds eightTickCode to expose its parameters and applies norm_num to verify the two arithmetic relations.
why it matters
This declaration supplies the concrete majority-voting threshold p < 3/8 for the 8-tick code, grounding the RS mechanism of error protection via eight-tick phase correlations (T7). It fills the classical bound inside the information module and connects to the phi-ladder correction for quantum channel capacity, though no downstream theorems yet invoke it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.