pith. machine review for the scientific record. sign in
structure definition def or abbrev high

SurfaceCode

show as:
view Lean formalization →

SurfaceCode defines a 2D lattice quantum error correction structure with side length L, L squared physical qubits, one logical qubit, and distance L. Physicists studying fault-tolerant quantum computing cite it when mapping Recognition Science eight-tick redundancy onto surface code thresholds near one percent. The declaration is a direct structure definition that assigns the three derived fields by default.

claimA surface code on a square lattice of side length $L$ consists of $L^2$ physical qubits that encode one logical qubit with code distance $L$.

background

The module INFO-007 derives quantum error correction from the eight-tick redundancy of Recognition Science. Errors appear as phase shifts across the eight phases; correction restores alignment. The surface code is presented as the leading scalable approach whose 2D lattice matches the holographic boundary structure in the framework. Upstream structures supply the J-cost calibration and the spectral emergence that forces three spatial dimensions and the eight-tick octave.

proof idea

The declaration is a structure definition. It introduces the field L and then supplies default values n_physical := L * L, n_logical := 1, and distance := L.

why it matters in Recognition Science

This definition supplies the surface-code instance inside the eight-tick QEC derivation. It directly implements the 2D lattice that the module links to holographic boundaries and the T7 eight-tick octave. No downstream theorems yet consume it, so the explicit derivation of the one-percent threshold from phi constants remains open.

scope and limits

formal statement (Lean)

 195structure SurfaceCode where
 196  /-- Lattice size -/
 197  L : ℕ
 198  /-- Number of physical qubits: ~L² -/
 199  n_physical : ℕ := L * L

proof body

Definition body.

 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. -/

depends on (13)

Lean names referenced from this declaration's body.