Equations over 𝔽₂

The equations of the affine system of a fair semi-circuit (Cslib.Circuits.Boolean.SemiCircuit): an equation states that the sum over 𝔽₂ of the values of its terms, a finite set of internal values, is a constant. Rerouting a term to a literal (Equation.subst) preserves the truth of the equation on assignments giving the term the value of the literal (Equation.holds_subst) and does not add terms (Equation.card_subst_le). An affine gate becomes an equation with at most three terms (affEqn, affEqn_holds).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit.Equation: equations, with Equation.Holds and Equation.subst.
• Cslib.Circuits.Boolean.SemiCircuit.affEqn: the equation of an affine gate.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.Equation.holds_subst: rerouting preserves equations.
• Cslib.Circuits.Boolean.SemiCircuit.affEqn_holds: the equation of an affine gate holds exactly when the gate takes its value.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits
• M. G. Find, A. Golovnev, E. A. Hirsch and A. S. Kulikov, A better-than-3n lower bound for the circuit complexity of an explicit function

Equations

structure Cslib.Circuits.Boolean.SemiCircuit.Equation : Type

An equation of the affine system: the sum over 𝔽₂ of the values of its terms is rhs.

• terms : Finset ℕ

  The internal values occurring in the equation.

• rhs : Bool

  The right-hand side.

theorem Cslib.Circuits.Boolean.SemiCircuit.symmDiff_singleton_eq (s : Finset ℕ) (t : ℕ) : symmDiff s {t} = if t ∈ s then s.erase t else insert t s

Adding t to a set of terms over 𝔽₂ removes it if present and inserts it otherwise.

theorem Cslib.Circuits.Boolean.SemiCircuit.sum_symmDiff_singleton (s : Finset ℕ) (t : ℕ) (val : ℕ → Bool) : ∑ i ∈ symmDiff s {t}, val i = ∑ i ∈ s, val i + val t

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_symmDiff_singleton {s : Finset ℕ} {t z : ℕ} : z ∈ symmDiff s {t} ↔ (z ∈ s ↔ z ≠ t)

theorem Cslib.Circuits.Boolean.SemiCircuit.card_symmDiff_singleton_le (s : Finset ℕ) (t : ℕ) : (symmDiff s {t}).card ≤ s.card + 1

def Cslib.Circuits.Boolean.SemiCircuit.Equation.Holds (E : Equation) (val : ℕ → Bool) : Prop

The equation holds under an assignment of the internal values.

@[instance_reducible]

instance Cslib.Circuits.Boolean.SemiCircuit.Equation.instDecidableHolds (E : Equation) (val : ℕ → Bool) : Decidable (E.Holds val)

def Cslib.Circuits.Boolean.SemiCircuit.Equation.subst (E : Equation) (v : ℕ) (ℓ : Lit) : Equation

Reroute the term v of an equation to the literal ℓ.

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.holds_subst {E : Equation} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (E.subst v ℓ).Holds val ↔ E.Holds val

Rerouting v to a literal with the value of v preserves the truth of every equation.

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.mem_subst_of_ne {E : Equation} {v : ℕ} {ℓ : Lit} {z : ℕ} (hzv : z ≠ v) (hzℓ : ℓ.arg ≠ Arg.node z) : z ∈ (E.subst v ℓ).terms ↔ z ∈ E.terms

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.mem_of_mem_subst {E : Equation} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : z ∈ (E.subst v ℓ).terms) : z ∈ E.terms ∨ v ∈ E.terms ∧ ℓ.arg = Arg.node z

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.card_subst_le {E : Equation} {v : ℕ} {ℓ : Lit} : (E.subst v ℓ).terms.card ≤ E.terms.card

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.notMem_subst {E : Equation} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ Arg.node v) : v ∉ (E.subst v ℓ).terms

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.subst_of_notMem {E : Equation} {v : ℕ} {ℓ : Lit} (h : v ∉ E.terms) : E.subst v ℓ = E

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.holds_congr {E : Equation} {val val' : ℕ → Bool} (h : ∀ i ∈ E.terms, val i = val' i) : E.Holds val ↔ E.Holds val'

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.holds_subst_update {E : Equation} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ Arg.node v) (val : ℕ → Bool) : (E.subst v ℓ).Holds val ↔ E.Holds (Function.update val v (ℓ.eval val))

An equation with v rerouted to a literal not reading v holds exactly when the equation holds on the assignment giving v the value of the literal.

theorem Cslib.Circuits.Boolean.SemiCircuit.Equation.holds_update_iff {E : Equation} {v p r : ℕ} (hterms : E.terms = {v, p, r}) (hvp : v ≠ p) (hvr : v ≠ r) (hpr : p ≠ r) (val : ℕ → Bool) (c : Bool) : E.Holds (Function.update val p (val r ^^ c)) ↔ val v = (E.rhs ^^ c)

Once p = r + c, the equation v + p + r = rhs reads v = rhs + c.

Moving affine gates into the affine system

def Cslib.Circuits.Boolean.SemiCircuit.addArg (p : Finset ℕ × Bool) (b : Bool) (a : Arg) : Finset ℕ × Bool

Add the argument a with coefficient b to the terms and right-hand side of an equation.

theorem Cslib.Circuits.Boolean.SemiCircuit.sum_addArg (p : Finset ℕ × Bool) (b : Bool) (a : Arg) (val : ℕ → Bool) : ∑ i ∈ (addArg p b a).1, val i + (addArg p b a).2 = ∑ i ∈ p.1, val i + p.2 + (b && Arg.eval val a)

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_addArg {p : Finset ℕ × Bool} {b : Bool} {a : Arg} {z : ℕ} (h : z ∈ (addArg p b a).1) : z ∈ p.1 ∨ a = Arg.node z

theorem Cslib.Circuits.Boolean.SemiCircuit.card_addArg_le (p : Finset ℕ × Bool) (b : Bool) (a : Arg) : (addArg p b a).1.card ≤ p.1.card + 1

def Cslib.Circuits.Boolean.SemiCircuit.affEqn (g : Gate) (J : ℕ) : Equation

The equation J + b₁ t₁ + b₂ t₂ = c replacing the affine gate J = b₁ t₁ + b₂ t₂ + c.

theorem Cslib.Circuits.Boolean.SemiCircuit.affEqn_holds {g : Gate} (hg : IsAffineOp g.op) (J : ℕ) (val : ℕ → Bool) : (affEqn g J).Holds val ↔ val J = g.eval val

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_affEqn {g : Gate} {J z : ℕ} (h : z ∈ (affEqn g J).terms) : z = J ∨ g.Reads z

theorem Cslib.Circuits.Boolean.SemiCircuit.card_affEqn_le (g : Gate) (J : ℕ) : (affEqn g J).terms.card ≤ 3