The dimension tensor formula for HGP: k = k₁k₂ + k₁ᵀk₂ᵀ

The number of logical qubits of the Tillich–Zémor hypergraph product satisfies a Künneth-type tensor formula:

$$k(\mathrm{HGP}(H_1,H_2)) \;=\; k_1k_2 + k_1^\top k_2^\top,\qquad k_1 = \dim\ker H_1,\quad k_1^\top=\dim\ker H_1^\top,$$

where $k = n - \operatorname{rank}H_X - \operatorname{rank}H_Z$ ($n = n_1n_2+r_1r_2$). The first part gives the construction and the CSS orthogonality, the second the compression identity and the third the distance lower bound; this module supplies the dimension side, and with it the picture is complete: both the distance side and the dimension side are structural theorems for arbitrary inputs $H_1,H_2$.

Proof outline

The rank of hgpHX is the rank of a block matrix:

$$\operatorname{rank}[,A\otimes I_s \mid I_p\otimes B^\top,] = \operatorname{rank}(A\otimes I_s) + \operatorname{rank}(I_p\otimes B^\top)

• \dim\big(\mathrm{im}(A\otimes I_s)\cap \mathrm{im}(I_p\otimes B^\top)\big),$$

and each of the three terms is a dimension fact from KunnethCore:

term	identification	dimension
im(A ⊗ I)	matrices with columns in col A (colsSub)	s · rank A (finrank_colsSub)
im(I ⊗ Bᵀ)	matrices with rows in row B (rowsSub)	p · rank B (finrank_rowsSub)
intersection	columns in col A and rows in row B	rank A · rank B

(`finrank_colsRows`, the tensor intersection of subspaces) |

For $H_Z$ the transport goes along the transpose code (mulVec_swap_eq from the third part): $H_Z(A,B)$ and $H_X(A^\top,B^\top)$ differ only by the block swap of the columns, so their ranks agree, and the distance side runs on the same argument.

Main results

• rank_hgpHX_add: rank H_X + rank A · rank B = n₂ · rank A + r₁ · rank B
• rank_hgpHZ_add: rank H_Z + rank A · rank B = r₂ · rank A + n₁ · rank B
• hgp_kunneth: $k = k_1k_2+k_1^\top k_2^\top$ (subtraction form).

1. The two block maps M ↦ A·M and N ↦ N·B

noncomputable def QECCertificates.mulLeft {p q s : ℕ} (A : Matrix (Fin p) (Fin q) (ZMod 2)) : VMat q s →ₗ[ZMod 2] VMat p s

Left multiplication block M ↦ A·M (that is, $A\otimes I$): the rows p carry the action of A and the columns stay fixed.

Equations

• QECCertificates.mulLeft A = { toFun := fun (M : QECCertificates.VMat q s) (ij : Fin p × Fin s) => ∑ a : Fin q, A ij.1 a * M (a, ij.2), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def QECCertificates.mulRight {p r s : ℕ} (B : Matrix (Fin r) (Fin s) (ZMod 2)) : VMat p r →ₗ[ZMod 2] VMat p s

Right multiplication block N ↦ N·B (that is, $I\otimes B$): the columns carry the action of B and the rows stay fixed.

Equations

• QECCertificates.mulRight B = { toFun := fun (N : QECCertificates.VMat p r) (ij : Fin p × Fin s) => ∑ t : Fin r, N (ij.1, t) * B t ij.2, map_add' := ⋯, map_smul' := ⋯ }

2. The images of the two blocks: column and row constraints

theorem QECCertificates.range_mulLeft {p q s : ℕ} (A : Matrix (Fin p) (Fin q) (ZMod 2)) : (mulLeft A).range = colsSub A.mulVecLin.range

The image of the left block is the column-constraint space: the image of M ↦ A·M consists exactly of the matrices whose every column lies in the column space of A.

theorem QECCertificates.range_mulRight {p r s : ℕ} (B : Matrix (Fin r) (Fin s) (ZMod 2)) : (mulRight B).range = rowsSub B.certificateRowSpace

The image of the right block is the row-constraint space: the image of N ↦ N·B consists exactly of the matrices whose every row lies in the row space of B.

3. The rank of H_X

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

Block reading (product index): the left block n₁×n₂.

Equations

• QECCertificates.blkL v ab = v (Sum.inl ab)

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

Block reading (product index): the right block r₁×r₂.

Equations

• QECCertificates.blkR v st = v (Sum.inr st)

theorem QECCertificates.hgpHX_mulVecLin_eq_blocks {r₁ n₁ r₂ n₂ : ℕ} (A : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (B : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) : (hgpHX A B).mulVecLin v = (mulLeft A) (blkL v) + (mulRight B) (blkR v)

The block action of H_X: H_X v = A·U + R·B (with U = blkL v and R = blkR v), the "sum of matrices" form of the compression identity.

theorem QECCertificates.rank_hgpHX_add {r₁ n₁ r₂ n₂ : ℕ} (A : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (B : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : (hgpHX A B).rank + A.rank * B.rank = A.rank * n₂ + B.rank * r₁

The rank of H_X equals the dimension of the sum of the images of the two blocks.

4. The rank of H_Z (transport along the transpose code)

theorem QECCertificates.rank_hgpHZ_eq {r₁ n₁ r₂ n₂ : ℕ} (A : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (B : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : (hgpHZ A B).rank = (hgpHX A.transpose B.transpose).rank

The rank of H_Z equals the rank of H_X on the transposed inputs: the two matrices differ only by the block swap of the columns (mulVec_swap_eq from the third part), so their images agree.

theorem QECCertificates.rank_hgpHZ_add {r₁ n₁ r₂ n₂ : ℕ} (A : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (B : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : (hgpHZ A B).rank + A.rank * B.rank = A.rank * r₂ + B.rank * n₁

The rank of H_Z: the same shape as rank_hgpHX_add, with n₂ ↦ r₂ and r₁ ↦ n₁.

5. The dimension tensor formula

theorem QECCertificates.hgp_kunneth_int {r₁ n₁ r₂ n₂ : ℕ} (A : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (B : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : ↑(hgpHX A B).rank + ↑(hgpHZ A B).rank + ((↑n₁ - ↑A.rank) * (↑n₂ - ↑B.rank) + (↑r₁ - ↑A.rank) * (↑r₂ - ↑B.rank)) = ↑n₁ * ↑n₂ + ↑r₁ * ↑r₂

Dimension tensor formula (integer form): rewrite k = n - rank H_X - rank H_Z additively and do the polynomial arithmetic over ℤ (nlinarith), which avoids truncated subtraction in ℕ.

theorem QECCertificates.hgp_kunneth {r₁ n₁ r₂ n₂ : ℕ} (A : Matrix (Fin r₁) (Fin n₁) (ZMod 2)) (B : Matrix (Fin r₂) (Fin n₂) (ZMod 2)) : n₁ * n₂ + r₁ * r₂ - (hgpHX A B).rank - (hgpHZ A B).rank = (n₁ - A.rank) * (n₂ - B.rank) + (r₁ - A.rank) * (r₂ - B.rank)

Dimension tensor formula for HGP (Künneth): the number of logical qubits $k = n - \operatorname{rank}H_X - \operatorname{rank}H_Z$ is exactly $k_1k_2 + k_1^\top k_2^\top$ (the sum of the products of the kernel dimensions of the two classical codes).

This is the last piece: the distance side (the third part together with the dual side) and the dimension side (this theorem) together give the HGP family parameters for $n\ge144$ a structural assertion that does not rely on enumeration.