Documentation

CslibFrontier.Logics.Propositional.CSP.Affine

Affine Boolean relations #

An affine equation is a list of variables and a Boolean right-hand side. Evaluation sums the listed bits in the existing Boolean ring, so repeated occurrences cancel in pairs. Empty lists express both constant equations, including the inconsistent equation 0 = 1.

For any finite coordinate type, preservation by ternary parity is equivalent to definability by a finite conjunction of these equations, without auxiliary variables. This is the normal-form claim of [Che06], Theorem 4.3, printed pp. 15–16 (arXiv version 1), including empty and nullary relations. The proof uses linear separation of the subgroup obtained by translating a nonempty relation, rather than Chen's induction on coordinates. No algorithmic complexity claim is made in this module.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Logic.PL.AffineEquation (V : Type u_2) :
Type u_2

An affine parity equation: a list of variables, with repetitions, and its right-hand side.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Logic.PL.AffineSystem (V : Type u_2) :
    Type u_2

    A finite conjunction of affine parity equations.

    Instances For
      source
      def Cslib.Logic.PL.AffineEquation.Holds {V : Type u_1} (e : AffineEquation V) (a : V → Bool) :
      Prop

      The sum of the listed bits equals the right-hand side in the Boolean ring.

      Instances For
        source
        def Cslib.Logic.PL.AffineSystem.Holds {V : Type u_1} (F : AffineSystem V) (a : V → Bool) :
        Prop

        Every equation in the system holds.

        Instances For
          source
          theorem Cslib.Logic.PL.AffineEquation.holds_cons_cons {V : Type u_1} (v : V) (vs : List V) (b : Bool) (a : V → Bool) :
          Holds (v :: v :: vs, b) a ↔ Holds (vs, b) a

          Two occurrences of the same variable cancel, with no condition on the remaining list.

          source
          theorem Cslib.Logic.PL.isPolymorphism_parity_iff {V : Type u_1} {R : Set (V → Bool)} :
          IsPolymorphism (parity 3) R ↔ ∀ x ∈ R, ∀ y ∈ R, ∀ z ∈ R, x + y + z ∈ R

          Ternary parity on the existing Boolean cube is coordinatewise addition of three tuples.

          source
          theorem Cslib.Logic.PL.AffineEquation.isPolymorphism_parity {V : Type u_1} (e : AffineEquation V) :
          IsPolymorphism (parity 3) {a : V → Bool | e.Holds a}

          Every affine equation is preserved by ternary parity.

          source
          theorem Cslib.Logic.PL.AffineSystem.isPolymorphism_parity {V : Type u_1} (F : AffineSystem V) :
          IsPolymorphism (parity 3) {a : V → Bool | F.Holds a}

          Every conjunction of affine equations is preserved by ternary parity.

          source
          theorem Cslib.Logic.PL.exists_separating_affineEquation {V : Type u_1} [Finite V] {R : Set (V → Bool)} (hR : IsPolymorphism (parity 3) R) {a : V → Bool} (ha : a ∉ R) :
          ∃ (e : AffineEquation V), (∀ b ∈ R, e.Holds b) ∧ ¬e.Holds a

          A tuple outside a finite parity-preserved relation can be separated by an affine equation. The empty relation is separated by the inconsistent constant equation.

          source
          theorem Cslib.Logic.PL.isPolymorphism_parity_iff_exists_affineSystem {V : Type u_1} [Finite V] (R : Set (V → Bool)) :
          IsPolymorphism (parity 3) R ↔ ∃ (F : AffineSystem V), ∀ (a : V → Bool), a ∈ R ↔ F.Holds a

          Parity preservation iff affine definability. Empty and nullary relations are included; there are no auxiliary variables. The defining system is finite, with no claimed size bound.