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.deleteGate, State.deleteEqn, State.dropEqn, State.dropTrivialEqn: the operations.

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)

Transporting validity

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.of_phi {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) (hcomp : ∀ (val : ℕ → Bool), S'.Consistent val → S'.out.eval val = f (S'.phi val)) : 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 computes f.

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

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrict_pairs {n : ℕ} (S : State n) (x : ℕ) (ℓ : SemiCircuit.Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).pairs = 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

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

@[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 ℓ

@[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 ℓ

theorem Cslib.Circuits.Boolean.AffineDisperser.State.RestrictOK.pairTame {n : ℕ} {S : State n} {x : ℕ} {ℓ : SemiCircuit.Lit} {P : Finset (ℕ × ℕ)} (h : S.RestrictOK x ℓ P) {k : ℕ} {τ : BitString k → ℕ → Bool} (htame : ∀ pr ∈ P, PairTame τ pr) (pr : ℕ × ℕ) : pr ∈ S.pairs → PairTame (fun (u : BitString k) => Function.update (τ u) x (ℓ.eval (τ u))) pr

Along an affine family on which the kept pairs are tame, the restricted family is affine and every pair is tame: a dropped pair has a constant member, or a constant sum when x is restricted to a literal of its partner.

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

@[simp]

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

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteGate_phi {n : ℕ} (S : State n) (J : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteGate J ℓ).phi = S.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 ℓ

@[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 ℓ

@[simp]

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

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

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)

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

@[simp]

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

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deleteEqn_phi {n : ℕ} (S : State n) (e v : ℕ) (ℓ : SemiCircuit.Lit) : (S.deleteEqn e v ℓ).phi = S.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

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)

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)

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

@[simp]

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

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

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)

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

@[simp]

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

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

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)

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.