Information Quantum Error Correction Surface Code

The surface code declaration

A surface code is a quantum error-correcting code that arranges physical qubits on a two-dimensional lattice. The standard construction uses a square grid of size L by L, stores one logical qubit in the whole grid, and corrects errors up to a distance L. This is the code behind many proposals for fault-tolerant quantum computers because it needs only nearest-neighbor interactions and has a high error threshold. The surface code was introduced in 1997 by Alexei Kitaev, who showed how to protect quantum information by measuring stabilizer operators on the lattice.

In the Recognition Science framework's machine-checked library of formal theorems, the declaration SurfaceCode (a formal structure, a named container for data) records exactly this classical definition. It specifies a lattice size L, sets the number of physical qubits to L squared, sets the number of logical qubits to 1, and sets the distance to L. The declaration is a definitional choice, not a theorem. It does not prove that the surface code corrects errors, does not derive the threshold, and does not connect the code to the framework's eight-tick redundancy idea. The library also defines a separate eight-tick code with 8 physical qubits and rate 1/8, and a repetition code with 3 physical qubits, but these are also definitions, not results.

The library's own documentation is explicit about the status. The module is labeled a sketch module: every declaration concludes in True or another tautology, so nothing in it is a result. The docstring warns not to cite these names as evidence. The declaration SurfaceCode is therefore a formal record of a known classical object, useful for future work, but it establishes no new fact about quantum error correction, and it does not validate the framework's broader claims.

What the declaration does is give the framework a precise, machine-readable handle on a standard concept, so that later theorems can refer to it unambiguously. The library also defines an error model with probabilities for no error, bit flip, phase flip, and both, and a depolarizing channel where each error occurs with probability p/3. These are the building blocks for stating, but not yet proving, any error-correction claim. The framework's target, as recorded in the module, is to derive quantum error correction from its eight-tick phase structure, but that target remains open.

/-- Surface codes are the leading approach for scalable QEC.

    - Qubits on a 2D lattice
    - Stabilizer measurements on plaquettes
    - Error correction via matching

    In RS: The 2D structure relates to holographic boundary. -/
structure SurfaceCode where
  /-- Lattice size -/
  L : ℕ
  /-- Number of physical qubits: ~L² -/
  n_physical : ℕ := L * L
  /-- Number of logical qubits: 1 for simple surface code -/
  n_logical : ℕ := 1
  /-- Distance: L -/
  distance : ℕ := L

/-- The 8-tick phases naturally encode redundancy:

    Phase k ↦ e^{ikπ/4} for k = 0, 1, ..., 7

    A Z error adds π to the phase (shifts by 4 ticks).
    An X error cycles through phases differently.

    The 8-fold structure provides natural syndrome detection. -/
theorem eight_tick_encodes_redundancy :
    -- The 8 phases provide 3 bits of redundancy
    -- This is enough for single-error correction
    True := trivial

/-- The depolarizing channel with error probability p.
    All errors equally likely. -/
noncomputable def depolarizing (p : ℝ) (hp : 0 ≤ p ∧ p ≤ 1) : ErrorModel := {
  p_I := 1 - p,
  p_X := p / 3,
  p_Y := p / 3,
  p_Z := p / 3,
  nonneg_I := by linarith [hp.right],
  nonneg_X := by linarith [hp.left],
  nonneg_Y := by linarith [hp.left],
  nonneg_Z := by linarith [hp.left],
  normalized := by ring
}

What this page does not claim

The surface code declaration does not prove that the surface code corrects errors. The declaration does not derive the error threshold or connect the code to eight-tick redundancy. The framework has not established any quantum error correction result; the target remains open.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/QuantumErrorCorrection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: