HGP, part two: the compression identity, the transpose code, and the single-block weight lower

bound (continued)

The first part (GF2/HGP) gives the construction and the CSS orthogonality. This module supplies the three building blocks needed for the distance analysis.

1. The compression identity

Read a vector v as two matrices over the two blocks of the column space, blockL v ($n_1\times n_2$) and blockR v ($r_1\times r_2$). Entrywise computation gives

$$H_X\, v = 0 \iff H_1 \cdot \mathrm{blockL}\,v = \mathrm{blockR}\,v \cdot H_2,\qquad H_Z\, v = 0 \iff \mathrm{blockL}\,v \cdot H_2^\top = H_1^\top \cdot \mathrm{blockR}\,v.$$

The first of the two presents the pair $U = \mathrm{blockL}\,v$, $R = \mathrm{blockR}\,v$ as a commuting square ($H_1 U = R H_2$), which is exactly the entrywise form of the "chain map" picture of the hypergraph product. Every case of the distance lower bound starts from the identity on that same side.

2. The transpose code

Take the inputs transposed and use them as new parity-check matrices. Then the column space of hgpHZ H₁ᵀ H₂ᵀ is $(r_1 r_2) \oplus (n_1 n_2)$ (the two blocks exchange their shapes), and after "swapping the two blocks" its row (a, d) agrees entrywise with the same row of hgpHX H₁ H₂:

hgpHZ H₁ᵀ H₂ᵀ x c = hgpHX H₁ H₂ x (sumComm c).

So HGP(H₁ᵀ, H₂ᵀ) is exactly the transpose code of HGP(H₁, H₂): the X-side analysis and the Z-side analysis are two applications of one and the same argument, which is the source of the distance of ker H₂ᵀ (the transpose-code distance) appearing in the lower bound formula.

3. The single-block weight lower bound

If an X-type operator has support only in the left block (blockR v = 0), the compression identity forces every column to be a kernel vector of $H_1$; the weight of any nonzero column is at least the left-code distance d₁, and the weight of a single column is at most the weight of the whole vector: d₁ ≤ hammingNorm (column) ≤ hammingNorm v

The right block gives d₂ᵀ (the distance of $\ker H_2^\top$) in the same way. The case where both blocks are nonzero at once, that is, where the two contributions cancel each other, requires the cleaning/quotient argument provided by GF2/HGPCleaning; this module supplies the single-block bounds used by that argument.

Main results

• hgpHX_mulVec_eq_zero_iff / hgpHZ_mulVec_eq_zero_iff: the compression identity.
• hgpHZ_transpose_inputs_apply: the transpose-code relation.
• hgp_hammingNorm_ge_of_pure_left / _of_pure_right: the single-block weight lower bound.

Reading the blocks

def QECCertificates.blockL {r₁ n₁ r₂ n₂ : ℕ} (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) : Matrix (Fin n₁) (Fin n₂) (ZMod 2)

Read a vector as a matrix on the left block ($n_1\times n_2$).

Equations

• QECCertificates.blockL v a b = v (Sum.inl (a, b))

def QECCertificates.blockR {r₁ n₁ r₂ n₂ : ℕ} (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) : Matrix (Fin r₁) (Fin r₂) (ZMod 2)

Read a vector as a matrix on the right block ($r_1\times r_2$).

Equations

• QECCertificates.blockR v s t = v (Sum.inr (s, t))

@[simp]

theorem QECCertificates.blockL_apply {r₁ n₁ r₂ n₂ : ℕ} (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) (a : Fin n₁) (b : Fin n₂) : blockL v a b = v (Sum.inl (a, b))

@[simp]

theorem QECCertificates.blockR_apply {r₁ n₁ r₂ n₂ : ℕ} (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) (s : Fin r₁) (t : Fin r₂) : blockR v s t = v (Sum.inr (s, t))

Slicing lemmas for the entrywise computation

theorem QECCertificates.sum_prod_slice_snd {m k : ℕ} (A : Fin m → ZMod 2) (F : Fin m → Fin k → ZMod 2) (j : Fin k) : ∑ p : Fin m × Fin k, (A p.1 * if j = p.2 then 1 else 0) * F p.1 p.2 = ∑ a : Fin m, A a * F a j

"Take one column" on a product index: Σ_{a,b} A a · [j = b] · F a b = Σ_a A a · F a j.

theorem QECCertificates.sum_prod_slice_fst {m k : ℕ} (B : Fin k → ZMod 2) (F : Fin m → Fin k → ZMod 2) (i : Fin m) : ∑ p : Fin m × Fin k, (if i = p.1 then 1 else 0) * B p.2 * F p.1 p.2 = ∑ b : Fin k, B b * F i b

"Take one row" on a product index: Σ_{a,b} [i = a] · B b · F a b = Σ_b B b · F i b.

The compression identity

theorem QECCertificates.hgpHX_mulVec_apply {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) (i : Fin r₁) (j : Fin n₂) : (hgpHX H₁ H₂).mulVec v (i, j) = (H₁ * blockL v) i j + (blockR v * H₂) i j

X side, entrywise: (H_X v)_{(i,j)} = (H_1 · U)_{ij} + (R · H_2)_{ij}, where U = blockL v and R = blockR v.

The two sums reduce by the definitions of H_X, H_1 ⊗ I and I ⊗ H_2 (at the rfl level), and one slicing lemma each then collapses the sum over the product index into a sum over a single index.

theorem QECCertificates.hgpHZ_mulVec_apply {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) (a : Fin n₁) (d : Fin r₂) : (hgpHZ H₁ H₂).mulVec v (a, d) = (blockL v * H₂.transpose) a d + (H₁.transpose * blockR v) a d

Z side, entrywise: (H_Z v)_{(a,d)} = (U · H_2ᵀ)_{ad} + (H_1ᵀ · R)_{ad}.

theorem QECCertificates.hgpHX_mulVec_eq_zero_iff {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) : (hgpHX H₁ H₂).mulVec v = 0 ↔ H₁ * blockL v = blockR v * H₂

Compression identity (X side): $H_X v = 0 \iff H_1\,U = R\,H_2$.

The equality on the right is the statement that $(U, R)$ is a chain map; the whole case analysis of the distance lower bound unfolds from it.

theorem QECCertificates.hgpHZ_mulVec_eq_zero_iff {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) : (hgpHZ H₁ H₂).mulVec v = 0 ↔ blockL v * H₂.transpose = H₁.transpose * blockR v

Compression identity (Z side): $H_Z v = 0 \iff U\,H_2^\top = H_1^\top\,R$.

The transpose code

theorem QECCertificates.hgpHZ_transpose_inputs_apply {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (x : Fin r₁ × Fin n₂) (c : Fin r₁ × Fin r₂ ⊕ Fin n₁ × Fin n₂) : hgpHZ H₁.transpose H₂.transpose x c = hgpHX H₁ H₂ x ((Equiv.sumComm (Fin r₁ × Fin r₂) (Fin n₁ × Fin n₂)) c)

Transpose-code relation: the Z parity-check matrix obtained from the transposed inputs agrees entrywise with the original X parity-check matrix, under the column relabelling that swaps the two blocks. Hence HGP(H₁ᵀ, H₂ᵀ) is the transpose code of HGP(H₁, H₂), and the X-side and Z-side distance analyses are two applications of one and the same argument.

The single-block weight lower bound

theorem QECCertificates.hammingNorm_le_of_injective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α → β) (he : Function.Injective e) (v : β → ZMod 2) : (hammingNorm fun (a : α) => v (e a)) ≤ hammingNorm v

Pulling a vector back along an injection does not increase its weight (the support embeds under the injection).

theorem QECCertificates.hgp_hammingNorm_ge_of_pure_left {r₁ n₁ r₂ n₂ : ℕ} {H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)} {H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)} {v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2} (hv : (hgpHX H₁ H₂).mulVec v = 0) (hR : blockR v = 0) {d : ℕ} (hd : ∀ (w : Vec n₁), w ≠ 0 → H₁.mulVec w = 0 → d ≤ hammingNorm w) (hL : blockL v ≠ 0) : d ≤ hammingNorm v

Single-block weight lower bound (left): an X-type operator supported only in the left block has weight at least the left-code distance d₁.

Every column of the left block lies in ker H₁ (compression identity plus blockR v = 0), a nonzero column has weight at least d₁, and a single column weighs no more than the whole vector.

theorem QECCertificates.hgp_hammingNorm_ge_of_pure_right {r₁ n₁ r₂ n₂ : ℕ} {H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)} {H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)} {v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2} (hv : (hgpHX H₁ H₂).mulVec v = 0) (hL : blockL v = 0) {d : ℕ} (hd : ∀ (w : Vec r₂), w ≠ 0 → H₂.transpose.mulVec w = 0 → d ≤ hammingNorm w) (hR : blockR v ≠ 0) : d ≤ hammingNorm v

Single-block weight lower bound (right): an X-type operator supported only in the right block has weight at least the distance of ker H₂ᵀ (the transpose-code distance d₂ᵀ), which is exactly why the transpose code appears in the lower bound formula.

Every row r_i of the right block satisfies H₂ᵀ r_i = 0 (compression identity plus blockL v = 0).