ClassicalCode
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.