ClassicalCode
ClassicalCode parametrizes classical linear codes by block length n, message length k and minimum distance d subject to k ≤ n and d > 0. Researchers building quantum error correction from 8-tick redundancy cite it when instantiating repetition codes or CSS codes. The declaration is a bare structure carrying only the four fields and two inequality constraints.
claimA classical linear code is given by natural numbers $n$, $k$, $d$ satisfying $k ≤ n$ and $d > 0$, where $d$ is the minimum distance that corrects at most $⌊(d-1)/2⌋$ errors.
background
The module derives quantum error correction principles from the 8-tick redundancy of Recognition Science, in which the eight phases supply natural redundancy and errors appear as phase shifts whose correction restores alignment. A classical code supplies the parameters for bit-flip correction inside CSS constructions. The upstream Block inductive type from PeriodicTable fixes φ-packing offsets for the s, p, d, f shells with no per-element tuning.
proof idea
The declaration is a structure definition with zero proof body lines; it directly introduces the fields n, k, d together with the two proof obligations k_le_n and d_pos.
why it matters in Recognition Science
It supplies the type for the two classical codes inside CSSCode and for the concrete repetitionCode3 instance that maps |0⟩ to |000⟩ and |1⟩ to |111⟩. This realizes the INFO-007 claim that quantum error correction emerges from 8-tick structure and connects to the eight-tick octave (T7) in the forcing chain.
scope and limits
- Does not define generator or parity-check matrices.
- Does not enforce linearity of the code subspace.
- Does not compute the explicit number of correctable errors.
- Does not tie the parameters to specific 8-tick phases.
Lean usage
def repetitionCode3 : ClassicalCode := { n := 3, k := 1, d := 3, k_le_n := by norm_num, d_pos := by norm_num }formal statement (Lean)
112structure ClassicalCode where
113 n : ℕ -- Block length
114 k : ℕ -- Message length
115 d : ℕ -- Minimum distance
116 k_le_n : k ≤ n
117 d_pos : d > 0
118
119/-- The 3-qubit repetition code.
120
121 |0⟩ → |000⟩
122 |1⟩ → |111⟩
123
124 Corrects single bit-flip errors. -/