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. -/
depends on (18)
Lean names referenced from this declaration's body.