Internals: extended-basis circuits as programs with shared gates

Proof internals for Complexitylib.Algebraic.LowerBound.KarchmerWigderson.Sharing.Extended. The occurrence counts Formula.occ/SharedProgram.occ, the substitution SharedProgram.substVar, and the fan-out counts argUses/sharedCount are reused from Complexitylib.Algebraic.LowerBound.KarchmerWigderson.Sharing.Circuit. This file adds:

• how input leaves change under substVar (SharedProgram.inputLeaves_substVar) and under the lifting substitution SharedProgram.liftSubst, which replaces a variable by a formula over two fresh shared values;
• the expansion Extended.expandBinaryGadget of an XOR or EQUIV gate into two shared values and a zero-input-leaf gadget;
• the construction Extended.exists_sharedProgram_of_program, which tracks the number of shared values and the input leaves while processing an extended-basis program from the last gate down;
• the two-parameter superlinearity criterion isLittleO_of_forall_mul_le_two.

Inserting two values

def Algebraic.KW.insertVal2 {N d : ℕ} (y : Fin (N + d) → Bool) (b₀ b₁ : Bool) : Fin (N + 2 + d) → Bool

Insert the two values b₀, b₁ at positions N, N + 1 of y, moving the later entries up by two.

Equations

• Algebraic.KW.insertVal2 y b₀ b₁ i = if h : ↑i < N then y ⟨↑i, ⋯⟩ else if x : ↑i = N then b₀ else if x : ↑i = N + 1 then b₁ else y ⟨↑i - 2, ⋯⟩

theorem Algebraic.KW.insertVal2_zero {N : ℕ} (y : Fin N → Bool) (b₀ b₁ : Bool) : insertVal2 y b₀ b₁ = Fin.snoc (Fin.snoc y b₀) b₁

With no later entries, insertVal2 appends the two values.

theorem Algebraic.KW.insertVal2_snoc {N d : ℕ} (y : Fin (N + d) → Bool) (g b₀ b₁ : Bool) : insertVal2 (Fin.snoc y g) b₀ b₁ = Fin.snoc (insertVal2 y b₀ b₁) g

insertVal2 commutes with appending a later entry.

Input leaves of formulas under substitution

@[simp]

theorem Algebraic.KW.Formula.inputLeaves_mapIndex_castLE {N M : ℕ} (m : ℕ) (h : N ≤ M) (F : Formula N) : (mapIndex (Fin.castLE h) F).inputLeaves m = F.inputLeaves m

theorem Algebraic.KW.Formula.inputLeaves_succ {N : ℕ} (m : ℕ) (F : Formula N) : F.inputLeaves (m + 1) = F.inputLeaves m + occ m F

Raising the input threshold from m to m + 1 adds the leaves on variable m.

theorem Algebraic.KW.Formula.occ_eq_zero_of_inputLeaves_eq_zero {N m v : ℕ} (hv : v < m) {F : Formula N} : F.inputLeaves m = 0 → occ v F = 0

A formula with no input leaves below m has no leaves on any variable v < m.

theorem Algebraic.KW.Formula.inputLeaves_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (F : Formula (N + 1 + d)) : (subst (φ.substVarMap d) F).inputLeaves N = F.inputLeaves N + occ N F * φ.inputLeaves N

def Algebraic.KW.Formula.liftSubstMap {N : ℕ} (ψ : Formula (N + 2)) (d : ℕ) (i : Fin (N + 1 + d)) : Formula (N + 2 + d)

The substitution behind SharedProgram.liftSubst: the variable N becomes ψ : Formula (N + 2), the variables below N are kept, and those above N move up by one to make room for the two new shared variables N and N + 1.

Equations

• ψ.liftSubstMap d i = if h : ↑i < N then Algebraic.KW.Formula.lit ⟨↑i, ⋯⟩ true else if x : ↑i = N then Algebraic.KW.Formula.mapIndex (Fin.castLE ⋯) ψ else Algebraic.KW.Formula.lit ⟨↑i + 1, ⋯⟩ true

theorem Algebraic.KW.Formula.inputLeaves_subst_liftSubstMap {N : ℕ} (ψ : Formula (N + 2)) (hψ : ψ.inputLeaves N = 0) (d : ℕ) (F : Formula (N + 1 + d)) : (subst (ψ.liftSubstMap d) F).inputLeaves N = F.inputLeaves N

theorem Algebraic.KW.Formula.occ_subst_liftSubstMap {N : ℕ} (ψ : Formula (N + 2)) (hψ : ψ.inputLeaves N = 0) (d : ℕ) {w : ℕ} (hw : w < N) (F : Formula (N + 1 + d)) : occ w (subst (ψ.liftSubstMap d) F) = occ w F

theorem Algebraic.KW.Formula.eval_subst_liftSubstMap {N : ℕ} (ψ : Formula (N + 2)) (d : ℕ) (F : Formula (N + 1 + d)) (y : Fin (N + d) → Bool) (b₀ b₁ : Bool) : (subst (ψ.liftSubstMap d) F).eval (insertVal2 y b₀ b₁) = F.eval (insertVal y (ψ.eval (insertVal2 (fun (j : Fin (N + 0)) => y (Fin.castLE ⋯ j)) b₀ b₁)))

Input leaves of programs under substitution

@[simp]

theorem Algebraic.KW.SharedProgram.inputLeaves_output {N : ℕ} (m : ℕ) (F : Formula N) : (output F).inputLeaves m = F.inputLeaves m

@[simp]

theorem Algebraic.KW.SharedProgram.inputLeaves_share {N k : ℕ} (m : ℕ) (G : Formula N) (P : SharedProgram (N + 1) k) : (share G P).inputLeaves m = G.inputLeaves m + P.inputLeaves m

theorem Algebraic.KW.SharedProgram.inputLeaves_succ (m : ℕ) {N k : ℕ} (P : SharedProgram N k) : P.inputLeaves (m + 1) = P.inputLeaves m + occ m P

Raising the input threshold from m to m + 1 adds the leaves on variable m.

theorem Algebraic.KW.SharedProgram.inputLeaves_substVar {N : ℕ} (φ : Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : (substVar φ P).inputLeaves N = P.inputLeaves N + occ N P * φ.inputLeaves N

def Algebraic.KW.SharedProgram.liftSubst {N : ℕ} (ψ : Formula (N + 2)) {d k : ℕ} : SharedProgram (N + 1 + d) k → SharedProgram (N + 2 + d) k

Substitute ψ : Formula (N + 2) for variable N in a program reading N + 1 + d variables, shifting variables above N up by one so the result reads N + 2 + d variables.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.KW.SharedProgram.liftSubst ψ (Algebraic.KW.SharedProgram.output F) = Algebraic.KW.SharedProgram.output (Algebraic.KW.Formula.subst (ψ.liftSubstMap x✝) F)

theorem Algebraic.KW.SharedProgram.eval_liftSubst {N : ℕ} (ψ : Formula (N + 2)) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) (y : Fin (N + d) → Bool) (b₀ b₁ : Bool) : (liftSubst ψ P).eval (insertVal2 y b₀ b₁) = P.eval (insertVal y (ψ.eval (insertVal2 (fun (j : Fin (N + 0)) => y (Fin.castLE ⋯ j)) b₀ b₁)))

theorem Algebraic.KW.SharedProgram.inputLeaves_liftSubst {N : ℕ} (ψ : Formula (N + 2)) (hψ : ψ.inputLeaves N = 0) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : (liftSubst ψ P).inputLeaves N = P.inputLeaves N

theorem Algebraic.KW.SharedProgram.occ_liftSubst {N : ℕ} (ψ : Formula (N + 2)) (hψ : ψ.inputLeaves N = 0) {w : ℕ} (hw : w < N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : occ w (liftSubst ψ P) = occ w P

Extended-basis gates as formulas

def Algebraic.KW.Extended.lineFormula {n t : ℕ} : Line signature n t → Formula (n + t)

The formula of one De Morgan gate over the earlier wires, numbered by Wire.index. On the xor and equiv gates it is a placeholder constant: those gates are expanded by expandBinaryGadget instead.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.KW.Extended.lineFormula { op := Algebraic.KW.Extended.Op.false, wires := wires } = Algebraic.KW.Formula.const false
• Algebraic.KW.Extended.lineFormula { op := Algebraic.KW.Extended.Op.true, wires := wires } = Algebraic.KW.Formula.const true
• Algebraic.KW.Extended.lineFormula { op := Algebraic.KW.Extended.Op.id, wires := w } = Algebraic.KW.Formula.lit (w ⟨0, Algebraic.KW.Extended.lineFormula._proof_3⟩).index true
• Algebraic.KW.Extended.lineFormula { op := Algebraic.KW.Extended.Op.not, wires := w } = Algebraic.KW.Formula.lit (w ⟨0, Algebraic.KW.Extended.lineFormula._proof_4⟩).index false
• Algebraic.KW.Extended.lineFormula { op := Algebraic.KW.Extended.Op.xor, wires := wires } = Algebraic.KW.Formula.const false
• Algebraic.KW.Extended.lineFormula { op := Algebraic.KW.Extended.Op.equiv, wires := wires } = Algebraic.KW.Formula.const true

def Algebraic.KW.Extended.wireValues {n t : ℕ} (p : Program signature n t) (x : Fin n → Bool) : Fin (n + t) → Bool

The values of the inputs and gates of an extended-basis program, numbered by Wire.index.

Equations

• Algebraic.KW.Extended.wireValues p x = Fin.append x (p.eval Algebraic.KW.Extended.interpretation x)

theorem Algebraic.KW.Extended.eval_lineFormula_of_isDeMorgan {n t : ℕ} (line : Line signature n t) (h : isDeMorgan line.op = true) (x : Fin n → Bool) (vals : Fin t → Bool) : (lineFormula line).eval (Fin.append x vals) = line.eval interpretation x vals

theorem Algebraic.KW.Extended.inputLeaves_lineFormula_le {n t : ℕ} (line : Line signature n t) : (lineFormula line).inputLeaves (n + t) ≤ deMorganCost line.op + 1

theorem Algebraic.KW.Extended.occ_lineFormula_le {n t : ℕ} (line : Line signature n t) (g : Fin t) : Formula.occ (n + ↑g) (lineFormula line) ≤ argUses line g

theorem Algebraic.KW.Extended.occ_two_wires_le {n t : ℕ} (op : Op) (ha : arity op = 2) (w : Fin (arity op) → Wire n t) (g : Fin t) : ((if ↑(w ⟨0, ⋯⟩).index = n + ↑g then 1 else 0) + if ↑(w ⟨1, ⋯⟩).index = n + ↑g then 1 else 0) ≤ argUses { op := op, wires := w } g

The two arguments of a binary gate read gate g at most argUses times in total.

theorem Algebraic.KW.Extended.eval_gate {n t : ℕ} (p : Program signature n t) (line : Line signature n t) (x : Fin n → Bool) : (p.gate line).eval interpretation x = Fin.snoc (p.eval interpretation x) (line.eval interpretation x (p.eval interpretation x))

theorem Algebraic.KW.Extended.wireValues_gate {n t : ℕ} (p : Program signature n t) (line : Line signature n t) (x : Fin n → Bool) : wireValues (p.gate line) x = Fin.snoc (wireValues p x) (line.eval interpretation x (p.eval interpretation x))

theorem Algebraic.KW.Extended.wireValues_empty {n : ℕ} (x : Fin n → Bool) : wireValues Program.empty x = x

def Algebraic.KW.Extended.expandBinaryGadget {N j : ℕ} (i₀ i₁ : Fin N) (ψ : Formula (N + 2)) (Q : SharedProgram (N + 1) j) : SharedProgram N (j + 2)

Expand one binary XOR or EQUIV gate at position N = n + t into two shared wire steps and substitute ψ (xorGadget or equivGadget) for variable N.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.KW.Extended.eval_expandBinaryGadget {N j : ℕ} (i₀ i₁ : Fin N) (ψ : Formula (N + 2)) (Q : SharedProgram (N + 1) j) (y : Fin N → Bool) : (expandBinaryGadget i₀ i₁ ψ Q).eval y = Q.eval (Fin.snoc y (ψ.eval (Fin.snoc (Fin.snoc y (y i₀)) (y i₁))))

theorem Algebraic.KW.Extended.inputLeaves_expandBinaryGadget {N j : ℕ} (i₀ i₁ : Fin N) (ψ : Formula (N + 2)) (hψ : ψ.inputLeaves N = 0) (Q : SharedProgram (N + 1) j) : (expandBinaryGadget i₀ i₁ ψ Q).inputLeaves N = 2 + Q.inputLeaves N

theorem Algebraic.KW.Extended.occ_expandBinaryGadget {N j : ℕ} (i₀ i₁ : Fin N) (ψ : Formula (N + 2)) (hψ : ψ.inputLeaves N = 0) (Q : SharedProgram (N + 1) j) {w : ℕ} (hw : w < N) : SharedProgram.occ w (expandBinaryGadget i₀ i₁ ψ Q) = ((if ↑i₀ = w then 1 else 0) + if ↑i₁ = w then 1 else 0) + SharedProgram.occ w Q

From extended-basis programs to programs with shared gates

theorem Algebraic.KW.Extended.exists_sharedProgram_of_program {n : ℕ} (f : Cslib.BooleanFunction n) {t : ℕ} (p : Program signature n t) (u : Fin t → ℕ) {j : ℕ} (Q : SharedProgram (n + t) j) : (∀ (x : Fin n → Bool), Q.eval (wireValues p x) = f x) → (∀ (g : Fin t), SharedProgram.occ (n + ↑g) Q ≤ u g) → ∃ (K : ℕ) (P : SharedProgram n K), K ≤ j + sharedCount p u + 2 * Program.cost xorCost p ∧ P.Computes f ∧ P.inputLeaves n ≤ Q.inputLeaves (n + t) + Program.cost deMorganCost p + sharedCount p u + 2 * Program.cost xorCost p

Build a SharedProgram from the last gate of an extended-basis program down, tracking the number of shared steps and inputLeaves (n + t). Q reads all wires of p, gate g occurring at most u g times. A De Morgan gate of total fan-out at least two becomes a shared gate and any other De Morgan gate is substituted; an XOR or EQUIV gate becomes two shared values (its arguments) and a zero-input-leaf gadget, whatever its fan-out.

Superlinearity with two sublinear parameters

theorem Algebraic.KW.isLittleO_of_forall_mul_le_two {k r s : ℕ → ℕ} {a b d : ℕ} (hk : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hr : (fun (n : ℕ) => ↑(r n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (h : ∀ (n C : ℕ), (a * k n + b * r n + d + 1) * (C + 1) ≤ n → C * n ≤ s n) : (fun (n : ℕ) => ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑(s n)

Superlinearity when two parameters k n = o(n) and r n = o(n) control the linear factor: if (a · k n + b · r n + d + 1) · (C + 1) ≤ n forces C · n ≤ s n for every n and C, then n = o(s n). The one-parameter version is isLittleO_of_forall_mul_le.