CSSCode
plain-language theorem explainer
CSS codes are defined as pairs of classical linear codes C1 and C2 with C2 contained in C1, where C1 handles bit-flip correction and the dual of C2 handles phase-flip correction. Researchers deriving fault-tolerant quantum computing from Recognition Science phase structure would cite this definition. It is introduced directly as a structure bundling the two codes and the dimension inequality without further proof steps.
Claim. A CSS code is a pair of classical linear codes $(C_1, C_2)$ satisfying $C_2.k ≤ C_1.k$, with $C_1$ correcting bit-flip errors and the dual of $C_2$ correcting phase-flip errors.
background
ClassicalCode is the structure for a linear code [n, k, d] with block length n, message length k, and minimum distance d that corrects floor((d-1)/2) errors. The module derives quantum error correction from the 8-tick redundancy of Recognition Science, where the eight phases supply natural repetition for restoring alignment after phase shifts. Upstream results include the phase definition from EightTick that supplies the periodic kπ/4 values and the correction factor from QuantumChannelCapacityFromPhi that scales capacity by 1/(phi N).
proof idea
This declaration is a structure definition that directly assembles two ClassicalCode instances with the single inequality c2.k ≤ c1.k; no tactics or lemmas are applied.
why it matters
The structure supplies the type for the downstream Steane code construction that encodes one logical qubit in seven physical qubits and corrects single-qubit errors. It fills the INFO-007 target of obtaining quantum error correction from 8-tick phase redundancy, aligning with the T7 eight-tick octave landmark where periodic phases generate the required redundancy. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.