Amplitudes, Pauli eigenvectors, and computational measurement weights

An amplitude is a complex function on binary strings. Computational outcome weights are defined by the Born rule Complex.normSq; normalization is the finite sum of those weights. The Pauli action is the explicit action of XᵘZᵛ on amplitudes, not an assumed measurement-distribution property.

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.Measurement.Bits (ι : Type u_1) : Type u_1

Computational-basis strings indexed by qubit sites.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.Bits ι = (ι → ZMod 2)

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.Measurement.Amplitude (ι : Type u_1) : Type u_1

Complex amplitudes on the computational basis.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.Amplitude ι = (LeanPool.SingleCopyStabilizer.Measurement.Bits ι → ℂ)

def LeanPool.SingleCopyStabilizer.Measurement.paritySign (a : ZMod 2) : ℂ

The binary character (-1)^a, without choosing integer representatives.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.paritySign a = if a = 0 then 1 else -1

@[simp]

theorem LeanPool.SingleCopyStabilizer.Measurement.paritySign_normSq (a : ZMod 2) : Complex.normSq (paritySign a) = 1

theorem LeanPool.SingleCopyStabilizer.Measurement.paritySign_injective : Function.Injective paritySign

def LeanPool.SingleCopyStabilizer.Measurement.bornWeight {ι : Type u_1} (ψ : Amplitude ι) (x : Bits ι) : ℝ

Born probability weight of a computational-basis outcome.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.bornWeight ψ x = Complex.normSq (ψ x)

def LeanPool.SingleCopyStabilizer.Measurement.IsNormalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) : Prop

Normalization of the finite Born weights to total mass one.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.IsNormalized ψ = (∑ x : LeanPool.SingleCopyStabilizer.Measurement.Bits ι, LeanPool.SingleCopyStabilizer.Measurement.bornWeight ψ x = 1)

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_nonneg {ι : Type u_1} (ψ : Amplitude ι) (x : Bits ι) : 0 ≤ bornWeight ψ x

@[simp]

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_pos {ι : Type u_1} (ψ : Amplitude ι) (x : Bits ι) : 0 < bornWeight ψ x ↔ ψ x ≠ 0

@[simp]

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_eq_zero {ι : Type u_1} (ψ : Amplitude ι) (x : Bits ι) : bornWeight ψ x = 0 ↔ ψ x = 0

def LeanPool.SingleCopyStabilizer.Measurement.bornPMF {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) : PMF (Bits ι)

Normalized amplitudes determine a mathlib probability mass function.

Equations

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

@[simp]

theorem LeanPool.SingleCopyStabilizer.Measurement.bornPMF_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (x : Bits ι) : (bornPMF ψ hψ) x = ENNReal.ofReal (bornWeight ψ x)

def LeanPool.SingleCopyStabilizer.Measurement.pauliAction {ι : Type u_1} [Fintype ι] (u v : Bits ι) (ψ : Amplitude ι) (x : Bits ι) : ℂ

(Xᵘ Zᵛ ψ)(x) = (-1)^(v·(x-u)) ψ(x-u), in the conventional operator order. The source basis vector x-u is first phased, then shifted.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.pauliAction u v ψ x = LeanPool.SingleCopyStabilizer.Measurement.paritySign (v ⬝ᵥ (x - u)) * ψ (x - u)

def LeanPool.SingleCopyStabilizer.Measurement.pauliOperator {ι : Type u_1} [Fintype ι] (u v : Bits ι) : Amplitude ι →ₗ[ℂ] Amplitude ι

The explicit action is complex-linear.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.pauliOperator u v = { toFun := LeanPool.SingleCopyStabilizer.Measurement.pauliAction u v, map_add' := ⋯, map_smul' := ⋯ }

def LeanPool.SingleCopyStabilizer.Measurement.IsPauliEigenvector {ι : Type u_1} [Fintype ι] (ψ : Amplitude ι) (u v : Bits ι) (ζ : ℂ) : Prop

The eigenvector premise is a pointwise equality of explicitly defined linear-operator amplitudes.

Equations

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

theorem LeanPool.SingleCopyStabilizer.Measurement.pauliAction_norm_preserving {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u v : Bits ι) (ψ : Amplitude ι) : ∑ x : Bits ι, bornWeight (pauliAction u v ψ) x = ∑ x : Bits ι, bornWeight ψ x

theorem LeanPool.SingleCopyStabilizer.Measurement.pauliAction_preserves_normalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u v : Bits ι) (ψ : Amplitude ι) (hψ : IsNormalized ψ) : IsNormalized (pauliAction u v ψ)

theorem LeanPool.SingleCopyStabilizer.Measurement.eigenvalue_normSq_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (u v : Bits ι) (ζ : ℂ) (heig : IsPauliEigenvector ψ u v ζ) : Complex.normSq ζ = 1

A normalized eigenvector of this explicit Pauli operator necessarily has a unit-modulus eigenvalue. No unit-modulus assumption is required.

theorem LeanPool.SingleCopyStabilizer.Measurement.eigenvector_bornWeight_translation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (u v : Bits ι) (ζ : ℂ) (heig : IsPauliEigenvector ψ u v ζ) (x : Bits ι) : bornWeight ψ (x + u) = bornWeight ψ x

Stabilizer X labels act as translation symmetries of the computational probabilities. This follows from the amplitude equation by taking norm squares.

theorem LeanPool.SingleCopyStabilizer.Measurement.diagonal_eigenvalue_at_nonzero {ι : Type u_1} [Fintype ι] (ψ : Amplitude ι) (s : Bits ι) (ζ : ℂ) (heig : IsPauliEigenvector ψ 0 s ζ) (x : Bits ι) (hx : ψ x ≠ 0) : paritySign (s ⬝ᵥ x) = ζ

At a nonzero amplitude of a diagonal Pauli eigenvector, the parity character is forced to equal the eigenvalue.

theorem LeanPool.SingleCopyStabilizer.Measurement.diagonal_eigenvector_difference {ι : Type u_1} [Fintype ι] (ψ : Amplitude ι) (s : Bits ι) (ζ : ℂ) (heig : IsPauliEigenvector ψ 0 s ζ) (x y : Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : s ⬝ᵥ (x - y) = 0

Two outcomes in the amplitude support of a diagonal eigenvector have the same parity, so their difference is orthogonal to its Z label.

def LeanPool.SingleCopyStabilizer.Measurement.orthogonalSet {ι : Type u_1} [Fintype ι] (D : Set (Bits ι)) : Set (Bits ι)

The orthogonal complement written directly in binary dot products.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.orthogonalSet D = {u : LeanPool.SingleCopyStabilizer.Measurement.Bits ι | ∀ s ∈ D, s ⬝ᵥ u = 0}

def LeanPool.SingleCopyStabilizer.Measurement.orthogonalSubgroup {ι : Type u_1} [Fintype ι] (D : Set (Bits ι)) : AddSubgroup (Bits ι)

The diagonal annihilator is an additive subgroup, without needing to assume that the supplied collection D is itself a subspace.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.orthogonalSubgroup D = { carrier := LeanPool.SingleCopyStabilizer.Measurement.orthogonalSet D, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem LeanPool.SingleCopyStabilizer.Measurement.mem_orthogonalSubgroup {ι : Type u_1} [Fintype ι] (D : Set (Bits ι)) (u : Bits ι) : u ∈ orthogonalSubgroup D ↔ u ∈ orthogonalSet D

theorem LeanPool.SingleCopyStabilizer.Measurement.supported_difference_orthogonal {ι : Type u_1} [Fintype ι] (ψ : Amplitude ι) (D : Set (Bits ι)) (hD : ∀ s ∈ D, ∃ (ζ : ℂ), IsPauliEigenvector ψ 0 s ζ) (x y : Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : x - y ∈ orthogonalSet D

Every computational difference lies in the annihilator of all diagonal stabilizers, even when the state has positive stabilizer nullity.

theorem LeanPool.SingleCopyStabilizer.Measurement.positive_probability_difference_orthogonal {ι : Type u_1} [Fintype ι] (ψ : Amplitude ι) (D : Set (Bits ι)) (hD : ∀ s ∈ D, ∃ (ζ : ℂ), IsPauliEigenvector ψ 0 s ζ) (x y : Bits ι) (hx : 0 < bornWeight ψ x) (hy : 0 < bornWeight ψ y) : x - y ∈ orthogonalSet D

The same guarantee stated in terms of positive-probability outcomes.

theorem LeanPool.SingleCopyStabilizer.Measurement.support_in_affine_annihilator {ι : Type u_1} [Fintype ι] (ψ : Amplitude ι) (D : Set (Bits ι)) (hD : ∀ s ∈ D, ∃ (ζ : ℂ), IsPauliEigenvector ψ 0 s ζ) (z : Bits ι) (hz : ψ z ≠ 0) (x : Bits ι) : ψ x ≠ 0 → x - z ∈ orthogonalSet D

Choosing any supported basepoint places the entire amplitude support in one affine coset of the diagonal annihilator.

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_invariant_of_eigenlabels {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (V : Set (Bits ι)) (hV : ∀ u ∈ V, ∃ (v : Bits ι) (ζ : ℂ), IsPauliEigenvector ψ u v ζ) (u : Bits ι) : u ∈ V → ∀ (x : Bits ι), bornWeight ψ (x + u) = bornWeight ψ x

A collection of actual Pauli eigenlabels gives probability invariance under every translation in their X projection.

noncomputable def LeanPool.SingleCopyStabilizer.Measurement.affineCoset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (V : AddSubgroup (Bits ι)) (z : Bits ι) : Finset (Bits ι)

The finite affine coset z + V, expressed by subtraction.

Equations

• LeanPool.SingleCopyStabilizer.Measurement.affineCoset V z = {x : LeanPool.SingleCopyStabilizer.Measurement.Bits ι | x - z ∈ V}

@[simp]

theorem LeanPool.SingleCopyStabilizer.Measurement.mem_affineCoset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (V : AddSubgroup (Bits ι)) (z x : Bits ι) : x ∈ affineCoset V z ↔ x - z ∈ V

theorem LeanPool.SingleCopyStabilizer.Measurement.affineCoset_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] (V : AddSubgroup (Bits ι)) (z : Bits ι) : (affineCoset V z).card = Nat.card ↥V

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_constant_on_affineCoset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (V : AddSubgroup (Bits ι)) (hinv : ∀ u ∈ V, ∀ (x : Bits ι), bornWeight ψ (x + u) = bornWeight ψ x) (z x : Bits ι) (hx : x ∈ affineCoset V z) : bornWeight ψ x = bornWeight ψ z

Invariance under all translations in V makes weights constant on every affine V-coset, even if different cosets have different masses.

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_uniform_affineCoset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (V : AddSubgroup (Bits ι)) (z : Bits ι) (hsupp : ∀ (x : Bits ι), ψ x ≠ 0 → x - z ∈ V) (hinv : ∀ u ∈ V, ∀ (x : Bits ι), bornWeight ψ (x + u) = bornWeight ψ x) (x : Bits ι) (hx : x ∈ affineCoset V z) : bornWeight ψ x = 1 / ↑(Nat.card ↥V)

If the support is confined to one coset and every translation in its direction space preserves probabilities, normalization forces the uniform distribution on that coset. This is a derived Born-weight statement.

theorem LeanPool.SingleCopyStabilizer.Measurement.bornWeight_uniform_affineCoset_ite {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (V : AddSubgroup (Bits ι)) (z : Bits ι) (hsupp : ∀ (x : Bits ι), ψ x ≠ 0 → x - z ∈ V) (hinv : ∀ u ∈ V, ∀ (x : Bits ι), bornWeight ψ (x + u) = bornWeight ψ x) (x : Bits ι) : bornWeight ψ x = if x ∈ affineCoset V z then 1 / ↑(Nat.card ↥V) else 0

The complete distribution, including its zero weights outside the coset.

theorem LeanPool.SingleCopyStabilizer.Measurement.normalized_has_nonzero_amplitude {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) : ∃ (z : Bits ι), ψ z ≠ 0

theorem LeanPool.SingleCopyStabilizer.Measurement.uniform_bornWeight_of_complete_eigenlabels {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Amplitude ι) (hψ : IsNormalized ψ) (D : Set (Bits ι)) (hD : ∀ s ∈ D, ∃ (ζ : ℂ), IsPauliEigenvector ψ 0 s ζ) (hX : ∀ u ∈ orthogonalSubgroup D, ∃ (v : Bits ι) (ζ : ℂ), IsPauliEigenvector ψ u v ζ) : ∃ (z : Bits ι), ∀ (x : Bits ι), bornWeight ψ x = if x ∈ affineCoset (orthogonalSubgroup D) z then 1 / ↑(Nat.card ↥(orthogonalSubgroup D)) else 0

Operational uniform-support consequence of a complete collection of Pauli eigenlabels. Diagonal eigenlabels confine the support, and a Pauli eigenlabel above every direction in their annihilator forces uniformity. The latter existence premise is the algebraic X-projection theorem for a maximal stabilizer space; no probability-uniformity hypothesis is assumed.