Hypergraph-product transpose transport

Swapping the column blocks identifies the Z check with the X check on transposed inputs, preserving kernels, row spaces and Hamming weight. This transport supports both the dimension formula and the distance bounds without importing a cleaning proof.

Split from upstream GF2/HGPCleaningDual.lean without changing the declarations.

1. The block swap

def QECCertificates.swapBlocks {α : Type u_1} {β : Type u_2} : α ⊕ β → β ⊕ α

The block swap, an involution: $\alpha\oplus\beta \to \beta\oplus\alpha$. It is exactly the Equiv.sumComm appearing in hgpHZ_transpose_inputs_apply.

Equations

• QECCertificates.swapBlocks = Sum.swap

theorem QECCertificates.swapBlocks_swapBlocks {α : Type u_1} {β : Type u_2} (c : α ⊕ β) : swapBlocks (swapBlocks c) = c

The block swap is an involution.

theorem QECCertificates.swapBlocks_injective {α : Type u_1} {β : Type u_2} : Function.Injective swapBlocks

The block swap is injective.

theorem QECCertificates.hammingNorm_swapBlocks {r₁ n₁ r₂ n₂ : ℕ} (v : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂ → ZMod 2) : (hammingNorm fun (c : Fin r₁ × Fin r₂ ⊕ Fin n₁ × Fin n₂) => v (swapBlocks c)) = hammingNorm v

The block swap preserves weight.

2. The row identity and the correspondence of kernels

theorem QECCertificates.hgpHZ_row_eq_swap {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₂) : hgpHZ H₁ H₂ x = fun (c : Fin n₁ × Fin n₂ ⊕ Fin r₁ × Fin r₂) => hgpHX H₁.transpose H₂.transpose x (swapBlocks c)

The row identity: row $x$ of $H_Z(H_1^\top,H_2^\top)$ is row $x$ of $H_X(H_1,H_2)$ followed by the block swap, entrywise, straight from the transpose-code relation of part two.

theorem QECCertificates.mulVec_swap_eq {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) (x : Fin n₁ × Fin r₂) : (hgpHZ H₁ H₂).mulVec v x = (hgpHX H₁.transpose H₂.transpose).mulVec (fun (c : Fin r₁ × Fin r₂ ⊕ Fin n₁ × Fin n₂) => v (swapBlocks c)) x

The row identity for the dot products: the two kernel conditions are equal row by row, not merely vanishing together.

theorem QECCertificates.hgpHZ_mulVec_eq_zero_iff_swap {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 ↔ ((hgpHX H₁.transpose H₂.transpose).mulVec fun (c : Fin r₁ × Fin r₂ ⊕ Fin n₁ × Fin n₂) => v (swapBlocks c)) = 0

The correspondence of kernels: $v\in\ker H_Z(H_1,H_2)$ exactly when the swapped $v$ lies in $\ker H_X(H_1^\top,H_2^\top)$.

theorem QECCertificates.mem_rowSpace_X_of_swap_mem_rowSpace_Z {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} (h : (fun (c : Fin r₁ × Fin r₂ ⊕ Fin n₁ × Fin n₂) => v (swapBlocks c)) ∈ (hgpHZ H₁.transpose H₂.transpose).certificateRowSpace) : v ∈ (hgpHX H₁ H₂).certificateRowSpace

The correspondence of row spaces: for a vector $w$ that after the swap lies in the row space of $H_Z(H_1^\top,H_2^\top)$, swapping once more puts it in the row space of $H_X(H_1,H_2)$; for $v := w\circ\text{swap}$ this says $v\in\mathrm{row}H_X(H_1,H_2)$.