A physical adaptive round on stabilizer amplitudes

The round is the actual CNOT basis permutation, followed by H or HS at the chosen pivot. Its label-space action is proved to be binaryRound. No membership oracle is used to define the amplitude action.

noncomputable def LeanPool.SingleCopyStabilizer.QuantumRound.correctionAmplitude {ι : Type u_1} [DecidableEq ι] (i : ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) : Measurement.Amplitude ι

Apply H for correction bit zero, and HS for correction bit one.

Equations

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

theorem LeanPool.SingleCopyStabilizer.QuantumRound.correctionAmplitude_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) : Measurement.IsNormalized (correctionAmplitude i b ψ)

theorem LeanPool.SingleCopyStabilizer.QuantumRound.localCorrection_zero {ι : Type u_1} [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) : localCorrection i 0 (u, v) = (CliffordAction.hadamardXLabel i u v, CliffordAction.hadamardZLabel i u v)

theorem LeanPool.SingleCopyStabilizer.QuantumRound.localCorrection_one {ι : Type u_1} [DecidableEq ι] (i : ι) (u v : Measurement.Bits ι) : localCorrection i 1 (u, v) = (CliffordAction.hadamardXLabel i u (CliffordAction.phaseZLabel i u v), CliffordAction.hadamardZLabel i u (CliffordAction.phaseZLabel i u v))

theorem LeanPool.SingleCopyStabilizer.QuantumRound.correctionAmplitude_eigenvector {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (u v : Measurement.Bits ι) (ζ : ℂ) (heig : Measurement.IsPauliEigenvector ψ u v ζ) : ∃ (η : ℂ), Measurement.IsPauliEigenvector (correctionAmplitude i b ψ) (localCorrection i b (u, v)).1 (localCorrection i b (u, v)).2 η

Actual H/HS eigenvector covariance yields the correction's label action; the output eigenvalue includes the physically relevant phase factors.

noncomputable def LeanPool.SingleCopyStabilizer.QuantumRound.applyRoundAmplitude {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) : Measurement.Amplitude ι

The physical round depends only on its observed difference and random bit. When the observed difference is zero, the state is left unchanged.

Equations

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

@[simp]

theorem LeanPool.SingleCopyStabilizer.QuantumRound.applyRoundAmplitude_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ZMod 2) (ψ : Measurement.Amplitude ι) : applyRoundAmplitude 0 b ψ = ψ

theorem LeanPool.SingleCopyStabilizer.QuantumRound.applyRoundAmplitude_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (hu : u ≠ 0) : applyRoundAmplitude u b ψ = correctionAmplitude (binaryPivot u hu) b (CNOTAction.applyCNOTs (binaryPivot u hu) (u - Pi.single (binaryPivot u hu) 1) ⋯ ψ)

theorem LeanPool.SingleCopyStabilizer.QuantumRound.roundEquiv_apply_eq_applyRoundAmplitude {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) : (Circuit.roundEquiv u b) ψ = applyRoundAmplitude u b ψ

The amplitude round is exactly the recorded complex-linear circuit round.

theorem LeanPool.SingleCopyStabilizer.QuantumRound.applyRoundAmplitude_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) : Measurement.IsNormalized (applyRoundAmplitude u b ψ)

theorem LeanPool.SingleCopyStabilizer.QuantumRound.adaptiveUpdate_eigenvector {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (u : BinaryVec ι) (b : ZMod 2) (hu : u i = 1) (ψ : Measurement.Amplitude ι) (a : Label (ZMod 2) ι) (ζ : ℂ) (heig : Measurement.IsPauliEigenvector ψ a.1 a.2 ζ) : ∃ (η : ℂ), Measurement.IsPauliEigenvector (correctionAmplitude i b (CNOTAction.applyCNOTs i (u - Pi.single i 1) ⋯ ψ)) (adaptiveUpdate i u b a).1 (adaptiveUpdate i u b a).2 η

Composition of the concrete CNOT and H/HS covariance theorems transports every eigenlabel through the paper's algebraic adaptive update.

theorem LeanPool.SingleCopyStabilizer.QuantumRound.applyRoundAmplitude_eigenlabels {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) (L : BinarySpace ι) (heig : HasEigenlabels ψ L) : HasEigenlabels (applyRoundAmplitude u b ψ) (binaryRound L u b)

The physical gate round implements the full unsigned label-space update, including arbitrary outcomes with zero probability.

noncomputable def LeanPool.SingleCopyStabilizer.QuantumRound.quantumRound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : PureStabilizerState ι

An actual normalized pure stabilizer state after the physical round.

Equations

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

@[simp]

theorem LeanPool.SingleCopyStabilizer.QuantumRound.quantumRound_labels {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : (quantumRound S o).labels = binaryRound S.labels o.1 o.2

@[simp]

theorem LeanPool.SingleCopyStabilizer.QuantumRound.quantumRound_amplitude {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : (quantumRound S o).amplitude = applyRoundAmplitude o.1 o.2 S.amplitude

theorem LeanPool.SingleCopyStabilizer.QuantumRound.quantumRound_amplitude_eq_roundEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : (quantumRound S o).amplitude = (Circuit.roundEquiv o.1 o.2) S.amplitude