`quantumErrorCorrection`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.ErrorCorrectionBounds
domain: Information
line: 138 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.ErrorCorrectionBounds on GitHub at line 138.

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

 135    Yet QEC is possible! Using entanglement and syndrome measurement.
 136
 137    In RS: 8-tick phases provide natural QEC through phase correlations. -/
 138def quantumErrorCorrection : String :=
 139  "Protect quantum states using redundancy and syndromes"
 140
 141/-- For majority voting on 8 phases, the threshold is p < 3/8.
 142    Below this error rate, the majority is always correct. -/
 143theorem threshold_majority_voting :
 144    (eightTickCode.d - 1) / 2 < eightTickCode.n ∧
 145    (eightTickCode.d - 1) / 2 = 3 := by
 146  unfold eightTickCode; constructor <;> norm_num
 147
 148/-! ## Topological Codes -/
 149
 150/-- Topological error correction:
 151
 152    - Encode information in global topological properties
 153    - Local errors don't affect global topology
 154    - Example: Surface codes (2D lattice)
 155
 156    In RS: The ledger's topology provides error protection. -/
 157def topologicalCodes : String :=
 158  "Information in global topological properties"
 159
 160/-- The toric code (Kitaev):
 161
 162    Qubits on edges of a torus.
 163    Logical qubits = homology classes.
 164    Error correction via local syndrome measurements.
 165
 166    Error threshold ~1% achievable! -/
 167def toricCode : String :=
 168  "Qubits on torus edges, information in homology"

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.