Stabilizer label spaces imply the operational computational distribution

This file joins finite-dimensional symplectic algebra to the explicit complex amplitude Pauli action. The public state premises are normalization, actual Pauli eigenvector equations, isotropy, and maximal label-space dimension. Uniform measurement distributions are conclusions, not premises.

def LeanPool.SingleCopyStabilizer.HasEigenlabels {ι : Type u_1} [Fintype ι] (ψ : Measurement.Amplitude ι) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) : Prop

Every label in L represents an actual Pauli eigenvector equation for ψ.

Equations

• LeanPool.SingleCopyStabilizer.HasEigenlabels ψ L = ∀ a ∈ L, ∃ (ζ : ℂ), LeanPool.SingleCopyStabilizer.Measurement.IsPauliEigenvector ψ a.1 a.2 ζ

structure LeanPool.SingleCopyStabilizer.PureStabilizerState (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Type u_2

A normalized amplitude together with its maximal isotropic eigenlabel space. Eigenvalue phases remain existential and are not discarded from the underlying quantum equations.

• amplitude : Measurement.Amplitude ι

  The actual pure-state amplitudes.

• normalized : Measurement.IsNormalized self.amplitude
• labels : Submodule (ZMod 2) (Label (ZMod 2) ι)

  The maximal isotropic space of actual Pauli eigenlabels.

• isotropic : IsIsotropic self.labels
• maximal : Module.finrank (ZMod 2) ↥self.labels = Fintype.card ι
• eigenlabels : HasEigenlabels self.amplitude self.labels

theorem LeanPool.SingleCopyStabilizer.measurement_orthogonalSubgroup_eq {ι : Type u_1} [Fintype ι] (D : Submodule (ZMod 2) (Measurement.Bits ι)) : Measurement.orthogonalSubgroup ↑D = (dotOrthogonal D).toAddSubgroup

theorem LeanPool.SingleCopyStabilizer.eigenlabels_diagonal {ι : Type u_1} [Fintype ι] (ψ : Measurement.Amplitude ι) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (s : Measurement.Bits ι) : s ∈ ↑(diagonalSpace L) → ∃ (ζ : ℂ), Measurement.IsPauliEigenvector ψ 0 s ζ

theorem LeanPool.SingleCopyStabilizer.eigenlabels_supported_difference {ι : Type u_1} [Fintype ι] (ψ : Measurement.Amplitude ι) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (x y : Measurement.Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : x - y ∈ dotOrthogonal (diagonalSpace L)

Supported outcome differences annihilate diagonal labels for any eigenlabel space, without a maximality or stabilizer-state promise.

theorem LeanPool.SingleCopyStabilizer.stabilizer_supported_difference {ι : Type u_1} [Fintype ι] (ψ : Measurement.Amplitude ι) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (hiso : IsIsotropic L) (hdim : Module.finrank (ZMod 2) ↥L = Fintype.card ι) (x y : Measurement.Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : ∃ (v : Vec (ZMod 2) ι), (x - y, v) ∈ L

For maximal isotropic eigenlabels the geometric X-projection theorem turns every supported difference into an actual stabilizer X direction.

theorem LeanPool.SingleCopyStabilizer.stabilizer_uniform_bornWeight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Measurement.Amplitude ι) (hnorm : Measurement.IsNormalized ψ) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (hiso : IsIsotropic L) (hdim : Module.finrank (ZMod 2) ↥L = Fintype.card ι) : ∃ (z : Measurement.Bits ι), ∀ (x : Measurement.Bits ι), Measurement.bornWeight ψ x = if x ∈ Measurement.affineCoset (xProjection L).toAddSubgroup z then 1 / ↑(Nat.card ↥(xProjection L)) else 0

The paper's affine uniform-support theorem, now derived from actual amplitude eigenvector equations and maximal isotropic label-space dimension.

theorem LeanPool.SingleCopyStabilizer.PureStabilizerState.uniform_bornWeight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) : ∃ (z : Measurement.Bits ι), ∀ (x : Measurement.Bits ι), Measurement.bornWeight S.amplitude x = if x ∈ Measurement.affineCoset (xProjection S.labels).toAddSubgroup z then 1 / ↑(Nat.card ↥(xProjection S.labels)) else 0

theorem LeanPool.SingleCopyStabilizer.full_diagonal_support_unique {ι : Type u_1} [Fintype ι] (ψ : Measurement.Amplitude ι) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (hfull : Module.finrank (ZMod 2) ↥(diagonalSpace L) = Fintype.card ι) (x y : Measurement.Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : x = y

Full diagonal dimension forces any two supported outcomes to coincide.

theorem LeanPool.SingleCopyStabilizer.full_diagonal_bornWeight_point_mass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Measurement.Amplitude ι) (hnorm : Measurement.IsNormalized ψ) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (hfull : Module.finrank (ZMod 2) ↥(diagonalSpace L) = Fintype.card ι) : ∃ (z : Measurement.Bits ι), ∀ (x : Measurement.Bits ι), Measurement.bornWeight ψ x = if x = z then 1 else 0

The termination readout is a point mass when diagonal rank is full. This theorem needs neither isotropy nor maximality beyond the stated full diagonal-rank condition.

theorem LeanPool.SingleCopyStabilizer.full_diagonal_basis_amplitude {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Measurement.Amplitude ι) (hnorm : Measurement.IsNormalized ψ) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (hfull : Module.finrank (ZMod 2) ↥(diagonalSpace L) = Fintype.card ι) : ∃ (z : Measurement.Bits ι) (c : ℂ), Complex.normSq c = 1 ∧ ψ = fun (x : Measurement.Bits ι) => if x = z then c else 0

Full diagonal rank identifies the amplitude with a basis vector times a unit-modulus scalar, making the global-phase qualification explicit.

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

Two independent fresh computational measurements followed by subtraction. The second distribution is constant in the first outcome, so this is an independent product experiment expressed with mathlib's PMF bind/map.

Equations

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

theorem LeanPool.SingleCopyStabilizer.pmf_map_sub_left_apply {ι : Type u_1} (p : PMF (Measurement.Bits ι)) (x u : Measurement.Bits ι) : (PMF.map (fun (y : Measurement.Bits ι) => x - y) p) u = p (x - u)

theorem LeanPool.SingleCopyStabilizer.bornDifferencePMF_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Measurement.Amplitude ι) (hnorm : Measurement.IsNormalized ψ) (u : Measurement.Bits ι) : (bornDifferencePMF ψ hnorm) u = ENNReal.ofReal (∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x * Measurement.bornWeight ψ (x - u))

The PMF subtraction pushforward equals the usual finite convolution formula, derived from bind and map rather than assumed.

theorem LeanPool.SingleCopyStabilizer.uniform_affine_difference_mass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Measurement.Amplitude ι) (V : AddSubgroup (Measurement.Bits ι)) (z : Measurement.Bits ι) (hp : ∀ (x : Measurement.Bits ι), Measurement.bornWeight ψ x = if x ∈ Measurement.affineCoset V z then 1 / ↑(Nat.card ↥V) else 0) (u : Measurement.Bits ι) : ∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x * Measurement.bornWeight ψ (x - u) = if u ∈ V then 1 / ↑(Nat.card ↥V) else 0

Finite convolution of one uniform affine distribution removes its affine offset and gives the uniform distribution on its direction subgroup.

theorem LeanPool.SingleCopyStabilizer.stabilizer_bornDifferencePMF_uniform {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : Measurement.Amplitude ι) (hnorm : Measurement.IsNormalized ψ) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) (hiso : IsIsotropic L) (hdim : Module.finrank (ZMod 2) ↥L = Fintype.card ι) (u : Measurement.Bits ι) : (bornDifferencePMF ψ hnorm) u = if u ∈ xProjection L then ENNReal.ofReal (1 / ↑(Nat.card ↥(xProjection L))) else 0

Actual independent Born-measurement differences of a stabilizer state have the uniform PMF on its X projection. The only assumptions are the quantum eigenvector equations and maximal isotropic label-space structure.

theorem LeanPool.SingleCopyStabilizer.PureStabilizerState.bornDifferencePMF_uniform {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (u : Measurement.Bits ι) : (bornDifferencePMF S.amplitude ⋯) u = if u ∈ xProjection S.labels then ENNReal.ofReal (1 / ↑(Nat.card ↥(xProjection S.labels))) else 0