ClassicalCode
plain-language theorem explainer
ClassicalCode defines the parameters of a classical linear code via block length n, message length k, and minimum distance d, subject to k ≤ n and d > 0. Researchers constructing CSS codes or repetition codes from eight-tick redundancy cite this structure. The declaration is a plain structure definition with the two inequalities recorded as fields.
Claim. A classical linear code is specified by natural numbers $n$, $k$, $d$ satisfying $k ≤ n$ and $d > 0$, where $n$ is the block length, $k$ the message length, and $d$ the minimum distance that corrects $⌊(d-1)/2⌋$ errors.
background
The module derives quantum error correction from the eight-tick redundancy of Recognition Science, where the eight phases supply natural redundancy and errors appear as phase shifts restored by alignment. ClassicalCode supplies the base parameters for classical codes that feed into CSS constructions. It depends on the Block inductive type, which enumerates s, p, d, f blocks carrying fixed φ-packing offsets with no per-element tuning.
proof idea
The declaration is a structure definition that introduces the three natural-number fields together with the two inequalities k_le_n and d_pos as explicit fields.
why it matters
ClassicalCode is instantiated by repetitionCode3 and supplies the c1 and c2 components of CSSCode for bit-flip and phase-flip correction. It supplies the base layer for the module's derivation of QEC from eight-tick redundancy, linking to the T7 eight-tick octave. The structure supports the paper proposition on quantum error correction from information-theoretic phase space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.