def definition def or abbrev

`eightTickLogicalCode`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 179def eightTickLogicalCode : EightTickCode := {

proof body

Definition body.

 180  n_physical := 8,
 181  n_logical := 1,
 182  uses_8tick := true,
 183  rate := 1/8
 184}
 185
 186/-! ## Surface Codes -/
 187
 188/-- Surface codes are the leading approach for scalable QEC.
 189
 190    - Qubits on a 2D lattice
 191    - Stabilizer measurements on plaquettes
 192    - Error correction via matching
 193
 194    In RS: The 2D structure relates to holographic boundary. -/

depends on (5)

Lean names referenced from this declaration's body.

via in IndisputableMonolith.Derivations.MassToLight decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
EightTickCode in IndisputableMonolith.Information.QuantumErrorCorrection decl_use
measurements in IndisputableMonolith.StandardModel.WeinbergAngle decl_use