oxilean_std/quantum_error_correction/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6
7use super::types::{
8    CSSCode, ConcatenatedCode, FaultToleranceThreshold, GKPCodeSimulator, MagicStateDistillation,
9    MagicStateProtocol, PauliOp, PauliOperator, PauliString, QECNormChecker, QuantumLDPC, ShorCode,
10    StabCode, StabilizerCode, StabilizerSimulator, SurfaceCode, SurfaceCodeDecoder,
11    SyndromeDecoder2, ThresholdEstimator,
12};
13
14pub fn app(f: Expr, a: Expr) -> Expr {
15    Expr::App(Box::new(f), Box::new(a))
16}
17pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
18    app(app(f, a), b)
19}
20pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
21    app(app2(f, a, b), c)
22}
23pub fn cst(s: &str) -> Expr {
24    Expr::Const(Name::str(s), vec![])
25}
26pub fn prop() -> Expr {
27    Expr::Sort(Level::zero())
28}
29pub fn type0() -> Expr {
30    Expr::Sort(Level::succ(Level::zero()))
31}
32pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
33    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
34}
35pub fn arrow(a: Expr, b: Expr) -> Expr {
36    pi(BinderInfo::Default, "_", a, b)
37}
38pub fn bvar(n: u32) -> Expr {
39    Expr::BVar(n)
40}
41pub fn nat_ty() -> Expr {
42    cst("Nat")
43}
44pub fn real_ty() -> Expr {
45    cst("Real")
46}
47pub fn bool_ty() -> Expr {
48    cst("Bool")
49}
50pub fn list_ty(elem: Expr) -> Expr {
51    app(cst("List"), elem)
52}
53/// `PauliOp : Type` — a single-qubit Pauli operator {I, X, Y, Z}.
54pub fn pauli_op_ty() -> Expr {
55    type0()
56}
57/// `PauliGroup : Nat → Type`
58/// The n-qubit Pauli group P_n = {±1,±i} × {I,X,Y,Z}^⊗n.
59pub fn pauli_group_ty() -> Expr {
60    arrow(nat_ty(), type0())
61}
62/// `PauliPhase : Type`
63/// The phase factor ∈ {1, i, -1, -i}.
64pub fn pauli_phase_ty() -> Expr {
65    type0()
66}
67/// `SymplecticRepresentation : Nat → Type`
68/// Symplectic representation of an n-qubit Pauli over F₂²ⁿ.
69pub fn symplectic_representation_ty() -> Expr {
70    arrow(nat_ty(), type0())
71}
72/// `CommutatorPauli : PauliGroup n → PauliGroup n → Bool`
73/// Test whether two Paulis commute (true) or anti-commute (false).
74pub fn commutator_pauli_ty() -> Expr {
75    arrow(
76        app(cst("PauliGroup"), nat_ty()),
77        arrow(app(cst("PauliGroup"), nat_ty()), bool_ty()),
78    )
79}
80/// `WeightPauli : PauliGroup n → Nat`
81/// Number of non-identity tensor factors (Hamming weight).
82pub fn weight_pauli_ty() -> Expr {
83    arrow(app(cst("PauliGroup"), nat_ty()), nat_ty())
84}
85/// Theorem: `PauliGroupNonAbelian`
86/// The n-qubit Pauli group is non-abelian for n ≥ 1.
87pub fn pauli_group_non_abelian_ty() -> Expr {
88    prop()
89}
90/// Theorem: `PauliSquareIdentity`
91/// σ² = I for σ ∈ {X, Y, Z}.
92pub fn pauli_square_identity_ty() -> Expr {
93    prop()
94}
95/// Theorem: `PauliAntiCommute`
96/// XY = iZ, YZ = iX, ZX = iY (Pauli anti-commutation relations).
97pub fn pauli_anti_commute_ty() -> Expr {
98    prop()
99}
100/// `StabilizerGroup : Nat → Nat → Type`
101/// Stabilizer group S ≤ P_n with k = n - |generators| logical qubits.
102pub fn stabilizer_group_ty() -> Expr {
103    arrow(nat_ty(), arrow(nat_ty(), type0()))
104}
105/// `StabilizerCode : Nat → Nat → Nat → Type`
106/// [[n, k, d]] stabilizer code: n physical, k logical, distance d.
107pub fn stabilizer_code_ty() -> Expr {
108    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
109}
110/// `ErrorSyndrome : Nat → Nat → Type`
111/// Syndrome vector in F₂^{n-k} from measuring stabilizer generators.
112pub fn error_syndrome_ty() -> Expr {
113    arrow(nat_ty(), arrow(nat_ty(), type0()))
114}
115/// `LogicalOperator : StabilizerCode n k d → PauliGroup n → Type`
116/// A logical Pauli operator commuting with all stabilizers but not in S.
117pub fn logical_operator_ty() -> Expr {
118    arrow(
119        app3(cst("StabilizerCode"), nat_ty(), nat_ty(), nat_ty()),
120        arrow(app(cst("PauliGroup"), nat_ty()), type0()),
121    )
122}
123/// `DecoderMap : Nat → Nat → Type`
124/// A syndrome decoding map σ ↦ correction ∈ P_n.
125pub fn decoder_map_ty() -> Expr {
126    arrow(nat_ty(), arrow(nat_ty(), type0()))
127}
128/// `CodeDistance : StabilizerCode n k d → Nat`
129/// d = min weight of a non-trivial logical operator.
130pub fn code_distance_ty() -> Expr {
131    arrow(
132        app3(cst("StabilizerCode"), nat_ty(), nat_ty(), nat_ty()),
133        nat_ty(),
134    )
135}
136/// Theorem: `KnillLaflammeConditions`
137/// Error set E is correctable iff ⟨ψ_i|E†_a E_b|ψ_j⟩ = C_{ab} δ_{ij}.
138pub fn knill_laflamme_conditions_ty() -> Expr {
139    prop()
140}
141/// Theorem: `QuantumSingletonBound`
142/// For an [[n,k,d]] code: k ≤ n - 4(d-1) (quantum Singleton bound).
143pub fn quantum_singleton_bound_ty() -> Expr {
144    prop()
145}
146/// Theorem: `QuantumHammingBound`
147/// For a non-degenerate [[n,k,d]] code: 2^k ∑_{j=0}^{t} C(n,j) 3^j ≤ 2^n.
148pub fn quantum_hamming_bound_ty() -> Expr {
149    prop()
150}
151/// Theorem: `GottesmanKnillTheorem`
152/// Clifford circuits (starting from computational basis) can be classically simulated.
153pub fn gottesman_knill_theorem_ty() -> Expr {
154    prop()
155}
156/// `ClassicalCode : Nat → Nat → Nat → Type`
157/// [n, k, d] classical linear code over F₂.
158pub fn classical_code_ty() -> Expr {
159    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
160}
161/// `CSSCode : Nat → Nat → Nat → Type`
162/// CSS code [[n, k₁+k₂-n, d]] from two classical codes C₁⊥ ⊆ C₂.
163pub fn css_code_ty() -> Expr {
164    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
165}
166/// `CSSXStabilizer : CSSCode n k d → Type`
167/// X-type stabilizers from the parity check matrix H₂.
168pub fn css_x_stabilizer_ty() -> Expr {
169    arrow(app3(cst("CSSCode"), nat_ty(), nat_ty(), nat_ty()), type0())
170}
171/// `CSSZStabilizer : CSSCode n k d → Type`
172/// Z-type stabilizers from the parity check matrix H₁.
173pub fn css_z_stabilizer_ty() -> Expr {
174    arrow(app3(cst("CSSCode"), nat_ty(), nat_ty(), nat_ty()), type0())
175}
176/// Theorem: `CSSConstruction`
177/// If C₁⊥ ⊆ C₂ then the CSS construction yields a valid quantum code.
178pub fn css_construction_ty() -> Expr {
179    prop()
180}
181/// Theorem: `CSSTransversalCNOT`
182/// CSS codes admit a transversal CNOT gate.
183pub fn css_transversal_cnot_ty() -> Expr {
184    prop()
185}
186/// `ShorCode : Type`
187/// The 9-qubit Shor code [[9,1,3]]: first quantum error correcting code.
188pub fn shor_code_ty() -> Expr {
189    type0()
190}
191/// `ShorLogicalZero : ShorCode → Type`
192/// |0̄⟩ = (|000⟩+|111⟩)^⊗3 / 2^{3/2}.
193pub fn shor_logical_zero_ty() -> Expr {
194    arrow(cst("ShorCode"), type0())
195}
196/// `ShorLogicalOne : ShorCode → Type`
197/// |1̄⟩ = (|000⟩−|111⟩)^⊗3 / 2^{3/2}.
198pub fn shor_logical_one_ty() -> Expr {
199    arrow(cst("ShorCode"), type0())
200}
201/// `ShorBitFlipCode : Type`
202/// The 3-qubit bit-flip repetition code (inner code of Shor).
203pub fn shor_bit_flip_code_ty() -> Expr {
204    type0()
205}
206/// `ShorPhaseFlipCode : Type`
207/// The 3-qubit phase-flip repetition code (outer code of Shor).
208pub fn shor_phase_flip_code_ty() -> Expr {
209    type0()
210}
211/// Theorem: `ShorCorrectsSingleErrors`
212/// The Shor code corrects any single-qubit error (X, Y, or Z).
213pub fn shor_corrects_single_errors_ty() -> Expr {
214    prop()
215}
216/// Theorem: `ShorIsCSS`
217/// The Shor code is a CSS code.
218pub fn shor_is_css_ty() -> Expr {
219    prop()
220}
221/// `SteaneCode : Type`
222/// The [[7,1,3]] Steane code from the [7,4,3] Hamming code.
223pub fn steane_code_ty() -> Expr {
224    type0()
225}
226/// `SteaneHMatrix : Type`
227/// Parity check matrix H of the classical [7,4,3] Hamming code.
228pub fn steane_h_matrix_ty() -> Expr {
229    type0()
230}
231/// `SteaneStabilizer : SteaneCode → Nat → Type`
232/// The i-th stabilizer generator (i = 1..6).
233pub fn steane_stabilizer_ty() -> Expr {
234    arrow(cst("SteaneCode"), arrow(nat_ty(), type0()))
235}
236/// Theorem: `SteaneCorrectsSingleErrors`
237/// The Steane [[7,1,3]] code corrects all single-qubit errors.
238pub fn steane_corrects_single_errors_ty() -> Expr {
239    prop()
240}
241/// Theorem: `SteaneTransversalClifford`
242/// The Steane code has transversal H, S, and CNOT gates.
243pub fn steane_transversal_clifford_ty() -> Expr {
244    prop()
245}
246/// Theorem: `SteaneIsCSS`
247/// The Steane code is a CSS code derived from the Hamming code.
248pub fn steane_is_css_ty() -> Expr {
249    prop()
250}
251/// `FaultTolerantGate : Nat → Nat → Nat → Type`
252/// A fault-tolerant implementation of a gate on an [[n,k,d]] code.
253pub fn fault_tolerant_gate_ty() -> Expr {
254    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
255}
256/// `TransversalGate : Type`
257/// A gate applied independently to each physical qubit in the code block.
258pub fn transversal_gate_ty() -> Expr {
259    type0()
260}
261/// `MagicStateInjection : Type`
262/// Protocol for injecting a T-gate resource state |T⟩ = T|+⟩.
263pub fn magic_state_injection_ty() -> Expr {
264    type0()
265}
266/// `TeleportedGate : Type`
267/// Gate teleportation using ancilla resource states.
268pub fn teleported_gate_ty() -> Expr {
269    type0()
270}
271/// Theorem: `EasttinKnillTheorem`
272/// No quantum code can have a universal set of transversal gates.
273pub fn easttin_knill_theorem_ty() -> Expr {
274    prop()
275}
276/// Theorem: `TransversalCliffordCSS`
277/// CSS codes admit transversal Clifford gates.
278pub fn transversal_clifford_css_ty() -> Expr {
279    prop()
280}
281/// Theorem: `MagicStateDistillationWorks`
282/// Noisy T-states can be distilled to high-fidelity T-states using Clifford operations.
283pub fn magic_state_distillation_works_ty() -> Expr {
284    prop()
285}
286/// `ErrorThreshold : Real`
287/// The fault-tolerance threshold p_th below which error rates can be suppressed.
288pub fn error_threshold_ty() -> Expr {
289    real_ty()
290}
291/// `ConcatenatedCode : Nat → Nat → Nat → Nat → Type`
292/// [[n,k,d]] code concatenated to level L.
293pub fn concatenated_code_ty() -> Expr {
294    arrow(
295        nat_ty(),
296        arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0()))),
297    )
298}
299/// `FaultToleranceOverhead : Nat → Nat → Real`
300/// Resource overhead O(polylog(1/ε)) for error rate ε at code distance d.
301pub fn fault_tolerance_overhead_ty() -> Expr {
302    arrow(nat_ty(), arrow(nat_ty(), real_ty()))
303}
304/// `PseudoThreshold : Nat → Nat → Nat → Real`
305/// Pseudo-threshold for an [[n,k,d]] code.
306pub fn pseudo_threshold_ty() -> Expr {
307    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), real_ty())))
308}
309/// Theorem: `ThresholdTheorem`
310/// If physical error rate p < p_th then logical error rate can be made arbitrarily small.
311pub fn threshold_theorem_ty() -> Expr {
312    prop()
313}
314/// Theorem: `ConcatenatedCodeDistance`
315/// Level-L concatenation of [[n,1,d]] code has distance d^L.
316pub fn concatenated_code_distance_ty() -> Expr {
317    prop()
318}
319/// Theorem: `PolytopeBound`
320/// The threshold p_th satisfies p_th ≥ 1/(c·(n-k)^2) for some constant c.
321pub fn polytope_bound_ty() -> Expr {
322    prop()
323}
324/// `ColorCode : Nat → Type`
325/// A 2D color code on a 4-8-8 or 6-6-6 lattice with distance d.
326pub fn color_code_ty() -> Expr {
327    arrow(nat_ty(), type0())
328}
329/// `ColorCodeLattice : Type`
330/// The trivalent 3-colorable lattice underlying a color code.
331pub fn color_code_lattice_ty() -> Expr {
332    type0()
333}
334/// `ColorCodeSyndrome : Nat → Type`
335/// Syndrome pattern (vertex/plaquette check violations) for a color code.
336pub fn color_code_syndrome_ty() -> Expr {
337    arrow(nat_ty(), type0())
338}
339/// Theorem: `ColorCodeTransversalT`
340/// 2D color codes on 4-8-8 lattice admit a transversal T gate.
341pub fn color_code_transversal_t_ty() -> Expr {
342    prop()
343}
344/// Theorem: `ColorCodeEquivalent`
345/// 2D color codes are equivalent to two copies of toric/surface codes.
346pub fn color_code_equivalent_ty() -> Expr {
347    prop()
348}
349/// `QuantumCapacity : Type → Real`
350/// Q(N) = max over n,ρ of (1/n) I_c(ρ, N^⊗n) (quantum capacity).
351pub fn quantum_capacity_ty() -> Expr {
352    arrow(type0(), real_ty())
353}
354/// `CoherentInformation : Type → Type → Real`
355/// I_c(ρ, N) = S(N(ρ)) − S((id⊗N)(|ψ⟩⟨ψ|)) (coherent information).
356pub fn coherent_information_ty() -> Expr {
357    arrow(type0(), arrow(type0(), real_ty()))
358}
359/// `HashingBound : Real → Real`
360/// Q ≥ 1 - H(p) - p log₂ 3 for depolarizing channel at rate p.
361pub fn hashing_bound_ty() -> Expr {
362    arrow(real_ty(), real_ty())
363}
364/// `QuantumErasureCapacity : Real → Real`
365/// Q of erasure channel with erasure probability ε is max(0, 1-2ε).
366pub fn quantum_erasure_capacity_ty() -> Expr {
367    arrow(real_ty(), real_ty())
368}
369/// Theorem: `QuantumNoiseThreshold`
370/// Depolarizing channel has positive quantum capacity for p < 1/4.
371pub fn quantum_noise_threshold_ty() -> Expr {
372    prop()
373}
374/// Theorem: `QuantumShannonTheorem`
375/// Q(N) = lim_{n→∞} (1/n) max_ρ I_c(ρ, N^⊗n).
376pub fn quantum_shannon_theorem_ty() -> Expr {
377    prop()
378}
379/// Theorem: `NoCloning`
380/// Q(N) > 0 implies the channel is not entanglement-breaking.
381pub fn no_cloning_capacity_ty() -> Expr {
382    prop()
383}
384/// `KLMatrix : Nat → Nat → Type`
385/// The matrix C_{ab} in Knill-Laflamme: ⟨ψ_i|E†_a E_b|ψ_j⟩ = C_{ab} δ_{ij}.
386pub fn kl_matrix_ty() -> Expr {
387    arrow(nat_ty(), arrow(nat_ty(), type0()))
388}
389/// `KLErrorSet : Nat → Type`
390/// A set of Kraus operators {E_a} for which KL conditions are checked.
391pub fn kl_error_set_ty() -> Expr {
392    arrow(nat_ty(), type0())
393}
394/// `KLCorrectableCode : Nat → Nat → Nat → Type`
395/// An [[n,k,d]] code satisfying the Knill-Laflamme conditions for a given error set.
396pub fn kl_correctable_code_ty() -> Expr {
397    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
398}
399/// `KLNecessaryCondition : KLErrorSet n → StabilizerCode n k d → Prop`
400/// Necessary KL condition: E†_a E_b must act as a scalar on the code space.
401pub fn kl_necessary_condition_ty() -> Expr {
402    arrow(
403        app(cst("KLErrorSet"), nat_ty()),
404        arrow(
405            app3(cst("StabilizerCode"), nat_ty(), nat_ty(), nat_ty()),
406            prop(),
407        ),
408    )
409}
410/// `KLSufficientCondition : KLErrorSet n → StabilizerCode n k d → Prop`
411/// Sufficient KL condition: there exists a recovery channel correcting all errors in E.
412pub fn kl_sufficient_condition_ty() -> Expr {
413    arrow(
414        app(cst("KLErrorSet"), nat_ty()),
415        arrow(
416            app3(cst("StabilizerCode"), nat_ty(), nat_ty(), nat_ty()),
417            prop(),
418        ),
419    )
420}
421/// Theorem: `KLEquivalence`
422/// A code is error-correcting for E iff KL necessary and sufficient conditions both hold.
423pub fn kl_equivalence_ty() -> Expr {
424    prop()
425}
426/// Theorem: `KLDegenerateCode`
427/// A degenerate code can correct errors where C_{ab} is non-scalar; KL still applies.
428pub fn kl_degenerate_code_ty() -> Expr {
429    prop()
430}
431/// `ReedMullerCode : Nat → Nat → Type`
432/// Classical Reed-Muller code R(r, m) with parameters [2^m, ∑_{i≤r} C(m,i), 2^{m-r}].
433pub fn reed_muller_code_ty() -> Expr {
434    arrow(nat_ty(), arrow(nat_ty(), type0()))
435}
436/// `QuantumReedMullerCode : Nat → Nat → Type`
437/// Quantum Reed-Muller code [[2^m, k, d]] from two RM codes.
438pub fn quantum_reed_muller_code_ty() -> Expr {
439    arrow(nat_ty(), arrow(nat_ty(), type0()))
440}
441/// `RMTransversalT : Nat → Nat → Prop`
442/// RM code CSS construction admits transversal T gate for appropriate r, m.
443pub fn rm_transversal_t_ty() -> Expr {
444    arrow(nat_ty(), arrow(nat_ty(), prop()))
445}
446/// `RMCodeConcatenation : Nat → Nat → Nat → Type`
447/// Concatenated RM code achieving fault-tolerance with transversal gates.
448pub fn rm_code_concatenation_ty() -> Expr {
449    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
450}
451/// Theorem: `RMTransversalUniversal`
452/// Concatenating two different RM codes yields a transversally universal gate set.
453pub fn rm_transversal_universal_ty() -> Expr {
454    prop()
455}
456/// Theorem: `RMCodeDistance`
457/// Quantum RM code [[2^m, 1, 2^{m-r}]] has distance 2^{m-r}.
458pub fn rm_code_distance_ty() -> Expr {
459    prop()
460}
461/// `SurfaceCode : Nat → Type`
462/// Distance-d surface code [[d², 1, d]] on a d×d planar lattice.
463pub fn surface_code_ty() -> Expr {
464    arrow(nat_ty(), type0())
465}
466/// `ToricCode : Nat → Type`
467/// Distance-d toric code [[2d², 2, d]] on a torus (Kitaev's toric code).
468pub fn toric_code_ty() -> Expr {
469    arrow(nat_ty(), type0())
470}
471/// `SurfaceCodeVertex : Nat → Type`
472/// Vertex (star) operators A_v = ∏_{e∈v} X_e for the surface code.
473pub fn surface_code_vertex_ty() -> Expr {
474    arrow(nat_ty(), type0())
475}
476/// `SurfaceCodePlaquette : Nat → Type`
477/// Plaquette operators B_p = ∏_{e∈p} Z_e for the surface code.
478pub fn surface_code_plaquette_ty() -> Expr {
479    arrow(nat_ty(), type0())
480}
481/// `SurfaceCodeLogical : Nat → Type`
482/// Logical X and Z operators as homologically non-trivial paths on the lattice.
483pub fn surface_code_logical_ty() -> Expr {
484    arrow(nat_ty(), type0())
485}
486/// Theorem: `SurfaceCodeDistance`
487/// The surface code [[d², 1, d]] has code distance d (minimum weight logical).
488pub fn surface_code_distance_ty() -> Expr {
489    prop()
490}
491/// Theorem: `ToricCodeAnyons`
492/// Excitations of toric code are Abelian anyons (e and m particles).
493pub fn toric_code_anyons_ty() -> Expr {
494    prop()
495}
496/// Theorem: `SurfaceCodeThreshold`
497/// Surface code has a fault-tolerance threshold ~1% under local noise.
498pub fn surface_code_threshold_ty() -> Expr {
499    prop()
500}
501/// `QLDPCCode : Nat → Nat → Nat → Type`
502/// Quantum low-density parity-check code [[n, k, d]] with constant check weight.
503pub fn qldpc_code_ty() -> Expr {
504    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
505}
506/// `FiberBundleCode : Nat → Nat → Type`
507/// Fiber bundle LDPC code with linear distance and constant check weight.
508pub fn fiber_bundle_code_ty() -> Expr {
509    arrow(nat_ty(), arrow(nat_ty(), type0()))
510}
511/// `GoodQLDPCCode : Nat → Nat → Nat → Prop`
512/// A good qLDPC code with k = Θ(n) logical qubits and d = Θ(n) distance.
513pub fn good_qldpc_code_ty() -> Expr {
514    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
515}
516/// `QLDPCTanner : Nat → Type`
517/// Tanner graph representation of a qLDPC code.
518pub fn qldpc_tanner_ty() -> Expr {
519    arrow(nat_ty(), type0())
520}
521/// Theorem: `QLDPCGoodCodes`
522/// Good quantum LDPC codes exist with k, d both linear in n.
523pub fn qldpc_good_codes_ty() -> Expr {
524    prop()
525}
526/// Theorem: `FiberBundleDistance`
527/// Fiber bundle codes achieve distance Ω(n^{3/5}).
528pub fn fiber_bundle_distance_ty() -> Expr {
529    prop()
530}
531/// `BosonicCode : Type`
532/// A quantum code encoding into bosonic (oscillator) modes.
533pub fn bosonic_code_ty() -> Expr {
534    type0()
535}
536/// `CatCode : Nat → Type`
537/// Cat code with S-fold symmetry protecting against amplitude damping.
538pub fn cat_code_ty() -> Expr {
539    arrow(nat_ty(), type0())
540}
541/// `GKPCode : Real → Type`
542/// Gottesman-Kitaev-Preskill code with lattice spacing Δ in phase space.
543pub fn gkp_code_ty() -> Expr {
544    arrow(real_ty(), type0())
545}
546/// `BinomialCode : Nat → Nat → Type`
547/// Binomial code [[N, M, d]]_b protecting against d-photon loss/gain errors.
548pub fn binomial_code_ty() -> Expr {
549    arrow(nat_ty(), arrow(nat_ty(), type0()))
550}
551/// `GKPDisplacementError : Real → Real → Type`
552/// A displacement error D(α) in phase space acting on a GKP codeword.
553pub fn gkp_displacement_error_ty() -> Expr {
554    arrow(real_ty(), arrow(real_ty(), type0()))
555}
556/// Theorem: `GKPCorrectsBoundedDisplacement`
557/// GKP code corrects displacement errors with |α| < Δ/2.
558pub fn gkp_corrects_bounded_displacement_ty() -> Expr {
559    prop()
560}
561/// Theorem: `CatCodeLossTolerance`
562/// S-cat code detects up to S-1 photon losses.
563pub fn cat_code_loss_tolerance_ty() -> Expr {
564    prop()
565}
566/// `NoiseModel : Type`
567/// A noise model specifying single-qubit, two-qubit, and measurement error rates.
568pub fn noise_model_ty() -> Expr {
569    type0()
570}
571/// `DepolarizingNoise : Real → Type`
572/// Depolarizing noise channel with uniform error rate p per gate.
573pub fn depolarizing_noise_ty() -> Expr {
574    arrow(real_ty(), type0())
575}
576/// `CircuitNoiseThreshold : NoiseModel → Real`
577/// The circuit-level noise threshold for a given noise model.
578pub fn circuit_noise_threshold_ty() -> Expr {
579    arrow(cst("NoiseModel"), real_ty())
580}
581/// `FaultToleranceGadget : Nat → Nat → Nat → Type`
582/// A fault-tolerant implementation gadget satisfying threshold conditions.
583pub fn fault_tolerance_gadget_ty() -> Expr {
584    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
585}
586/// Theorem: `CircuitThresholdTheorem`
587/// For circuit-level noise below threshold, arbitrarily long computations are possible.
588pub fn circuit_threshold_theorem_ty() -> Expr {
589    prop()
590}
591/// Theorem: `ThresholdUpperBound`
592/// No fault-tolerance threshold exists above 50% for arbitrary noise models.
593pub fn threshold_upper_bound_ty() -> Expr {
594    prop()
595}
596/// `MagicState : Type`
597/// A non-stabilizer (magic) resource state enabling non-Clifford gates.
598pub fn magic_state_ty() -> Expr {
599    type0()
600}
601/// `TState : Type`
602/// The T-gate magic state |T⟩ = T|+⟩ = (|0⟩ + e^{iπ/4}|1⟩)/√2.
603pub fn t_state_ty() -> Expr {
604    type0()
605}
606/// `DistillationProtocol : Nat → Nat → Real → Type`
607/// A distillation protocol consuming n input magic states to produce k outputs at fidelity F.
608pub fn distillation_protocol_ty() -> Expr {
609    arrow(nat_ty(), arrow(nat_ty(), arrow(real_ty(), type0())))
610}
611/// `MagicStateRobustness : Real`
612/// Robustness of magic: minimum overhead for simulating non-Clifford operations.
613pub fn magic_state_robustness_ty() -> Expr {
614    real_ty()
615}
616/// Theorem: `BravyiKitaevDistillation`
617/// The 15-to-1 distillation protocol asymptotically achieves cubic error suppression.
618pub fn bravyi_kitaev_distillation_ty() -> Expr {
619    prop()
620}
621/// Theorem: `MagicStateNonStabilizer`
622/// Magic states are not stabilizer states; their Wigner function has negative values.
623pub fn magic_state_non_stabilizer_ty() -> Expr {
624    prop()
625}
626/// `MWPMDecoder : Nat → Nat → Nat → Type`
627/// Minimum-weight perfect matching decoder for [[n,k,d]] stabilizer codes.
628pub fn mwpm_decoder_ty() -> Expr {
629    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
630}
631/// `BeliefPropDecoder : Nat → Nat → Nat → Type`
632/// Belief propagation decoder for qLDPC codes.
633pub fn belief_prop_decoder_ty() -> Expr {
634    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
635}
636/// `UnionFindDecoder : Nat → Type`
637/// Union-find decoder achieving near-linear decoding time.
638pub fn union_find_decoder_ty() -> Expr {
639    arrow(nat_ty(), type0())
640}
641/// `MLDecoder : Nat → Nat → Nat → Type`
642/// Maximum-likelihood decoder (optimal but exponential complexity).
643pub fn ml_decoder_ty() -> Expr {
644    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
645}
646/// `DecodingThreshold : Type → Real`
647/// The decoding threshold for a given decoder: physical error rate below which decoding succeeds.
648pub fn decoding_threshold_ty() -> Expr {
649    arrow(type0(), real_ty())
650}
651/// Theorem: `MWPMOptimalSurface`
652/// MWPM achieves the optimal threshold for the surface code under independent noise.
653pub fn mwpm_optimal_surface_ty() -> Expr {
654    prop()
655}
656/// Theorem: `BPConvergenceLDPC`
657/// Belief propagation converges for cycle-free factor graphs (tree-like codes).
658pub fn bp_convergence_ldpc_ty() -> Expr {
659    prop()
660}
661/// `SubsystemCode : Nat → Nat → Nat → Nat → Type`
662/// [[n, k, r, d]] subsystem (operator) code with k logical and r gauge qubits.
663pub fn subsystem_code_ty() -> Expr {
664    arrow(
665        nat_ty(),
666        arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0()))),
667    )
668}
669/// `GaugeGroup : Nat → Nat → Nat → Nat → Type`
670/// Gauge group G of a subsystem code (generated by gauge operators).
671pub fn gauge_group_ty() -> Expr {
672    arrow(
673        nat_ty(),
674        arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0()))),
675    )
676}
677/// `BaconShorCode : Nat → Type`
678/// Bacon-Shor code on an m×m grid: [[m², 1, r, m]] subsystem code.
679pub fn bacon_shor_code_ty() -> Expr {
680    arrow(nat_ty(), type0())
681}
682/// `OperatorQEC : Nat → Nat → Nat → Nat → Prop`
683/// Operator quantum error correction condition for subsystem codes.
684pub fn operator_qec_ty() -> Expr {
685    arrow(
686        nat_ty(),
687        arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop()))),
688    )
689}
690/// Theorem: `SubsystemCodeCorrection`
691/// A subsystem code corrects E iff the operator QEC conditions hold for gauge-reduced errors.
692pub fn subsystem_code_correction_ty() -> Expr {
693    prop()
694}
695/// Theorem: `BaconShorSingleFaultTolerant`
696/// The Bacon-Shor code is single-fault-tolerant for adversarial noise.
697pub fn bacon_shor_single_fault_tolerant_ty() -> Expr {
698    prop()
699}
700/// `CodeSwitching : Nat → Nat → Nat → Nat → Nat → Nat → Type`
701/// Protocol for switching between two codes [[n1,k,d1]] and [[n2,k,d2]].
702pub fn code_switching_ty() -> Expr {
703    arrow(
704        nat_ty(),
705        arrow(
706            nat_ty(),
707            arrow(
708                nat_ty(),
709                arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0()))),
710            ),
711        ),
712    )
713}
714/// `GateSynthesis : Nat → Real → Type`
715/// Approximation of a target unitary to precision ε using n gates from a fault-tolerant set.
716pub fn gate_synthesis_ty() -> Expr {
717    arrow(nat_ty(), arrow(real_ty(), type0()))
718}
719/// `SolovayKitaevApprox : Real → Nat`
720/// Solovay-Kitaev theorem: approximation to ε requires O(log^c(1/ε)) gates.
721pub fn solovay_kitaev_approx_ty() -> Expr {
722    arrow(real_ty(), nat_ty())
723}
724/// Theorem: `SolovayKitaevTheorem`
725/// Any single-qubit unitary can be approximated to ε using O(log^{3.97}(1/ε)) Clifford+T gates.
726pub fn solovay_kitaev_theorem_ty() -> Expr {
727    prop()
728}
729/// Theorem: `TCountOptimality`
730/// Minimizing T-count in Clifford+T circuits is #P-hard in general.
731pub fn t_count_optimality_ty() -> Expr {
732    prop()
733}
734#[allow(clippy::too_many_arguments)]
735pub fn build_quantum_error_correction_env(env: &mut Environment) -> Result<(), String> {
736    let axioms: &[(&str, Expr)] = &[
737        ("PauliOp", pauli_op_ty()),
738        ("PauliGroup", pauli_group_ty()),
739        ("PauliPhase", pauli_phase_ty()),
740        ("SymplecticRepresentation", symplectic_representation_ty()),
741        ("CommutatorPauli", commutator_pauli_ty()),
742        ("WeightPauli", weight_pauli_ty()),
743        ("PauliGroupNonAbelian", pauli_group_non_abelian_ty()),
744        ("PauliSquareIdentity", pauli_square_identity_ty()),
745        ("PauliAntiCommute", pauli_anti_commute_ty()),
746        ("StabilizerGroup", stabilizer_group_ty()),
747        ("StabilizerCode", stabilizer_code_ty()),
748        ("ErrorSyndrome", error_syndrome_ty()),
749        ("LogicalOperator", logical_operator_ty()),
750        ("DecoderMap", decoder_map_ty()),
751        ("CodeDistance", code_distance_ty()),
752        ("KnillLaflammeConditions", knill_laflamme_conditions_ty()),
753        ("QuantumSingletonBound", quantum_singleton_bound_ty()),
754        ("QuantumHammingBound", quantum_hamming_bound_ty()),
755        ("GottesmanKnillTheorem", gottesman_knill_theorem_ty()),
756        ("ClassicalCode", classical_code_ty()),
757        ("CSSCode", css_code_ty()),
758        ("CSSXStabilizer", css_x_stabilizer_ty()),
759        ("CSSZStabilizer", css_z_stabilizer_ty()),
760        ("CSSConstruction", css_construction_ty()),
761        ("CSSTransversalCNOT", css_transversal_cnot_ty()),
762        ("ShorCode", shor_code_ty()),
763        ("ShorLogicalZero", shor_logical_zero_ty()),
764        ("ShorLogicalOne", shor_logical_one_ty()),
765        ("ShorBitFlipCode", shor_bit_flip_code_ty()),
766        ("ShorPhaseFlipCode", shor_phase_flip_code_ty()),
767        ("ShorCorrectsSingleErrors", shor_corrects_single_errors_ty()),
768        ("ShorIsCSS", shor_is_css_ty()),
769        ("SteaneCode", steane_code_ty()),
770        ("SteaneHMatrix", steane_h_matrix_ty()),
771        ("SteaneStabilizer", steane_stabilizer_ty()),
772        (
773            "SteaneCorrectsSingleErrors",
774            steane_corrects_single_errors_ty(),
775        ),
776        (
777            "SteaneTransversalClifford",
778            steane_transversal_clifford_ty(),
779        ),
780        ("SteaneIsCSS", steane_is_css_ty()),
781        ("FaultTolerantGate", fault_tolerant_gate_ty()),
782        ("TransversalGate", transversal_gate_ty()),
783        ("MagicStateInjection", magic_state_injection_ty()),
784        ("TeleportedGate", teleported_gate_ty()),
785        ("EasttinKnillTheorem", easttin_knill_theorem_ty()),
786        ("TransversalCliffordCSS", transversal_clifford_css_ty()),
787        (
788            "MagicStateDistillationWorks",
789            magic_state_distillation_works_ty(),
790        ),
791        ("ErrorThreshold", error_threshold_ty()),
792        ("ConcatenatedCode", concatenated_code_ty()),
793        ("FaultToleranceOverhead", fault_tolerance_overhead_ty()),
794        ("PseudoThreshold", pseudo_threshold_ty()),
795        ("ThresholdTheorem", threshold_theorem_ty()),
796        ("ConcatenatedCodeDistance", concatenated_code_distance_ty()),
797        ("PolytopeBound", polytope_bound_ty()),
798        ("ColorCode", color_code_ty()),
799        ("ColorCodeLattice", color_code_lattice_ty()),
800        ("ColorCodeSyndrome", color_code_syndrome_ty()),
801        ("ColorCodeTransversalT", color_code_transversal_t_ty()),
802        ("ColorCodeEquivalent", color_code_equivalent_ty()),
803        ("QuantumCapacity", quantum_capacity_ty()),
804        ("CoherentInformation", coherent_information_ty()),
805        ("HashingBound", hashing_bound_ty()),
806        ("QuantumErasureCapacity", quantum_erasure_capacity_ty()),
807        ("QuantumNoiseThreshold", quantum_noise_threshold_ty()),
808        ("QuantumShannonTheorem", quantum_shannon_theorem_ty()),
809        ("NoCloning", no_cloning_capacity_ty()),
810        ("KLMatrix", kl_matrix_ty()),
811        ("KLErrorSet", kl_error_set_ty()),
812        ("KLCorrectableCode", kl_correctable_code_ty()),
813        ("KLNecessaryCondition", kl_necessary_condition_ty()),
814        ("KLSufficientCondition", kl_sufficient_condition_ty()),
815        ("KLEquivalence", kl_equivalence_ty()),
816        ("KLDegenerateCode", kl_degenerate_code_ty()),
817        ("ReedMullerCode", reed_muller_code_ty()),
818        ("QuantumReedMullerCode", quantum_reed_muller_code_ty()),
819        ("RMTransversalT", rm_transversal_t_ty()),
820        ("RMCodeConcatenation", rm_code_concatenation_ty()),
821        ("RMTransversalUniversal", rm_transversal_universal_ty()),
822        ("RMCodeDistance", rm_code_distance_ty()),
823        ("SurfaceCode", surface_code_ty()),
824        ("ToricCode", toric_code_ty()),
825        ("SurfaceCodeVertex", surface_code_vertex_ty()),
826        ("SurfaceCodePlaquette", surface_code_plaquette_ty()),
827        ("SurfaceCodeLogical", surface_code_logical_ty()),
828        ("SurfaceCodeDistance", surface_code_distance_ty()),
829        ("ToricCodeAnyons", toric_code_anyons_ty()),
830        ("SurfaceCodeThreshold", surface_code_threshold_ty()),
831        ("QLDPCCode", qldpc_code_ty()),
832        ("FiberBundleCode", fiber_bundle_code_ty()),
833        ("GoodQLDPCCode", good_qldpc_code_ty()),
834        ("QLDPCTanner", qldpc_tanner_ty()),
835        ("QLDPCGoodCodes", qldpc_good_codes_ty()),
836        ("FiberBundleDistance", fiber_bundle_distance_ty()),
837        ("BosonicCode", bosonic_code_ty()),
838        ("CatCode", cat_code_ty()),
839        ("GKPCode", gkp_code_ty()),
840        ("BinomialCode", binomial_code_ty()),
841        ("GKPDisplacementError", gkp_displacement_error_ty()),
842        (
843            "GKPCorrectsBoundedDisplacement",
844            gkp_corrects_bounded_displacement_ty(),
845        ),
846        ("CatCodeLossTolerance", cat_code_loss_tolerance_ty()),
847        ("NoiseModel", noise_model_ty()),
848        ("DepolarizingNoise", depolarizing_noise_ty()),
849        ("CircuitNoiseThreshold", circuit_noise_threshold_ty()),
850        ("FaultToleranceGadget", fault_tolerance_gadget_ty()),
851        ("CircuitThresholdTheorem", circuit_threshold_theorem_ty()),
852        ("ThresholdUpperBound", threshold_upper_bound_ty()),
853        ("MagicState", magic_state_ty()),
854        ("TState", t_state_ty()),
855        ("DistillationProtocol", distillation_protocol_ty()),
856        ("MagicStateRobustness", magic_state_robustness_ty()),
857        ("BravyiKitaevDistillation", bravyi_kitaev_distillation_ty()),
858        ("MagicStateNonStabilizer", magic_state_non_stabilizer_ty()),
859        ("MWPMDecoder", mwpm_decoder_ty()),
860        ("BeliefPropDecoder", belief_prop_decoder_ty()),
861        ("UnionFindDecoder", union_find_decoder_ty()),
862        ("MLDecoder", ml_decoder_ty()),
863        ("DecodingThreshold", decoding_threshold_ty()),
864        ("MWPMOptimalSurface", mwpm_optimal_surface_ty()),
865        ("BPConvergenceLDPC", bp_convergence_ldpc_ty()),
866        ("SubsystemCode", subsystem_code_ty()),
867        ("GaugeGroup", gauge_group_ty()),
868        ("BaconShorCode", bacon_shor_code_ty()),
869        ("OperatorQEC", operator_qec_ty()),
870        ("SubsystemCodeCorrection", subsystem_code_correction_ty()),
871        (
872            "BaconShorSingleFaultTolerant",
873            bacon_shor_single_fault_tolerant_ty(),
874        ),
875        ("CodeSwitching", code_switching_ty()),
876        ("GateSynthesis", gate_synthesis_ty()),
877        ("SolovayKitaevApprox", solovay_kitaev_approx_ty()),
878        ("SolovayKitaevTheorem", solovay_kitaev_theorem_ty()),
879        ("TCountOptimality", t_count_optimality_ty()),
880    ];
881    for (name, ty) in axioms {
882        env.add(Declaration::Axiom {
883            name: Name::str(*name),
884            univ_params: vec![],
885            ty: ty.clone(),
886        })
887        .map_err(|e| format!("Failed to add '{}': {:?}", name, e))?;
888    }
889    Ok(())
890}
891/// Compute the binary entropy H(p) = -p log₂ p - (1-p) log₂(1-p).
892pub fn binary_entropy(p: f64) -> f64 {
893    if p <= 0.0 || p >= 1.0 {
894        return 0.0;
895    }
896    -p * p.log2() - (1.0 - p) * (1.0 - p).log2()
897}
898/// Hashing bound for the depolarizing channel with error rate p.
899/// Q ≥ max(0, 1 - H(p) - p log₂ 3).
900pub fn hashing_bound(p: f64) -> f64 {
901    let q = 1.0 - binary_entropy(p) - p * 3.0_f64.log2();
902    q.max(0.0)
903}
904/// Quantum capacity of the erasure channel with erasure probability ε.
905/// Q = max(0, 1 - 2ε).
906pub fn erasure_channel_capacity(epsilon: f64) -> f64 {
907    (1.0 - 2.0 * epsilon).max(0.0)
908}
909/// Approximate quantum capacity of the amplitude damping channel.
910/// Q ≈ 1 - H(γ) for small γ.
911pub fn amplitude_damping_capacity(gamma: f64) -> f64 {
912    (1.0 - binary_entropy(gamma)).max(0.0)
913}
914/// T-state fidelity after one round of [[15,1,3]] distillation.
915/// Input fidelity F → output fidelity F_out ≈ 1 - 35(1-F)³.
916pub fn distill_t_state_fidelity(f_in: f64) -> f64 {
917    let eps = 1.0 - f_in;
918    let f_out = 1.0 - 35.0 * eps.powi(3);
919    f_out.min(1.0).max(0.0)
920}
921/// Number of T-state distillation rounds needed to reach target fidelity.
922pub fn distillation_rounds(f_init: f64, f_target: f64) -> usize {
923    let mut f = f_init;
924    let mut rounds = 0;
925    while f < f_target && rounds < 100 {
926        f = distill_t_state_fidelity(f);
927        rounds += 1;
928    }
929    rounds
930}
931/// Overhead (input T-states per output T-state) for k rounds.
932/// Each round uses 15 input states to produce 1 output.
933pub fn distillation_overhead(rounds: usize) -> u64 {
934    15u64.pow(rounds as u32)
935}
936#[cfg(test)]
937mod tests {
938    use super::*;
939    #[test]
940    fn test_pauli_commutation() {
941        assert!(!PauliOp::X.commutes_with(PauliOp::Z));
942        assert!(!PauliOp::X.commutes_with(PauliOp::Y));
943        assert!(PauliOp::X.commutes_with(PauliOp::X));
944        for &p in &[PauliOp::I, PauliOp::X, PauliOp::Y, PauliOp::Z] {
945            assert!(PauliOp::I.commutes_with(p));
946        }
947    }
948    #[test]
949    fn test_pauli_string_commutation() {
950        let a = PauliString::new(vec![PauliOp::Z, PauliOp::Z, PauliOp::I]);
951        let b = PauliString::new(vec![PauliOp::I, PauliOp::Z, PauliOp::Z]);
952        assert!(a.commutes_with(&b));
953        let c = PauliString::new(vec![PauliOp::X, PauliOp::X, PauliOp::I]);
954        assert!(!c.commutes_with(&b));
955    }
956    #[test]
957    fn test_stabilizer_code_3qubit() {
958        let code = StabilizerCode::bit_flip_3();
959        assert_eq!(code.n, 3);
960        assert_eq!(code.k, 1);
961        let x_err = vec![0u8; 3];
962        let z_err = vec![0u8; 3];
963        let synd = code.syndrome(&x_err, &z_err);
964        assert!(synd.iter().all(|&s| s == 0));
965        let x_err1 = vec![1u8, 0, 0];
966        assert!(code.detects_error(&x_err1, &z_err));
967    }
968    #[test]
969    fn test_steane_7_code() {
970        let code = StabilizerCode::steane_7();
971        assert_eq!(code.n, 7);
972        assert_eq!(code.k, 1);
973        assert_eq!(code.d, 3);
974        let x_err = vec![0u8; 7];
975        let z_err = vec![0u8; 7];
976        let synd = code.syndrome(&x_err, &z_err);
977        assert!(
978            synd.iter().all(|&s| s == 0),
979            "No-error syndrome should be zero"
980        );
981        assert!(code.satisfies_singleton_bound());
982        assert!(code.satisfies_hamming_bound());
983    }
984    #[test]
985    fn test_shor_code() {
986        let shor = ShorCode::new();
987        assert_eq!(shor.n(), 9);
988        assert_eq!(shor.k(), 1);
989        assert_eq!(shor.d(), 3);
990        assert!(shor.corrects_single_qubit_error());
991        assert!(shor.satisfies_singleton_bound());
992        let x_err = vec![0u8; 9];
993        let z_err = vec![0u8; 9];
994        let synd = shor.syndrome(&x_err, &z_err);
995        assert!(synd.iter().all(|&s| s == 0));
996    }
997    #[test]
998    fn test_css_steane_syndrome() {
999        let css = CSSCode::steane();
1000        let no_err = vec![0u8; 7];
1001        assert!(!css.detects_x_error(&no_err));
1002        assert!(!css.detects_z_error(&no_err));
1003        let mut x_err = vec![0u8; 7];
1004        x_err[0] = 1;
1005        assert!(css.detects_x_error(&x_err));
1006    }
1007    #[test]
1008    fn test_hashing_bound() {
1009        assert!((hashing_bound(0.0) - 1.0).abs() < 1e-9);
1010        let q = hashing_bound(0.25);
1011        assert!(q >= 0.0);
1012        assert!((erasure_channel_capacity(0.0) - 1.0).abs() < 1e-9);
1013        assert!((erasure_channel_capacity(0.5)).abs() < 1e-9);
1014        assert!(erasure_channel_capacity(0.3) > 0.0);
1015    }
1016    #[test]
1017    fn test_magic_state_distillation() {
1018        let f_init = 0.95;
1019        let f_out = distill_t_state_fidelity(f_init);
1020        assert!(f_out > f_init, "Distillation should improve fidelity");
1021        let rounds = distillation_rounds(f_init, 0.9999);
1022        assert!(rounds >= 1);
1023        assert_eq!(distillation_overhead(1), 15);
1024        assert_eq!(distillation_overhead(2), 225);
1025    }
1026    #[test]
1027    fn test_concatenated_code() {
1028        let cc = ConcatenatedCode::new(7, 3, 2);
1029        assert_eq!(cc.num_physical_qubits(), 49);
1030        assert_eq!(cc.distance(), 9);
1031        let cc1 = ConcatenatedCode::new(7, 3, 1);
1032        let cc2 = ConcatenatedCode::new(7, 3, 2);
1033        let p = 0.001;
1034        let th = 0.01;
1035        assert!(cc2.logical_error_rate(p, th) < cc1.logical_error_rate(p, th));
1036    }
1037    #[test]
1038    fn test_build_quantum_error_correction_env() {
1039        let mut env = oxilean_kernel::Environment::new();
1040        let result = build_quantum_error_correction_env(&mut env);
1041        assert!(
1042            result.is_ok(),
1043            "build_quantum_error_correction_env failed: {:?}",
1044            result.err()
1045        );
1046    }
1047    #[test]
1048    fn test_surface_code_decoder() {
1049        let decoder = SurfaceCodeDecoder::new(3);
1050        let corrections = decoder.decode(&[]);
1051        assert!(corrections.is_empty());
1052        let d3 = SurfaceCodeDecoder::new(3);
1053        let d5 = SurfaceCodeDecoder::new(5);
1054        let p = 0.001;
1055        assert!(d5.logical_error_rate(p) < d3.logical_error_rate(p));
1056        assert!(d3.logical_error_rate(0.005) < 0.5);
1057    }
1058    #[test]
1059    fn test_surface_code_decoder_syndrome_matching() {
1060        let decoder = SurfaceCodeDecoder::new(5);
1061        let syndrome = vec![(1, 1), (1, 2)];
1062        let corrections = decoder.decode(&syndrome);
1063        assert!(!corrections.is_empty());
1064    }
1065    #[test]
1066    fn test_stabilizer_simulator_init() {
1067        let sim = StabilizerSimulator::new(3);
1068        assert_eq!(sim.measure_z(0), 0);
1069        assert_eq!(sim.measure_z(1), 0);
1070        assert_eq!(sim.measure_z(2), 0);
1071    }
1072    #[test]
1073    fn test_stabilizer_simulator_hadamard() {
1074        let mut sim = StabilizerSimulator::new(2);
1075        sim.hadamard(0);
1076        assert_eq!(sim.stab_x[0][0], 1);
1077        assert_eq!(sim.stab_z[0][0], 0);
1078    }
1079    #[test]
1080    fn test_stabilizer_simulator_phase_gate() {
1081        let mut sim = StabilizerSimulator::new(1);
1082        sim.phase_gate(0);
1083        assert_eq!(sim.stab_z[0][0], 1);
1084        assert_eq!(sim.stab_x[0][0], 0);
1085    }
1086    #[test]
1087    fn test_fault_tolerance_threshold() {
1088        let ft = FaultToleranceThreshold::new(7, 1, 3);
1089        let p_th = ft.estimate_threshold();
1090        assert!(p_th > 0.0);
1091        assert!((ft.logical_error_rate(p_th, 1) - 0.5).abs() < 1e-10);
1092        let p = p_th * 0.5;
1093        assert!(ft.logical_error_rate(p, 2) < ft.logical_error_rate(p, 1));
1094        let level = ft.min_level(p, 1e-6);
1095        assert!(level < u32::MAX);
1096    }
1097    #[test]
1098    fn test_qec_norm_checker_steane() {
1099        let code = StabilizerCode::steane_7();
1100        let checker = QECNormChecker::new(code);
1101        assert!(
1102            checker.all_single_qubit_errors_correctable(),
1103            "Steane code should correct all single-qubit errors"
1104        );
1105    }
1106    #[test]
1107    fn test_qec_norm_checker_kl_condition() {
1108        let code = StabilizerCode::steane_7();
1109        let checker = QECNormChecker::new(code);
1110        assert!(checker.satisfies_kl_conditions(&[0u8; 7], &[0u8; 7]));
1111        let mut x_err = vec![0u8; 7];
1112        x_err[0] = 1;
1113        assert!(checker.satisfies_kl_conditions(&x_err, &[0u8; 7]));
1114    }
1115    #[test]
1116    fn test_gkp_code_simulator_correction() {
1117        let gkp = GKPCodeSimulator::new();
1118        let delta = gkp.lattice_spacing;
1119        assert!(gkp.is_correctable(delta * 0.1, delta * 0.1));
1120        assert!(!gkp.is_correctable(delta * 0.6, 0.0));
1121        let (rq, rp) = gkp.correct_displacement(0.1, 0.05);
1122        assert!(rq.abs() < delta / 2.0);
1123        assert!(rp.abs() < delta / 2.0);
1124    }
1125    #[test]
1126    fn test_gkp_code_simulator_logical_error_rate() {
1127        let gkp = GKPCodeSimulator::new();
1128        let rate_small = gkp.logical_error_rate_gaussian(0.1);
1129        let rate_large = gkp.logical_error_rate_gaussian(0.5);
1130        assert!(
1131            rate_small < rate_large,
1132            "Larger noise should give larger error rate"
1133        );
1134        assert_eq!(gkp.logical_error_rate_gaussian(0.0), 0.0);
1135    }
1136    #[test]
1137    fn test_gkp_simulate_errors() {
1138        let gkp = GKPCodeSimulator::new();
1139        let delta = gkp.lattice_spacing;
1140        let displacements = vec![
1141            (delta * 0.1, delta * 0.1),
1142            (delta * 0.4, delta * 0.4),
1143            (delta * 0.6, 0.0),
1144        ];
1145        let uncorrected = gkp.simulate_errors(&displacements);
1146        assert_eq!(
1147            uncorrected, 1,
1148            "Only one displacement should be uncorrectable"
1149        );
1150    }
1151}
1152#[cfg(test)]
1153mod tests_qec_extra {
1154    use super::*;
1155    #[test]
1156    fn test_pauli_commutation() {
1157        let x = PauliOperator::single_x(2, 0);
1158        let z = PauliOperator::single_z(2, 0);
1159        assert!(!x.commutes_with(&z), "X and Z anticommute");
1160        let x1 = PauliOperator::single_x(2, 0);
1161        let x2 = PauliOperator::single_x(2, 1);
1162        assert!(x1.commutes_with(&x2), "X on different qubits commute");
1163    }
1164    #[test]
1165    fn test_five_qubit_code() {
1166        let code = StabCode::five_qubit_code();
1167        assert_eq!(code.n_physical, 5);
1168        assert_eq!(code.k_logical, 1);
1169        assert_eq!(code.generators.len(), 4);
1170        for i in 0..4 {
1171            for j in (i + 1)..4 {
1172                assert!(
1173                    code.generators[i].commutes_with(&code.generators[j]),
1174                    "Generator {} must commute with {}",
1175                    i,
1176                    j
1177                );
1178            }
1179        }
1180    }
1181    #[test]
1182    fn test_steane_code_structure() {
1183        let code = StabCode::steane_code();
1184        assert_eq!(code.n_physical, 7);
1185        assert_eq!(code.k_logical, 1);
1186        assert_eq!(code.generators.len(), 6);
1187    }
1188    #[test]
1189    fn test_syndrome_decoder_weight1() {
1190        let code = StabCode::five_qubit_code();
1191        let mut decoder = SyndromeDecoder2::new(code);
1192        decoder.build_weight1_table();
1193        assert!(decoder.lookup_table.len() <= 15);
1194    }
1195    #[test]
1196    fn test_threshold_estimator() {
1197        let est = ThresholdEstimator::new(0.001, 3, 10);
1198        let threshold = 0.01;
1199        assert!(est.is_below_threshold(threshold));
1200        let logical_rate = est.logical_error_rate(threshold);
1201        assert!(
1202            logical_rate < est.physical_error_rate,
1203            "Logical rate should improve below threshold"
1204        );
1205    }
1206    #[test]
1207    fn test_surface_code() {
1208        let sc = SurfaceCode::new(5);
1209        assert_eq!(sc.code_distance(), 5);
1210        assert_eq!(sc.n_data_qubits, 25);
1211        assert!(sc.total_qubits() > 25);
1212        assert!(SurfaceCode::depolarizing_threshold() > 0.0);
1213    }
1214    #[test]
1215    fn test_magic_state_distillation() {
1216        let msd = MagicStateDistillation::new(0.01, 1e-10, MagicStateProtocol::FifteenToOne);
1217        let out = msd.output_error_rate();
1218        assert!(
1219            out < msd.input_error_rate,
1220            "Distillation should reduce error"
1221        );
1222        let rounds = msd.n_rounds_needed();
1223        assert!(rounds > 0);
1224    }
1225    #[test]
1226    fn test_quantum_ldpc() {
1227        let code = QuantumLDPC::new(100, 10, 10, 6, 6);
1228        assert!(code.rate() > 0.0);
1229        let hp = QuantumLDPC::hypergraph_product(4, 8, 4, 8);
1230        assert!(hp.n > 0);
1231    }
1232}
oxilean_std/quantum_error_correction/functions.rs

oxilean_std/quantum_error_correction/
functions.rs
