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.addArg, 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.

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)

Decidability of whether an equation holds under a value assignment.

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

Rerouting v to ℓ preserves membership in E.terms for any node distinct from v and not read by ℓ.

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

Every term of E.subst v ℓ either already belongs to E.terms or arises from v ∈ E.terms with ℓ reading that node.

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

Rerouting a variable in an equation does not increase the number of terms.

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

Rerouting v to a literal not reading v eliminates v from the terms of the equation.

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

Rerouting a variable that does not occur in E.terms leaves the equation unchanged.

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'

Whether E holds depends only on the values assigned to E.terms.

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.mem_addArg {p : Finset ℕ × Bool} {b : Bool} {a : Arg} {z : ℕ} (h : z ∈ (addArg p b a).1) : z ∈ p.1 ∨ a = Arg.node z

Any term in (addArg p b a).1 either belongs to p.1 or is the node read by a.

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

For an affine gate g, the equation affEqn g J holds under val if and only if 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

Every term of affEqn g J is either the output wire J or a node read by g.

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

The equation affEqn g J of a binary gate has at most three terms.