Tensor decomposition of the hypergraph-product (HGP) parity-check matrices

The Tillich–Zémor hypergraph product glues two classical codes $C_1, C_2$ (parity-check matrices $H_1 : r_1 \times n_1$ and $H_2 : r_2 \times n_2$) into a quantum code on $n_1 n_2 + r_1 r_2$ qubits, whose two families of checks take block tensor form:

$$H_X = [\,H_1 \otimes I_{n_2} \;\middle|\; I_{r_1} \otimes H_2^\top\,],\qquad H_Z = [\,I_{n_1} \otimes H_2 \;\middle|\; H_1^\top \otimes I_{r_2}\,].$$

This module gives the entrywise definition of the construction (hgpHX / hgpHZ) and the first structural theorem:

• hgp_orthogonal: $H_X H_Z^\top = 0$. The CSS compatibility condition holds for arbitrary inputs $H_1, H_2$, and the proof is purely algebraic (the two blocks each contribute $H_1 \otimes H_2^\top$, which cancel over GF(2)); it enumerates nothing.

The distance bounds are proved in GF2/HGPCleaning and GF2/HGPCleaningDual; GF2/HGPKunneth supplies the rank and dimension formula. Concrete code instances from upstream are outside this import.

Index conventions

• Rows and columns are product and sum types (not flattened to Fin), so no relabelling is needed: the rows of hgpHX are Fin r₁ × Fin n₂ and the rows of hgpHZ are Fin n₁ × Fin r₂, and both share the column space (Fin n₁ × Fin n₂) ⊕ (Fin r₁ × Fin r₂).
• Flattening to Fin (for the instance anchor) is left to Matrix.reindex.

Construction

def QECCertificates.hgpHX {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : Matrix (Fin r₁ × Fin n₂) (Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂) (ZMod 2)

The X-type checks of the HGP $H_X = [H_1 \otimes I_{n_2} \mid I_{r_1} \otimes H_2^\top]$.

A row is (i, j) : r₁ × n₂. On the left half of the columns, (a, b) : n₁ × n₂, the entry is $H_1\, i\,a \cdot [j = b]$; on the right half, (s, t) : r₁ × r₂, it is $[i = s] \cdot H_2\, t\, j$ (the $(j, t)$ entry of $H_2^\top$).

Equations

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

def QECCertificates.hgpHZ {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : Matrix (Fin n₁ × Fin r₂) (Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂) (ZMod 2)

The Z-type checks of the HGP $H_Z = [I_{n_1} \otimes H_2 \mid H_1^\top \otimes I_{r_2}]$.

A row is (a, d) : n₁ × r₂. On the left half of the columns the entry is $[a = a'] \cdot H_2\, d\, b$; on the right half it is $H_1\, s\, a \cdot [d = t]$.

Equations

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

theorem QECCertificates.hgpHX_inl {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₂) (ab : Fin n₁ × Fin n₂) : hgpHX H₁ H₂ x (Sum.inl ab) = H₁ x.1 ab.1 * if x.2 = ab.2 then 1 else 0

The four blocks, described entrywise (rfl level).

theorem QECCertificates.hgpHX_inr {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₂) (st : Fin r₁ × Fin r₂) : hgpHX H₁ H₂ x (Sum.inr st) = (if x.1 = st.1 then 1 else 0) * H₂ st.2 x.2

theorem QECCertificates.hgpHZ_inl {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (x : Fin n₁ × Fin r₂) (ab : Fin n₁ × Fin n₂) : hgpHZ H₁ H₂ x (Sum.inl ab) = (if x.1 = ab.1 then 1 else 0) * H₂ x.2 ab.2

theorem QECCertificates.hgpHZ_inr {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (x : Fin n₁ × Fin r₂) (st : Fin r₁ × Fin r₂) : hgpHZ H₁ H₂ x (Sum.inr st) = H₁ st.1 x.1 * if x.2 = st.2 then 1 else 0

The structural theorem: CSS compatibility

theorem QECCertificates.hgp_orthogonal {r₁ n₁ r₂ n₂ : ℕ} (H₁ : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (H₂ : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : hgpHX H₁ H₂ * (hgpHZ H₁ H₂).transpose = 0

CSS compatibility of the HGP (structural theorem): $H_X H_Z^\top = 0$ for arbitrary $H_1, H_2$.

The two blocks contribute $(H_1 \otimes I)(I \otimes H_2)^\top = H_1 \otimes H_2^\top$ and $(I \otimes H_2^\top)(H_1^\top \otimes I)^\top = H_1 \otimes H_2^\top$ respectively, that is, the same matrix added to itself, which is zero over GF(2). The two Finset.sum_eq_single applications in the proof are this tensor identity at the entrywise level: each product $H_1\, i\, a \cdot H_2\, d\, j$ is contributed exactly once, by $(a, j)$ on the left half and by $(i, d)$ on the right half.