`threshold_majority_voting`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.ErrorCorrectionBounds on GitHub at line 143.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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"
 169
 170/-! ## The 8-Tick Syndrome -/
 171
 172/-- Error syndromes from 8-tick phases:
 173

papers checked against this theorem

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