Affine flats are XOR cosets

Translating a ternary-XOR-closed nonempty set by any of its points gives an XOR-closed set of the same size. The checked sumset-disperser obstruction therefore applies directly to our original Boolean-coordinate affine flats.

theorem Algebraic.Aggregate.Geometry.AffineFlat.exists_xorCoset {n : ℕ} (S : AffineFlat n) : ∃ (a : Fin n → Bool) (V : Finset (Fin n → Bool)), (∀ x ∈ V, ∀ y ∈ V, Cutwidth.xorInput x y ∈ V) ∧ Finset.image (Cutwidth.xorInput a) V = S.carrier ∧ V.card = S.carrier.card

A nonempty ternary-XOR-closed flat is a translate of an XOR-closed set.

theorem Algebraic.Aggregate.Geometry.AffineFlat.card_lt_of_constant {n : ℕ} (S : AffineFlat n) {f : Cslib.BooleanFunction n} {K : ℕ} (disperse : Cutwidth.FlatSumsetDisperser f K) (mono : ConstantOn S f) : S.carrier.card < K

A monochromatic affine flat is smaller than the sumset-disperser threshold.