Rem_20: Cohen Scheme as Gauging

Statement

The Cohen et al. scheme for logical measurement can be recovered as a hypergraph gauging measurement.

Cohen et al. scheme setup: Consider the restriction of the Z-type checks to the support of an irreducible X logical L. This defines a hypergraph of Z constraints with the only nontrivial element in the kernel being the logical operator L.

Recovery via gauging:

1. Add d layers of dummy vertices for each qubit in supp(L)
2. Connect the d copies of each vertex via a line graph (chain)
3. Join the vertices in each layer via a copy of the same underlying hypergraph

Applying the generalized hypergraph gauging procedure to this construction exactly reproduces the Cohen et al. measurement scheme.

Cross et al. modification: The scheme from Cross et al. can similarly be recovered by using fewer than d layers of dummy vertices.

Product measurement: The procedures for joining ancilla systems designed for irreducible logicals to measure their products can be captured as a gauging measurement by adding edges between the graphs corresponding to the individual ancilla systems.

Main Results

• CohenHypergraph : The Z-constraint hypergraph from the Cohen scheme
• cohen_kernel_characterization : The kernel has {0, L} as only elements
• LayeredCohenConstruction : The d-layer construction with chains and hypergraph copies
• layered_vertex_count : Total vertices = W * (d + 1)
• layered_hyperedge_count : Total hyperedges = W * d + |H| * (d + 1)
• layered_kernel_is_logical : The all-ones vector on the base layer is in the kernel
• cross_et_al_fewer_layers : Cross et al. uses m < d layers
• ProductMeasurementGraph : Graph for product measurement via bridge edges
• product_measurement_kernel_contains_product : Product of logicals is in the kernel

Cohen et al. Scheme Setup

The Cohen scheme restricts Z-type checks to supp(L), forming a hypergraph whose kernel characterizes the X-type operators commuting with these checks. The key property is that the only nontrivial element in the kernel is L itself.

@[reducible, inline]

abbrev QEC1.CohenSchemeAsGauging.CohenHypergraph (W numChecks : ℕ) : Type

The Cohen hypergraph: Z-type checks restricted to supp(L). Vertices are the W qubits in supp(L), and hyperedges are the restricted Z-type checks.

Equations

• QEC1.CohenSchemeAsGauging.CohenHypergraph W numChecks = QEC1.HypergraphGeneralization.Hypergraph (Fin W) (Fin numChecks)

def QEC1.CohenSchemeAsGauging.logicalVector (W : ℕ) : HypergraphGeneralization.Hypergraph.VectorV (Fin W)

The all-ones vector on Fin W represents the logical operator L = ∏_{v ∈ supp(L)} X_v.

Equations

• QEC1.CohenSchemeAsGauging.logicalVector W x✝ = 1

theorem QEC1.CohenSchemeAsGauging.logicalVector_ne_zero {W : ℕ} (hW : W ≥ 1) : logicalVector W ≠ 0

The logical vector is nonzero when W ≥ 1.

def QEC1.CohenSchemeAsGauging.CohenKernelProperty {W numChecks : ℕ} (HG : CohenHypergraph W numChecks) : Prop

Property that the kernel of the Cohen hypergraph is exactly {0, L}. This is the defining property of the Cohen scheme: the restriction of Z-type checks to supp(L) has kernel spanned by L (the logical operator is irreducible).

Equations

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

theorem QEC1.CohenSchemeAsGauging.cohen_logical_in_kernel {W numChecks : ℕ} (HG : CohenHypergraph W numChecks) (hker : CohenKernelProperty HG) : logicalVector W ∈ HypergraphGeneralization.Hypergraph.operatorKernel HG

When the Cohen kernel property holds, L is in the kernel.

theorem QEC1.CohenSchemeAsGauging.cohen_kernel_characterization {W numChecks : ℕ} (HG : CohenHypergraph W numChecks) (hker : CohenKernelProperty HG) (x : HypergraphGeneralization.Hypergraph.VectorV (Fin W)) : x ∈ HypergraphGeneralization.Hypergraph.operatorKernel HG → x = 0 ∨ x = logicalVector W

When the Cohen kernel property holds, the kernel has exactly {0, L}.

theorem QEC1.CohenSchemeAsGauging.cohen_kernel_contains_zero_and_L {W numChecks : ℕ} (HG : CohenHypergraph W numChecks) (hker : CohenKernelProperty HG) : 0 ∈ HypergraphGeneralization.Hypergraph.operatorKernel HG ∧ logicalVector W ∈ HypergraphGeneralization.Hypergraph.operatorKernel HG

Both 0 and L are in the kernel.

Layered Construction for Recovery via Gauging

The construction to recover the Cohen scheme via gauging:

1. Start with W qubits (vertices of supp(L))
2. Add d layers of dummy vertices (W vertices per layer)
3. Connect d copies of each vertex via a line graph (chain of length d)
4. Join vertices in each layer via copies of the same underlying hypergraph

Total vertices: W * (d + 1) (original layer + d dummy layers) Total hyperedges: W * d (chain edges) + numChecks * (d + 1) (hypergraph copies per layer)

@[reducible, inline]

abbrev QEC1.CohenSchemeAsGauging.LayeredVertex (W d : ℕ) : Type

Vertex type for the layered construction: (layer, qubit_index). Layer 0 is the original (base) layer, layers 1..d are dummy layers.

Equations

• QEC1.CohenSchemeAsGauging.LayeredVertex W d = (Fin (d + 1) × Fin W)

theorem QEC1.CohenSchemeAsGauging.layered_vertex_count (W d : ℕ) : Fintype.card (LayeredVertex W d) = (d + 1) * W

The total number of vertices in the layered construction.

def QEC1.CohenSchemeAsGauging.baseLayerVertices (W d : ℕ) : Finset (LayeredVertex W d)

The base layer vertices (layer 0) correspond to the original qubits in supp(L).

Equations

• QEC1.CohenSchemeAsGauging.baseLayerVertices W d = {v : QEC1.CohenSchemeAsGauging.LayeredVertex W d | v.1 = ⟨0, ⋯⟩}

def QEC1.CohenSchemeAsGauging.dummyLayerVertices (W d : ℕ) : Finset (LayeredVertex W d)

The dummy layer vertices (layers 1..d).

Equations

• QEC1.CohenSchemeAsGauging.dummyLayerVertices W d = {v : QEC1.CohenSchemeAsGauging.LayeredVertex W d | v.1 ≠ ⟨0, ⋯⟩}

theorem QEC1.CohenSchemeAsGauging.base_layer_card (W d : ℕ) : (baseLayerVertices W d).card = W

The base layer has exactly W vertices.

theorem QEC1.CohenSchemeAsGauging.dummy_layers_card (W d : ℕ) : (dummyLayerVertices W d).card = d * W

The dummy layers have exactly d * W vertices.

Edge Types in the Layered Construction

Two types of edges/hyperedges:

1. Chain edges: connecting (layer, i) to (layer+1, i) for each qubit i and layer 0..d-1
2. Hypergraph copies: a copy of the original Z-constraint hypergraph in each layer

inductive QEC1.CohenSchemeAsGauging.LayeredHyperedge (W d numChecks : ℕ) : Type

Combined edge/hyperedge type for the layered construction.

• chain {W d numChecks : ℕ} : Fin d → Fin W → LayeredHyperedge W d numChecks

  Chain edge connecting (l, i) to (l+1, i)

• hypergraphCopy {W d numChecks : ℕ} : Fin (d + 1) → Fin numChecks → LayeredHyperedge W d numChecks

  Copy of a hypergraph check in a given layer

def QEC1.CohenSchemeAsGauging.instDecidableEqLayeredHyperedge.decEq {W✝ d✝ numChecks✝ : ℕ} (x✝ x✝¹ : LayeredHyperedge W✝ d✝ numChecks✝) : Decidable (x✝ = x✝¹)

Equations

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

instance QEC1.CohenSchemeAsGauging.instDecidableEqLayeredHyperedge {W✝ d✝ numChecks✝ : ℕ} : DecidableEq (LayeredHyperedge W✝ d✝ numChecks✝)

Equations

• QEC1.CohenSchemeAsGauging.instDecidableEqLayeredHyperedge = QEC1.CohenSchemeAsGauging.instDecidableEqLayeredHyperedge.decEq

instance QEC1.CohenSchemeAsGauging.instFintypeLayeredHyperedge (W d numChecks : ℕ) : Fintype (LayeredHyperedge W d numChecks)

Equations

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

theorem QEC1.CohenSchemeAsGauging.chain_edge_count (W d numChecks : ℕ) : (Finset.image (fun (p : Fin d × Fin W) => LayeredHyperedge.chain p.1 p.2) Finset.univ).card = d * W

The number of chain edges is d * W.

theorem QEC1.CohenSchemeAsGauging.hypergraph_copy_count (W d numChecks : ℕ) : (Finset.image (fun (p : Fin (d + 1) × Fin numChecks) => LayeredHyperedge.hypergraphCopy p.1 p.2) Finset.univ).card = (d + 1) * numChecks

The number of hypergraph copy edges is (d + 1) * numChecks.

Layered Hypergraph Construction

Build the layered hypergraph from the original Cohen hypergraph.

def QEC1.CohenSchemeAsGauging.LayeredCohenConstruction (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) : HypergraphGeneralization.Hypergraph (LayeredVertex W d) (LayeredHyperedge W d numChecks)

Construct the layered hypergraph from the original Cohen hypergraph.

• Chain edges connect (l, i) to (l+1, i) (2-element hyperedges)
• Hypergraph copies replicate the original Z-constraint hypergraph in each layer

Equations

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

theorem QEC1.CohenSchemeAsGauging.chain_edge_is_pair (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) (l : Fin d) (i : Fin W) : ((LayeredCohenConstruction W d numChecks HG).incidence (LayeredHyperedge.chain l i)).card = 2

Each chain edge is a 2-element hyperedge (graph-like).

theorem QEC1.CohenSchemeAsGauging.hypergraph_copy_card (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) (layer : Fin (d + 1)) (check : Fin numChecks) : ((LayeredCohenConstruction W d numChecks HG).incidence (LayeredHyperedge.hypergraphCopy layer check)).card = (HG.incidence check).card

Hypergraph copy edges have the same cardinality as the original.

Kernel Properties of the Layered Construction

The all-ones vector on all layers represents the product of L across layers. The layered construction preserves the property that this vector is in the kernel.

def QEC1.CohenSchemeAsGauging.baseLogicalVector (W d : ℕ) : HypergraphGeneralization.Hypergraph.VectorV (LayeredVertex W d)

The all-ones vector on the base layer, zeros elsewhere.

Equations

• QEC1.CohenSchemeAsGauging.baseLogicalVector W d v = if v.1 = ⟨0, ⋯⟩ then 1 else 0

def QEC1.CohenSchemeAsGauging.allLayersLogicalVector (W d : ℕ) : HypergraphGeneralization.Hypergraph.VectorV (LayeredVertex W d)

The all-ones vector on all layers represents the full product.

Equations

• QEC1.CohenSchemeAsGauging.allLayersLogicalVector W d x✝ = 1

theorem QEC1.CohenSchemeAsGauging.layered_kernel_is_logical (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) (hker : CohenKernelProperty HG) : allLayersLogicalVector W d ∈ (LayeredCohenConstruction W d numChecks HG).operatorKernel

The all-layers logical vector is in the kernel if L is in the kernel of each copy.

Chain Structure: Line Graph Connectivity

The d copies of each vertex are connected via a chain (line graph). This provides a path of length d from the base layer to the top layer.

theorem QEC1.CohenSchemeAsGauging.chain_adjacency (W d : ℕ) (l : Fin d) (_i : Fin W) : ⟨↑l, ⋯⟩ ≠ ⟨↑l + 1, ⋯⟩

Adjacency in the chain: vertex i in layers l and l+1 are connected.

theorem QEC1.CohenSchemeAsGauging.chain_path_length (W d : ℕ) (_hd : d ≥ 1) (_i : Fin W) : ∃ (edges : Finset (Fin d)), edges.card = d ∧ edges = Finset.univ

The chain from layer 0 to layer d for vertex i has exactly d edges.

Cross et al. Modification

The Cross et al. scheme uses m < d layers of dummy vertices instead of d. This is captured by instantiating the layered construction with a smaller parameter.

def QEC1.CohenSchemeAsGauging.CrossEtAlLayers (W d m : ℕ) (_hm : m < d) : Type

The Cross et al. modification uses m layers where m < d.

Equations

• QEC1.CohenSchemeAsGauging.CrossEtAlLayers W d m _hm = (Fin (m + 1) × Fin W)

theorem QEC1.CohenSchemeAsGauging.cross_et_al_fewer_layers (W d m : ℕ) (hm : m < d) (hW : W ≥ 1) : (m + 1) * W < (d + 1) * W

The Cross et al. construction has fewer total vertices when W ≥ 1.

def QEC1.CohenSchemeAsGauging.CrossEtAlConstruction (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) (m : ℕ) (_hm : m < d) : HypergraphGeneralization.Hypergraph (Fin (m + 1) × Fin W) (LayeredHyperedge W m numChecks)

The Cross et al. layered construction with m < d layers.

Equations

• QEC1.CohenSchemeAsGauging.CrossEtAlConstruction W d numChecks HG m _hm = QEC1.CohenSchemeAsGauging.LayeredCohenConstruction W m numChecks HG

theorem QEC1.CohenSchemeAsGauging.cross_et_al_kernel_preserved (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) (hker : CohenKernelProperty HG) (m : ℕ) (hm : m < d) : allLayersLogicalVector W m ∈ (CrossEtAlConstruction W d numChecks HG m hm).operatorKernel

The Cross et al. construction preserves the kernel property.

Product Measurement via Bridge Edges

To measure products of irreducible logicals, join the ancilla systems for individual logicals by adding edges between their corresponding graphs.

@[reducible, inline]

abbrev QEC1.CohenSchemeAsGauging.ProductVertex (W₁ W₂ : ℕ) : Type

Vertex type for the combined product measurement graph.

Equations

• QEC1.CohenSchemeAsGauging.ProductVertex W₁ W₂ = (Fin W₁ ⊕ Fin W₂)

instance QEC1.CohenSchemeAsGauging.instDecidableEqProductVertex {W₁ W₂ : ℕ} : DecidableEq (ProductVertex W₁ W₂)

Equations

• QEC1.CohenSchemeAsGauging.instDecidableEqProductVertex = inferInstance

instance QEC1.CohenSchemeAsGauging.instFintypeProductVertex {W₁ W₂ : ℕ} : Fintype (ProductVertex W₁ W₂)

Equations

• QEC1.CohenSchemeAsGauging.instFintypeProductVertex = inferInstance

theorem QEC1.CohenSchemeAsGauging.product_vertex_count {W₁ W₂ : ℕ} : Fintype.card (ProductVertex W₁ W₂) = W₁ + W₂

The total vertex count of the product measurement graph.

structure QEC1.CohenSchemeAsGauging.BridgeEdgeConfig (W₁ W₂ : ℕ) : Type

Bridge edges connect specific vertices between the two ancilla systems.

• bridges : Finset (Fin W₁ × Fin W₂)

  The set of bridge connections: pairs (v₁, v₂) to connect

• nonempty : self.bridges.Nonempty

  At least one bridge edge exists

inductive QEC1.CohenSchemeAsGauging.ProductHyperedge (W₁ W₂ nc₁ nc₂ : ℕ) : Type

Hyperedge type for the product measurement construction.

• left {W₁ W₂ nc₁ nc₂ : ℕ} : Fin nc₁ → ProductHyperedge W₁ W₂ nc₁ nc₂

  A check from the first ancilla system

• right {W₁ W₂ nc₁ nc₂ : ℕ} : Fin nc₂ → ProductHyperedge W₁ W₂ nc₁ nc₂

  A check from the second ancilla system

• bridge {W₁ W₂ nc₁ nc₂ : ℕ} : Fin W₁ → Fin W₂ → ProductHyperedge W₁ W₂ nc₁ nc₂

  A bridge edge between the two systems

instance QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge {W₁✝ W₂✝ nc₁✝ nc₂✝ : ℕ} : DecidableEq (ProductHyperedge W₁✝ W₂✝ nc₁✝ nc₂✝)

Equations

• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge = QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq

def QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq {W₁✝ W₂✝ nc₁✝ nc₂✝ : ℕ} (x✝ x✝¹ : ProductHyperedge W₁✝ W₂✝ nc₁✝ nc₂✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq (QEC1.CohenSchemeAsGauging.ProductHyperedge.left a) (QEC1.CohenSchemeAsGauging.ProductHyperedge.right a_1) = isFalse ⋯
• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq (QEC1.CohenSchemeAsGauging.ProductHyperedge.left a) (QEC1.CohenSchemeAsGauging.ProductHyperedge.bridge a_1 a_2) = isFalse ⋯
• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq (QEC1.CohenSchemeAsGauging.ProductHyperedge.right a) (QEC1.CohenSchemeAsGauging.ProductHyperedge.left a_1) = isFalse ⋯
• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq (QEC1.CohenSchemeAsGauging.ProductHyperedge.right a) (QEC1.CohenSchemeAsGauging.ProductHyperedge.bridge a_1 a_2) = isFalse ⋯
• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq (QEC1.CohenSchemeAsGauging.ProductHyperedge.bridge a a_1) (QEC1.CohenSchemeAsGauging.ProductHyperedge.left a_2) = isFalse ⋯
• QEC1.CohenSchemeAsGauging.instDecidableEqProductHyperedge.decEq (QEC1.CohenSchemeAsGauging.ProductHyperedge.bridge a a_1) (QEC1.CohenSchemeAsGauging.ProductHyperedge.right a_2) = isFalse ⋯

instance QEC1.CohenSchemeAsGauging.instFintypeProductHyperedge {W₁ W₂ nc₁ nc₂ : ℕ} : Fintype (ProductHyperedge W₁ W₂ nc₁ nc₂)

Equations

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

def QEC1.CohenSchemeAsGauging.ProductMeasurementGraph {W₁ W₂ nc₁ nc₂ : ℕ} (HG₁ : HypergraphGeneralization.Hypergraph (Fin W₁) (Fin nc₁)) (HG₂ : HypergraphGeneralization.Hypergraph (Fin W₂) (Fin nc₂)) (_bridges : Finset (Fin W₁ × Fin W₂)) : HypergraphGeneralization.Hypergraph (ProductVertex W₁ W₂) (ProductHyperedge W₁ W₂ nc₁ nc₂)

The product measurement hypergraph combining two ancilla systems with bridge edges.

Equations

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

theorem QEC1.CohenSchemeAsGauging.bridge_edge_is_pair {W₁ W₂ nc₁ nc₂ : ℕ} (HG₁ : HypergraphGeneralization.Hypergraph (Fin W₁) (Fin nc₁)) (HG₂ : HypergraphGeneralization.Hypergraph (Fin W₂) (Fin nc₂)) (bridges : Finset (Fin W₁ × Fin W₂)) (i : Fin W₁) (j : Fin W₂) : ((ProductMeasurementGraph HG₁ HG₂ bridges).incidence (ProductHyperedge.bridge i j)).card = 2

Bridge edges are 2-element hyperedges (graph-like).

theorem QEC1.CohenSchemeAsGauging.left_check_card {W₁ W₂ nc₁ nc₂ : ℕ} (HG₁ : HypergraphGeneralization.Hypergraph (Fin W₁) (Fin nc₁)) (HG₂ : HypergraphGeneralization.Hypergraph (Fin W₂) (Fin nc₂)) (bridges : Finset (Fin W₁ × Fin W₂)) (h : Fin nc₁) : ((ProductMeasurementGraph HG₁ HG₂ bridges).incidence (ProductHyperedge.left h)).card = (HG₁.incidence h).card

Left check edges have the same cardinality as in the original system.

theorem QEC1.CohenSchemeAsGauging.right_check_card {W₁ W₂ nc₁ nc₂ : ℕ} (HG₁ : HypergraphGeneralization.Hypergraph (Fin W₁) (Fin nc₁)) (HG₂ : HypergraphGeneralization.Hypergraph (Fin W₂) (Fin nc₂)) (bridges : Finset (Fin W₁ × Fin W₂)) (h : Fin nc₂) : ((ProductMeasurementGraph HG₁ HG₂ bridges).incidence (ProductHyperedge.right h)).card = (HG₂.incidence h).card

Right check edges have the same cardinality as in the original system.

def QEC1.CohenSchemeAsGauging.productLogicalVector {W₁ W₂ : ℕ} : HypergraphGeneralization.Hypergraph.VectorV (ProductVertex W₁ W₂)

The product logical vector: all-ones on both systems.

Equations

• QEC1.CohenSchemeAsGauging.productLogicalVector x✝ = 1

theorem QEC1.CohenSchemeAsGauging.product_measurement_kernel_contains_product {W₁ W₂ nc₁ nc₂ : ℕ} (HG₁ : HypergraphGeneralization.Hypergraph (Fin W₁) (Fin nc₁)) (HG₂ : HypergraphGeneralization.Hypergraph (Fin W₂) (Fin nc₂)) (bridges : Finset (Fin W₁ × Fin W₂)) (hL₁ : HypergraphGeneralization.Hypergraph.allOnesV ∈ HG₁.operatorKernel) (hL₂ : HypergraphGeneralization.Hypergraph.allOnesV ∈ HG₂.operatorKernel) : productLogicalVector ∈ (ProductMeasurementGraph HG₁ HG₂ bridges).operatorKernel

The product of logicals is in the kernel when both individual logicals are, and all bridge edges have even-cardinality incidence (they are 2-element).

Recovery Correspondence

The full Cohen et al. scheme is recovered by applying the generalized hypergraph gauging procedure (Rem_15) to the layered construction:

1. Gauss's law operators: For each vertex (l, i), the operator A_{(l,i)} = X_{(l,i)} ∏_{e ∋ (l,i)} X_e This includes contributions from chain edges and hypergraph copy edges.

2. Product = L: The product of all A_v operators on the base layer yields L, while dummy layers contribute +1 (as per Rem_2 dummy vertex property).

3. Flux operators: The cycles in the construction give rise to flux operators B_p that stabilize the edge qubits.

theorem QEC1.CohenSchemeAsGauging.layered_gaussLaw_vertex_sum (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) : ∑ v : LayeredVertex W d, (LayeredCohenConstruction W d numChecks HG).gaussLawVertexSupport v = fun (x : LayeredVertex W d) => 1

The generalized Gauss's law vertex support sum equals all-ones (instantiation of the hypergraph Gauss's law property).

theorem QEC1.CohenSchemeAsGauging.layered_klocal_preserved (W d numChecks : ℕ) (HG : CohenHypergraph W numChecks) (k : ℕ) (hk : k ≥ 2) (hHG : HypergraphGeneralization.Hypergraph.isKLocalHypergraph HG k) : (LayeredCohenConstruction W d numChecks HG).isKLocalHypergraph k

The layered construction is k-local when the original Cohen hypergraph is k-local (chain edges have size 2, so the locality bound is max(2, k)).

Summary

The Cohen et al. scheme for logical measurement is recovered as a hypergraph gauging measurement through the following correspondence:

1. Cohen setup: The Z-type checks restricted to supp(L) define a hypergraph whose kernel is {0, L} (the logical is irreducible).

2. Layered construction: d layers of dummy vertices + chain connections + hypergraph copies per layer give the full gauging hypergraph.

3. Kernel preservation: The all-ones vector (representing L) remains in the kernel of the layered construction, ensuring the gauging measurement recovers L.

4. Cross et al.: Using m < d layers gives a more efficient variant.

5. Product measurement: Adding bridge edges between individual ancilla systems allows measuring products of irreducible logicals via a single gauging measurement.