docs(quantum-info): add qubit API map

Physlib/QuantumMechanics/Qubit/API-map.yaml

@@ -0,0 +1,112 @@
+version: v0.1
+
+Title: Qubits
+
+Overview: |
+    The key data structure is `Qubit`, the two element type labelling the computational
+    basis of a two-level quantum system. The content specific to qubits is the standard
+    single-qubit gates, the controlled version of a unitary with a qubit as control
+    register, and the Bloch sphere with its angular parameterization. Qubit states are
+    not built separately: a pure state of a qubit is a ket on `Qubit`, defined for an
+    arbitrary finite index type in `QuantumInfo/States/Pure/Braket.lean`, and a general
+    state is a density matrix on `Qubit`. The ambient theory of a finite dimensional
+    system, in particular density matrices with their evolution, measurements and
+    distinguishability measures, is left to a separate API map. Two modules of the
+    source directory, `BlochSphere.lean` and `BargmannInvariant.lean`, are not
+    imported by `QuantumInfo.lean` and so are not built with the library; the two
+    requirements that point at them record that.
+
+ParentAPIs:
+  - "Kets and bras of a finite dimensional system (QuantumInfo/States/Pure)"
+  - "Mixed states (QuantumInfo/States/Mixed)"
+
+References:
+  - "M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Chapters 1, 2, 4 and 9"
+  - "S. Pancharatnam, Generalized theory of interference, and its applications, Proc. Indian Acad. Sci. A 44, 247 (1956)"
+  - "M. V. Berry, Quantal phase factors accompanying adiabatic changes, Proc. R. Soc. London A 392, 45 (1984)"
+
+Requirements:
+
+  - description: "The key data structure `Qubit`, the two element type labelling the computational basis of a two-level quantum system, is defined."
+    done: true
+    location: "QuantumInfo/States/Pure/Qubit.lean (Qubit)"
+
+  - description: "Kets and bras of a finite dimensional system are defined, carrying coercions to functions and to each other, and the API contains the bra-ket pairing, the normalization condition in both its componentwise and its inner product form, the computational basis states and the uniform superposition."
+    done: true
+    location: "QuantumInfo/States/Pure/Braket.lean (Ket, Bra, FunLike (Ket d) d ℂ, FunLike (Bra d) d ℂ, Coe (Ket d) (Bra d), Coe (Bra d) (Ket d), FunLike (Bra d) (Ket d) ℂ, dot, Ket.normalized, Ket.basis, uniform_superposition, Braket.dot_self_eq_one)"
+
+  - description: "The API contains the standard single-qubit gates `Z`, `X`, `Y`, `H`, `S` and `T`, each as an element of the unitary group on `Qubit`."
+    done: true
+    location: "QuantumInfo/States/Pure/Qubit.lean (Z, X, Y, H, S, T)"
+
+  - description: "The API contains the squares of the standard single-qubit gates, the anticommutation relations of the three Pauli gates, the commutation of the phase gates `S` and `T` with `Z` and with each other, and the exchange of `X` and `Z` under conjugation by the Hadamard gate."
+    done: true
+    location: "QuantumInfo/States/Pure/Qubit.lean (Z_sq, X_sq, Y_sq, H_sq, S_sq, T_sq, X_Y_anticomm, Y_Z_anticomm, Z_X_anticomm, H_mul_X_eq_Z_mul_H, H_mul_Z_eq_X_mul_H, S_Z_comm, T_Z_comm, S_T_comm)"
+
+  - description: "The API contains the controlled version of a unitary on an arbitrary register, with a qubit as the control, its entries on the block where the control is one, the controlled-NOT gate and its matrix, the composition rules for controlled gates, and the effect of conjugating the control by `X`."
+    done: true
+    location: "QuantumInfo/States/Pure/Qubit.lean (controllize, CNOT, CNOT_matrix, controllize_apply_one_one, controllize_mul, controllize_one, controllize_mul_inv, X_controllize_X)"
+
+  - description: "The API shall contain the Bloch sphere as the unit sphere of three-dimensional Euclidean space, with its parameterization by a polar and an azimuthal angle and the dot product of two of its points in terms of those angles. Stated as `BlochSphere`, `blochPoint`, `blochPoint_val` and `dot_blochPoint` in `QuantumInfo/States/Pure/BlochSphere.lean`, a module that `QuantumInfo.lean` does not import and that is therefore not built with the library."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the solid angle of a geodesic triangle on the Bloch sphere, together with the Bargmann invariant of three pure states, its phase, the invariance of that phase under cyclic permutation of the three, its negation under reversal of their order as an equation of angles, and the bound of one on the norm of the invariant. Stated as `solidAngle` in `QuantumInfo/States/Pure/BlochSphere.lean` and as `bargmannInvariantThree`, `bargmannPhaseThree`, `bargmannPhaseThree_cyclic`, `bargmannPhaseThree_reverse` and `norm_bargmannInvariantThree_le_one` in `QuantumInfo/States/Pure/BargmannInvariant.lean`, two modules that `QuantumInfo.lean` does not import and that are therefore not built with the library."
+    done: false
+    location: "N/A"
+
+  - description: "The product of two systems carries product and entangled kets and the maximally entangled state, so that Bell-type states of a pair of qubits can be written."
+    done: true
+    location: "QuantumInfo/States/Pure/Braket.lean (Ket.prod, Ket.IsProd, Ket.IsEntangled, Ket.MES, Ket.MES_isEntangled)"
+
+  - description: "States up to a global phase are defined, as the quotient of kets by the relation of differing by a unit complex number."
+    done: true
+    location: "QuantumInfo/States/Pure/Braket.lean (Ket.PhaseEquiv, KetUpToPhase, KetUpToPhase.mk, KetUpToPhase.lift)"
+
+  - description: "The API shall contain the Bloch vector of a state of a qubit, the triple of expectation values of the Pauli gates, and shall show that it is a bijection from states onto the closed unit ball of three-dimensional Euclidean space."
+    done: false
+    location: N/A
+
+  - description: "The API shall show that the Bloch vector restricts to a bijection from pure states up to a global phase onto the Bloch sphere, so that `blochPoint` presents the pure state with the given polar and azimuthal angles."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the decomposition of a state of a qubit as one half of the identity plus a real combination of the Pauli gates, and shall show that the identity together with the three Pauli gates is a basis of the self-adjoint two by two complex matrices."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the rotation gates about the three coordinate axes, the decomposition of an arbitrary single-qubit unitary into such rotations and a phase, and the identification of conjugation by a single-qubit unitary with a rotation of the Bloch sphere."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the measurement of a qubit in the computational basis, with the Born rule giving the two outcome probabilities as the squared norms of the components of the state."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the Bell basis of the states of a pair of qubits, its orthonormality, and the action of the standard gates on it."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the singlet and triplet states of a pair of qubits, and the splitting of their state space into an antisymmetric line and a symmetric plane."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain a closed form for the fidelity of two states of a qubit in terms of their traces and determinants."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the completeness of the positive partial transpose test for a pair of qubits, that a state is separable if and only if its partial transpose is positive semidefinite."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain registers of several qubits, with the state space of a register given by an iterated product, and the extension of a single-qubit gate to a gate acting on one component of a register."
+    done: false
+    location: N/A
+
+  - description: "The API shall show that the Hadamard, `T` and controlled-NOT gates generate a dense subgroup of the special unitary group of a register, so that they are universal for quantum computation."
+    done: false
+    location: N/A
+
+  - description: "The API shall relate `Qubit` to the finite dimensional Hilbert space of a two element target in Physlib, identifying kets on `Qubit` with the unit vectors of that Hilbert space."
+    done: false
+    location: N/A