Residue-changing directions supported on a coordinate block

Restricting a system of binary linear equations to any block with more than twice as many coordinates as equations leaves a supported direction that changes full Hamming residue. Coordinates outside the block are untouched.

noncomputable def Algebraic.BooleanCube.ModThree.extendByZero {ι : Type u_1} (B : Finset ι) : (↥B → ZMod 2) →ₗ[ZMod 2] ι → ZMod 2

Extend a vector on a finite coordinate block by zero outside the block.

Equations

• Algebraic.BooleanCube.ModThree.extendByZero B = { toFun := fun (v : ↥B → ZMod 2) (i : ι) => if hi : i ∈ B then v ⟨i, hi⟩ else 0, map_add' := ⋯, map_smul' := ⋯ }

theorem Algebraic.BooleanCube.ModThree.residue_extendByZero_sub {ι : Type u_1} [Fintype ι] (B : Finset ι) (a : ι → ZMod 2) (v : ↥B → ZMod 2) : residue (a + (extendByZero B) v) - residue a = residue ((fun (i : ↥B) => a ↑i) + v) - residue fun (i : ↥B) => a ↑i

The change in residue after a supported update is entirely within its block.

theorem Algebraic.BooleanCube.ModThree.exists_supported_kernel_residue_ne {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (R : (ι → ZMod 2) →ₗ[ZMod 2] κ → ZMod 2) (a : ι → ZMod 2) (B : Finset ι) (large : 2 * Fintype.card κ < B.card) : ∃ (u : ι → ZMod 2), R u = 0 ∧ (∀ i ∉ B, u i = 0) ∧ residue (a + u) ≠ residue a

Every sufficiently large coordinate block contains a residue-changing direction satisfying the original homogeneous equations.