Restructuring to a minimal AND

Section 4.2 of Mishra and Santhanam. In a normal state with d < a (State.Normal), the minimal gate is an AND-type gate G on two distinct inputs among the parameters and auxiliary variables (State.Valid.exists_minGate).

Restructuring (Section 4.2) uses preparatory operations (State.Preparation), which keep m, s and q and do not increase W. An auxiliary input of G is exchanged with a parameter it depends on by the affine reparameterisation (State.Valid.exists_preparation_auxIn_lt), and a child of G reading an input of G is relabelled to read both inputs instead (State.Valid.exists_preparation_childIn_lt). Afterwards G is a minimal AND (State.MinimalAnd, State.Valid.exists_minimalAnd): it reads two unpaired parameters x and y with 2 ≤ deg y ≤ deg x, no child of G reads them, and G is not the output and has a child.

Elimination of the minimal AND (Section 4.3, State.Valid.step_of_minimalAnd) is in Complexity/Computability/Circuit/Boolean/AffineDisperser/Elimination.lean.

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.auxIn, Cslib.Circuits.Boolean.AffineDisperser.State.childIn: the measures of the restructuring.
• Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd: the minimal AND.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_preparation_auxIn_lt, Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_preparation_childIn_lt: the restructuring.
• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_minimalAnd: the restructured minimal gate is a minimal AND (MinimalAnd), eliminated in Elimination.lean.

References

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

Exchanging a parameter and an auxiliary variable

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_eqn_of_aux {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {v : ℕ} (hv : v ∈ S.aux) : ∃ e ∈ S.eqns, v ∈ (S.eqn e).terms

An auxiliary variable of a valid state occurs in some equation: otherwise the affine system would not determine it.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.preparation_swap {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x Q : ℕ} {c : Bool} {T : Finset ℕ} (hx : x ∈ S.unpaired) (hxdeg : 2 ≤ S.deg x) (hQ : Q ∈ S.aux) (hQdeg : 2 ≤ S.deg Q) (haff : SemiCircuit.AffineIn Q c T) (hxT : x ∈ T) : Preparation f S (S.swap x Q c T)

The affine reparameterisation of an unpaired parameter x of degree at least two and an auxiliary variable Q of degree at least two depending on it is a preparatory operation: it keeps every child, and both weights are 7.

Rewiring a gate

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.preparation_rewire {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} {g : SemiCircuit.Gate} (h : S.RewireOK J g) (hdeg : ∀ (t : ℕ), g.Reads t → t ∈ S.unpaired → 2 ≤ S.deg t) : Preparation f S (S.rewire J g)

Rewiring a gate to a gate reading only parameters of degree at least two is a preparatory operation: only those parameters may gain a child, and their weight is already 7.

Degenerate minimal gates allow deletions

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletionAvailable_of_degenerate {n : ℕ} {S : State n} {J : ℕ} (hJ : J ∈ S.gates) (h : (S.gate J).Degenerate) : S.DeletionAvailable

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletionAvailable_of_const_input {n : ℕ} {S : State n} {J t : ℕ} (hJ : J ∈ S.gates) {c : Bool} (ht : (S.gate J).Reads t) (hc : ∀ (val : ℕ → Bool), S.EqnsHold val → val t = c) : S.DeletionAvailable

A gate one of whose inputs is constant on the solutions of the affine system allows (D1).

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletionAvailable_of_dependent {n : ℕ} {S : State n} {J t t' : ℕ} (hJ : J ∈ S.gates) {c : Bool} (hargs : (S.gate J).left = SemiCircuit.Arg.node t ∧ (S.gate J).right = SemiCircuit.Arg.node t' ∨ (S.gate J).left = SemiCircuit.Arg.node t' ∧ (S.gate J).right = SemiCircuit.Arg.node t) (hc : ∀ (val : ℕ → Bool), S.EqnsHold val → val t' = (val t ^^ c)) : S.DeletionAvailable

A gate whose inputs differ by a constant on the solutions of the affine system allows (D1).

The minimal gate of a normal state

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.not_out_reads_aux {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) {v : ℕ} (hv : v ∈ S.aux) : ¬S.out.Reads v

The output of a valid state with d < a is not a literal of an auxiliary variable.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_minGate {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (hmov : ∀ (J : ℕ), ¬S.Movable J) (hdel : ¬S.DeletionAvailable) : ∃ (h : S.gates.Nonempty), ¬SemiCircuit.IsAffineOp (S.gate (S.gates.min' h)).op ∧ ∃ (t₁ : ℕ) (t₂ : ℕ), (S.gate (S.gates.min' h)).left = SemiCircuit.Arg.node t₁ ∧ (S.gate (S.gates.min' h)).right = SemiCircuit.Arg.node t₂ ∧ t₁ ≠ t₂ ∧ t₁ ∈ S.params ∪ S.aux ∧ t₂ ∈ S.params ∪ S.aux

In a valid state with d < a where no affine gate can be moved and no deletion applies, there are gates, and the minimal one is an AND-type gate reading two distinct inputs among the parameters and auxiliary variables.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_param_of_aux_input {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hN : S.Normal) {G Q o : ℕ} (hG : G ∈ S.gates) (hargs : (S.gate G).left = SemiCircuit.Arg.node Q ∧ (S.gate G).right = SemiCircuit.Arg.node o ∨ (S.gate G).left = SemiCircuit.Arg.node o ∧ (S.gate G).right = SemiCircuit.Arg.node Q) (hQ : Q ∈ S.aux) (hQo : Q ≠ o) : ∃ (x : ℕ) (c : Bool) (T : Finset ℕ), SemiCircuit.AffineIn Q c T ∧ x ∈ T ∧ x ≠ o ∧ x ∈ S.unpaired ∧ 2 ≤ S.deg x ∧ 2 ≤ S.deg Q

An auxiliary input Q of the minimal gate depends on a parameter x other than the other input; when no preliminary reduction applies, x is unpaired of degree at least two, and Q has degree at least two.

The measures of the restructuring

def Cslib.Circuits.Boolean.AffineDisperser.State.auxArgs {n : ℕ} (S : State n) (g : SemiCircuit.Gate) : ℕ

The number of auxiliary inputs of a gate.

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

The number of auxiliary inputs of the minimal gate.

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

The number of children of the minimal gate reading one of its parameter inputs.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.auxIn_eq {n : ℕ} {S : State n} (hne : S.gates.Nonempty) : S.auxIn = S.auxArgs (S.gate (S.gates.min' hne))

theorem Cslib.Circuits.Boolean.AffineDisperser.State.auxArgs_nodes {n : ℕ} (S : State n) {g : SemiCircuit.Gate} {t₁ t₂ : ℕ} (hl : g.left = SemiCircuit.Arg.node t₁) (hr : g.right = SemiCircuit.Arg.node t₂) : S.auxArgs g = (if t₁ ∈ S.aux then 1 else 0) + if t₂ ∈ S.aux then 1 else 0

theorem Cslib.Circuits.Boolean.AffineDisperser.State.childIn_eq {n : ℕ} {S : State n} (hne : S.gates.Nonempty) : S.childIn = {K ∈ S.gates | (S.gate K).Reads (S.gates.min' hne) ∧ ∃ t ∈ S.params, (S.gate (S.gates.min' hne)).Reads t ∧ (S.gate K).Reads t}.card

Restructuring the minimal AND

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_preparation_auxIn_lt {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hN : S.Normal) (hne : S.gates.Nonempty) {Q o : ℕ} (hargs : (S.gate (S.gates.min' hne)).left = SemiCircuit.Arg.node Q ∧ (S.gate (S.gates.min' hne)).right = SemiCircuit.Arg.node o ∨ (S.gate (S.gates.min' hne)).left = SemiCircuit.Arg.node o ∧ (S.gate (S.gates.min' hne)).right = SemiCircuit.Arg.node Q) (hQ : Q ∈ S.aux) (hQo : Q ≠ o) : ∃ (S₁ : State n), Preparation f S S₁ ∧ S₁.gates = S.gates ∧ S₁.auxIn < S.auxIn

Exchanging an auxiliary input of the minimal gate of a normal state with a parameter it depends on is a preparatory operation lowering the number of auxiliary inputs of the minimal gate.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_preparation_childIn_lt {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hne : S.gates.Nonempty) {t₁ t₂ : ℕ} (hl : (S.gate (S.gates.min' hne)).left = SemiCircuit.Arg.node t₁) (hr : (S.gate (S.gates.min' hne)).right = SemiCircuit.Arg.node t₂) (ht12 : t₁ ≠ t₂) (hx : t₁ ∈ S.params) (hy : t₂ ∈ S.params) (hxdeg : 2 ≤ S.deg t₁) (hydeg : 2 ≤ S.deg t₂) {K : ℕ} (hK : K ∈ S.gates) (hKG : (S.gate K).Reads (S.gates.min' hne)) (hKt : (S.gate K).Reads t₁ ∨ (S.gate K).Reads t₂) : ∃ (S₁ : State n), Preparation f S S₁ ∧ S₁.gates = S.gates ∧ S₁.auxIn = S.auxIn ∧ S₁.childIn < S.childIn

Rerouting a child K of the minimal gate that reads one of its parameter inputs, by relabelling K with the operation it computes on the two inputs, is a preparatory operation lowering the number of such children.

Eliminating the minimal AND

structure Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd {n : ℕ} (S : State n) (G x y : ℕ) : Prop

The configuration of Section 4.3: G is an AND-type gate reading the distinct unpaired parameters x and y with 2 ≤ deg y ≤ deg x, no child of G reads x or y, and G is not the output and has a child.

• mem : G ∈ S.gates

  G is a gate.

• and_op : ¬SemiCircuit.IsAffineOp (S.gate G).op

  G is AND-type.

• args : (S.gate G).left = SemiCircuit.Arg.node x ∧ (S.gate G).right = SemiCircuit.Arg.node y ∨ (S.gate G).left = SemiCircuit.Arg.node y ∧ (S.gate G).right = SemiCircuit.Arg.node x

  G reads x and y.

• unpaired_x : x ∈ S.unpaired

  x is unpaired.

• unpaired_y : y ∈ S.unpaired

  y is unpaired.

• ne : x ≠ y

  x and y are distinct.

• deg_y : 2 ≤ S.deg y

  y has degree at least two.

• deg_le : S.deg y ≤ S.deg x

  x has degree at least that of y.

• children (K : ℕ) : K ∈ S.gates → (S.gate K).Reads G → ¬(S.gate K).Reads x ∧ ¬(S.gate K).Reads y

  No child of G reads x or y.

• not_out : ¬S.out.Reads G

  G is not the output.

• has_child : ∃ K ∈ S.gates, (S.gate K).Reads G

  G has a child.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.mem_params_x {n : ℕ} {S : State n} {G x y : ℕ} (h : S.MinimalAnd G x y) : x ∈ S.params

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.mem_params_y {n : ℕ} {S : State n} {G x y : ℕ} (h : S.MinimalAnd G x y) : y ∈ S.params

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.mem_children_x {n : ℕ} {S : State n} {G x y : ℕ} (h : S.MinimalAnd G x y) : Sum.inl G ∈ S.children x

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.mem_children_y {n : ℕ} {S : State n} {G x y : ℕ} (h : S.MinimalAnd G x y) : Sum.inl G ∈ S.children y

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.exists_op {n : ℕ} {S : State n} {G x y : ℕ} (h : S.MinimalAnd G x y) : ∃ (φ : Bool → Bool → Bool), ¬SemiCircuit.IsAffineOp φ ∧ ∀ (val : ℕ → Bool), (S.gate G).eval val = φ (val x) (val y)

The minimal AND computes an AND-type operation of its inputs.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.ne_gate {n : ℕ} {f : BooleanFunction n} {S : State n} {G x y : ℕ} (hS : S.Valid f) (h : S.MinimalAnd G x y) {u : ℕ} (hu : u ∈ S.params) : u ≠ G

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.eq_inl_of_mem_children {n : ℕ} {f : BooleanFunction n} {S : State n} {G x y : ℕ} (hS : S.Valid f) (h : S.MinimalAnd G x y) {N : ℕ ⊕ ℕ} (hN : N ∈ S.children G) : ∃ K ∈ S.gates, N = Sum.inl K ∧ (S.gate K).Reads G

The children of G are gates.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_minimalAnd {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (hN : S.Normal) {G t₁ t₂ : ℕ} (hG : G ∈ S.gates) (hand : ¬SemiCircuit.IsAffineOp (S.gate G).op) (hl : (S.gate G).left = SemiCircuit.Arg.node t₁) (hr : (S.gate G).right = SemiCircuit.Arg.node t₂) (ht12 : t₁ ≠ t₂) (hx : t₁ ∈ S.params) (hy : t₂ ∈ S.params) (hch : ∀ K ∈ S.gates, (S.gate K).Reads G → ¬(S.gate K).Reads t₁ ∧ ¬(S.gate K).Reads t₂) : ∃ (x : ℕ) (y : ℕ), S.MinimalAnd G x y

In a normal state with d < a, an AND-type gate G reading two parameters, no child of which reads them, is a minimal AND in the sense of Section 4.3, its inputs ordered by degree: by Lemma 2.3, G is not the output, and it has a child since no deletion applies.