Rem_2: Graph Convention

Statement

Given a connected graph $G = (V_G, E_G)$ with vertex set $V_G$ and edge set $E_G$, we identify the vertices of $G$ with the qubits in the support of the logical operator $L$. For each edge $e \in E_G$, we introduce an auxiliary 'gauge qubit' initialized in the state $|0\rangle_e$. The graph $G$ may also include additional 'dummy vertices' beyond the qubits in the support of $L$. For each dummy vertex $v$, we add an auxiliary qubit initialized in the $|+\rangle$ state and gauge the operator $L \cdot X_v$. These dummy vertices have no effect on the gauging measurement outcome since measuring $X_v$ on a $|+\rangle$ state always returns $+1$.

Main Definitions

• GaugingGraphConvention : The convention for a gauging graph relating G to logical operator L
• QubitType : Classification of qubits (logical, edge, dummy)
• InitialState : The initial quantum state for each qubit type
• DummyVertexMeasurementOutcome : The measurement outcome for dummy vertices is always +1

Key Properties

• vertex_qubit_correspondence : Vertices are identified with logical support qubits
• edge_qubit_initialization : Edge qubits are initialized in |0⟩
• dummy_vertex_initialization : Dummy qubits are initialized in |+⟩
• dummy_measurement_always_plus_one : Measuring X on |+⟩ always returns +1

Qubit Types in the Gauging Protocol

inductive QubitType : Type

The different types of qubits involved in the gauging measurement protocol

• LogicalSupport : QubitType

  Original code qubits in the support of L

• EdgeQubit : QubitType

  Auxiliary gauge qubits on edges, initialized in |0⟩

• DummyQubit : QubitType

  Auxiliary qubits for dummy vertices, initialized in |+⟩

instance instDecidableEqQubitType : DecidableEq QubitType

Equations

• instDecidableEqQubitType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprQubitType.repr : QubitType → ℕ → Std.Format

Equations

• instReprQubitType.repr QubitType.LogicalSupport prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QubitType.LogicalSupport")).group prec✝
• instReprQubitType.repr QubitType.EdgeQubit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QubitType.EdgeQubit")).group prec✝
• instReprQubitType.repr QubitType.DummyQubit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QubitType.DummyQubit")).group prec✝

instance instReprQubitType : Repr QubitType

Equations

• instReprQubitType = { reprPrec := instReprQubitType.repr }

inductive QubitType.InitialState : Type

The initial state for each qubit type

• zero : InitialState

  The |0⟩ state (computational basis zero)

• plus : InitialState

  The |+⟩ state ((|0⟩ + |1⟩)/√2)

• encoded : InitialState

  Unspecified (for logical qubits, depends on encoded state)

instance QubitType.instDecidableEqInitialState : DecidableEq InitialState

Equations

• QubitType.instDecidableEqInitialState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def QubitType.instReprInitialState.repr : InitialState → ℕ → Std.Format

Equations

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

instance QubitType.instReprInitialState : Repr InitialState

Equations

• QubitType.instReprInitialState = { reprPrec := QubitType.instReprInitialState.repr }

def QubitType.initialState : QubitType → InitialState

The initial state for each qubit type in the gauging protocol

Equations

• QubitType.LogicalSupport.initialState = QubitType.InitialState.encoded
• QubitType.EdgeQubit.initialState = QubitType.InitialState.zero
• QubitType.DummyQubit.initialState = QubitType.InitialState.plus

@[simp]

theorem QubitType.logicalSupport_initialState : LogicalSupport.initialState = InitialState.encoded

@[simp]

theorem QubitType.edgeQubit_initialState : EdgeQubit.initialState = InitialState.zero

@[simp]

theorem QubitType.dummyQubit_initialState : DummyQubit.initialState = InitialState.plus

Measurement Outcomes

inductive GraphMeasurementOutcome : Type

Possible measurement outcomes for X-basis measurements

• plus : GraphMeasurementOutcome

  Outcome +1

• minus : GraphMeasurementOutcome

  Outcome -1

instance instDecidableEqGraphMeasurementOutcome : DecidableEq GraphMeasurementOutcome

Equations

• instDecidableEqGraphMeasurementOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprGraphMeasurementOutcome.repr : GraphMeasurementOutcome → ℕ → Std.Format

Equations

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

instance instReprGraphMeasurementOutcome : Repr GraphMeasurementOutcome

Equations

• instReprGraphMeasurementOutcome = { reprPrec := instReprGraphMeasurementOutcome.repr }

def GraphMeasurementOutcome.toSign : GraphMeasurementOutcome → ℤ

Convert measurement outcome to a sign (±1 as integer)

Equations

• GraphMeasurementOutcome.plus.toSign = 1
• GraphMeasurementOutcome.minus.toSign = -1

@[simp]

theorem GraphMeasurementOutcome.plus_toSign : plus.toSign = 1

@[simp]

theorem GraphMeasurementOutcome.minus_toSign : minus.toSign = -1

def GraphMeasurementOutcome.mul : GraphMeasurementOutcome → GraphMeasurementOutcome → GraphMeasurementOutcome

Multiplication of measurement outcomes (product of signs)

Equations

• GraphMeasurementOutcome.plus.mul x✝ = x✝
• GraphMeasurementOutcome.minus.mul GraphMeasurementOutcome.plus = GraphMeasurementOutcome.minus
• GraphMeasurementOutcome.minus.mul GraphMeasurementOutcome.minus = GraphMeasurementOutcome.plus

instance GraphMeasurementOutcome.instMul : Mul GraphMeasurementOutcome

Equations

• GraphMeasurementOutcome.instMul = { mul := GraphMeasurementOutcome.mul }

@[simp]

theorem GraphMeasurementOutcome.plus_mul (m : GraphMeasurementOutcome) : plus * m = m

@[simp]

theorem GraphMeasurementOutcome.mul_plus (m : GraphMeasurementOutcome) : m * plus = m

@[simp]

theorem GraphMeasurementOutcome.minus_mul_minus : minus * minus = plus

@[simp]

theorem GraphMeasurementOutcome.minus_mul_plus : minus * plus = minus

@[simp]

theorem GraphMeasurementOutcome.plus_mul_minus : plus * minus = minus

instance GraphMeasurementOutcome.instOne : One GraphMeasurementOutcome

Equations

• GraphMeasurementOutcome.instOne = { one := GraphMeasurementOutcome.plus }

@[simp]

theorem GraphMeasurementOutcome.one_eq_plus : 1 = plus

Key Property: X measurement on |+⟩ always returns +1

def xMeasurementOnPlusState : GraphMeasurementOutcome

The key property that measuring X on the |+⟩ state always yields +1. This is because |+⟩ is the +1 eigenstate of the Pauli X operator: X|+⟩ = |+⟩ (eigenvalue +1)

Equations

• xMeasurementOnPlusState = GraphMeasurementOutcome.plus

theorem x_measurement_on_plus_is_plus : xMeasurementOnPlusState = GraphMeasurementOutcome.plus

Theorem: X measurement on |+⟩ always returns +1

structure DeterministicPlusOutcome : Type

The deterministic outcome property: measuring X on |+⟩ has probability 1 for +1 outcome

• is_plus_state : QubitType.InitialState

  The state is |+⟩ (X eigenstate with eigenvalue +1)

• state_eq_plus : self.is_plus_state = QubitType.InitialState.plus

  The state condition

• outcome : GraphMeasurementOutcome

  The measurement outcome is deterministically +1

• outcome_is_plus : self.outcome = GraphMeasurementOutcome.plus

  Outcome is always +1

Gauging Graph Convention Structure

structure GaugingGraphConvention : Type 1

A gauging graph convention specifies how a connected graph G relates to the logical operator L being measured. This captures the key conventions from Rem_2:

1. Vertices of G are identified with qubits in supp(L)
2. Each edge e ∈ E_G gets an auxiliary gauge qubit in |0⟩
3. Dummy vertices (V_G \ supp(L)) get auxiliary qubits in |+⟩
4. Dummy vertices have no effect on measurement outcome (X on |+⟩ → +1)

• Vertex : Type

  The vertex type of the graph

• vertexFintype : Fintype self.Vertex

  Vertices form a finite type

• vertexDecEq : DecidableEq self.Vertex

  Decidable equality on vertices

• graph : SimpleGraph self.Vertex

  The simple graph structure

• adjDecidable : DecidableRel self.graph.Adj

  Decidable adjacency

• connected : self.graph.Connected

  The graph is connected

• logicalSupport : Finset self.Vertex

  The support set of the logical operator L (embedded in vertices)

• support_nonempty : self.logicalSupport.Nonempty

  The logical support is nonempty (L is nontrivial)

Vertex Classification

def GaugingGraphConvention.isSupportVertex (G : GaugingGraphConvention) (v : G.Vertex) : Prop

A vertex is a support vertex if it corresponds to a qubit in supp(L)

Equations

• G.isSupportVertex v = (v ∈ G.logicalSupport)

def GaugingGraphConvention.isDummyVertex (G : GaugingGraphConvention) (v : G.Vertex) : Prop

A vertex is a dummy vertex if it's not in the logical support

Equations

• G.isDummyVertex v = (v ∉ G.logicalSupport)

instance GaugingGraphConvention.instDecidableIsSupportVertex (G : GaugingGraphConvention) (v : G.Vertex) : Decidable (G.isSupportVertex v)

Decidability of support vertex membership

Equations

• G.instDecidableIsSupportVertex v = inferInstanceAs (Decidable (v ∈ G.logicalSupport))

instance GaugingGraphConvention.instDecidableIsDummyVertex (G : GaugingGraphConvention) (v : G.Vertex) : Decidable (G.isDummyVertex v)

Decidability of dummy vertex membership

Equations

• G.instDecidableIsDummyVertex v = inferInstanceAs (Decidable (v ∉ G.logicalSupport))

theorem GaugingGraphConvention.vertex_classification (G : GaugingGraphConvention) (v : G.Vertex) : G.isSupportVertex v ∨ G.isDummyVertex v

Every vertex is either a support vertex or a dummy vertex

theorem GaugingGraphConvention.support_dummy_exclusive (G : GaugingGraphConvention) (v : G.Vertex) : ¬(G.isSupportVertex v ∧ G.isDummyVertex v)

Support and dummy vertices are mutually exclusive

def GaugingGraphConvention.dummyVertices (G : GaugingGraphConvention) : Finset G.Vertex

The set of dummy vertices

Equations

• G.dummyVertices = {v : G.Vertex | G.isDummyVertex v}

def GaugingGraphConvention.numDummyVertices (G : GaugingGraphConvention) : ℕ

The number of dummy vertices

Equations

• G.numDummyVertices = G.dummyVertices.card

theorem GaugingGraphConvention.vertex_partition (G : GaugingGraphConvention) : Fintype.card G.Vertex = G.logicalSupport.card + G.numDummyVertices

Vertices partition into support and dummy

Qubit Type Assignment

def GaugingGraphConvention.vertexQubitType (G : GaugingGraphConvention) (v : G.Vertex) : QubitType

Assign a qubit type to each vertex

Equations

• G.vertexQubitType v = if G.isSupportVertex v then QubitType.LogicalSupport else QubitType.DummyQubit

@[simp]

theorem GaugingGraphConvention.supportVertex_qubitType (G : GaugingGraphConvention) (v : G.Vertex) (h : G.isSupportVertex v) : G.vertexQubitType v = QubitType.LogicalSupport

Support vertices are assigned LogicalSupport type

@[simp]

theorem GaugingGraphConvention.dummyVertex_qubitType (G : GaugingGraphConvention) (v : G.Vertex) (h : G.isDummyVertex v) : G.vertexQubitType v = QubitType.DummyQubit

Dummy vertices are assigned DummyQubit type

def GaugingGraphConvention.edgeQubitType (G : GaugingGraphConvention) (_e : Sym2 G.Vertex) : QubitType

All edges are assigned EdgeQubit type

Equations

• G.edgeQubitType _e = QubitType.EdgeQubit

Initial States

def GaugingGraphConvention.vertexInitialState (G : GaugingGraphConvention) (v : G.Vertex) : QubitType.InitialState

The initial state for a vertex qubit

Equations

• G.vertexInitialState v = (G.vertexQubitType v).initialState

def GaugingGraphConvention.edgeInitialState (G : GaugingGraphConvention) (_e : Sym2 G.Vertex) : QubitType.InitialState

The initial state for an edge qubit

Equations

• G.edgeInitialState _e = QubitType.InitialState.zero

@[simp]

theorem GaugingGraphConvention.dummyVertex_initialState (G : GaugingGraphConvention) (v : G.Vertex) (h : G.isDummyVertex v) : G.vertexInitialState v = QubitType.InitialState.plus

Dummy vertex qubits are initialized in |+⟩

@[simp]

theorem GaugingGraphConvention.edge_initialState (G : GaugingGraphConvention) (e : Sym2 G.Vertex) : G.edgeInitialState e = QubitType.InitialState.zero

Edge qubits are initialized in |0⟩

Dummy Vertex Measurement Property

def GaugingGraphConvention.dummyVertexMeasurementOutcome (G : GaugingGraphConvention) (_v : G.Vertex) (_h : G.isDummyVertex _v) : GraphMeasurementOutcome

The key property: measuring X on a dummy vertex always gives +1. This is because the dummy qubit is in |+⟩, which is the +1 eigenstate of X.

Equations

• G.dummyVertexMeasurementOutcome _v _h = GraphMeasurementOutcome.plus

theorem GaugingGraphConvention.dummy_measurement_always_plus (G : GaugingGraphConvention) (v : G.Vertex) (h : G.isDummyVertex v) : G.dummyVertexMeasurementOutcome v h = GraphMeasurementOutcome.plus

Measuring X on any dummy vertex returns +1

theorem GaugingGraphConvention.dummy_product_is_one (G : GaugingGraphConvention) (S : Finset G.Vertex) : (∀ v ∈ S, G.isDummyVertex v) → ∏ _v ∈ S, 1 = 1

The product of measurement outcomes over dummy vertices is +1. This is formulated using integers since GraphMeasurementOutcome doesn't have CommMonoid.

Edge and Qubit Counts

noncomputable def GaugingGraphConvention.numEdges (G : GaugingGraphConvention) : ℕ

The number of edges in the graph (= number of gauge qubits)

Equations

• G.numEdges = G.graph.edgeFinset.card

noncomputable def GaugingGraphConvention.numAuxiliaryQubits (G : GaugingGraphConvention) : ℕ

The total number of auxiliary qubits = edge qubits + dummy qubits

Equations

• G.numAuxiliaryQubits = G.numEdges + G.numDummyVertices

noncomputable def GaugingGraphConvention.totalQubits (G : GaugingGraphConvention) : ℕ

The total number of qubits involved = logical support + auxiliary

Equations

• G.totalQubits = G.logicalSupport.card + G.numAuxiliaryQubits

theorem GaugingGraphConvention.totalQubits_eq (G : GaugingGraphConvention) : G.totalQubits = G.logicalSupport.card + G.numEdges + G.numDummyVertices

Total qubits formula expanded

Gauging Operator Extension

def GaugingGraphConvention.effectiveLogicalSupport (G : GaugingGraphConvention) : Finset G.Vertex

When gauging L with dummy vertices, we actually gauge L · ∏_{v ∈ dummy} X_v. Since each dummy vertex measurement gives +1, this doesn't change the outcome.

This captures: "gauge the operator L · X_v" for each dummy vertex v.

Equations

• G.effectiveLogicalSupport = Finset.univ

theorem GaugingGraphConvention.effectiveSupport_is_all_vertices (G : GaugingGraphConvention) : G.effectiveLogicalSupport = Finset.univ

The effective logical support includes all vertices (support ∪ dummy)

theorem GaugingGraphConvention.logicalSupport_subset_effective (G : GaugingGraphConvention) : G.logicalSupport ⊆ G.effectiveLogicalSupport

The effective logical support contains the original logical support

Key Theorem: Dummy Vertices Don't Affect Outcome

theorem GaugingGraphConvention.dummy_vertices_no_effect (G : GaugingGraphConvention) (dummies : Finset G.Vertex) : (∀ v ∈ dummies, G.isDummyVertex v) → (∏ v ∈ dummies, if G.isDummyVertex v then 1 else 0) = 1

The main theorem of this remark: dummy vertices have no effect on the gauging measurement outcome because:

1. Each dummy vertex v has qubit initialized in |+⟩
2. The gauging measures X_v on the dummy qubit
3. Measuring X on |+⟩ always returns +1
4. Therefore, the product over dummy vertices contributes factor 1

theorem GaugingGraphConvention.dummy_contribution_neutral (G : GaugingGraphConvention) (v : G.Vertex) (hv : G.isDummyVertex v) : (G.dummyVertexMeasurementOutcome v hv).toSign = 1

Alternative formulation: the contribution of dummy vertices to the measurement outcome is the neutral element

Summary of Convention

The graph convention establishes:

1. Vertex-Qubit Correspondence: Vertices V_G ↔ qubits, with supp(L) ⊆ V_G
2. Edge Qubits: Each edge e ∈ E_G gets an auxiliary qubit initialized in |0⟩
3. Dummy Vertices: Vertices in V_G \ supp(L) get auxiliary qubits in |+⟩
4. No-Effect Property: Dummy vertices don't affect measurement outcome because measuring X on |+⟩ deterministically gives +1

This convention allows the gauging graph to be larger than supp(L), enabling graph constructions that satisfy expansion and path-length requirements while maintaining the correctness of the logical measurement.