eight_tick_corrects_3
plain-language theorem explainer
The eight-tick code has minimum distance 7 and therefore corrects up to three errors via the standard relation t = (d-1)/2. Researchers deriving quantum error correction bounds from Recognition Science phase structure would cite this equality when bounding channel capacity. The proof is a direct reflexivity check on the distance parameter already assigned in the code definition.
Claim. For the error-correcting code built from the eight-tick phases, the minimum distance $d$ satisfies $(d-1)/2 = 3$.
background
The module derives error correction bounds from the eight-tick structure. The fundamental time quantum is one tick, and the eight phases are defined as $kπ/4$ for $k=0,…,7$, giving the periodic octave that supplies natural redundancy through phase correlations. Upstream results fix the tick as the RS-native time unit and establish the phase function over Fin 8.
proof idea
The proof is a one-line wrapper that applies reflexivity to the pre-defined minimum distance of the eight-tick code.
why it matters
This equality supplies the concrete distance for the eight-tick code, supporting the module claim that eight-tick phases furnish natural quantum error correction. It sits inside the eight-tick octave step of the forcing chain and connects to quantum channel capacity results that use the same phase structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.