Rem_10: Parallelization of Gauging Measurements

Statement

The gauging measurement can be applied to multiple logical operators in parallel, provided that:

1. Commutativity: No pair of logical operators being measured simultaneously act on a common qubit via different non-trivial Pauli operators (e.g., one acts by $X$ and another by $Z$ on the same qubit).

2. Bounded overlap: To maintain an LDPC code during code deformation, only a constant number of logical operators being measured share support on any single qubit.

For codes supporting many disjoint logical representatives, this offers highly parallelized logical gates. Additionally, one can trade space overhead for time overhead by performing $2m-1$ measurements of equivalent logical operators in parallel for $d/m$ rounds and taking a majority vote to determine the classical outcome.

Main Definitions

• PauliCompatible: Two logical operators are Pauli-compatible on a qubit
• CommutativityCondition: No pair acts differently on a common qubit (Condition 1)
• BoundedOverlapCondition: At most k operators share any qubit (Condition 2)
• ParallelizableLogicals: A set of logicals satisfying both conditions
• SpaceTimeTradeoff: The space-time tradeoff parameters

Main Results

• parallel_measurement_conditions: The two conditions for parallel measurement
• disjoint_logicals_parallelizable: Disjoint logicals trivially satisfy parallelizability
• majority_vote_rounds: The number of rounds for majority voting is d/m
• total_parallel_measurements: Total parallel measurements is 2m-1

Pauli Compatibility Condition

def QEC1.StabPauliType.compatible (p q : StabPauliType) : Prop

Two Pauli types are compatible if they don't conflict on the same qubit. A conflict occurs when one acts as purely X-type and the other as purely Z-type. (e.g., X and Z conflict, but X and X are compatible, I and anything is compatible)

Compatible means: NOT (one is purely X-type AND the other is purely Z-type).

Equations

• QEC1.StabPauliType.compatible p q = (¬(p = StabPauliType.X ∧ q = StabPauliType.Z) ∧ ¬(p = StabPauliType.Z ∧ q = StabPauliType.X))

theorem QEC1.StabPauliType.X_Z_not_compatible : ¬compatible StabPauliType.X StabPauliType.Z

X and Z are incompatible

theorem QEC1.StabPauliType.Z_X_not_compatible : ¬compatible StabPauliType.Z StabPauliType.X

Z and X are incompatible

theorem QEC1.StabPauliType.self_compatible (p : StabPauliType) : compatible p p

Same Pauli types are always compatible

theorem QEC1.StabPauliType.I_compatible_left (p : StabPauliType) : compatible StabPauliType.I p

Identity is compatible with everything

theorem QEC1.StabPauliType.I_compatible_right (p : StabPauliType) : compatible p StabPauliType.I

theorem QEC1.StabPauliType.compatible_comm (p q : StabPauliType) : compatible p q ↔ compatible q p

Compatibility is symmetric

Condition 1: Commutativity (Pauli Compatibility on Shared Qubits)

def QEC1.PauliCompatible {n : ℕ} (P Q : PauliOp n) : Prop

Two Pauli operators are Pauli-compatible if for every qubit where both act nontrivially, their Pauli types are compatible (i.e., not one X-type and one Z-type).

Equations

• QEC1.PauliCompatible P Q = ∀ (i : Fin n), QEC1.StabPauliType.compatible (P.paulis i) (Q.paulis i)

theorem QEC1.PauliCompatible.symmetric {n : ℕ} {P Q : PauliOp n} (h : PauliCompatible P Q) : PauliCompatible Q P

Pauli compatibility implies the operators can be measured in parallel without conflict

theorem QEC1.PauliCompatible.identity_left {n : ℕ} (P : PauliOp n) : PauliCompatible (PauliOp.identity n) P

The identity operator is compatible with any operator

theorem QEC1.PauliCompatible.identity_right {n : ℕ} (P : PauliOp n) : PauliCompatible P (PauliOp.identity n)

def QEC1.CommutativityCondition {C : StabilizerCode} (logicals : Finset (LogicalOp C)) : Prop

Commutativity Condition for parallel gauging measurement: A set of logical operators satisfies the commutativity condition if every pair is Pauli-compatible on their shared support.

Equations

• QEC1.CommutativityCondition logicals = ∀ L₁ ∈ logicals, ∀ L₂ ∈ logicals, QEC1.PauliCompatible L₁.op L₂.op

theorem QEC1.CommutativityCondition.singleton {C : StabilizerCode} (L : LogicalOp C) : CommutativityCondition {L}

Singleton sets trivially satisfy commutativity

Condition 2: Bounded Overlap

def QEC1.overlapDegree {C : StabilizerCode} (logicals : Finset (LogicalOp C)) (i : Fin C.n) : ℕ

The overlap degree of a qubit with respect to a set of operators: how many operators in the set have support on this qubit.

Equations

• QEC1.overlapDegree logicals i = {L ∈ logicals | i ∈ L.op.support}.card

def QEC1.BoundedOverlapCondition {C : StabilizerCode} (logicals : Finset (LogicalOp C)) (k : ℕ) : Prop

Bounded Overlap Condition: At most k logical operators share support on any single qubit. This is required to maintain LDPC property during code deformation.

Equations

• QEC1.BoundedOverlapCondition logicals k = ∀ (i : Fin C.n), QEC1.overlapDegree logicals i ≤ k

theorem QEC1.BoundedOverlapCondition.of_card_le {C : StabilizerCode} (logicals : Finset (LogicalOp C)) (k : ℕ) (h : logicals.card ≤ k) : BoundedOverlapCondition logicals k

If k ≥ |logicals|, the bounded overlap condition is trivially satisfied

theorem QEC1.BoundedOverlapCondition.singleton {C : StabilizerCode} (L : LogicalOp C) : BoundedOverlapCondition {L} 1

Singleton sets have overlap degree at most 1

Parallelizable Logicals

structure QEC1.ParallelizableLogicals (C : StabilizerCode) : Type

A set of logical operators is parallelizable if it satisfies both conditions:

1. Commutativity: no pair acts differently (X vs Z) on a common qubit
2. Bounded overlap: at most k operators share any qubit

The bound k must be constant to maintain LDPC property.

• logicals : Finset (LogicalOp C)

  The set of logical operators to measure in parallel

• overlapBound : ℕ

  The bound on overlap degree (must be constant for LDPC)

• commutativity : CommutativityCondition self.logicals

  Condition 1: Commutativity

• boundedOverlap : BoundedOverlapCondition self.logicals self.overlapBound

  Condition 2: Bounded overlap

def QEC1.ParallelizableLogicals.numLogicals {C : StabilizerCode} (P : ParallelizableLogicals C) : ℕ

The number of logical operators being measured in parallel

Equations

• P.numLogicals = P.logicals.card

def QEC1.ParallelizableLogicals.singleton {C : StabilizerCode} (L : LogicalOp C) : ParallelizableLogicals C

Any single logical operator is trivially parallelizable

Equations

• QEC1.ParallelizableLogicals.singleton L = { logicals := {L}, overlapBound := 1, commutativity := ⋯, boundedOverlap := ⋯ }

@[simp]

theorem QEC1.ParallelizableLogicals.singleton_numLogicals {C : StabilizerCode} (L : LogicalOp C) : (singleton L).numLogicals = 1

Disjoint Logicals

def QEC1.DisjointSupport {C : StabilizerCode} (L₁ L₂ : LogicalOp C) : Prop

Two logical operators have disjoint support if they share no qubits.

Equations

• QEC1.DisjointSupport L₁ L₂ = Disjoint L₁.op.support L₂.op.support

def QEC1.PairwiseDisjointSupport {C : StabilizerCode} (logicals : Finset (LogicalOp C)) : Prop

A set of logicals has pairwise disjoint support if every pair is disjoint.

Equations

• QEC1.PairwiseDisjointSupport logicals = ∀ L₁ ∈ logicals, ∀ L₂ ∈ logicals, L₁ ≠ L₂ → QEC1.DisjointSupport L₁ L₂

theorem QEC1.DisjointSupport.pauli_compatible {C : StabilizerCode} {L₁ L₂ : LogicalOp C} (h : DisjointSupport L₁ L₂) : PauliCompatible L₁.op L₂.op

Disjoint operators are Pauli-compatible (vacuously, no shared qubit).

theorem QEC1.PairwiseDisjointSupport.commutativity {C : StabilizerCode} {logicals : Finset (LogicalOp C)} (h : PairwiseDisjointSupport logicals) : CommutativityCondition logicals

Pairwise disjoint logicals satisfy the commutativity condition.

theorem QEC1.PairwiseDisjointSupport.overlap_degree_le_one {C : StabilizerCode} {logicals : Finset (LogicalOp C)} (h : PairwiseDisjointSupport logicals) : BoundedOverlapCondition logicals 1

Pairwise disjoint logicals have overlap degree at most 1 everywhere.

def QEC1.ParallelizableLogicals.fromDisjoint {C : StabilizerCode} (logicals : Finset (LogicalOp C)) (h : PairwiseDisjointSupport logicals) : ParallelizableLogicals C

Disjoint logicals are parallelizable: codes with many disjoint logical representatives can perform highly parallelized logical gates.

Equations

• QEC1.ParallelizableLogicals.fromDisjoint logicals h = { logicals := logicals, overlapBound := 1, commutativity := ⋯, boundedOverlap := ⋯ }

theorem QEC1.disjoint_logicals_parallelizable {C : StabilizerCode} (logicals : Finset (LogicalOp C)) (h : PairwiseDisjointSupport logicals) : ∃ (P : ParallelizableLogicals C), P.logicals = logicals ∧ P.overlapBound = 1

Space-Time Tradeoff

structure QEC1.SpaceTimeTradeoff : Type

Space-Time Tradeoff for the gauging measurement.

One can trade space overhead for time overhead:

• Perform 2m-1 measurements of equivalent logical operators in parallel
• For d/m rounds
• Take a majority vote to determine the classical outcome

Parameters:

• d: the code distance
• m: the tradeoff parameter (divides d)
• The number of parallel equivalent measurements is 2m-1
• The number of rounds is d/m

• distance : ℕ

  Code distance

• m : ℕ

  Tradeoff parameter

• m_pos : self.m > 0

  m must be positive

• m_divides_d : self.m ∣ self.distance

  m divides d (for clean arithmetic)

def QEC1.SpaceTimeTradeoff.numParallelMeasurements (T : SpaceTimeTradeoff) : ℕ

Number of parallel measurements of equivalent logical operators: 2m - 1

Equations

• T.numParallelMeasurements = 2 * T.m - 1

def QEC1.SpaceTimeTradeoff.numRounds (T : SpaceTimeTradeoff) : ℕ

Number of rounds for the measurement: d/m

Equations

• T.numRounds = T.distance / T.m

theorem QEC1.SpaceTimeTradeoff.numRounds_mul_m (T : SpaceTimeTradeoff) : T.numRounds * T.m = T.distance

When m divides d, numRounds * m = d

def QEC1.SpaceTimeTradeoff.majorityThreshold (T : SpaceTimeTradeoff) : ℕ

The majority vote threshold: more than half of 2m-1 measurements, i.e., at least m

Equations

• T.majorityThreshold = T.m

theorem QEC1.SpaceTimeTradeoff.majorityThreshold_eq (T : SpaceTimeTradeoff) : T.majorityThreshold = (T.numParallelMeasurements + 1) / 2

Majority threshold is exactly half of 2m-1 rounded up

def QEC1.SpaceTimeTradeoff.totalMeasurements (T : SpaceTimeTradeoff) : ℕ

Total logical measurements across all rounds

Equations

• T.totalMeasurements = T.numParallelMeasurements * T.numRounds

theorem QEC1.SpaceTimeTradeoff.totalMeasurements_eq (T : SpaceTimeTradeoff) : T.totalMeasurements = (2 * T.m - 1) * (T.distance / T.m)

The total measurements formula: (2m-1) * (d/m)

Special cases

def QEC1.SpaceTimeTradeoff.minSpace (d : ℕ) (hd : d > 0) : SpaceTimeTradeoff

Minimal space overhead: m = d, giving 2d-1 parallel measurements in 1 round

Equations

• QEC1.SpaceTimeTradeoff.minSpace d hd = { distance := d, m := d, m_pos := hd, m_divides_d := ⋯ }

@[simp]

theorem QEC1.SpaceTimeTradeoff.minSpace_numParallel (d : ℕ) (hd : d > 0) : (minSpace d hd).numParallelMeasurements = 2 * d - 1

@[simp]

theorem QEC1.SpaceTimeTradeoff.minSpace_numRounds (d : ℕ) (hd : d > 0) : (minSpace d hd).numRounds = 1

def QEC1.SpaceTimeTradeoff.minTime (d : ℕ) (_hd : d > 0) : SpaceTimeTradeoff

Minimal time overhead: m = 1, giving 1 parallel measurement in d rounds

Equations

• QEC1.SpaceTimeTradeoff.minTime d _hd = { distance := d, m := 1, m_pos := Nat.one_pos, m_divides_d := ⋯ }

@[simp]

theorem QEC1.SpaceTimeTradeoff.minTime_numParallel (d : ℕ) (hd : d > 0) : (minTime d hd).numParallelMeasurements = 1

@[simp]

theorem QEC1.SpaceTimeTradeoff.minTime_numRounds (d : ℕ) (_hd : d > 0) : (minTime d _hd).numRounds = d

Combined Parallelization Theorem

theorem QEC1.parallel_measurement_conditions {C : StabilizerCode} (logicals : Finset (LogicalOp C)) (k : ℕ) : CommutativityCondition logicals ∧ BoundedOverlapCondition logicals k ↔ ∃ (P : ParallelizableLogicals C), P.logicals = logicals ∧ P.overlapBound = k

The parallelization theorem: gauging measurement can be applied to multiple logical operators in parallel if and only if both conditions are satisfied.

Condition 1 (Commutativity): No pair acts by different non-trivial Paulis on any qubit. Condition 2 (Bounded Overlap): At most k operators share support on any qubit.

This theorem captures the main claim of Rem_10.

Majority Vote Correctness

theorem QEC1.numParallelMeasurements_odd (T : SpaceTimeTradeoff) : Odd T.numParallelMeasurements

For the space-time tradeoff: (2m-1) is always odd, ensuring a clear majority.

theorem QEC1.majority_vote_no_tie (T : SpaceTimeTradeoff) : T.numParallelMeasurements % 2 = 1

The majority vote always gives a definite outcome (no ties possible).

Summary

The parallelization remark establishes:

1. Commutativity Condition: For parallel measurement, no pair of logical operators should act on a common qubit via different non-trivial Paulis (e.g., X vs Z).

2. Bounded Overlap Condition: To maintain LDPC property during code deformation, at most a constant number of logicals can share support on any single qubit.

3. Disjoint Representatives: Codes with many disjoint logical representatives naturally satisfy both conditions (overlap degree 1).

4. Space-Time Tradeoff: One can trade space for time:

   • 2m-1 parallel measurements of equivalent logicals
   • d/m rounds of measurement
   • Majority vote determines the classical outcome