Remark 14: Parallel Gauging Measurement

Statement

The gauging measurement (Definition 5) can be applied to multiple logical operators in parallel, subject to compatibility conditions:

1. Non-overlapping support: If logical operators L₁, …, Lₘ have disjoint supports, they can be gauged simultaneously with independent graphs G₁, …, Gₘ.

2. Same-type overlapping support: If Lᵢ and Lⱼ share support where both act by the same Pauli type on every shared qubit, they can be gauged in parallel.

3. LDPC constraint: At most a constant number of logical operators should share support on any single qubit to maintain the LDPC property.

4. Time-space tradeoff: Measuring 2m-1 copies in parallel with ⌈d/m⌉ rounds and majority vote trades time for space.

Main Results

• DisjointSupports : definition of disjoint support condition
• SameTypeOverlap : definition of same-type overlap condition
• ParallelLDPCBound : definition of the LDPC qubit-degree bound
• disjoint_supports_imply_commutation : disjoint Pauli operators commute
• sameType_overlap_implies_commutation : same-type overlap implies commutation
• parallel_qubit_degree_bound : LDPC qubit degree bound under parallel gauging
• time_space_tradeoff_summary : combined time-space tradeoff properties
• majority_vote_correct : majority vote over 2m-1 copies gives correct outcome

Part 1: Non-overlapping support — Disjoint supports imply commutation

def ParallelGaugingMeasurement.DisjointSupports {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) : Prop

Two Pauli operators have disjoint supports if no qubit belongs to both supports.

Equations

• ParallelGaugingMeasurement.DisjointSupports P Q = Disjoint P.support Q.support

def ParallelGaugingMeasurement.PairwiseDisjointSupports {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) : Prop

A family of logical operators has pairwise disjoint supports.

Equations

• ParallelGaugingMeasurement.PairwiseDisjointSupports ops = ∀ (i j : Fin m), i ≠ j → ParallelGaugingMeasurement.DisjointSupports (ops i) (ops j)

theorem ParallelGaugingMeasurement.disjoint_supports_imply_commutation {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (h : DisjointSupports P Q) : P.PauliCommute Q

Operators with disjoint supports commute: if P and Q act on disjoint qubits, their symplectic inner product vanishes.

theorem ParallelGaugingMeasurement.pairwise_disjoint_implies_pairwise_commute {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (h : PairwiseDisjointSupports ops) (i j : Fin m) : (ops i).PauliCommute (ops j)

Multiple operators with pairwise disjoint supports all pairwise commute.

theorem ParallelGaugingMeasurement.disjointSupports_comm {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) : DisjointSupports P Q ↔ DisjointSupports Q P

Disjoint supports are symmetric.

theorem ParallelGaugingMeasurement.disjointSupports_one {V : Type u_1} [Fintype V] [DecidableEq V] (P : PauliOp V) : DisjointSupports P 1

Disjoint supports with identity.

Part 2: Same-type overlapping support

def ParallelGaugingMeasurement.SameTypeXOverlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) : Prop

Two Pauli operators have same-type X overlap if on every shared support qubit, both have X-type action (xVec ≠ 0) and neither has Z-type action (zVec = 0).

Equations

• ParallelGaugingMeasurement.SameTypeXOverlap P Q = ∀ v ∈ P.support, v ∈ Q.support → P.zVec v = 0 ∧ Q.zVec v = 0

def ParallelGaugingMeasurement.SameTypeZOverlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) : Prop

Two Pauli operators have same-type Z overlap if on every shared support qubit, both have Z-type action (zVec ≠ 0) and neither has X-type action (xVec = 0).

Equations

• ParallelGaugingMeasurement.SameTypeZOverlap P Q = ∀ v ∈ P.support, v ∈ Q.support → P.xVec v = 0 ∧ Q.xVec v = 0

def ParallelGaugingMeasurement.SameTypeOverlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) : Prop

Two Pauli operators have same-type overlap if on every shared support qubit, both act by the same Pauli type (both X or both Z). Equivalently: on shared qubits, either both have zero Z-component or both have zero X-component.

Equations

• ParallelGaugingMeasurement.SameTypeOverlap P Q = ∀ v ∈ P.support, v ∈ Q.support → P.zVec v = 0 ∧ Q.zVec v = 0 ∨ P.xVec v = 0 ∧ Q.xVec v = 0

theorem ParallelGaugingMeasurement.sameTypeXOverlap_implies_sameTypeOverlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (h : SameTypeXOverlap P Q) : SameTypeOverlap P Q

Same-type X overlap implies same-type overlap.

theorem ParallelGaugingMeasurement.sameTypeZOverlap_implies_sameTypeOverlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (h : SameTypeZOverlap P Q) : SameTypeOverlap P Q

Same-type Z overlap implies same-type overlap.

theorem ParallelGaugingMeasurement.disjointSupports_implies_sameTypeOverlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (h : DisjointSupports P Q) : SameTypeOverlap P Q

Disjoint supports imply same-type overlap vacuously.

theorem ParallelGaugingMeasurement.sameType_overlap_implies_commutation {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (h : SameTypeOverlap P Q) : P.PauliCommute Q

Same-type overlap implies commutation: if P and Q share support only with the same Pauli type on each shared qubit, their symplectic inner product vanishes (each shared qubit contributes 0 to the sum).

theorem ParallelGaugingMeasurement.gaussLaw_pure_X_type {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (GaussFlux.gaussLawOp G v).zVec = 0

The Gauss's law operator A_v is pure X-type, so any pure X-type logical operator has same-type X overlap with it on the extended system.

theorem ParallelGaugingMeasurement.pure_X_sameType_overlap {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hP : P.zVec = 0) (hQ : Q.zVec = 0) : SameTypeXOverlap P Q

For a pure X-type operator (zVec = 0), same-type X overlap with any other pure X-type operator holds automatically.

theorem ParallelGaugingMeasurement.pure_X_commute {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hP : P.zVec = 0) (hQ : Q.zVec = 0) : P.PauliCommute Q

Pure X-type operators commute (special case of same-type overlap).

theorem ParallelGaugingMeasurement.pure_Z_commute {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hP : P.xVec = 0) (hQ : Q.xVec = 0) : P.PauliCommute Q

Pure Z-type operators commute (special case of same-type overlap).

Part 3: LDPC constraint for parallel gauging

def ParallelGaugingMeasurement.qubitParticipationCount {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (v : V) : ℕ

The qubit participation count for parallel gauging: the number of logical operators (from a family) whose support contains qubit v.

Equations

• ParallelGaugingMeasurement.qubitParticipationCount ops v = {i : Fin m | v ∈ (ops i).support}.card

def ParallelGaugingMeasurement.ParallelLDPCBound {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (c : ℕ) : Prop

The LDPC bound for parallel gauging: each qubit participates in at most c logical operators' supports.

Equations

• ParallelGaugingMeasurement.ParallelLDPCBound ops c = ∀ (v : V), ParallelGaugingMeasurement.qubitParticipationCount ops v ≤ c

theorem ParallelGaugingMeasurement.disjoint_participation_le_one {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (h : PairwiseDisjointSupports ops) (v : V) : qubitParticipationCount ops v ≤ 1

For disjoint supports, the participation count is at most 1.

theorem ParallelGaugingMeasurement.disjoint_implies_LDPC_bound {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (h : PairwiseDisjointSupports ops) : ParallelLDPCBound ops 1

Disjoint supports trivially satisfy the LDPC bound with c = 1.

theorem ParallelGaugingMeasurement.participation_le_total {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (v : V) : qubitParticipationCount ops v ≤ m

The participation count is bounded by the total number of operators.

theorem ParallelGaugingMeasurement.sum_participation_eq_sum_support {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) : ∑ v : V, qubitParticipationCount ops v = ∑ i : Fin m, (ops i).support.card

The sum of participation counts equals the sum of support sizes.

theorem ParallelGaugingMeasurement.parallel_qubit_degree_bound {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (c : ℕ) (hbound : ParallelLDPCBound ops c) (v : V) : qubitParticipationCount ops v ≤ c

When the LDPC bound holds with constant c, the contribution of each qubit to the total check degree of the deformed code from parallel gauging is bounded.

Part 4: Time-space tradeoff

def ParallelGaugingMeasurement.numCopies (m : ℕ) : ℕ

The number of parallel copies in the time-space tradeoff: 2m - 1 for m ≥ 1. Each copy is an equivalent logical representative with its own gauging graph.

Equations

• ParallelGaugingMeasurement.numCopies m = 2 * m - 1

def ParallelGaugingMeasurement.numRounds (d m : ℕ) : ℕ

The number of rounds in the time-space tradeoff: ⌈d/m⌉ for distance d and parameter m. This is the ceiling division.

Equations

• ParallelGaugingMeasurement.numRounds d m = (d + m - 1) / m

@[simp]

theorem ParallelGaugingMeasurement.numCopies_one : numCopies 1 = 1

numCopies 1 = 1: no parallelism, standard case.

@[simp]

theorem ParallelGaugingMeasurement.numRounds_one (d : ℕ) : numRounds d 1 = d

numRounds d 1 = d: no parallelism, standard number of rounds.

theorem ParallelGaugingMeasurement.numCopies_pos {m : ℕ} (hm : 1 ≤ m) : 1 ≤ numCopies m

numCopies is always positive for m ≥ 1.

theorem ParallelGaugingMeasurement.numCopies_odd {m : ℕ} (hm : 1 ≤ m) : ¬2 ∣ numCopies m

numCopies is odd: 2m - 1 is always odd for m ≥ 1.

theorem ParallelGaugingMeasurement.numRounds_pos {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : 0 < numRounds d m

numRounds is always positive when d > 0 and m > 0.

theorem ParallelGaugingMeasurement.numRounds_le {d m : ℕ} (hm : 1 ≤ m) : numRounds d m ≤ d

numRounds is at most d (we never need more rounds than the original).

theorem ParallelGaugingMeasurement.tradeoff_total_work_ge {d m : ℕ} (hm : 1 ≤ m) : d ≤ numCopies m * numRounds d m

The key tradeoff: numCopies * numRounds ≥ d.

theorem ParallelGaugingMeasurement.qubit_overhead_factor (n m : ℕ) (_hm : 1 ≤ m) : numCopies m * n = (2 * m - 1) * n

The qubit overhead factor: using 2m-1 copies multiplies the qubit count.

theorem ParallelGaugingMeasurement.numCopies_monotone {m₁ m₂ : ℕ} (hm : m₁ ≤ m₂) : numCopies m₁ ≤ numCopies m₂

As m increases, numCopies increases (monotonicity).

theorem ParallelGaugingMeasurement.numRounds_antitone {d m₁ m₂ : ℕ} (hm : m₁ ≤ m₂) (hm₁ : 0 < m₁) : numRounds d m₂ ≤ numRounds d m₁

numRounds is antitonically related to m for fixed d: larger m means fewer rounds.

Majority vote correctness

def ParallelGaugingMeasurement.majorityThreshold (m : ℕ) : ℕ

The majority vote threshold: more than half of 2m-1 copies must agree.

Equations

• ParallelGaugingMeasurement.majorityThreshold m = m

theorem ParallelGaugingMeasurement.majorityThreshold_gt_half {m : ℕ} (hm : 1 ≤ m) : 2 * majorityThreshold m > numCopies m

The majority threshold is always a strict majority of numCopies.

theorem ParallelGaugingMeasurement.majorityThreshold_le_copies {m : ℕ} (hm : 1 ≤ m) : majorityThreshold m ≤ numCopies m

The majority threshold is at most numCopies.

theorem ParallelGaugingMeasurement.majority_vote_correct (m : ℕ) (hm : 1 ≤ m) (agree total : ℕ) (htotal : total = numCopies m) (hagree : m ≤ agree) (hle : agree ≤ total) : 2 * agree > total

If at least m out of 2m-1 copies give outcome σ, the majority vote returns σ. Here we prove the combinatorial fact: a set of at least m elements out of 2m-1 total constitutes a strict majority.

theorem ParallelGaugingMeasurement.minority_vote_bound (m : ℕ) (hm : 1 ≤ m) (agree total : ℕ) (htotal : total = numCopies m) (hagree : m ≤ agree) (hle : agree ≤ total) : total - agree < m

The complement: if at least m out of 2m-1 agree, the minority has fewer than m.

Combined properties

theorem ParallelGaugingMeasurement.disjoint_parallel_gauging_compatible {V : Type u_1} [Fintype V] [DecidableEq V] {m : ℕ} (ops : Fin m → PauliOp V) (h : PairwiseDisjointSupports ops) : (∀ (i j : Fin m), (ops i).PauliCommute (ops j)) ∧ ParallelLDPCBound ops 1

Summary: for pairwise disjoint supports, all conditions for parallel gauging are automatically satisfied (commutation + LDPC with c = 1).

theorem ParallelGaugingMeasurement.time_space_tradeoff_summary (d n m : ℕ) (hm : 1 ≤ m) : numCopies m * n = (2 * m - 1) * n ∧ numRounds d m ≤ d ∧ d ≤ numCopies m * numRounds d m

For any m ≥ 1, the time-space tradeoff reduces rounds from d to ⌈d/m⌉ at the cost of (2m-1) copies.

theorem ParallelGaugingMeasurement.no_parallelism_case (d n : ℕ) : numCopies 1 * n = n ∧ numRounds d 1 = d

Special case: m = 1 (no parallelism). One copy, d rounds.

theorem ParallelGaugingMeasurement.max_parallelism_case (d : ℕ) (hd : 1 ≤ d) : numRounds d d = 1 ∧ numCopies d = 2 * d - 1

Special case: m = d (maximum parallelism). 2d-1 copies, 1 round.

theorem ParallelGaugingMeasurement.overhead_additional_copies (m : ℕ) (hm : 1 ≤ m) : numCopies m - 1 = 2 * (m - 1)

The overhead ratio: additional copies are 2(m-1).