Skip to main content

Module functions

oxilean_std::quantum_error_correction

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

amplitude_damping_capacity
Approximate quantum capacity of the amplitude damping channel. Q β‰ˆ 1 - H(Ξ³) for small Ξ³.
app
app2
app3
arrow
bacon_shor_code_ty
BaconShorCode : Nat β†’ Type Bacon-Shor code on an mΓ—m grid: [[mΒ², 1, r, m]] subsystem code.
bacon_shor_single_fault_tolerant_ty
Theorem: BaconShorSingleFaultTolerant The Bacon-Shor code is single-fault-tolerant for adversarial noise.
belief_prop_decoder_ty
BeliefPropDecoder : Nat β†’ Nat β†’ Nat β†’ Type Belief propagation decoder for qLDPC codes.
binary_entropy
Compute the binary entropy H(p) = -p logβ‚‚ p - (1-p) logβ‚‚(1-p).
binomial_code_ty
BinomialCode : Nat β†’ Nat β†’ Type Binomial code [[N, M, d]]_b protecting against d-photon loss/gain errors.
bool_ty
bosonic_code_ty
BosonicCode : Type A quantum code encoding into bosonic (oscillator) modes.
bp_convergence_ldpc_ty
Theorem: BPConvergenceLDPC Belief propagation converges for cycle-free factor graphs (tree-like codes).
bravyi_kitaev_distillation_ty
Theorem: BravyiKitaevDistillation The 15-to-1 distillation protocol asymptotically achieves cubic error suppression.
build_quantum_error_correction_env
bvar
cat_code_loss_tolerance_ty
Theorem: CatCodeLossTolerance S-cat code detects up to S-1 photon losses.
cat_code_ty
CatCode : Nat β†’ Type Cat code with S-fold symmetry protecting against amplitude damping.
circuit_noise_threshold_ty
CircuitNoiseThreshold : NoiseModel β†’ Real The circuit-level noise threshold for a given noise model.
circuit_threshold_theorem_ty
Theorem: CircuitThresholdTheorem For circuit-level noise below threshold, arbitrarily long computations are possible.
classical_code_ty
ClassicalCode : Nat β†’ Nat β†’ Nat β†’ Type [n, k, d] classical linear code over Fβ‚‚.
code_distance_ty
CodeDistance : StabilizerCode n k d β†’ Nat d = min weight of a non-trivial logical operator.
code_switching_ty
CodeSwitching : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Nat β†’ Nat β†’ Type Protocol for switching between two codes [[n1,k,d1]] and [[n2,k,d2]].
coherent_information_ty
CoherentInformation : Type β†’ Type β†’ Real I_c(ρ, N) = S(N(ρ)) βˆ’ S((idβŠ—N)(|ψ⟩⟨ψ|)) (coherent information).
color_code_equivalent_ty
Theorem: ColorCodeEquivalent 2D color codes are equivalent to two copies of toric/surface codes.
color_code_lattice_ty
ColorCodeLattice : Type The trivalent 3-colorable lattice underlying a color code.
color_code_syndrome_ty
ColorCodeSyndrome : Nat β†’ Type Syndrome pattern (vertex/plaquette check violations) for a color code.
color_code_transversal_t_ty
Theorem: ColorCodeTransversalT 2D color codes on 4-8-8 lattice admit a transversal T gate.
color_code_ty
ColorCode : Nat β†’ Type A 2D color code on a 4-8-8 or 6-6-6 lattice with distance d.
commutator_pauli_ty
CommutatorPauli : PauliGroup n β†’ PauliGroup n β†’ Bool Test whether two Paulis commute (true) or anti-commute (false).
concatenated_code_distance_ty
Theorem: ConcatenatedCodeDistance Level-L concatenation of [[n,1,d]] code has distance d^L.
concatenated_code_ty
ConcatenatedCode : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Type [[n,k,d]] code concatenated to level L.
css_code_ty
CSSCode : Nat β†’ Nat β†’ Nat β†’ Type CSS code [[n, k₁+kβ‚‚-n, d]] from two classical codes C₁βŠ₯ βŠ† Cβ‚‚.
css_construction_ty
Theorem: CSSConstruction If C₁βŠ₯ βŠ† Cβ‚‚ then the CSS construction yields a valid quantum code.
css_transversal_cnot_ty
Theorem: CSSTransversalCNOT CSS codes admit a transversal CNOT gate.
css_x_stabilizer_ty
CSSXStabilizer : CSSCode n k d β†’ Type X-type stabilizers from the parity check matrix Hβ‚‚.
css_z_stabilizer_ty
CSSZStabilizer : CSSCode n k d β†’ Type Z-type stabilizers from the parity check matrix H₁.
cst
decoder_map_ty
DecoderMap : Nat β†’ Nat β†’ Type A syndrome decoding map Οƒ ↦ correction ∈ P_n.
decoding_threshold_ty
DecodingThreshold : Type β†’ Real The decoding threshold for a given decoder: physical error rate below which decoding succeeds.
depolarizing_noise_ty
DepolarizingNoise : Real β†’ Type Depolarizing noise channel with uniform error rate p per gate.
distill_t_state_fidelity
T-state fidelity after one round of [[15,1,3]] distillation. Input fidelity F β†’ output fidelity F_out β‰ˆ 1 - 35(1-F)Β³.
distillation_overhead
Overhead (input T-states per output T-state) for k rounds. Each round uses 15 input states to produce 1 output.
distillation_protocol_ty
DistillationProtocol : Nat β†’ Nat β†’ Real β†’ Type A distillation protocol consuming n input magic states to produce k outputs at fidelity F.
distillation_rounds
Number of T-state distillation rounds needed to reach target fidelity.
easttin_knill_theorem_ty
Theorem: EasttinKnillTheorem No quantum code can have a universal set of transversal gates.
erasure_channel_capacity
Quantum capacity of the erasure channel with erasure probability Ξ΅. Q = max(0, 1 - 2Ξ΅).
error_syndrome_ty
ErrorSyndrome : Nat β†’ Nat β†’ Type Syndrome vector in Fβ‚‚^{n-k} from measuring stabilizer generators.
error_threshold_ty
ErrorThreshold : Real The fault-tolerance threshold p_th below which error rates can be suppressed.
fault_tolerance_gadget_ty
FaultToleranceGadget : Nat β†’ Nat β†’ Nat β†’ Type A fault-tolerant implementation gadget satisfying threshold conditions.
fault_tolerance_overhead_ty
FaultToleranceOverhead : Nat β†’ Nat β†’ Real Resource overhead O(polylog(1/Ξ΅)) for error rate Ξ΅ at code distance d.
fault_tolerant_gate_ty
FaultTolerantGate : Nat β†’ Nat β†’ Nat β†’ Type A fault-tolerant implementation of a gate on an [[n,k,d]] code.
fiber_bundle_code_ty
FiberBundleCode : Nat β†’ Nat β†’ Type Fiber bundle LDPC code with linear distance and constant check weight.
fiber_bundle_distance_ty
Theorem: FiberBundleDistance Fiber bundle codes achieve distance Ξ©(n^{3/5}).
gate_synthesis_ty
GateSynthesis : Nat β†’ Real β†’ Type Approximation of a target unitary to precision Ξ΅ using n gates from a fault-tolerant set.
gauge_group_ty
GaugeGroup : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Type Gauge group G of a subsystem code (generated by gauge operators).
gkp_code_ty
GKPCode : Real β†’ Type Gottesman-Kitaev-Preskill code with lattice spacing Ξ” in phase space.
gkp_corrects_bounded_displacement_ty
Theorem: GKPCorrectsBoundedDisplacement GKP code corrects displacement errors with |Ξ±| < Ξ”/2.
gkp_displacement_error_ty
GKPDisplacementError : Real β†’ Real β†’ Type A displacement error D(Ξ±) in phase space acting on a GKP codeword.
good_qldpc_code_ty
GoodQLDPCCode : Nat β†’ Nat β†’ Nat β†’ Prop A good qLDPC code with k = Θ(n) logical qubits and d = Θ(n) distance.
gottesman_knill_theorem_ty
Theorem: GottesmanKnillTheorem Clifford circuits (starting from computational basis) can be classically simulated.
hashing_bound
Hashing bound for the depolarizing channel with error rate p. Q β‰₯ max(0, 1 - H(p) - p logβ‚‚ 3).
hashing_bound_ty
HashingBound : Real β†’ Real Q β‰₯ 1 - H(p) - p logβ‚‚ 3 for depolarizing channel at rate p.
kl_correctable_code_ty
KLCorrectableCode : Nat β†’ Nat β†’ Nat β†’ Type An [[n,k,d]] code satisfying the Knill-Laflamme conditions for a given error set.
kl_degenerate_code_ty
Theorem: KLDegenerateCode A degenerate code can correct errors where C_{ab} is non-scalar; KL still applies.
kl_equivalence_ty
Theorem: KLEquivalence A code is error-correcting for E iff KL necessary and sufficient conditions both hold.
kl_error_set_ty
KLErrorSet : Nat β†’ Type A set of Kraus operators {E_a} for which KL conditions are checked.
kl_matrix_ty
KLMatrix : Nat β†’ Nat β†’ Type The matrix C_{ab} in Knill-Laflamme: ⟨ψ_i|E†a E_b|ψ_j⟩ = C{ab} Ξ΄_{ij}.
kl_necessary_condition_ty
KLNecessaryCondition : KLErrorSet n β†’ StabilizerCode n k d β†’ Prop Necessary KL condition: E†_a E_b must act as a scalar on the code space.
kl_sufficient_condition_ty
KLSufficientCondition : KLErrorSet n β†’ StabilizerCode n k d β†’ Prop Sufficient KL condition: there exists a recovery channel correcting all errors in E.
knill_laflamme_conditions_ty
Theorem: KnillLaflammeConditions Error set E is correctable iff ⟨ψ_i|E†a E_b|ψ_j⟩ = C{ab} Ξ΄_{ij}.
list_ty
logical_operator_ty
LogicalOperator : StabilizerCode n k d β†’ PauliGroup n β†’ Type A logical Pauli operator commuting with all stabilizers but not in S.
magic_state_distillation_works_ty
Theorem: MagicStateDistillationWorks Noisy T-states can be distilled to high-fidelity T-states using Clifford operations.
magic_state_injection_ty
MagicStateInjection : Type Protocol for injecting a T-gate resource state |T⟩ = T|+⟩.
magic_state_non_stabilizer_ty
Theorem: MagicStateNonStabilizer Magic states are not stabilizer states; their Wigner function has negative values.
magic_state_robustness_ty
MagicStateRobustness : Real Robustness of magic: minimum overhead for simulating non-Clifford operations.
magic_state_ty
MagicState : Type A non-stabilizer (magic) resource state enabling non-Clifford gates.
ml_decoder_ty
MLDecoder : Nat β†’ Nat β†’ Nat β†’ Type Maximum-likelihood decoder (optimal but exponential complexity).
mwpm_decoder_ty
MWPMDecoder : Nat β†’ Nat β†’ Nat β†’ Type Minimum-weight perfect matching decoder for [[n,k,d]] stabilizer codes.
mwpm_optimal_surface_ty
Theorem: MWPMOptimalSurface MWPM achieves the optimal threshold for the surface code under independent noise.
nat_ty
no_cloning_capacity_ty
Theorem: NoCloning Q(N) > 0 implies the channel is not entanglement-breaking.
noise_model_ty
NoiseModel : Type A noise model specifying single-qubit, two-qubit, and measurement error rates.
operator_qec_ty
OperatorQEC : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Prop Operator quantum error correction condition for subsystem codes.
pauli_anti_commute_ty
Theorem: PauliAntiCommute XY = iZ, YZ = iX, ZX = iY (Pauli anti-commutation relations).
pauli_group_non_abelian_ty
Theorem: PauliGroupNonAbelian The n-qubit Pauli group is non-abelian for n β‰₯ 1.
pauli_group_ty
PauliGroup : Nat β†’ Type The n-qubit Pauli group P_n = {Β±1,Β±i} Γ— {I,X,Y,Z}^βŠ—n.
pauli_op_ty
PauliOp : Type β€” a single-qubit Pauli operator {I, X, Y, Z}.
pauli_phase_ty
PauliPhase : Type The phase factor ∈ {1, i, -1, -i}.
pauli_square_identity_ty
Theorem: PauliSquareIdentity σ² = I for Οƒ ∈ {X, Y, Z}.
pi
polytope_bound_ty
Theorem: PolytopeBound The threshold p_th satisfies p_th β‰₯ 1/(cΒ·(n-k)^2) for some constant c.
prop
pseudo_threshold_ty
PseudoThreshold : Nat β†’ Nat β†’ Nat β†’ Real Pseudo-threshold for an [[n,k,d]] code.
qldpc_code_ty
QLDPCCode : Nat β†’ Nat β†’ Nat β†’ Type Quantum low-density parity-check code [[n, k, d]] with constant check weight.
qldpc_good_codes_ty
Theorem: QLDPCGoodCodes Good quantum LDPC codes exist with k, d both linear in n.
qldpc_tanner_ty
QLDPCTanner : Nat β†’ Type Tanner graph representation of a qLDPC code.
quantum_capacity_ty
QuantumCapacity : Type β†’ Real Q(N) = max over n,ρ of (1/n) I_c(ρ, N^βŠ—n) (quantum capacity).
quantum_erasure_capacity_ty
QuantumErasureCapacity : Real β†’ Real Q of erasure channel with erasure probability Ξ΅ is max(0, 1-2Ξ΅).
quantum_hamming_bound_ty
Theorem: QuantumHammingBound For a non-degenerate [[n,k,d]] code: 2^k βˆ‘_{j=0}^{t} C(n,j) 3^j ≀ 2^n.
quantum_noise_threshold_ty
Theorem: QuantumNoiseThreshold Depolarizing channel has positive quantum capacity for p < 1/4.
quantum_reed_muller_code_ty
QuantumReedMullerCode : Nat β†’ Nat β†’ Type Quantum Reed-Muller code [[2^m, k, d]] from two RM codes.
quantum_shannon_theorem_ty
Theorem: QuantumShannonTheorem Q(N) = lim_{nβ†’βˆž} (1/n) max_ρ I_c(ρ, N^βŠ—n).
quantum_singleton_bound_ty
Theorem: QuantumSingletonBound For an [[n,k,d]] code: k ≀ n - 4(d-1) (quantum Singleton bound).
real_ty
reed_muller_code_ty
ReedMullerCode : Nat β†’ Nat β†’ Type Classical Reed-Muller code R(r, m) with parameters [2^m, βˆ‘_{i≀r} C(m,i), 2^{m-r}].
rm_code_concatenation_ty
RMCodeConcatenation : Nat β†’ Nat β†’ Nat β†’ Type Concatenated RM code achieving fault-tolerance with transversal gates.
rm_code_distance_ty
Theorem: RMCodeDistance Quantum RM code [[2^m, 1, 2^{m-r}]] has distance 2^{m-r}.
rm_transversal_t_ty
RMTransversalT : Nat β†’ Nat β†’ Prop RM code CSS construction admits transversal T gate for appropriate r, m.
rm_transversal_universal_ty
Theorem: RMTransversalUniversal Concatenating two different RM codes yields a transversally universal gate set.
shor_bit_flip_code_ty
ShorBitFlipCode : Type The 3-qubit bit-flip repetition code (inner code of Shor).
shor_code_ty
ShorCode : Type The 9-qubit Shor code [[9,1,3]]: first quantum error correcting code.
shor_corrects_single_errors_ty
Theorem: ShorCorrectsSingleErrors The Shor code corrects any single-qubit error (X, Y, or Z).
shor_is_css_ty
Theorem: ShorIsCSS The Shor code is a CSS code.
shor_logical_one_ty
ShorLogicalOne : ShorCode β†’ Type |1Μ„βŸ© = (|000βŸ©βˆ’|111⟩)^βŠ—3 / 2^{3/2}.
shor_logical_zero_ty
ShorLogicalZero : ShorCode β†’ Type |0Μ„βŸ© = (|000⟩+|111⟩)^βŠ—3 / 2^{3/2}.
shor_phase_flip_code_ty
ShorPhaseFlipCode : Type The 3-qubit phase-flip repetition code (outer code of Shor).
solovay_kitaev_approx_ty
SolovayKitaevApprox : Real β†’ Nat Solovay-Kitaev theorem: approximation to Ξ΅ requires O(log^c(1/Ξ΅)) gates.
solovay_kitaev_theorem_ty
Theorem: SolovayKitaevTheorem Any single-qubit unitary can be approximated to Ξ΅ using O(log^{3.97}(1/Ξ΅)) Clifford+T gates.
stabilizer_code_ty
StabilizerCode : Nat β†’ Nat β†’ Nat β†’ Type [[n, k, d]] stabilizer code: n physical, k logical, distance d.
stabilizer_group_ty
StabilizerGroup : Nat β†’ Nat β†’ Type Stabilizer group S ≀ P_n with k = n - |generators| logical qubits.
steane_code_ty
SteaneCode : Type The [[7,1,3]] Steane code from the [7,4,3] Hamming code.
steane_corrects_single_errors_ty
Theorem: SteaneCorrectsSingleErrors The Steane [[7,1,3]] code corrects all single-qubit errors.
steane_h_matrix_ty
SteaneHMatrix : Type Parity check matrix H of the classical [7,4,3] Hamming code.
steane_is_css_ty
Theorem: SteaneIsCSS The Steane code is a CSS code derived from the Hamming code.
steane_stabilizer_ty
SteaneStabilizer : SteaneCode β†’ Nat β†’ Type The i-th stabilizer generator (i = 1..6).
steane_transversal_clifford_ty
Theorem: SteaneTransversalClifford The Steane code has transversal H, S, and CNOT gates.
subsystem_code_correction_ty
Theorem: SubsystemCodeCorrection A subsystem code corrects E iff the operator QEC conditions hold for gauge-reduced errors.
subsystem_code_ty
SubsystemCode : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Type [[n, k, r, d]] subsystem (operator) code with k logical and r gauge qubits.
surface_code_distance_ty
Theorem: SurfaceCodeDistance The surface code [[dΒ², 1, d]] has code distance d (minimum weight logical).
surface_code_logical_ty
SurfaceCodeLogical : Nat β†’ Type Logical X and Z operators as homologically non-trivial paths on the lattice.
surface_code_plaquette_ty
SurfaceCodePlaquette : Nat β†’ Type Plaquette operators B_p = ∏_{e∈p} Z_e for the surface code.
surface_code_threshold_ty
Theorem: SurfaceCodeThreshold Surface code has a fault-tolerance threshold ~1% under local noise.
surface_code_ty
SurfaceCode : Nat β†’ Type Distance-d surface code [[dΒ², 1, d]] on a dΓ—d planar lattice.
surface_code_vertex_ty
SurfaceCodeVertex : Nat β†’ Type Vertex (star) operators A_v = ∏_{e∈v} X_e for the surface code.
symplectic_representation_ty
SymplecticRepresentation : Nat β†’ Type Symplectic representation of an n-qubit Pauli over F₂²ⁿ.
t_count_optimality_ty
Theorem: TCountOptimality Minimizing T-count in Clifford+T circuits is #P-hard in general.
t_state_ty
TState : Type The T-gate magic state |T⟩ = T|+⟩ = (|0⟩ + e^{iΟ€/4}|1⟩)/√2.
teleported_gate_ty
TeleportedGate : Type Gate teleportation using ancilla resource states.
threshold_theorem_ty
Theorem: ThresholdTheorem If physical error rate p < p_th then logical error rate can be made arbitrarily small.
threshold_upper_bound_ty
Theorem: ThresholdUpperBound No fault-tolerance threshold exists above 50% for arbitrary noise models.
toric_code_anyons_ty
Theorem: ToricCodeAnyons Excitations of toric code are Abelian anyons (e and m particles).
toric_code_ty
ToricCode : Nat β†’ Type Distance-d toric code [[2dΒ², 2, d]] on a torus (Kitaev’s toric code).
transversal_clifford_css_ty
Theorem: TransversalCliffordCSS CSS codes admit transversal Clifford gates.
transversal_gate_ty
TransversalGate : Type A gate applied independently to each physical qubit in the code block.
type0
union_find_decoder_ty
UnionFindDecoder : Nat β†’ Type Union-find decoder achieving near-linear decoding time.
weight_pauli_ty
WeightPauli : PauliGroup n β†’ Nat Number of non-identity tensor factors (Hamming weight).