The half-dimension obstruction for full Hamming residue modulo three

A binary affine flat on which the full Hamming-weight residue modulo three is constant has dimension at most half the ambient number of coordinates. This statement concerns the three-valued residue, not one Boolean MOD3 predicate. The proof groups affine coordinates by their linear parts. Dedekind's independence of characters forces every nonzero part to occur at least twice.

theorem Algebraic.BooleanCube.ModThree.two_mul_finrank_le_of_constant {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [Fintype ι] (a : ι → ZMod 2) (L : V →ₗ[ZMod 2] ι → ZMod 2) (injective : Function.Injective fun (u : V) => a + L u) (constant : ∀ (u : V), residue (a + L u) = residue a) : 2 * Module.finrank (ZMod 2) V ≤ Fintype.card ι

An injective affine parametrization with constant full residue uses at least two coordinates per parameter dimension.

theorem Algebraic.BooleanCube.ModThree.two_mul_finrank_submodule_le {ι : Type u_2} [Fintype ι] (W : Submodule (ZMod 2) (ι → ZMod 2)) (a : ι → ZMod 2) (constant : ∀ u ∈ W, residue (a + u) = residue a) : 2 * Module.finrank (ZMod 2) ↥W ≤ Fintype.card ι

A coset with constant full Hamming residue has at most half the ambient dimension.

theorem Algebraic.BooleanCube.ModThree.exists_residue_ne_of_lt_two_mul_finrank {ι : Type u_2} [Fintype ι] (W : Submodule (ZMod 2) (ι → ZMod 2)) (a : ι → ZMod 2) (large : Fintype.card ι < 2 * Module.finrank (ZMod 2) ↥W) : ∃ u ∈ W, residue (a + u) ≠ residue a

A coset of dimension above half the ambient dimension contains a point whose full Hamming residue differs from the residue of its base point.