Affine flats in the Boolean cube

A nonempty subset of the Boolean cube is an affine flat exactly when it is closed under ternary XOR. This finite presentation keeps the original Boolean coordinates. Affine Boolean functions preserve that ternary operation on their domain flat.

def Algebraic.Aggregate.Geometry.xorThree {n : ℕ} (x y z : Fin n → Bool) : Fin n → Bool

Ternary affine addition over the two-element field.

Equations

• Algebraic.Aggregate.Geometry.xorThree x y z = Algebraic.Cutwidth.xorInput (Algebraic.Cutwidth.xorInput x y) z

structure Algebraic.Aggregate.Geometry.AffineFlat (n : ℕ) : Type

A finite nonempty affine flat, expressed without changing the input encoding.

• carrier : Finset (Fin n → Bool)

  The points of the flat, in the original Boolean-coordinate representation.

• nonempty : self.carrier.Nonempty

  Affine restrictions retain at least one point.

• closed (x : Fin n → Bool) : x ∈ self.carrier → ∀ y ∈ self.carrier, ∀ z ∈ self.carrier, xorThree x y z ∈ self.carrier

  The characteristic affine closure law in characteristic two.

def Algebraic.Aggregate.Geometry.AffineOn {n : ℕ} (S : AffineFlat n) (f : (Fin n → Bool) → Bool) : Prop

A Boolean function is affine on a flat when it preserves ternary XOR.

Equations

• Algebraic.Aggregate.Geometry.AffineOn S f = ∀ x ∈ S.carrier, ∀ y ∈ S.carrier, ∀ z ∈ S.carrier, f (Algebraic.Aggregate.Geometry.xorThree x y z) = (f x ^^ f y ^^ f z)

def Algebraic.Aggregate.Geometry.ConstantOn {n : ℕ} (S : AffineFlat n) (f : (Fin n → Bool) → Bool) : Prop

The function has one constant value throughout the flat.

Equations

• Algebraic.Aggregate.Geometry.ConstantOn S f = ∃ (b : Bool), ∀ x ∈ S.carrier, f x = b