CSSCode
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not supply explicit generator matrices or parity-check matrices for C1 or C2.
- Does not prove the distance or error-correction capability of the induced quantum code.
- Does not reference the phi-ladder mass formula or J-cost function.
- Does not address channel capacity corrections beyond the imported correction factor.
formal statement (Lean)
141structure CSSCode where
142 c1 : ClassicalCode -- For bit-flip correction
143 c2 : ClassicalCode -- For phase-flip correction (via dual)
144 containment : c2.k ≤ c1.k -- C₂ ⊆ C₁
145
146/-- The Steane [[7,1,3]] code.
147
148 Based on the [7,4,3] Hamming code.
149 Encodes 1 logical qubit in 7 physical qubits.
150 Corrects any single-qubit error. -/