Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Affine.Direction

The direction subspace of an affine flat #

In prime-field coordinates, every affine flat of the Boolean cube is a translate a + U of a subspace U with exactly as many points as the flat. This turns the size of a flat into the dimension of its direction space.

source
def Algebraic.Aggregate.Geometry.boolVector {N : ℕ} (v : Fin N → ZMod 2) :
Fin N → Bool

Read a prime-field vector as Boolean coordinates.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.Aggregate.Geometry.bitVector_boolVector {N : ℕ} (v : Fin N → ZMod 2) :
    bitVector (boolVector v) = v

    Boolean coordinates of a prime-field vector recover that vector.

    source
    @[simp]
    theorem Algebraic.Aggregate.Geometry.boolVector_bitVector {N : ℕ} (x : Fin N → Bool) :
    boolVector (bitVector x) = x

    Prime-field coordinates of a Boolean point recover that point.

    source
    theorem Algebraic.Aggregate.Geometry.bitVector_xorThree {N : ℕ} (x y z : Fin N → Bool) :
    bitVector (xorThree x y z) = bitVector x + bitVector y + bitVector z

    Prime-field coordinates convert ternary XOR into addition.

    source
    theorem Algebraic.Aggregate.Geometry.AffineFlat.exists_direction {N : ℕ} (S : AffineFlat N) :
    ∃ (a : Fin N → ZMod 2) (U : Submodule (ZMod 2) (Fin N → ZMod 2)), 2 ^ Module.finrank (ZMod 2) ↥U = S.carrier.card ∧ ∀ u ∈ U, ∃ x ∈ S.carrier, bitVector x = a + u

    Every affine flat is a translate of a prime-field subspace with as many points.