steaneCode
SteaneCode supplies the standard [[7,1,3]] CSS quantum code built from the classical [7,4,3] Hamming code for bit-flip correction and a compatible [7,3,4] subcode for phase-flip correction. Quantum information researchers working on fault-tolerant codes or Recognition Science investigators linking error correction to eight-tick phase redundancy would cite this instance. The definition is a direct record construction whose only obligations are discharged by numerical normalization of the dimension and distance inequalities.
claimThe Steane code is the CSS code with classical codes $C_1$ the [7,4,3] Hamming code and $C_2$ a [7,3,4] code satisfying $C_2subseteq C_1$, encoding one logical qubit in seven physical qubits and correcting any single-qubit error.
background
CSSCode is the structure whose fields are two classical codes c1 (for bit-flip correction) and c2 (for phase-flip correction via the dual) together with the containment proof that the dimension of c2 is at most that of c1. The module sets this construction inside the Recognition Science derivation of quantum error correction from eight-tick redundancy, where the eight discrete phases supply natural redundancy for syndrome detection. Upstream results supply the fundamental tick as the RS time quantum and the phase function kπ/4 for k in Fin 8, which together generate the discrete phase shifts that errors induce.
proof idea
The definition directly populates the CSSCode record with the parameters n=7, k=4, d=3 for c1 and n=7, k=3, d=4 for c2, then applies norm_num to discharge the three inequalities k_le_n, d_pos and containment.
why it matters in Recognition Science
This definition realizes the Steane code as a concrete CSSCode instance inside the Information.QuantumErrorCorrection module, directly addressing the module's target of deriving QEC principles from RS 8-tick structure. It supplies the standard [[7,1,3]] code that can be used to explore how eight phases encode syndrome information for bit and phase flips. The construction touches the module's noted patent potential for novel codes based on the 8-tick structure.
scope and limits
- Does not prove the minimum distance or explicit error-correction capability beyond the supplied CSS parameters.
- Does not derive the code parameters from the eight-tick phase function.
- Does not address decoding algorithms or fault-tolerance thresholds.
formal statement (Lean)
151def steaneCode : CSSCode := {
proof body
Definition body.
152 c1 := { n := 7, k := 4, d := 3, k_le_n := by norm_num, d_pos := by norm_num },
153 c2 := { n := 7, k := 3, d := 4, k_le_n := by norm_num, d_pos := by norm_num },
154 containment := by norm_num
155}
156
157/-! ## The 8-Tick Connection -/
158
159/-- The 8-tick phases naturally encode redundancy:
160
161 Phase k ↦ e^{ikπ/4} for k = 0, 1, ..., 7
162
163 A Z error adds π to the phase (shifts by 4 ticks).
164 An X error cycles through phases differently.
165
166 The 8-fold structure provides natural syndrome detection. -/