Remark 26: Cohen et al. Scheme Recovery

Statement

The Cohen et al. scheme for logical measurement is recovered as a special case of the hypergraph gauging procedure (Rem_17).

Given a CSS stabilizer code and an irreducible X logical operator L:

1. Restrict Z-type checks to the support of L → defines hypergraph H = (V_L, E_L)
2. The only nontrivial element in ker(∂) is the all-ones vector (= L)
3. Cohen et al. = hypergraph gauging with d layers
4. Cross et al. = fewer layers with sufficient Cheeger expansion
5. Joint measurement = adding edges between individual graphs

Main Results

• restrictedZCheckIncident : incidence relation for Z-checks restricted to supp(L)
• restrictedBoundaryMap : the boundary map of the restricted hypergraph
• IsIrreducibleXLogical : irreducible X logical operator definition
• zCheck_restricted_support_even : commutation implies even overlap (row evenness)
• prodX_centralizer_of_even_overlap : prodX(S) is in centralizer when S has even overlap
• coboundary_ker_gives_centralizer_pair : ker(δ) elements give centralizer factorizations
• kernel_restricted_boundary_trivial : kernel triviality from irreducibility
• layeredIncident : the d-layer incidence combining inter/intra-layer edges
• cohen_layered_all_ones_measures_L : all-ones Gauss product measures L
• jointIncident : joint incidence for measuring products of logicals
• joint_gauss_product_measures_product : joint measurement by adding edges

Restricted hypergraph from Z-checks on logical support

def CohenEtAlSchemeRecovery.logicalSupport {Q : Type u_1} [Fintype Q] [DecidableEq Q] (L : PauliOp Q) : Finset Q

The support of L as a finset of qubits (X-support).

Equations

• CohenEtAlSchemeRecovery.logicalSupport L = L.supportX

def CohenEtAlSchemeRecovery.isZTypeCheck {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (i : C.I) : Prop

A Z-type check index: a check with no X-support.

Equations

• CohenEtAlSchemeRecovery.isZTypeCheck C i = ((C.check i).xVec = 0)

instance CohenEtAlSchemeRecovery.isZTypeCheck_decidable {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (i : C.I) : Decidable (isZTypeCheck C i)

Equations

• CohenEtAlSchemeRecovery.isZTypeCheck_decidable C i = inferInstanceAs (Decidable ((C.check i).xVec = 0))

def CohenEtAlSchemeRecovery.relevantZChecks {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) [DecidableEq C.I] : Finset C.I

The Z-type check indices that have nonempty intersection with supp(L).

Equations

• CohenEtAlSchemeRecovery.relevantZChecks C L = {i : C.I | CohenEtAlSchemeRecovery.isZTypeCheck C i ∧ ((C.check i).supportZ ∩ CohenEtAlSchemeRecovery.logicalSupport L).Nonempty}

def CohenEtAlSchemeRecovery.restrictedZCheckIncident {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) [DecidableEq C.I] (q : Q) (i : C.I) : Prop

The incidence relation for the restricted hypergraph: qubit q is incident to Z-check i iff q ∈ supp(L) and the check has Z-action at q.

Equations

• CohenEtAlSchemeRecovery.restrictedZCheckIncident C L q i = (q ∈ CohenEtAlSchemeRecovery.logicalSupport L ∧ (C.check i).zVec q ≠ 0 ∧ CohenEtAlSchemeRecovery.isZTypeCheck C i)

instance CohenEtAlSchemeRecovery.restrictedZCheckIncident_decidable {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) [DecidableEq C.I] (q : Q) (i : C.I) : Decidable (restrictedZCheckIncident C L q i)

Equations

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

def CohenEtAlSchemeRecovery.restrictedBoundaryMap {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) [DecidableEq C.I] : (C.I → ZMod 2) →ₗ[ZMod 2] Q → ZMod 2

The restricted hypergraph boundary map: ∂ : Z₂^{E_L} → Z₂^{V_L}.

Equations

• CohenEtAlSchemeRecovery.restrictedBoundaryMap C L = HypergraphGeneralization.hyperBoundaryMap (CohenEtAlSchemeRecovery.restrictedZCheckIncident C L)

def CohenEtAlSchemeRecovery.restrictedCoboundaryMap {Q : Type u_1} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) [DecidableEq C.I] : (Q → ZMod 2) →ₗ[ZMod 2] C.I → ZMod 2

The restricted hypergraph coboundary map: δ : Z₂^{V_L} → Z₂^{E_L}.

Equations

• CohenEtAlSchemeRecovery.restrictedCoboundaryMap C L = HypergraphGeneralization.hyperCoboundaryMap (CohenEtAlSchemeRecovery.restrictedZCheckIncident C L)

Irreducible X logical operators

def CohenEtAlSchemeRecovery.IsXTypeLogical {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) : Prop

An X-type logical operator: pure X-type (zVec = 0), in the centralizer, not a stabilizer, and not identity.

Equations

• CohenEtAlSchemeRecovery.IsXTypeLogical C L = (L.zVec = 0 ∧ C.isLogicalOp L)

def CohenEtAlSchemeRecovery.IsIrreducibleXLogical {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) (L : PauliOp Q) : Prop

An irreducible X logical operator: an X-type logical that cannot be written as a product of two lower-weight X-type operators that are both in the centralizer.

Equations

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

Commutation and kernel properties for the restricted hypergraph

theorem CohenEtAlSchemeRecovery.zCheck_restricted_support_even {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (hL_pure_X : L.zVec = 0) (hL_comm : C.inCentralizer L) (i : C.I) (hZ : isZTypeCheck C i) : Even {q : Q | restrictedZCheckIncident C L q i}.card

If L is pure X-type and commutes with all checks, then for each Z-type check s_j, the Z-support of s_j intersected with supp(L) has even cardinality (row evenness). This is because ⟨L, s_j⟩_symp = Σ_q L.xVec(q) · s_j.zVec(q) = 0 (commutation), and L.xVec(q) = 1 iff q ∈ supp(L), so the sum counts |S_Z(s_j) ∩ supp(L)| mod 2.

Pure X operators in the centralizer

For a CSS code, a pure X-type operator prodX(S) is in the centralizer iff for each Z-type check s_j, the intersection |S ∩ supp_Z(s_j)| is even. X-type checks commute automatically (both pure X-type).

theorem CohenEtAlSchemeRecovery.prodX_commutes_zCheck_iff_even {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (S : Finset Q) (j : C.I) (hZ : isZTypeCheck C j) : (PauliOp.prodX S).PauliCommute (C.check j) ↔ Even {q ∈ S | (C.check j).zVec q ≠ 0}.card

For a CSS code, prodX(S) commutes with a Z-type check s_j iff |S ∩ supp_Z(s_j)| is even.

theorem CohenEtAlSchemeRecovery.prodX_centralizer_of_even_overlap {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (S : Finset Q) (hcss : SteaneStyleMeasurement.IsCSS C) (heven : ∀ (j : C.I), isZTypeCheck C j → Even {q ∈ S | (C.check j).zVec q ≠ 0}.card) : C.inCentralizer (PauliOp.prodX S)

For a CSS code, prodX(S) is in the centralizer iff S has even overlap with every Z-type check's support.

Coboundary kernel elements give centralizer factorizations

The key algebraic step: an element f ∈ ker(δ) of the restricted coboundary map (where δ is the transpose of the boundary map ∂) gives a factorization of L into two pure X-type centralizer elements. Specifically, if f : Q → ZMod 2 satisfies δf = 0 (meaning for each relevant Z-check j, #{q : f(q)=1 and q incident to j} is even), then prodX(supp(f) ∩ V_L) is in the centralizer of C.

theorem CohenEtAlSchemeRecovery.coboundary_ker_gives_centralizer_pair {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (hcss : SteaneStyleMeasurement.IsCSS C) (f : Q → ZMod 2) (hf_ker : f ∈ (restrictedCoboundaryMap C L).ker) (hf_supp : ∀ q ∉ logicalSupport L, f q = 0) : C.inCentralizer (PauliOp.prodX {q : Q | f q ≠ 0})

An element f in the kernel of the restricted coboundary map (i.e., for each relevant Z-check j, the number of vertices q with f(q) ≠ 0 incident to j is even) gives a pure X-type operator prodX(supp(f) ∩ V_L) that commutes with all Z-type checks, via prodX_centralizer_of_even_overlap.

This is the key step connecting the linear algebra of the restricted hypergraph to the PauliOp centralizer structure.

ProdX helper lemmas for the kernel triviality proof

Z₂ rank-nullity for incidence matrices

The key linear algebra step: for an incidence relation between finite types V and E, the boundary map ∂ = M · and coboundary map δ = Mᵀ · satisfy dim(ker(δ)) + |E| = dim(ker(∂)) + |V| via Matrix.rank_transpose and rank-nullity. This is used to show that if ker(∂) has dimension ≥ 2, then (given |V| ≥ |E|) ker(δ) also has dimension ≥ 2.

theorem CohenEtAlSchemeRecovery.z2_finrank_ker_formula {V₀ : Type u_2} {E₀ : Type u_3} [Fintype V₀] [DecidableEq V₀] [Fintype E₀] [DecidableEq E₀] (inc : V₀ → E₀ → Prop) [(v : V₀) → (e : E₀) → Decidable (inc v e)] : Module.finrank (ZMod 2) ↥(HypergraphGeneralization.hyperCoboundaryMap inc).ker + Fintype.card E₀ = Module.finrank (ZMod 2) ↥(HypergraphGeneralization.hyperBoundaryMap inc).ker + Fintype.card V₀

Z₂ rank-nullity for incidence matrices. dim(ker(δ)) + |E| = dim(ker(∂)) + |V|, where ∂ = M · and δ = Mᵀ ·. This follows from Matrix.rank_transpose and LinearMap.finrank_range_add_finrank_ker.

theorem CohenEtAlSchemeRecovery.coboundary_third_element {V₀ : Type u_2} {E₀ : Type u_3} [Fintype V₀] [DecidableEq V₀] [Fintype E₀] [DecidableEq E₀] (inc : V₀ → E₀ → Prop) [(v : V₀) → (e : E₀) → Decidable (inc v e)] (hVE : Fintype.card E₀ ≤ Fintype.card V₀) (hker : 2 ≤ Module.finrank (ZMod 2) ↥(HypergraphGeneralization.hyperBoundaryMap inc).ker) (w : V₀ → ZMod 2) (hw : w ∈ (HypergraphGeneralization.hyperCoboundaryMap inc).ker) : ∃ g ∈ (HypergraphGeneralization.hyperCoboundaryMap inc).ker, g ≠ 0 ∧ g ≠ w

Given dim(ker(boundary)) ≥ 2 and |E| ≤ |V|, and any w ∈ ker(coboundary), there exists g ∈ ker(coboundary) with g ≠ 0 and g ≠ w.

Kernel triviality: the core structural property

For an irreducible X logical L, the kernel of ∂ on the restricted hypergraph consists only of 0 and the all-ones vector on E_L. The argument proceeds in two steps:

Step 1 (rank-nullity): If ker(∂) has dimension ≥ 2 (i.e., contains a nontrivial γ besides 0 and all-ones), then ker(δ) also has dimension ≥ 2 (given |V_L| ≥ |E_L|), yielding a nontrivial vertex function f ∈ ker(δ) with f ≠ 0 and f ≠ all-ones. This uses rank(∂) = rank(δ) (since δ = ∂^T via Matrix.rank_transpose) and z2_finrank_ker_formula.

Step 2 (irreducibility contradiction): Such f gives a factorization L = prodX(supp(f)) · prodX(V_L \ supp(f)) where both factors are in the centralizer (by coboundary_ker_gives_centralizer_pair). Irreducibility then forces one factor to have weight ≥ wt(L) or be identity, meaning supp(f) = ∅ or supp(f) = V_L, contradicting f ≠ 0 and f ≠ all-ones.

Core incidence on subtype and lifting

def CohenEtAlSchemeRecovery.coreIncident {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) : { q : Q // q ∈ logicalSupport L } → { i : C.I // i ∈ relevantZChecks C L } → Prop

The core incidence on subtypes: vertex in VL incident to check in EL iff zVec ≠ 0.

Equations

• CohenEtAlSchemeRecovery.coreIncident C L q i = ((C.check ↑i).zVec ↑q ≠ 0)

instance CohenEtAlSchemeRecovery.coreIncident_decidable {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (q : { q : Q // q ∈ logicalSupport L }) (i : { i : C.I // i ∈ relevantZChecks C L }) : Decidable (coreIncident C L q i)

Equations

• CohenEtAlSchemeRecovery.coreIncident_decidable C L q i = inferInstanceAs (Decidable ((C.check ↑i).zVec ↑q ≠ 0))

def CohenEtAlSchemeRecovery.liftVL {Q : Type u_2} [Fintype Q] [DecidableEq Q] (L : PauliOp Q) (g : { q : Q // q ∈ logicalSupport L } → ZMod 2) : Q → ZMod 2

Lift a function on VL to a function on Q by extending with zeros.

Equations

• CohenEtAlSchemeRecovery.liftVL L g q = if hq : q ∈ CohenEtAlSchemeRecovery.logicalSupport L then g ⟨q, hq⟩ else 0

theorem CohenEtAlSchemeRecovery.liftVL_injective {Q : Type u_2} [Fintype Q] [DecidableEq Q] (L : PauliOp Q) : Function.Injective (liftVL L)

The lift is injective.

theorem CohenEtAlSchemeRecovery.liftVL_supp {Q : Type u_2} [Fintype Q] [DecidableEq Q] (L : PauliOp Q) (g : { q : Q // q ∈ logicalSupport L } → ZMod 2) (q : Q) : q ∉ logicalSupport L → liftVL L g q = 0

The lift is supported on VL.

@[simp]

theorem CohenEtAlSchemeRecovery.liftVL_zero {Q : Type u_2} [Fintype Q] [DecidableEq Q] (L : PauliOp Q) : liftVL L 0 = 0

Lift of 0 is 0.

theorem CohenEtAlSchemeRecovery.liftVL_allones {Q : Type u_2} [Fintype Q] [DecidableEq Q] (L : PauliOp Q) : (liftVL L fun (x : { q : Q // q ∈ logicalSupport L }) => 1) = fun (q : Q) => if q ∈ logicalSupport L then 1 else 0

Lift of all-ones on VL.

theorem CohenEtAlSchemeRecovery.liftVL_ker_coboundary {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (g : { q : Q // q ∈ logicalSupport L } → ZMod 2) (hg : g ∈ (HypergraphGeneralization.hyperCoboundaryMap (coreIncident C L)).ker) : liftVL L g ∈ (restrictedCoboundaryMap C L).ker

If g ∈ ker(coreCoboundary), then liftVL g ∈ ker(restrictedCoboundary). This holds because the restricted incidence is trivial outside VL and EL.

theorem CohenEtAlSchemeRecovery.coboundary_from_boundary_step {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (hL : IsIrreducibleXLogical C L) (γ : C.I → ZMod 2) (hγ_ker : γ ∈ (restrictedBoundaryMap C L).ker) (hγ_ne : γ ≠ 0) (hallones_ker : (fun (i : C.I) => if i ∈ relevantZChecks C L then 1 else 0) ∈ (restrictedBoundaryMap C L).ker) (hγ_ne_allones : γ ≠ fun (i : C.I) => if i ∈ relevantZChecks C L then 1 else 0) (hγ_supp : ∀ i ∉ relevantZChecks C L, γ i = 0) (hVL_ge_EL : (relevantZChecks C L).card ≤ (logicalSupport L).card) : ∃ f ∈ (restrictedCoboundaryMap C L).ker, (∀ q ∉ logicalSupport L, f q = 0) ∧ f ≠ 0 ∧ ∃ q ∈ logicalSupport L, f q = 0

Coboundary from boundary step (rank-nullity). If ker(restricted ∂) contains two EL-supported linearly independent elements, and |VL| ≥ |EL|, then ker(restricted δ) contains a VL-supported element f ≠ 0 with ∃ q ∈ VL, f q = 0. This replaces the former hypothesis hcoboundary_from_boundary using the Z₂ rank-nullity theorem.

theorem CohenEtAlSchemeRecovery.irrelevant_check_no_incident {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (i : C.I) (hi : i ∉ relevantZChecks C L) (q : Q) : ¬restrictedZCheckIncident C L q i

theorem CohenEtAlSchemeRecovery.ker_restrict_to_relevant {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (γ : C.I → ZMod 2) (hγ : γ ∈ (restrictedBoundaryMap C L).ker) : (fun (i : C.I) => if i ∈ relevantZChecks C L then γ i else 0) ∈ (restrictedBoundaryMap C L).ker

If γ ∈ ker(∂) and γ' agrees with γ on relevant checks and is 0 on irrelevant ones, then γ' ∈ ker(∂) as well.

theorem CohenEtAlSchemeRecovery.complement_in_ker {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (γ : C.I → ZMod 2) (hγ_ker : γ ∈ (restrictedBoundaryMap C L).ker) (hallones_ker : (fun (i : C.I) => if i ∈ relevantZChecks C L then 1 else 0) ∈ (restrictedBoundaryMap C L).ker) : (fun (i : C.I) => if i ∈ relevantZChecks C L then 1 + γ i else 0) ∈ (restrictedBoundaryMap C L).ker

The complement of a kernel element (relative to all-ones on relevant checks) is also in the kernel.

theorem CohenEtAlSchemeRecovery.gamma_add_complement {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (γ : C.I → ZMod 2) (hγ_supp : ∀ i ∉ relevantZChecks C L, γ i = 0) (i : C.I) : (γ i + if i ∈ relevantZChecks C L then 1 + γ i else 0) = if i ∈ relevantZChecks C L then 1 else 0

γ and its complement on relevant checks sum to the all-ones vector.

theorem CohenEtAlSchemeRecovery.kernel_restricted_boundary_trivial {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (hL : IsIrreducibleXLogical C L) (hcss : SteaneStyleMeasurement.IsCSS C) (hVL_ge_EL : (relevantZChecks C L).card ≤ (logicalSupport L).card) (γ : C.I → ZMod 2) : γ ∈ (restrictedBoundaryMap C L).ker → (∀ i ∉ relevantZChecks C L, γ i = 0) → (fun (i : C.I) => if i ∈ relevantZChecks C L then 1 else 0) ∈ (restrictedBoundaryMap C L).ker → γ = 0 ∨ ∀ i ∈ relevantZChecks C L, γ i = 1

Kernel triviality from irreducibility.

For an irreducible X logical operator L of a CSS stabilizer code C, the kernel of the restricted boundary map ∂ : Z₂^{E_L} → Z₂^{V_L} consists only of 0 and the all-ones vector on E_L (corresponding to L itself).

The proof combines two ingredients:

1. Coboundary kernel → centralizer factorization: Any nontrivial f ∈ ker(δ) gives a factorization L = prodX(supp(f)) · prodX(V_L \ supp(f)) with both factors in the centralizer (by coboundary_ker_gives_centralizer_pair).
2. Irreducibility contradiction: Such a factorization contradicts the irreducibility of L (both factors have weight < wt(L) unless trivial).

The Z₂-rank-nullity step (coboundary_from_boundary_step) proves that if ker(∂) has a nontrivial element besides 0 and the all-ones vector, then ker(δ) contains a nontrivial element f with f ≠ 0 and f ≠ all-ones-on-V_L. This uses dim(ker(δ)) = |V_L| - |E_L| + dim(ker(∂)) ≥ 2 when |V_L| ≥ |E_L|, via Matrix.rank_transpose and z2_finrank_ker_formula.

Cohen et al. d-layer construction as hypergraph gauging

The Cohen et al. construction creates d copies of the logical support vertices, connects copies of the same vertex across layers via path graphs (chains), and joins vertices within each layer via the same hypergraph structure.

This is the layered incidence relation on Q × Fin d. The hypergraph gauging framework from Rem_17 applies directly to this layered incidence, giving pure X-type commuting Gauss operators and kernel characterization.

@[reducible, inline]

abbrev CohenEtAlSchemeRecovery.CohenVertex (Q : Type u_3) (d : ℕ) : Type u_3

The Cohen et al. layered vertex type: d copies of the qubit set Q.

Equations

• CohenEtAlSchemeRecovery.CohenVertex Q d = (Q × Fin d)

@[reducible, inline]

abbrev CohenEtAlSchemeRecovery.InterLayerEdge (Q : Type u_3) (d : ℕ) : Type u_3

The inter-layer edge type: connects copies of the same vertex in consecutive layers.

Equations

• CohenEtAlSchemeRecovery.InterLayerEdge Q d = (Q × Fin (d - 1))

@[reducible, inline]

abbrev CohenEtAlSchemeRecovery.IntraLayerEdge (I : Type u_3) (d : ℕ) : Type u_3

The intra-layer edge type: replicates the original check structure within each layer.

Equations

• CohenEtAlSchemeRecovery.IntraLayerEdge I d = (I × Fin d)

@[reducible, inline]

abbrev CohenEtAlSchemeRecovery.CohenEdge (Q : Type u_3) (I : Type u_4) (d : ℕ) : Type (max u_3 u_4)

The combined edge type for the Cohen construction.

Equations

• CohenEtAlSchemeRecovery.CohenEdge Q I d = (CohenEtAlSchemeRecovery.InterLayerEdge Q d ⊕ CohenEtAlSchemeRecovery.IntraLayerEdge I d)

def CohenEtAlSchemeRecovery.layeredIncident {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (d : ℕ) : CohenVertex Q d → CohenEdge Q C.I d → Prop

The incidence relation for the layered construction. A vertex (q, ℓ) in the layered graph is incident to:

• Inter-layer edge (q', k): q = q' and ℓ ∈ {k, k+1} (path graph connection)
• Intra-layer edge (i, ℓ'): ℓ = ℓ' and q is incident to check i in restricted hypergraph

Equations

• CohenEtAlSchemeRecovery.layeredIncident C L d (q, ℓ) (Sum.inl (q', k)) = (q = q' ∧ (↑ℓ = ↑k ∨ ↑ℓ = ↑k + 1))
• CohenEtAlSchemeRecovery.layeredIncident C L d (q, ℓ) (Sum.inr (i, ℓ')) = (ℓ = ℓ' ∧ CohenEtAlSchemeRecovery.restrictedZCheckIncident C L q i)

instance CohenEtAlSchemeRecovery.layeredIncident_decidable {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (d : ℕ) (v : CohenVertex Q d) (e : CohenEdge Q C.I d) : Decidable (layeredIncident C L d v e)

Equations

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

theorem CohenEtAlSchemeRecovery.cohen_layered_all_ones_measures_L {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (d : ℕ) (v : CohenVertex Q d) : (HypergraphGeneralization.hyperGaussSubsetProduct (layeredIncident C L d) fun (x : CohenVertex Q d) => 1).xVec (Sum.inl v) = 1 ∧ (HypergraphGeneralization.hyperGaussSubsetProduct (layeredIncident C L d) fun (x : CohenVertex Q d) => 1).zVec = 0

The Cohen et al. scheme is recovered as hypergraph gauging (Rem_17) applied to the layered incidence with d copies.

The all-ones Gauss subset product measures L: its xVec restricts to 1 on all vertex qubits by hyperGaussSubsetProduct_xVec_vertex, and it is pure X-type by hyperGaussSubsetProduct_zVec.

The Gauss operators are pure X-type (hyperGaussLawOp_zVec) and mutually commute (hyperGaussLaw_commute). The kernel of the layered boundary map characterizes which operators can be measured (ker_boundary_iff_commutes_all_gaussLaw).

Cross et al. modification: fewer layers with Cheeger expansion

The Cross et al. modification uses R < d layers of dummy vertices. This is recovered by choosing fewer layers in the hypergraph gauging construction while maintaining sufficient expansion (Cheeger constant ≥ 1, Rem_4/Rem_11) in the inter-layer graph.

By Lemma 3 (deformed_distance_ge_min_cheeger_d): with Cheeger constant h(G) of the inter-layer graph, the deformed code distance satisfies d* ≥ min(h(G), 1) · d. When h(G) ≥ 1 (sufficient expansion, SufficientExpansion), d* ≥ d (distance fully preserved, deformed_distance_ge_d_sufficient_expansion).

def CohenEtAlSchemeRecovery.pathGraphAdj (R : ℕ) (a b : Fin R) : Prop

The path graph on R vertices: vertices are Fin R, edges connect consecutive vertices. This is the inter-layer connectivity graph in the Cross et al. modification.

Equations

• CohenEtAlSchemeRecovery.pathGraphAdj R a b = (↑a + 1 = ↑b ∨ ↑b + 1 = ↑a)

instance CohenEtAlSchemeRecovery.pathGraphAdj_decidable (R : ℕ) (a b : Fin R) : Decidable (pathGraphAdj R a b)

Equations

• CohenEtAlSchemeRecovery.pathGraphAdj_decidable R a b = inferInstanceAs (Decidable (↑a + 1 = ↑b ∨ ↑b + 1 = ↑a))

theorem CohenEtAlSchemeRecovery.cross_layered_gauss_product_pure_X_with_vertex_values {Q : Type u_2} [Fintype Q] [DecidableEq Q] (C : StabilizerCode Q) [DecidableEq C.I] (L : PauliOp Q) (R : ℕ) (c : CohenVertex Q R → ZMod 2) : (HypergraphGeneralization.hyperGaussSubsetProduct (layeredIncident C L R) c).zVec = 0 ∧ ∀ (v : CohenVertex Q R), (HypergraphGeneralization.hyperGaussSubsetProduct (layeredIncident C L R) c).xVec (Sum.inl v) = c v

The Cross et al. scheme applies the same layered construction with R ≤ d layers. The Gauss product for coefficient c gives a pure X-type operator with c as its vertex X-vector, by the hypergraph gauging framework (Rem_17).

theorem CohenEtAlSchemeRecovery.pathGraphAdj_symm (R : ℕ) (a b : Fin R) : pathGraphAdj R a b → pathGraphAdj R b a

The path graph adjacency relation is symmetric.

theorem CohenEtAlSchemeRecovery.pathGraphAdj_irrefl (R : ℕ) (a : Fin R) : ¬pathGraphAdj R a a

The path graph adjacency is irreflexive.

def CohenEtAlSchemeRecovery.pathGraph (R : ℕ) : SimpleGraph (Fin R)

The path graph on R vertices as a SimpleGraph.

Equations

• CohenEtAlSchemeRecovery.pathGraph R = { Adj := fun (a b : Fin R) => CohenEtAlSchemeRecovery.pathGraphAdj R a b, symm := ⋯, loopless := ⋯ }

instance CohenEtAlSchemeRecovery.pathGraph_decidableRel (R : ℕ) : DecidableRel (pathGraph R).Adj

Equations

• CohenEtAlSchemeRecovery.pathGraph_decidableRel R a b = CohenEtAlSchemeRecovery.pathGraphAdj_decidable R a b

theorem CohenEtAlSchemeRecovery.cross_expansion_bound (R : ℕ) (S : Finset (Fin R)) (hne : S.Nonempty) (hsize : 2 * S.card ≤ Fintype.card (Fin R)) (c : ℝ) (hc : c ≤ QEC1.cheegerConstant (pathGraph R)) : c * ↑S.card ≤ ↑(QEC1.SimpleGraph.edgeBoundary (pathGraph R) S).card

For the Cross et al. scheme with R layers: the edge boundary of any valid subset S satisfies |∂S| ≥ c · |S| for any c ≤ h(P_R), connecting the Cheeger constant of the path graph to the distance bound from Lemma 3.

Joint measurement of products via edge addition

Given two systems (Q₁, E₁, incident₁) and (Q₂, E₂, incident₂), the joint system has vertices Q₁ ⊕ Q₂ and edges E₁ ⊕ E₂ ⊕ B (where B are bridge edges connecting the two systems). The key property is that the joint Gauss product measures the product of the individual logicals L₁ ⊗ L₂.

def CohenEtAlSchemeRecovery.jointIncident {Q₁ : Type u_2} {Q₂ : Type u_3} {E₁ : Type u_4} (incident₁ : Q₁ → E₁ → Prop) {E₂ : Type u_5} (incident₂ : Q₂ → E₂ → Prop) {B : Type u_6} [DecidableEq B] (bridgeQ1 : B → Q₁) (bridgeQ2 : B → Q₂) : Q₁ ⊕ Q₂ → E₁ ⊕ E₂ ⊕ B → Prop

The joint incidence: combines the two individual incidence relations with bridge edges connecting specified pairs across Q₁ and Q₂.

Equations

• CohenEtAlSchemeRecovery.jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2 (Sum.inl q₁) (Sum.inl e₁) = incident₁ q₁ e₁
• CohenEtAlSchemeRecovery.jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2 (Sum.inr q₂) (Sum.inr (Sum.inl e₂)) = incident₂ q₂ e₂
• CohenEtAlSchemeRecovery.jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2 (Sum.inl q₁) (Sum.inr (Sum.inr b)) = (q₁ = bridgeQ1 b)
• CohenEtAlSchemeRecovery.jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2 (Sum.inr q₂) (Sum.inr (Sum.inr b)) = (q₂ = bridgeQ2 b)
• CohenEtAlSchemeRecovery.jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2 q e = False

theorem CohenEtAlSchemeRecovery.joint_gauss_product_measures_product {Q₁ : Type u_2} {Q₂ : Type u_3} [Fintype Q₁] [DecidableEq Q₁] [Fintype Q₂] [DecidableEq Q₂] {E₁ : Type u_4} [Fintype E₁] [DecidableEq E₁] (incident₁ : Q₁ → E₁ → Prop) [(q : Q₁) → (e : E₁) → Decidable (incident₁ q e)] {E₂ : Type u_5} [Fintype E₂] [DecidableEq E₂] (incident₂ : Q₂ → E₂ → Prop) [(q : Q₂) → (e : E₂) → Decidable (incident₂ q e)] {B : Type u_6} [Fintype B] [DecidableEq B] (bridgeQ1 : B → Q₁) (bridgeQ2 : B → Q₂) (c₁ : Q₁ → ZMod 2) (c₂ : Q₂ → ZMod 2) (c : Q₁ ⊕ Q₂ → ZMod 2) (hc : c = Sum.elim c₁ c₂) : (∀ (q₁ : Q₁), (HypergraphGeneralization.hyperGaussSubsetProduct (jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2) c).xVec (Sum.inl (Sum.inl q₁)) = c₁ q₁) ∧ (∀ (q₂ : Q₂), (HypergraphGeneralization.hyperGaussSubsetProduct (jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2) c).xVec (Sum.inl (Sum.inr q₂)) = c₂ q₂) ∧ (HypergraphGeneralization.hyperGaussSubsetProduct (jointIncident incident₁ incident₂ bridgeQ1 bridgeQ2) c).zVec = 0

Adding bridge edges enables joint measurement: the joint Gauss subset product for coefficient (c₁, c₂) on Q₁ ⊕ Q₂ gives a pure X-type operator that restricts to c₁ on Q₁ and c₂ on Q₂, measuring L₁ ⊗ L₂.