repetitionCode3
The repetitionCode3 definition supplies the parameters for the 3-qubit repetition code as a classical linear code with block length 3, message length 1, and minimum distance 3. Researchers deriving quantum error correction from eight-tick phase redundancy would cite this when mapping Recognition Science structures to standard QEC building blocks. The definition is assembled by direct assignment of the parameters followed by numeric normalization to confirm the two inequalities.
claimThe classical linear code with block length $n=3$, message length $k=1$, and minimum distance $d=3$ that satisfies $k≤n$ and $d>0$, encoding the logical states $|0⟩$ as $|000⟩$ and $|1⟩$ as $|111⟩$ to correct single bit-flip errors.
background
ClassicalCode is the structure recording a linear code by its block length $n$, message length $k$, minimum distance $d$, together with the proofs that $k≤n$ and $d>0$. The module sets quantum error correction inside Recognition Science by deriving redundancy from the eight phases of the 8-tick cycle, where phase shifts act as errors and alignment restoration supplies correction. Upstream results include the definition of the eight phases as $kπ/4$ for $k=0..7$ and the factorization of the ledger that calibrates the J-cost function used to measure information defects.
proof idea
One-line wrapper that directly constructs the ClassicalCode record by setting n=3, k=1, d=3 and discharges the two proof obligations k_le_n and d_pos by norm_num.
why it matters in Recognition Science
This definition supplies the classical seed for the CSS construction later in the module and for the eight-tick logical code that follows. It fills the concrete instance required by the module's target of obtaining QEC from 8-tick redundancy, where the three physical qubits mirror the three-bit repetition that arises naturally from the period-8 phase structure. No downstream uses are recorded yet, leaving open the explicit embedding into the full eight-tick encoder.
scope and limits
- Does not prove that the code corrects bit-flip errors
- Does not define the corresponding quantum encoding map
- Does not connect the parameters to the J-cost or defect distance
- Does not derive the code from the eight-tick phase function
formal statement (Lean)
125def repetitionCode3 : ClassicalCode := {
proof body
Definition body.
126 n := 3,
127 k := 1,
128 d := 3,
129 k_le_n := by norm_num,
130 d_pos := by norm_num
131}
132
133/-! ## CSS Codes -/
134
135/-- CSS (Calderbank-Shor-Steane) codes are built from two classical codes.
136
137 C₁ ⊇ C₂ (C₂ is a subcode of C₁)
138
139 - C₁ corrects bit-flip errors
140 - C₂⊥ corrects phase-flip errors -/