Elementary gate semantics of the recorded learning circuit

The instruction lists counted in ExactResources denote exactly the complex-linear Clifford operations in Circuit. In particular the counted individual CNOTs implement the simultaneous target-mask operation.

def LeanPool.SingleCopyStabilizer.InstructionSemantics.WellFormed {ι : Type u_1} : ExactResources.Instruction ι → Prop

A CNOT's control and target must be distinct.

Equations

• LeanPool.SingleCopyStabilizer.InstructionSemantics.WellFormed (LeanPool.SingleCopyStabilizer.ExactResources.Instruction.cnot i j) = (i ≠ j)
• LeanPool.SingleCopyStabilizer.InstructionSemantics.WellFormed (LeanPool.SingleCopyStabilizer.ExactResources.Instruction.phase site) = True
• LeanPool.SingleCopyStabilizer.InstructionSemantics.WellFormed (LeanPool.SingleCopyStabilizer.ExactResources.Instruction.hadamard site) = True

noncomputable def LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionEquiv {ι : Type u_1} [DecidableEq ι] : ExactResources.Instruction ι → Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

Elementary physical gate interpretation. A malformed self-target CNOT is totalized as the identity; generated instruction lists never use that case.

Equations

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

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionEquiv_cnot_of_ne {ι : Type u_1} [DecidableEq ι] (i j : ι) (h : j ≠ i) : instructionEquiv (ExactResources.Instruction.cnot i j) = Circuit.cnotEquiv i (Pi.single j 1) ⋯

def LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv {ι : Type u_1} [DecidableEq ι] : List (ExactResources.Instruction ι) → Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι

Chronological composition of elementary instructions.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv [] = LinearEquiv.refl ℂ (LeanPool.SingleCopyStabilizer.Measurement.Amplitude ι)

@[simp]

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv_nil {ι : Type u_1} [DecidableEq ι] : instructionsEquiv [] = LinearEquiv.refl ℂ (Measurement.Amplitude ι)

@[simp]

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv_cons {ι : Type u_1} [DecidableEq ι] (g : ExactResources.Instruction ι) (gs : List (ExactResources.Instruction ι)) : instructionsEquiv (g :: gs) = instructionEquiv g ≪≫ₗ instructionsEquiv gs

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv_append {ι : Type u_1} [DecidableEq ι] (xs ys : List (ExactResources.Instruction ι)) : instructionsEquiv (xs ++ ys) = instructionsEquiv xs ≪≫ₗ instructionsEquiv ys

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.cnotEquiv_trans {ι : Type u_1} (i : ι) (w v : Measurement.Bits ι) (hw : w i = 0) (hv : v i = 0) : Circuit.cnotEquiv i w hw ≪≫ₗ Circuit.cnotEquiv i v hv = Circuit.cnotEquiv i (w + v) ⋯

CNOT masks sharing a control add under composition.

@[simp]

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.cnotEquiv_zero {ι : Type u_1} (i : ι) : Circuit.cnotEquiv i 0 ⋯ = LinearEquiv.refl ℂ (Measurement.Amplitude ι)

def LeanPool.SingleCopyStabilizer.InstructionSemantics.targetMask {ι : Type u_1} [DecidableEq ι] (targets : List ι) : Measurement.Bits ι

Mask obtained from a list of CNOT targets, counting repeated targets modulo two.

Equations

• LeanPool.SingleCopyStabilizer.InstructionSemantics.targetMask targets = (List.map (fun (j : ι) => Pi.single j 1) targets).sum

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.targetMask_control_zero {ι : Type u_1} [DecidableEq ι] (i : ι) (targets : List ι) (hi : i ∉ targets) : targetMask targets i = 0

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv_cnots {ι : Type u_1} [DecidableEq ι] (i : ι) (targets : List ι) (hi : i ∉ targets) : instructionsEquiv (List.map (ExactResources.Instruction.cnot i) targets) = Circuit.cnotEquiv i (targetMask targets) ⋯

A list of single-target CNOTs realizes its simultaneous target mask.

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.pivot_not_mem_targets {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (i : ι) : i ∉ ExactResources.cnotTargets u i

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.roundInstructions_wellFormed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : ExactResources.RoundOutcome ι) (g : ExactResources.Instruction ι) (hg : g ∈ ExactResources.roundInstructions outcome) : WellFormed g

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.cnotTargets_mask {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (i : ι) (hu : u i = 1) : targetMask (ExactResources.cnotTargets u i).toList = u - Pi.single i 1

For a pivot bit equal to one, the elementary target list is exactly the paper's mask u - eᵢ.

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.instructionsEquiv_cnotTargets {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (i : ι) (hu : u i = 1) : instructionsEquiv (List.map (ExactResources.Instruction.cnot i) (ExactResources.cnotTargets u i).toList) = Circuit.cnotEquiv i (u - Pi.single i 1) ⋯

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.roundInstructions_denote {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : ExactResources.RoundOutcome ι) : instructionsEquiv (ExactResources.roundInstructions outcome) = Circuit.roundEquiv outcome.1 outcome.2

The counted elementary instructions implement exactly one physical learning round, including its zero-difference branch.

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.circuitInstructions_denote {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (ExactResources.RoundOutcome ι)) : instructionsEquiv (ExactResources.circuitInstructions outcomes) = Circuit.circuitEquiv outcomes

The complete counted elementary circuit implements exactly the same operation as the recorded outcome circuit used by the decoder.

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.circuitInstructions_wellFormed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (ExactResources.RoundOutcome ι)) (g : ExactResources.Instruction ι) (hg : g ∈ ExactResources.circuitInstructions outcomes) : WellFormed g

theorem LeanPool.SingleCopyStabilizer.InstructionSemantics.decode_eq_inverse_instructions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (ExactResources.RoundOutcome ι)) (z : Measurement.Bits ι) : Circuit.decode outcomes z = (instructionsEquiv (ExactResources.circuitInstructions outcomes)).symm (Circuit.basis z)

The learned amplitude is exactly the inverse of the counted elementary instruction circuit, applied to the final computational basis string.