def
definition
toricCode
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Information.ErrorCorrectionBounds on GitHub at line 167.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
164 Error correction via local syndrome measurements.
165
166 Error threshold ~1% achievable! -/
167def toricCode : String :=
168 "Qubits on torus edges, information in homology"
169
170/-! ## The 8-Tick Syndrome -/
171
172/-- Error syndromes from 8-tick phases:
173
174 If phase pattern is (0, 0, 1, 0, 0, 0, 0, 0):
175 - Error detected at phase 2
176 - Syndrome = [0, 0, 1, 0, 0, 0, 0, 0]
177
178 Recovery: Flip phase 2 back to 0.
179
180 The 8-tick structure naturally supports syndrome-based EC! -/
181def eightTickSyndrome (phases : Fin 8 → Bool) : List Bool :=
182 List.ofFn (fun i => phases i)
183
184/-- 8-tick: detect up to d-1 = 7 errors, correct up to ⌊(d-1)/2⌋ = 3. -/
185theorem detect_vs_correct :
186 (eightTickCode.d - 1 = 7) ∧ ((eightTickCode.d - 1) / 2 = 3) := by
187 constructor <;> rfl
188
189/-! ## Bounds from 8-Tick -/
190
191/-- The 8-tick structure implies natural bounds:
192
193 **Rate bound**: R ≤ 7/8 for single-error correction
194 (Need 1 redundant bit per 8 for parity)
195
196 **Error bound**: p < 3/8 = 37.5% for majority voting
197 (Need majority of 8 to be correct)