Symbolic gate and copy costs of the exact protocol

An outcome list determines explicit symbolic CNOT/S/H instructions. Costs count those instructions and their repeated execution on fresh copies. These are not running-time claims about Lean's noncomputable state simulation.

inductive LeanPool.SingleCopyStabilizer.ExactResources.Instruction (ι : Type u_1) : Type u_1

Elementary instructions counted by the protocol's gate model.

• cnot {ι : Type u_1} (control target : ι) : Instruction ι
• phase {ι : Type u_1} (site : ι) : Instruction ι
• hadamard {ι : Type u_1} (site : ι) : Instruction ι

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.ExactResources.RoundOutcome (ι : Type u_1) : Type u_1

The classical difference and correction coin recorded for one round.

Equations

• LeanPool.SingleCopyStabilizer.ExactResources.RoundOutcome ι = (LeanPool.SingleCopyStabilizer.BinaryVec ι × ZMod 2)

def LeanPool.SingleCopyStabilizer.ExactResources.cnotTargets {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (pivot : ι) : Finset ι

Actual targets in the simultaneous pivot-controlled CNOT circuit.

Equations

• LeanPool.SingleCopyStabilizer.ExactResources.cnotTargets u pivot = {j : ι | j ≠ pivot ∧ u j = 1}

theorem LeanPool.SingleCopyStabilizer.ExactResources.cnotTargets_card_add_one_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : BinaryVec ι) (pivot : ι) : (cnotTargets u pivot).card + 1 ≤ Fintype.card ι

The pivot itself is never a CNOT target.

noncomputable def LeanPool.SingleCopyStabilizer.ExactResources.roundInstructions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : RoundOutcome ι) : List (Instruction ι)

In chronological order: the pivot CNOTs, optional S, then H. A zero computational difference appends no gates.

Equations

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

noncomputable def LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : RoundOutcome ι) : ℕ

Gate cost is the length of the actual symbolic instruction list.

Equations

• LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount outcome = (LeanPool.SingleCopyStabilizer.ExactResources.roundInstructions outcome).length

@[simp]

theorem LeanPool.SingleCopyStabilizer.ExactResources.roundInstructions_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ZMod 2) : roundInstructions (0, b) = []

@[simp]

theorem LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ZMod 2) : roundGateCount (0, b) = 0

theorem LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : RoundOutcome ι) (hzero : outcome.1 ≠ 0) : roundGateCount outcome = (cnotTargets outcome.1 (binaryPivot outcome.1 hzero)).card + 1 + if outcome.2 = 0 then 0 else 1

The nonzero branch has exactly the chosen CNOTs, one H, and at most one S.

theorem LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : RoundOutcome ι) : roundGateCount outcome ≤ Fintype.card ι + 1

One round appends at most n+1 gates, including both possible corrections.

noncomputable def LeanPool.SingleCopyStabilizer.ExactResources.circuitInstructions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) : List (Instruction ι)

The accumulated circuit appends each round's instructions in order.

Equations

• LeanPool.SingleCopyStabilizer.ExactResources.circuitInstructions outcomes = List.flatMap LeanPool.SingleCopyStabilizer.ExactResources.roundInstructions outcomes

noncomputable def LeanPool.SingleCopyStabilizer.ExactResources.listCircuitGateCount {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) : ℕ

The accumulated gate count is the sum of all appended round costs.

Equations

• LeanPool.SingleCopyStabilizer.ExactResources.listCircuitGateCount outcomes = (List.map LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount outcomes).sum

theorem LeanPool.SingleCopyStabilizer.ExactResources.circuitInstructions_length {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) : (circuitInstructions outcomes).length = listCircuitGateCount outcomes

The sum-based cost equals the length of the actual flattened gate list.

theorem LeanPool.SingleCopyStabilizer.ExactResources.listCircuitGateCount_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) : listCircuitGateCount outcomes ≤ (Fintype.card ι + 1) * outcomes.length

A circuit accumulated over T rounds has at most (n+1)T gates.

theorem LeanPool.SingleCopyStabilizer.ExactResources.prefixCircuitGateCount_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) (t : ℕ) : listCircuitGateCount (List.take t outcomes) ≤ (Fintype.card ι + 1) * t

Prefix circuits have a gate count linear in the prefix index.

noncomputable def LeanPool.SingleCopyStabilizer.ExactResources.protocolGateCost {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) : ℕ

Total gate applications: execute the current prefix twice in every round, then execute the complete circuit once for the final computational readout.

Equations

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

theorem LeanPool.SingleCopyStabilizer.ExactResources.twice_prefix_sum_add (T : ℕ) : 2 * ∑ t ∈ Finset.range T, t + T = T ^ 2

Twice the triangular sum plus its endpoint equals the square.

theorem LeanPool.SingleCopyStabilizer.ExactResources.protocolGateCost_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) : protocolGateCost outcomes ≤ (Fintype.card ι + 1) * outcomes.length ^ 2

Total quantum gate applications are at most (n+1)T², for every possible outcome history, including unsuccessful histories.

theorem LeanPool.SingleCopyStabilizer.ExactResources.protocolGateCost_le_two_n {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) (hn : 1 ≤ Fintype.card ι) : protocolGateCost outcomes ≤ 2 * Fintype.card ι * outcomes.length ^ 2

For at least one qubit this is the explicit 2nT² gate-resource bound.

theorem LeanPool.SingleCopyStabilizer.ExactResources.roundGateCount_of_zero_qubits {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcome : RoundOutcome ι) (hn : Fintype.card ι = 0) : roundGateCount outcome = 0

A zero-qubit register can produce no nonzero difference and appends no gates.

theorem LeanPool.SingleCopyStabilizer.ExactResources.listCircuitGateCount_of_zero_qubits {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) (hn : Fintype.card ι = 0) : listCircuitGateCount outcomes = 0

The full symbolic circuit is empty on a zero-qubit register.

theorem LeanPool.SingleCopyStabilizer.ExactResources.protocolGateCost_of_zero_qubits {ι : Type u_1} [Fintype ι] [DecidableEq ι] (outcomes : List (RoundOutcome ι)) (hn : Fintype.card ι = 0) : protocolGateCost outcomes = 0

Zero-qubit executions require no gates, regardless of the round count.

def LeanPool.SingleCopyStabilizer.ExactResources.protocolCopyCount {ι : Type u_1} (outcomes : List (RoundOutcome ι)) : ℕ

Every round consumes two input copies, and final readout consumes one. Even rounds whose difference is zero consume their two measurement copies.

Equations

• LeanPool.SingleCopyStabilizer.ExactResources.protocolCopyCount outcomes = 2 * outcomes.length + 1

@[simp]

theorem LeanPool.SingleCopyStabilizer.ExactResources.protocolCopyCount_nil {ι : Type u_1} : protocolCopyCount [] = 1

theorem LeanPool.SingleCopyStabilizer.ExactResources.protocolCopyCount_cons {ι : Type u_1} (outcome : RoundOutcome ι) (outcomes : List (RoundOutcome ι)) : protocolCopyCount (outcome :: outcomes) = protocolCopyCount outcomes + 2

Appending a round always consumes exactly two additional copies.

theorem LeanPool.SingleCopyStabilizer.ExactResources.protocolCopyCount_eq {ι : Type u_1} (outcomes : List (RoundOutcome ι)) (T : ℕ) (hT : outcomes.length = T) : protocolCopyCount outcomes = 2 * T + 1

The protocol's exact total copy count.