Character coefficients of constant Hamming residue

Dedekind's linear independence of characters isolates the signed multiplicity of every nonzero linear coordinate form. In particular no such form occurs once.

def Algebraic.BooleanCube.ModThree.Internal.character {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (L : V →ₗ[ZMod 2] ZMod 2) : Multiplicative V →* ZMod 3

The character associated to a binary linear form.

Equations

• Algebraic.BooleanCube.ModThree.Internal.character L = { toFun := fun (u : Multiplicative V) => Algebraic.BooleanCube.ModThree.sign (L (Multiplicative.toAdd u)), map_one' := ⋯, map_mul' := ⋯ }

theorem Algebraic.BooleanCube.ModThree.Internal.signedMultiplicity_eq_zero {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] {ι : Type u_2} [Fintype ι] (a : ι → ZMod 2) (L : ι → V →ₗ[ZMod 2] ZMod 2) (constant : ∀ (u : V), (residue fun (i : ι) => a i + (L i) u) = residue a) (K : V →ₗ[ZMod 2] ZMod 2) (nonzero : K ≠ 0) : (∑ i : ι, if L i = K then sign (a i) else 0) = 0

Constancy of the full residue cancels each nonzero character coefficient.

theorem Algebraic.BooleanCube.ModThree.Internal.exists_duplicate {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] {ι : Type u_2} [Fintype ι] (a : ι → ZMod 2) (L : ι → V →ₗ[ZMod 2] ZMod 2) (constant : ∀ (u : V), (residue fun (i : ι) => a i + (L i) u) = residue a) (i : ι) (nonzero : L i ≠ 0) : ∃ (j : ι), j ≠ i ∧ L j = L i

Every nonzero form appearing in a constant-residue parametrization repeats.

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

Constant full residue forces at least two coordinates per parameter dimension.