steaneCode
plain-language theorem explainer
The declaration supplies the Steane [[7,1,3]] code as an instance of the CSSCode structure, using the [7,4,3] Hamming code for bit-flip correction and its dual for phase-flip correction. Workers on fault-tolerant quantum computing within the Recognition Science setting would cite this construction when linking error correction to eight-tick phase redundancy. The definition is assembled by direct record assignment of the classical-code parameters together with norm_num verification of the length, dimension, and distance inequalities.
Claim. The Steane code is the CSS code whose bit-flip code $C_1$ is the classical [7,4,3] Hamming code and whose phase-flip code $C_2$ is the classical [7,3,4] code satisfying $C_2subseteq C_1$.
background
CSSCode is the structure that packages two classical codes together with a containment relation: $c_1$ corrects bit flips while $c_2$ (via its dual) corrects phase flips, and the field containment records $c_2.kleq c_1.k$. The module sets the local theoretical setting by deriving quantum error correction from eight-tick redundancy, where the eight phases $kpi/4$ supply natural syndrome detection for phase shifts. Upstream, the phase definition supplies the eight-tick angles, tick supplies the fundamental time quantum, and the Tick structure treats time as discrete ledger steps rather than a background manifold.
proof idea
The definition is assembled by direct record construction. The two ClassicalCode records are populated with the parameters n=7, k=4, d=3 and n=7, k=3, d=4 respectively; each k_le_n and d_pos field is discharged by a single norm_num tactic call, and the final containment field is likewise settled by norm_num.
why it matters
The definition supplies the concrete Steane instance required by the module's program of obtaining quantum error correction from eight-tick phase redundancy (T7). It sits immediately before the explicit eight-tick connection comment that links phase shifts of four ticks to Z errors. No downstream theorems yet consume the definition, leaving open the question of whether the eight-tick structure can be shown to generate the Hamming-code parameters rather than merely host them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.