Actual arbitrary-qubit local phase and Hadamard actions on amplitudes.

theorem LeanPool.SingleCopyStabilizer.CliffordAction.bit_eq_zero_or_one (a : ZMod 2) : a = 0 ∨ a = 1

Every residue modulo two is zero or one.

theorem LeanPool.SingleCopyStabilizer.CliffordAction.paritySign_add (a b : ZMod 2) : Measurement.paritySign (a + b) = Measurement.paritySign a * Measurement.paritySign b

theorem LeanPool.SingleCopyStabilizer.CliffordAction.paritySign_mul_self (a : ZMod 2) : Measurement.paritySign a * Measurement.paritySign a = 1

def LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit (a : ZMod 2) : ℂ

Scalar phase contributed by a computational-basis bit under an S gate.

Equations

• LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit a = if a = 0 then 1 else Complex.I

@[simp]

theorem LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit_normSq (a : ZMod 2) : Complex.normSq (phaseBit a) = 1

theorem LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit_twist (a x : ZMod 2) : Measurement.paritySign (a * (x - a)) * phaseBit (x - a) = star (phaseBit a) * phaseBit x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.update_sub {ι : Type u_1} [DecidableEq ι] (x u : Measurement.Bits ι) (i : ι) (b : ZMod 2) : Function.update x i b - u = Function.update (x - u) i (b - u i)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.sub_update {ι : Type u_1} [DecidableEq ι] (x u : Measurement.Bits ι) (i : ι) (b : ZMod 2) : x - Function.update u i b = Function.update (x - u) i (x i - b)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.update_as_add_single {ι : Type u_1} [DecidableEq ι] (x : Measurement.Bits ι) (i : ι) (b : ZMod 2) : Function.update x i b = x + (b - x i) • Pi.single i 1

theorem LeanPool.SingleCopyStabilizer.CliffordAction.dot_update_left {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u v : Measurement.Bits ι) (i : ι) (b : ZMod 2) : Function.update u i b ⬝ᵥ v = u ⬝ᵥ v + (b - u i) * v i

theorem LeanPool.SingleCopyStabilizer.CliffordAction.dot_update_right {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u v : Measurement.Bits ι) (i : ι) (b : ZMod 2) : u ⬝ᵥ Function.update v i b = u ⬝ᵥ v + u i * (b - v i)

def LeanPool.SingleCopyStabilizer.CliffordAction.localPhase {ι : Type u_1} (i : ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : ℂ

Apply S at one site of the full register amplitude.

Equations

• LeanPool.SingleCopyStabilizer.CliffordAction.localPhase i ψ x = LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit (x i) * ψ x

def LeanPool.SingleCopyStabilizer.CliffordAction.phaseZLabel {ι : Type u_1} [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) : Measurement.Bits ι

The Z-label update under conjugation by a local S gate.

Equations

• LeanPool.SingleCopyStabilizer.CliffordAction.phaseZLabel i u v = v + u i • Pi.single i 1

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localPhase_bornWeight {ι : Type u_1} (i : ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : Measurement.bornWeight (localPhase i ψ) x = Measurement.bornWeight ψ x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localPhase_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) : Measurement.IsNormalized (localPhase i ψ)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localPhase_covariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : Measurement.pauliAction u (phaseZLabel i u v) (localPhase i ψ) x = star (phaseBit (u i)) * localPhase i (Measurement.pauliAction u v ψ) x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localPhase_eigenvector {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) (u v : Measurement.Bits ι) (ζ : ℂ) (heig : Measurement.IsPauliEigenvector ψ u v ζ) : Measurement.IsPauliEigenvector (localPhase i ψ) u (phaseZLabel i u v) (star (phaseBit (u i)) * ζ)

noncomputable def LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard {ι : Type u_1} [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : ℂ

Apply H at one site through its two-term amplitude formula.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.SingleCopyStabilizer.CliffordAction.hadamardXLabel {ι : Type u_1} [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) : Measurement.Bits ι

Replace the selected X label by its old Z label.

Equations

• LeanPool.SingleCopyStabilizer.CliffordAction.hadamardXLabel i u v = Function.update u i (v i)

def LeanPool.SingleCopyStabilizer.CliffordAction.hadamardZLabel {ι : Type u_1} [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) : Measurement.Bits ι

Replace the selected Z label by its old X label.

Equations

• LeanPool.SingleCopyStabilizer.CliffordAction.hadamardZLabel i u v = Function.update v i (u i)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard_covariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : Measurement.pauliAction (hadamardXLabel i u v) (hadamardZLabel i u v) (localHadamard i ψ) x = Measurement.paritySign (u i * v i) * localHadamard i (Measurement.pauliAction u v ψ) x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard_eigenvector {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) (u v : Measurement.Bits ι) (ζ : ℂ) (heig : Measurement.IsPauliEigenvector ψ u v ζ) : Measurement.IsPauliEigenvector (localHadamard i ψ) (hadamardXLabel i u v) (hadamardZLabel i u v) (Measurement.paritySign (u i * v i) * ζ)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.hadamardCoefficient_normSq : Complex.normSq QubitGates.hadamardCoefficient = 1 / 2

theorem LeanPool.SingleCopyStabilizer.CliffordAction.hadamard_pair_norm (a b : ℂ) : Complex.normSq (QubitGates.hadamardCoefficient * (a + b)) + Complex.normSq (QubitGates.hadamardCoefficient * (a - b)) = Complex.normSq a + Complex.normSq b

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard_pair_bornWeight {ι : Type u_1} [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : Measurement.bornWeight (localHadamard i ψ) (Function.update x i 0) + Measurement.bornWeight (localHadamard i ψ) (Function.update x i 1) = Measurement.bornWeight ψ (Function.update x i 0) + Measurement.bornWeight ψ (Function.update x i 1)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.flip_eq_update {ι : Type u_1} [DecidableEq ι] (i : ι) (x : Measurement.Bits ι) : x + Pi.single i 1 = Function.update x i (x i + 1)

theorem LeanPool.SingleCopyStabilizer.CliffordAction.sum_update_pair {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (f : Measurement.Bits ι → ℝ) : ∑ x : ι → ZMod 2, (f (Function.update x i 0) + f (Function.update x i 1)) = 2 * ∑ x : Measurement.Bits ι, f x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard_norm_preserving {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) : ∑ x : Measurement.Bits ι, Measurement.bornWeight (localHadamard i ψ) x = ∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) : Measurement.IsNormalized (localHadamard i ψ)

def LeanPool.SingleCopyStabilizer.CliffordAction.localPhaseInverse {ι : Type u_1} (i : ι) (ψ : Measurement.Amplitude ι) (x : Measurement.Bits ι) : ℂ

The adjoint S action on amplitudes.

Equations

• LeanPool.SingleCopyStabilizer.CliffordAction.localPhaseInverse i ψ x = star (LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit (x i)) * ψ x

theorem LeanPool.SingleCopyStabilizer.CliffordAction.phaseBit_star_mul (a : ZMod 2) : star (phaseBit a) * phaseBit a = 1

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localPhaseInverse_localPhase {ι : Type u_1} (i : ι) (ψ : Measurement.Amplitude ι) : localPhaseInverse i (localPhase i ψ) = ψ

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localPhase_localPhaseInverse {ι : Type u_1} (i : ι) (ψ : Measurement.Amplitude ι) : localPhase i (localPhaseInverse i ψ) = ψ

theorem LeanPool.SingleCopyStabilizer.CliffordAction.localHadamard_involutive {ι : Type u_1} [DecidableEq ι] (i : ι) (ψ : Measurement.Amplitude ι) : localHadamard i (localHadamard i ψ) = ψ

noncomputable def LeanPool.SingleCopyStabilizer.CliffordAction.localHadamardEquiv {ι : Type u_1} [DecidableEq ι] (i : ι) : Measurement.Amplitude ι ≃ Measurement.Amplitude ι

H is a bijection on the full amplitude space, with itself as inverse.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.SingleCopyStabilizer.CliffordAction.localPhaseEquiv {ι : Type u_1} (i : ι) : Measurement.Amplitude ι ≃ Measurement.Amplitude ι

S is a bijection on the full amplitude space with the explicit S† inverse.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.SingleCopyStabilizer.CliffordAction.localHadamardLinearEquiv {ι : Type u_1} [DecidableEq ι] (i : ι) : Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

The complex-linear involution induced by H at a selected site.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.SingleCopyStabilizer.CliffordAction.localPhaseLinearEquiv {ι : Type u_1} (i : ι) : Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

The complex-linear equivalence induced by S at a selected site.

Equations

• One or more equations did not get rendered due to their size.