Restrictions and deletions on states

The restrictions and deletions of Mishra and Santhanam, Sections 2.4 and 3.1 on states of gate elimination, each with its validity and its effect on the counted quantities and on the children of the parameters:

• State.restrict: fixing a parameter to a constant or to a literal of another parameter, the restrictions (UF) and (PF) of the source;
• State.deleteGate: deleting a gate that computes a literal of one of its inputs, or a constant, or that is unused, rerouting its uses (D1) and (D2);
• State.deleteEqn: deleting an equation v = ℓ together with its auxiliary variable v, rerouting v to ℓ (D3);
• State.dropEqn: deleting an equation together with an auxiliary variable occurring nowhere else (the second half of D4), and State.dropTrivialEqn: deleting an equation without terms.

Each operation acts on the semi-circuit as the corresponding simplification of Complexity.Computability.Circuit.Boolean.SemiCircuit.Simplification, which preserves well-formedness. Validity then follows from the semi-circuit level: an operation keeping the parameter map is valid when consistent assignments lift (State.Valid.of_liftsTo), and in general validity is transported along a map σ from the new assignments to the old ones under the obligations State.Transport (State.Valid.of_transport).

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.Transport: the obligations of transporting validity.
• Cslib.Circuits.Boolean.AffineDisperser.State.restrict, State.RestrictOK, State.deleteGate, State.deleteEqn, State.dropEqn, State.dropTrivialEqn: the operations and the restriction hypotheses.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.of_transport: transporting validity.
• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.restrict, Valid.deleteGate, Valid.deleteEqn, Valid.dropEqn, Valid.dropTrivialEqn: the operations preserve validity.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits

theorem Cslib.Circuits.Boolean.AffineDisperser.isAffine_lit_eval {k : ℕ} {τ : BitString k → ℕ → Bool} (hτ : BitString.IsAffine τ) (ℓ : SemiCircuit.Lit) : BitString.IsAffine fun (u : BitString k) => ℓ.eval (τ u)

Evaluating a literal ℓ along an affine family of assignments τ defines an affine Boolean function.

Transporting validity

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.of_liftsTo {n : ℕ} {f : BooleanFunction n} {S S' : State n} (hS : S.Valid f) (hparams : S'.params = S.params) (hpairs : S'.pairs = S.pairs) (hphi : S'.phi = S.phi) (hwf : S'.WellFormed) (hlift : S'.LiftsTo S.toSemiCircuit) : S'.Valid f

A state with the parameters, pairs and parameter map of a valid state is valid when its semi-circuit is well formed and its consistent assignments lift to the old semi-circuit.

structure Cslib.Circuits.Boolean.AffineDisperser.State.Transport {n : ℕ} (S S' : State n) (σ : (ℕ → Bool) → ℕ → Bool) : Prop

The obligations for transporting validity from S to S' along a map σ from the assignments of S' to those of S: σ maps consistent assignments to consistent assignments with the same output, the new parameter map is the old one after σ, σ matches the parameters of both states injectively, and σ maps affine families on which the new pairs are tame to families agreeing on the old parameters with affine families on which the old pairs are tame.

• pair_mem (pr : ℕ × ℕ) : pr ∈ S'.pairs → pr.1 ∈ S'.params ∧ pr.2 ∈ S'.params ∧ pr.1 ≠ pr.2
• pairs_disjoint (pr : ℕ × ℕ) : pr ∈ S'.pairs → ∀ pr' ∈ S'.pairs, pr ≠ pr' → pr.1 ≠ pr'.1 ∧ pr.1 ≠ pr'.2 ∧ pr.2 ≠ pr'.1 ∧ pr.2 ≠ pr'.2
• phi (val : ℕ → Bool) : S'.phi val = S.phi (σ val)
• congr (val val' : ℕ → Bool) : (∀ j ∈ S'.params, val j = val' j) → ∀ j ∈ S.params, σ val j = σ val' j
• inj (val val' : ℕ → Bool) : (∀ j ∈ S.params, σ val j = σ val' j) → ∀ j ∈ S'.params, val j = val' j
• affine (k : ℕ) (τ : BitString k → ℕ → Bool) : BitString.IsAffine τ → (∀ pr ∈ S'.pairs, PairTame τ pr) → ∃ (τ' : BitString k → ℕ → Bool), BitString.IsAffine τ' ∧ (∀ pr ∈ S.pairs, PairTame τ' pr) ∧ ∀ (u : BitString k), ∀ j ∈ S.params, τ' u j = σ (τ u) j
• consistent (val : ℕ → Bool) : S'.Consistent val → S.Consistent (σ val)
• out (val : ℕ → Bool) : S'.Consistent val → S'.out.eval val = S.out.eval (σ val)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.of_transport {n : ℕ} {f : BooleanFunction n} {S S' : State n} (hS : S.Valid f) {σ : (ℕ → Bool) → ℕ → Bool} (hwf : S'.WellFormed) (h : S.Transport S' σ) : S'.Valid f

Validity transported along a map σ from the assignments of a new, well-formed state to those of a valid state.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.not_reads_self {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} (hJ : J ∈ S.gates) : ¬(S.gate J).Reads J

A gate does not read itself.

Restrictions (UF) and (PF)

def Cslib.Circuits.Boolean.AffineDisperser.State.restrict {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) : State n

Restrict the parameter x to the literal ℓ, a constant or a literal of another parameter, keeping the pairs P.

structure Cslib.Circuits.Boolean.AffineDisperser.State.RestrictOK {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) : Prop

The hypotheses of a restriction: x is a parameter, ℓ reads at most another parameter, the kept pairs avoid x, and every dropped pair contains x and the other parameter read by ℓ, if any.

• mem : x ∈ S.params
• reads (y : ℕ) : ℓ.Reads y → y ∈ S.params ∧ y ≠ x
• subset : P ⊆ S.pairs
• avoid (pr : ℕ × ℕ) : pr ∈ P → pr.1 ≠ x ∧ pr.2 ≠ x
• drop (pr : ℕ × ℕ) : pr ∈ S.pairs → pr ∉ P → (pr.1 = x ∨ pr.2 = x) ∧ ∀ (y : ℕ), ℓ.Reads y → y = pr.1 ∨ y = pr.2

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_params {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).params = S.params.erase x

Restricting x removes x from the parameters of S.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_pairs {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).pairs = P

The pairs of S.restrict x ℓ P are P.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_children {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) (z : ℕ) : (S.restrict x ℓ P).children z = (S.subst x ℓ).children z

The children of z in S.restrict x ℓ P are its children after substituting x with ℓ.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_size {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).size = S.size

Restricting a parameter preserves the size of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_gate {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) (J : ℕ) : (S.restrict x ℓ P).gate J = (S.gate J).subst x ℓ

Restricting x to ℓ substitutes x with ℓ in every gate.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_eqn {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) (e : ℕ) : (S.restrict x ℓ P).eqn e = (S.eqn e).subst x ℓ

Restricting x to ℓ substitutes x with ℓ in every equation.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.restrict {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x : ℕ} {ℓ : SemiCircuit.Lit} {P : Finset (ℕ × ℕ)} (h : S.RestrictOK x ℓ P) : (S.restrict x ℓ P).Valid f

Restrictions preserve validity.

Deleting a gate (D1) and (D2)

def Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) : State n

Delete the gate J, rerouting its uses to the literal ℓ.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_params {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteGate J ℓ).params = S.params

Deleting a gate preserves the parameters of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_pairs {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteGate J ℓ).pairs = S.pairs

Deleting a gate preserves the pairs of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_phi {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteGate J ℓ).phi = S.phi

Deleting a gate preserves the parameter map phi.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_gate {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) (K : ℕ) : (S.deleteGate J ℓ).gate K = (S.gate K).subst J ℓ

Deleting gate J with replacement ℓ substitutes J with ℓ in every gate.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_eqn {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) (e : ℕ) : (S.deleteGate J ℓ).eqn e = (S.eqn e).subst J ℓ

Deleting gate J with replacement ℓ substitutes J with ℓ in every equation.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_gates {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteGate J ℓ).gates = S.gates.erase J

Deleting gate J removes J from S.gates.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_size {n : ℕ} {S : State n} {J : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteGateOK J ℓ) : (S.deleteGate J ℓ).size + 1 = S.size

Deleting a gate decreases the size of the state by 1.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_children_subset {n : ℕ} {S : State n} {J : ℕ} {ℓ : SemiCircuit.Lit} (z : ℕ) : (S.deleteGate J ℓ).children z ⊆ ((S.subst J ℓ).children z).erase (Sum.inl J)

After deleting gate J with replacement ℓ, the children of z are contained in the children of z after substituting J with ℓ with .inl J removed.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_children_of_ne {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteGateOK J ℓ) {z : ℕ} (hz : z ∈ S.params) (hzℓ : ¬ℓ.Reads z) : (S.deleteGate J ℓ).children z ⊆ (S.children z).erase (Sum.inl J)

Deleting a gate removes it from the children of every parameter other than the target of ℓ.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.deleteGate {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteGateOK J ℓ) : (S.deleteGate J ℓ).Valid f

Deleting a gate preserves validity.

Deleting an equation (D3)

def Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn {n : ℕ} (S : State n) (e v : ℕ) (ℓ : SemiCircuit.Lit) : State n

Delete the equation e, which reads v = ℓ, and the auxiliary variable v, rerouting v to ℓ.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_params {n : ℕ} (S : State n) (e v : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteEqn e v ℓ).params = S.params

Deleting an equation preserves the parameters of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_pairs {n : ℕ} (S : State n) (e v : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteEqn e v ℓ).pairs = S.pairs

Deleting an equation preserves the pairs of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_phi {n : ℕ} (S : State n) (e v : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteEqn e v ℓ).phi = S.phi

Deleting an equation preserves the parameter map phi.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_size {n : ℕ} {S : State n} {e v : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteEqnOK e v ℓ) : (S.deleteEqn e v ℓ).size + 1 = S.size

Deleting an equation decreases the size of the state by 1.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_children_subset {n : ℕ} {S : State n} {e v : ℕ} {ℓ : SemiCircuit.Lit} (z : ℕ) : (S.deleteEqn e v ℓ).children z ⊆ ((S.subst v ℓ).children z).erase (Sum.inr e)

After deleting equation e and auxiliary variable v with replacement ℓ, the children of z are contained in the children of z after substituting v with ℓ with .inr e removed.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_children_of_ne {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteEqnOK e v ℓ) {z : ℕ} (hz : z ∈ S.params) (hzℓ : ¬ℓ.Reads z) : (S.deleteEqn e v ℓ).children z ⊆ (S.children z).erase (Sum.inr e)

Deleting an equation removes it from the children of every parameter other than the target of ℓ.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.deleteEqn {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteEqnOK e v ℓ) : (S.deleteEqn e v ℓ).Valid f

Deleting an equation v = ℓ with its auxiliary variable preserves validity.

Dropping an equation (D4)

def Cslib.Circuits.Boolean.AffineDisperser.State.dropEqn {n : ℕ} (S : State n) (e v : ℕ) : State n

Delete the equation e together with an auxiliary variable v occurring nowhere else.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropEqn_params {n : ℕ} (S : State n) (e v : ℕ) : (S.dropEqn e v).params = S.params

Dropping an equation preserves the parameters of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropEqn_pairs {n : ℕ} (S : State n) (e v : ℕ) : (S.dropEqn e v).pairs = S.pairs

Dropping an equation preserves the pairs of the state.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropEqn_size {n : ℕ} {S : State n} {e v : ℕ} (h : S.DropEqnOK e v) : (S.dropEqn e v).size + 1 = S.size

Dropping an equation decreases the size of the state by 1.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropEqn_children {n : ℕ} (S : State n) (e v z : ℕ) : (S.dropEqn e v).children z = (S.children z).erase (Sum.inr e)

Dropping equation e removes .inr e from the children of z.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.dropEqn {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e v : ℕ} (h : S.DropEqnOK e v) : (S.dropEqn e v).Valid f

Dropping an equation with an auxiliary variable occurring only there preserves validity.

def Cslib.Circuits.Boolean.AffineDisperser.State.dropTrivialEqn {n : ℕ} (S : State n) (e : ℕ) : State n

Delete an equation without terms.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropTrivialEqn_params {n : ℕ} (S : State n) (e : ℕ) : (S.dropTrivialEqn e).params = S.params

Dropping a trivial equation preserves the parameters of the state.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropTrivialEqn_pairs {n : ℕ} (S : State n) (e : ℕ) : (S.dropTrivialEqn e).pairs = S.pairs

Dropping a trivial equation preserves the pairs of the state.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropTrivialEqn_size {n : ℕ} {S : State n} {e : ℕ} (he : e ∈ S.eqns) : (S.dropTrivialEqn e).size + 1 = S.size

Dropping a trivial equation decreases the size of the state by 1.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.dropTrivialEqn_children {n : ℕ} (S : State n) (e z : ℕ) : (S.dropTrivialEqn e).children z = (S.children z).erase (Sum.inr e)

Dropping trivial equation e removes .inr e from the children of z.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.dropTrivialEqn {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e : ℕ} (he : e ∈ S.eqns) (hterms : (S.eqn e).terms = ∅) : (S.dropTrivialEqn e).Valid f

Deleting an equation without terms preserves validity.