repetitionCode3
plain-language theorem explainer
The 3-qubit repetition code is instantiated as the classical linear code with block length 3, message length 1 and minimum distance 3. Researchers deriving quantum error correction from Recognition Science 8-tick redundancy would cite this as the elementary bit-flip correcting code. The definition is a direct record construction whose two inequality obligations are discharged by norm_num.
Claim. The 3-qubit repetition code is the classical linear code with block length $n=3$, message length $k=1$ and minimum distance $d=3$.
background
ClassicalCode is the structure that records a classical linear code by its block length n, message length k, minimum distance d together with the proofs k ≤ n and d > 0. The module Information.QuantumErrorCorrection derives quantum error correction principles from the RS 8-tick structure, where the eight phases supply natural redundancy and errors correspond to phase shifts. Upstream results include the definition of the 8-tick phases as kπ/4 for k in Fin 8.
proof idea
The definition constructs the ClassicalCode record by supplying the explicit parameters n=3, k=1, d=3 and discharging the two inequalities with norm_num.
why it matters
This definition supplies the base repetition code used to construct CSS codes later in the same module. It instantiates the 8-tick redundancy principle for quantum error correction described in the module documentation, where the repetition code corrects single bit-flip errors via the mapping |0⟩ → |000⟩ and |1⟩ → |111⟩. The construction fills the elementary case in the INFO-007 target of deriving QEC from RS phase structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.