No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
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.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
correction
in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use