Elementary affine-flat operations

Restrictions preserve affineness and constants. Every nonconstant affine Boolean function has two equally large fibers, and each fiber is again an affine flat.

@[simp]

theorem Algebraic.Aggregate.Geometry.xorThree_self_right {n : ℕ} (x y : Fin n → Bool) : xorThree x y y = x

Adding the same translation twice cancels it.

@[simp]

theorem Algebraic.Aggregate.Geometry.xorThree_translate_translate {n : ℕ} (x a b : Fin n → Bool) : xorThree (xorThree x a b) a b = x

Translation by the difference of two points is an involution.

noncomputable def Algebraic.Aggregate.Geometry.AffineFlat.full (n : ℕ) : AffineFlat n

The full Boolean cube is an affine flat.

Equations

• Algebraic.Aggregate.Geometry.AffineFlat.full n = { carrier := Finset.univ, nonempty := ⋯, closed := ⋯ }

@[simp]

theorem Algebraic.Aggregate.Geometry.AffineFlat.card_full (n : ℕ) : (full n).carrier.card = 2 ^ n

The full Boolean cube contains exactly one point per input assignment.

theorem Algebraic.Aggregate.Geometry.AffineOn.mono {n : ℕ} {S T : AffineFlat n} {f : (Fin n → Bool) → Bool} (h : AffineOn S f) (sub : T.carrier ⊆ S.carrier) : AffineOn T f

Restricting to a smaller flat preserves affineness.

theorem Algebraic.Aggregate.Geometry.ConstantOn.mono {n : ℕ} {S T : AffineFlat n} {f : (Fin n → Bool) → Bool} (h : ConstantOn S f) (sub : T.carrier ⊆ S.carrier) : ConstantOn T f

A function made constant remains constant on every later restriction.

theorem Algebraic.Aggregate.Geometry.AffineOn.congr {n : ℕ} {S : AffineFlat n} {f g : (Fin n → Bool) → Bool} (h : AffineOn S f) (same : ∀ x ∈ S.carrier, f x = g x) : AffineOn S g

Only values on the flat matter for affineness.

theorem Algebraic.Aggregate.Geometry.ConstantOn.affine {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} (h : ConstantOn S f) : AffineOn S f

Every constant function preserves ternary XOR.

theorem Algebraic.Aggregate.Geometry.affineOn_const {n : ℕ} {S : AffineFlat n} (b : Bool) : AffineOn S fun (x : Fin n → Bool) => b

Constant Boolean functions are affine on every flat.

theorem Algebraic.Aggregate.Geometry.affineOn_coordinate {n : ℕ} {S : AffineFlat n} (i : Fin n) : AffineOn S fun (x : Fin n → Bool) => x i

Each original input coordinate is an affine function.

theorem Algebraic.Aggregate.Geometry.AffineOn.xor {n : ℕ} {S : AffineFlat n} {f g : (Fin n → Bool) → Bool} (hf : AffineOn S f) (hg : AffineOn S g) : AffineOn S fun (x : Fin n → Bool) => f x ^^ g x

XOR of two affine Boolean functions remains affine.

theorem Algebraic.Aggregate.Geometry.AffineOn.unary {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} (hf : AffineOn S f) (u : Bool → Bool) : AffineOn S fun (x : Fin n → Bool) => u (f x)

Every unary Boolean operation preserves affineness.

theorem Algebraic.Aggregate.Geometry.exists_mem_eq_of_not_constant {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} (h : ¬ConstantOn S f) (b : Bool) : ∃ x ∈ S.carrier, f x = b

A nonconstant Boolean function takes both values on a nonempty flat.

theorem Algebraic.Aggregate.Geometry.AffineOn.exists_half {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} (affine : AffineOn S f) (nonconstant : ¬ConstantOn S f) (b : Bool) : ∃ (T : AffineFlat n), T.carrier ⊆ S.carrier ∧ (∀ x ∈ T.carrier, f x = b) ∧ 2 * T.carrier.card = S.carrier.card

Each fiber of a nonconstant affine Boolean function is a half-sized affine flat.