def
definition
eightTickLogicalCode
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Information.QuantumErrorCorrection on GitHub at line 179.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
176 |1_L⟩ = (|2⟩ + |6⟩)/√2 (other even phases)
177
178 Or more sophisticated encodings using all 8 phases. -/
179def eightTickLogicalCode : EightTickCode := {
180 n_physical := 8,
181 n_logical := 1,
182 uses_8tick := true,
183 rate := 1/8
184}
185
186/-! ## Surface Codes -/
187
188/-- Surface codes are the leading approach for scalable QEC.
189
190 - Qubits on a 2D lattice
191 - Stabilizer measurements on plaquettes
192 - Error correction via matching
193
194 In RS: The 2D structure relates to holographic boundary. -/
195structure SurfaceCode where
196 /-- Lattice size -/
197 L : ℕ
198 /-- Number of physical qubits: ~L² -/
199 n_physical : ℕ := L * L
200 /-- Number of logical qubits: 1 for simple surface code -/
201 n_logical : ℕ := 1
202 /-- Distance: L -/
203 distance : ℕ := L
204
205/-- Surface code threshold: p_threshold ≈ 1%.
206
207 Below this error rate, arbitrarily long computation is possible.
208 Above it, errors accumulate faster than correction. -/
209noncomputable def surfaceCodeThreshold : ℝ := 0.01