States, gates, tensor products

A qubit is a unit vector, up to phase

A qubit is a unit vector |ψ〉 = α|0〉 + β|1〉 in C², with |α|² + |β|² = 1, and two vectors that differ by an overall phase e^iγ are the same state. Fixing the phase so that α is real and non-negative leaves two real numbers:

|psi> = cos(theta/2)|0> + e^{i phi} sin(theta/2)|1>,     0 <= theta <= pi,  0 <= phi < 2 pi

The density matrix ρ = |ψ〉〈ψ| then equals (I + r·σ)/2 with r = (sinθ cosφ, sinθ sinφ, cosθ), a point on the unit sphere: the Bloch sphere. Antipodal points are orthogonal states.

Unitary, and why

A gate is a linear map that sends unit vectors to unit vectors. If 〈Uψ|Uψ〉 = 〈ψ|ψ〉 for every ψ, then by polarisation U preserves every inner product, which is U^†U = I. So gates are unitary, and the single-qubit ones act on the Bloch sphere as rotations. The Pauli matrices and their algebra:

X^2 = Y^2 = Z^2 = I          XY = iZ,  YZ = iX,  ZX = iY          XZ = -ZX
H = (X + Z)/sqrt 2    =>    HXH = Z,  HZH = X,  HYH = -Y
S = diag(1, i),  T = diag(1, e^{i pi/4}),   T^2 = S,  S^2 = Z

Derivation of HXH = Z. HXH = ½(X + Z)X(X + Z) = ½(1 + ZX)(X + Z) = ½(X + Z + ZXX + ZXZ). Since XX = I and ZXZ = −X (X and Z anticommute), this is ½(X + Z + Z − X) = Z.

Rotations. For a unit vector n, (n·σ)² = I (expand the square; the cross terms cancel by anticommutation). So in the power series for exp(−iθ n·σ/2) the even powers give cos(θ/2)I and the odd powers give −i sin(θ/2) n·σ, the closed form R_n(θ) = cos(θ/2) I − i sin(θ/2) n·σ. Acting on the Bloch vector it rotates by θ about n.

Two qubits, and what a product state is

Two qubits live in C² ⊗ C² = C⁴, with basis |00〉, |01〉, |10〉, |11〉; n qubits live in dimension 2ⁿ. A general state is a|00〉 + b|01〉 + c|10〉 + d|11〉. It is a product state (α|0〉 + β|1〉) ⊗ (γ|0〉 + δ|1〉) exactly when its coefficient matrix has rank one, i.e. when ad − bc = 0: for a product, a = αγ, b = αδ, c = βγ, d = βδ, so ad = bc; conversely if ad = bc the rows are proportional and the state factors. The quantity 2|ad − bc| is the concurrence. The Bell state (|00〉 + |11〉)/√2 has ad − bc = 1/2: not a product, and no choice of single-qubit states can reproduce it.

There is no unitary that copies an unknown state

Suppose a unitary U satisfies U(|ψ〉 ⊗ |0〉) = |ψ〉 ⊗ |ψ〉 for two states φ, ψ. Take the inner product of the two equations. The left side gives 〈φ|ψ〉〈0|0〉 = 〈φ|ψ〉, since U preserves inner products; the right side gives 〈φ|ψ〉². So c = c² for c = 〈φ|ψ〉, and over the complex numbers c(c − 1) = 0 forces c = 0 or c = 1: a single machine can copy only states that are orthogonal or identical. CNOT copies |0〉 and |1〉, and applied to |+〉|0〉 produces a Bell state, whose overlap with |+〉|+〉 is 1/2.

Every identity above, numerically

qm1-verify.py checks, to 10⁻¹²: unitarity of X, Y, Z, H, S, T and CNOT and of 200 random rotations; every Pauli relation above, HXH = Z included; the series of exp(−iθ n·σ/2) against the closed form on 200 random axes and angles; ρ = (I + r·σ)/2 with |r| = 1 and the rotation R_z acting as a rotation on 200 random states; ad − bc = 0 on 200 random product states and concurrence 1 on all four Bell states; and CNOT's fidelity with |+〉|+〉 is exactly 0.5. Controls: a non-unitary matrix changes the norm; the wrong-sign Bloch rotation does not match; ad − bc is nonzero on a Bell state; the CNOT cloner fails on a superposition.

A Lean file, Orthogenesis/Quantum/QubitAlgebra.lean, states the Pauli algebra, the conjugation (X + Z)X(X + Z) = 2Z, and the abstract no-cloning argument (a linear isometry with a tensor-product pairing). It has not been compiled: no Lean toolchain was available when it was written, and it is not yet imported from Orthogenesis.lean. The file's header says what each theorem does and does not say.

Run it: python3 quantum-maths/qm1-verify.py (standard library only; the sourcing block says SKIP, never PASS, if the source PDF is not in ~/Downloads).