Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

adiabatic_qc_equivalence_ty

AdiabaticQCEquivalence : Prop Adiabatic quantum computation is polynomially equivalent to the standard gate model of quantum computation.

adiabatic_theorem_ty

AdiabaticTheorem : ∀ (gap : Real), Prop The adiabatic theorem: if a Hamiltonian is evolved slowly enough (relative to the inverse square of the spectral gap), the system remains in its instantaneous ground state.

amplitude_amplification_ty

AmplitudeAmplification : ∀ n : Nat, ∀ k : Nat, Prop General amplitude amplification: if a state has success probability p, then after O(1/√p) oracle calls the success probability is amplified to nearly 1.

anyon_ty

Anyon : Type An anyon: a quasi-particle in (2+1)D that obeys fractional (non-Abelian) statistics under exchange.

app

app2

app3

arrow

bb84_key_rate_ty

BB84KeyRate : ∀ e : Real, Prop The BB84 asymptotic key rate r(e) = 1 − 2H(e), where H is the binary entropy function and e is the quantum bit-error rate.

bb84_security_ty

BB84Security : Prop Information-theoretic security of the BB84 protocol: any eavesdropper introduces detectable disturbance, and the secret key rate is positive below the QBER threshold ≈ 11%.

bool_ty

boson_sampling_hardness_ty

BosonSamplingHardness : Prop Boson sampling is classically hard to simulate (under plausible complexity theoretic conjectures): efficient classical simulation would imply P^#P = BPP^NP.

boson_sampling_ty

BosonSampling : Nat → Type The boson sampling problem on n photons: sample from the output distribution of a linear optical network acting on Fock states.

bqp_contains_bpp_ty

BQPContainsBPP : Prop The complexity class BQP (bounded-error quantum polynomial time) contains BPP (bounded-error probabilistic polynomial time): BPP ⊆ BQP.

bqp_in_psharp_p_ty

BQPInPSHARPP : Prop BQP is contained in P^#P (and hence in PSPACE): BQP ⊆ P^#P.

braiding_operator_ty

BraidingOperator : Anyon → Anyon → Type The unitary braiding operator R_{ij} arising from exchanging two anyons.

build_quantum_computing_env

cst

dense_coding_protocol_ty

DenseCodingProtocol : Prop Super-dense coding: using one shared Bell pair, Alice can send 2 classical bits to Bob using only a single qubit transmission.

entanglement_ty

Entanglement : Type — entangled quantum state (e.g., Bell state).

fault_tolerant_threshold_ty

FaultTolerantThreshold : Prop The threshold theorem: if the physical error rate p is below a constant threshold p_th ≈ 10⁻², arbitrarily long quantum computations can be performed with exponentially suppressed logical error rates.

fibonacci_anyon_ty

FibonacciAnyon : Prop Fibonacci anyons are universal for topological quantum computation: any unitary can be approximated by braiding Fibonacci anyons.

gate_set_ty

GateSet : Type — a finite set of quantum gates.

grover_iterations

Optimal number of Grover iterations for n_qubits qubits.

grover_optimality_ty

GroverOptimality : Prop Grover’s algorithm is optimal: any quantum algorithm requires Ω(√N) oracle queries for unstructured search.

grover_speedup_ty

Grover’s Quadratic Speedup: Grover’s algorithm solves unstructured search on N items in O(√N) queries, a quadratic speedup over classical O(N).

grover_success_prob

Probability of success after iterations Grover iterations on n_qubits qubits.

hamiltonian_simulation_ty

HamiltonianSimulation : ∀ (t : Real), Prop For any local Hamiltonian H, the time-evolution operator e^{−iHt} can be approximated to precision ε in poly(n, t, 1/ε) gate complexity.

ht_clifford_universal_ty

HTCliffordUniversal : Prop The gate set {H, T, CNOT} is universal for quantum computation.

local_hamiltonian_qma_complete_ty

LocalHamiltonianQMAComplete : Prop The k-local Hamiltonian problem is QMA-complete for k ≥ 2.

measurement_ty

Measurement : Type — quantum measurement (observable).

nat_ty

no_cloning_ty

No-Cloning Theorem: it is impossible to create an identical copy of an arbitrary unknown quantum state.

no_deleting_ty

No-Deleting Theorem: it is impossible to delete a copy of an arbitrary unknown quantum state given two identical copies.

non_abelian_statistics_ty

NonAbelianStatistics : Prop Non-Abelian anyons: the braiding operators do not commute in general, enabling topologically protected quantum gates.

period_finding_ty

PeriodFinding : ∀ (N a : Nat), Prop Shor’s period-finding subroutine: for coprime a, N, the quantum period finding algorithm finds the order r of a mod N in polynomial time.

phase_estimation_precision_ty

PhaseEstimationPrecision : ∀ n : Nat, PhaseError n ≤ Real.pow 2 n The phase estimation error is bounded by 2^{-n}.

phase_estimation_ty

PhaseEstimation : ∀ (n : Nat), Prop Quantum phase estimation approximates the eigenvalue e^{2πiφ} of a unitary U to n bits of precision using n ancilla qubits and O(2^n) controlled-U applications.

pi

prop

qaoa_approximation_ty

QAOAApproximation : ∀ p : Nat, Prop As the QAOA depth p → ∞, the algorithm converges to the exact solution of the combinatorial optimization problem.

qaoa_state_ty

QAOAState : Nat → Type The variational state produced by the Quantum Approximate Optimization Algorithm (QAOA) at depth p.

qft_complexity_ty

QFTComplexity : ∀ n : Nat, QFTGateCount n ≤ Nat.pow n 2 The QFT on n qubits requires O(n²) gates.

qft_correctness_ty

QFTCorrectness : ∀ n : Nat, Prop The quantum Fourier transform on n qubits correctly computes the DFT of the amplitude vector.

qft_state_ty

QFTState : Nat → Type The state produced by the quantum Fourier transform on n qubits.

qma_definition_ty

QMADefinition : Prop QMA (Quantum Merlin-Arthur) is the quantum analogue of NP: a problem is in QMA if there exists a polynomial-time quantum verifier and a quantum witness state.

quantum_circuit_ty

QuantumCircuit : Type — sequence of quantum gates applied to a register.

quantum_gate_ty

QuantumGate : Nat → Type — unitary operator on n qubits.

quantum_hamming_bound_ty

QuantumHammingBound : ∀ (n k t : Nat), Prop The quantum Hamming (Singleton) bound: n − k ≥ 4t for a code correcting t errors.

quantum_teleportation_ty

Quantum Teleportation Theorem: the quantum teleportation protocol faithfully transmits an arbitrary unknown qubit state using one shared Bell pair and two classical bits.

quantum_volume_monotone_ty

QuantumVolumeMonotone : ∀ (n m : Nat), Prop Quantum volume is monotone: improvements in gate fidelity and connectivity cannot decrease the quantum volume.

quantum_volume_ty

QuantumVolume : Nat → Nat The quantum volume V_Q = 2^n where n is the largest square quantum circuit that a device can implement with at-least-2/3 probability of success.

qubit_ty

Qubit : Type — qubit state α|0⟩ + β|1⟩ in ℂ².

real_ty

shor_exponential_ty

Shor’s Exponential Speedup: Shor’s algorithm factors an n-bit integer in polynomial time O(n³), an exponential speedup over the best classical algorithm.

shor_factoring_ty

ShorFactoring : ∀ N : Nat, Prop Given access to the period-finding subroutine, Shor’s algorithm factors N in O(log³ N) quantum gate operations with high probability.

solovay_kitaev_ty

SolovayKitaev : ∀ (g : GateSet), UniversalGateSet g → Prop The Solovay-Kitaev theorem: any universal gate set can approximate any single-qubit unitary to precision ε in O(log^c(1/ε)) gates.

stabilizer_code_corrects_errors_ty

StabilizerCodeCorrectsErrors : ∀ (n k d : Nat), Prop An [[n, k, d]] stabilizer code can correct ⌊(d−1)/2⌋ arbitrary qubit errors.

stabilizer_code_ty

StabilizerCode : Nat → Nat → Type An [[n, k]] stabilizer code encodes k logical qubits into n physical qubits.

standard_quantum_algorithms

Standard quantum algorithms summary.

surface_code_distance_ty

SurfaceCodeDistance : ∀ d : Nat, Prop The surface code with parameter d has code distance d, i.e., the minimum weight of any undetectable logical error is d.

surface_code_ty

SurfaceCode : Nat → Type A surface code of linear size d (code distance d, n ≈ 2d² physical qubits, 1 logical qubit).

topological_protection_ty

TopologicalProtection : Prop Topological quantum computation is inherently fault-tolerant: logical operations correspond to global topological properties immune to local perturbations.

trotter_suzuki_error_ty

TrotterSuzukiError : ∀ (t : Real) (r : Nat), Prop The first-order Trotter-Suzuki product formula has error O(t²/r) for r time steps.

type0

universal_gate_set_ty

UniversalGateSet : GateSet → Prop A gate set G is universal if any unitary can be approximated arbitrarily well by a circuit from G.

vqe_state_ty

VQEState : Type The parameterized ansatz state used in the variational quantum eigensolver.

vqe_variational_principle_ty

VQEVariationalPrinciple : Prop The variational principle underlying VQE: the expectation value of any Hamiltonian H with any normalized state |ψ⟩ satisfies ⟨ψ|H|ψ⟩ ≥ E_0, where E_0 is the ground-state energy.