pith. machine review for the scientific record. sign in
def

eightTickLogicalCode

definition
show as:
view math explainer →
module
IndisputableMonolith.Information.QuantumErrorCorrection
domain
Information
line
179 · github
papers citing
none yet

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

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

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