Internals of programs with shared gates over the full binary basis

Proof internals for Complexitylib.Algebraic.LowerBound.Nechiporuk.Sharing:

• leaf and occurrence bookkeeping for Binary.Formula, including reindexing (mapIndex) and substitution of a formula for a variable (subst, substVarMap);
• the block-advancing combinatorics of SharedProgram.castBlock, snocBlock, and stepBlock, and the gluing identities used to restrict a share step to a block (SharedProgram.glue_castBlock, SharedProgram.glue_snocBlock), which yield the one-step subfunction bounds SharedProgram.card_subfunctions_share_le_of_leavesIn_eq_zero and SharedProgram.card_subfunctions_share_le_mul;
• substitution of a formula for a shared variable (SharedProgram.substVar) and its effect on gates, occurrences, and active measures;
• the translation of a full-binary-basis program into a SharedProgram, processing gates from the last one down (exists_sharedProgram_of_program): a gate read at least twice becomes a shared gate, and any other gate is substituted into the program;
• the characterization of gateActive by the syntactic input support (Internal.gateActive_eq_true_iff), the resulting block-span bound over disjoint blocks (Internal.gateBlockSpan_le_card_wireSupport), and the counting of gate-argument uses behind Internal.sharedFanOut_le_two_mul_size_add_one.

theorem Algebraic.Binary.Formula.leaves_le_gates_add_one {N : ℕ} (F : Formula N) : F.leaves ≤ F.gates + 1

The variable leaves of a binary formula number at most its binary gates plus one.

def Algebraic.Binary.Formula.mapIndex {N M : ℕ} (φ : Fin N → Fin M) : Formula N → Formula M

Reindex the variables of a formula.

Equations

• Algebraic.Binary.Formula.mapIndex φ (Algebraic.Binary.Formula.var i) = Algebraic.Binary.Formula.var (φ i)
• Algebraic.Binary.Formula.mapIndex φ (Algebraic.Binary.Formula.const b) = Algebraic.Binary.Formula.const b
• Algebraic.Binary.Formula.mapIndex φ (Algebraic.Binary.Formula.gate op l r) = Algebraic.Binary.Formula.gate op (Algebraic.Binary.Formula.mapIndex φ l) (Algebraic.Binary.Formula.mapIndex φ r)

@[simp]

theorem Algebraic.Binary.Formula.eval_mapIndex {N M : ℕ} (φ : Fin N → Fin M) (F : Formula N) (x : Fin M → Bool) : (mapIndex φ F).eval x = F.eval (x ∘ φ)

Evaluating a reindexed formula is evaluating the original on the reindexed assignment.

@[simp]

theorem Algebraic.Binary.Formula.gates_mapIndex {N M : ℕ} (φ : Fin N → Fin M) (F : Formula N) : (mapIndex φ F).gates = F.gates

Reindexing variables does not change the number of gates.

theorem Algebraic.Binary.Formula.leavesIn_mapIndex {N M : ℕ} (φ : Fin N → Fin M) (Y : Finset (Fin M)) (F : Formula N) : leavesIn Y (mapIndex φ F) = leavesIn {i : Fin N | φ i ∈ Y} F

The leaves of a reindexed formula in Y are the leaves of the original in the preimage of Y.

def Algebraic.Binary.Formula.subst {N M : ℕ} (σ : Fin N → Formula M) : Formula N → Formula M

Substitute a formula for each variable.

Equations

• Algebraic.Binary.Formula.subst σ (Algebraic.Binary.Formula.var i) = σ i
• Algebraic.Binary.Formula.subst σ (Algebraic.Binary.Formula.const b) = Algebraic.Binary.Formula.const b
• Algebraic.Binary.Formula.subst σ (Algebraic.Binary.Formula.gate op l r) = Algebraic.Binary.Formula.gate op (Algebraic.Binary.Formula.subst σ l) (Algebraic.Binary.Formula.subst σ r)

theorem Algebraic.Binary.Formula.eval_subst {N M : ℕ} (σ : Fin N → Formula M) (F : Formula N) (x : Fin M → Bool) : (subst σ F).eval x = F.eval fun (i : Fin N) => (σ i).eval x

Evaluating a substituted formula evaluates the original on the values of the substitutes.

@[simp]

theorem Algebraic.Binary.Formula.occ_mapIndex_castLE {N M : ℕ} (v : ℕ) (h : N ≤ M) (F : Formula N) : occ v (mapIndex (Fin.castLE h) F) = occ v F

Embedding the variables with Fin.castLE preserves occurrence counts.

theorem Algebraic.Binary.Formula.occ_eq_zero_of_ge {N v : ℕ} (hv : N ≤ v) (F : Formula N) : occ v F = 0

A variable index at least N never occurs in a formula on N variables.

theorem Algebraic.Binary.Formula.inputLeaves_le_leaves {N : ℕ} (m : ℕ) (F : Formula N) : F.inputLeaves m ≤ F.leaves

The input leaves are among all variable leaves.

theorem Algebraic.Binary.Formula.inputLeaves_le_gates_add_one {N : ℕ} (m : ℕ) (F : Formula N) : F.inputLeaves m ≤ F.gates + 1

The input leaves of a binary formula number at most its binary gates plus one.

theorem Algebraic.Binary.Formula.sharedLeaves_eq_zero_of_le {N m : ℕ} (hm : N ≤ m) (F : Formula N) : F.sharedLeaves m = 0

A formula on N variables has no leaves on variables from m ≥ N on.

@[simp]

theorem Algebraic.Binary.Formula.sharedLeaves_mapIndex_castLE {N M : ℕ} (m : ℕ) (h : N ≤ M) (F : Formula N) : (mapIndex (Fin.castLE h) F).sharedLeaves m = F.sharedLeaves m

Embedding the variables with Fin.castLE preserves shared-leaf counts.

theorem Algebraic.Binary.Formula.sharedLeaves_eq_occ_add_sharedLeaves_succ {N : ℕ} (m : ℕ) (F : Formula N) : F.sharedLeaves m = occ m F + F.sharedLeaves (m + 1)

The shared leaves from m on split into the occurrences of m and the shared leaves from m + 1 on.

theorem Algebraic.Binary.Formula.sum_inputLeavesIn_le_inputLeaves {N m n : ℕ} (Y : Fin m → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin m) => Disjoint (Y i) (Y j)) (F : Formula N) : ∑ i : Fin m, inputLeavesIn (Y i) F ≤ F.inputLeaves n

Over pairwise disjoint blocks of Fin n, inputLeavesIn sums to at most inputLeaves n.

def Algebraic.Binary.Formula.extendBlock (N : ℕ) {n : ℕ} (Y : Finset (Fin n)) : Finset (Fin N)

Extend a block Y ⊆ Fin n to Fin N by including all shared variables i ≥ n.

Equations

• Algebraic.Binary.Formula.extendBlock N Y = {i : Fin N | if h : ↑i < n then ⟨↑i, h⟩ ∈ Y else True}

theorem Algebraic.Binary.Formula.extendBlock_self {n : ℕ} (Y : Finset (Fin n)) : extendBlock n Y = Y

Extending a block of Fin n to Fin n itself does not change it.

theorem Algebraic.Binary.Formula.leavesIn_extendBlock (N : ℕ) {n : ℕ} (Y : Finset (Fin n)) (F : Formula N) : leavesIn (extendBlock N Y) F = inputLeavesIn Y F + F.sharedLeaves n

The leaves in the extended block are the input leaves in Y plus all shared leaves.

theorem Algebraic.Binary.Formula.leavesIn_eq_inputLeavesIn_add_sum_occ {N n : ℕ} (Y₀ : Finset (Fin n)) (Y : Finset (Fin N)) (hY : ∀ (i : Fin N) (hi : ↑i < n), i ∈ Y ↔ ⟨↑i, hi⟩ ∈ Y₀) (F : Formula N) : leavesIn Y F = inputLeavesIn Y₀ F + ∑ i ∈ Y, if n ≤ ↑i then occ (↑i) F else 0

Decompose F.leavesIn Y into input leaves in Y₀ and occurrences of shared variables in Y when Y agrees with Y₀ below n.

def Algebraic.Binary.Formula.liftBlock {N d : ℕ} (b : Bool) (W : Finset (Fin (N + d))) : Finset (Fin (N + 1 + d))

Insert membership b at variable N, shifting variables ≥ N up by one.

Equations

• Algebraic.Binary.Formula.liftBlock b W = {i : Fin (N + 1 + d) | if h : ↑i < N then ⟨↑i, ⋯⟩ ∈ W else if x : ↑i = N then b = true else ⟨↑i - 1, ⋯⟩ ∈ W}

theorem Algebraic.Binary.Formula.leavesIn_liftBlock_true {N : ℕ} (d : ℕ) (W : Finset (Fin (N + d))) (F : Formula (N + 1 + d)) : leavesIn (liftBlock true W) F = leavesIn (liftBlock false W) F + occ N F

Including variable N in a lifted block adds exactly the occurrences of N.

def Algebraic.Binary.Formula.substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (i : Fin (N + 1 + d)) : Formula (N + d)

The substitution map replacing variable N by φ, keeping variables below N, and shifting variables above N down by one.

Equations

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

theorem Algebraic.Binary.Formula.gates_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (F : Formula (N + 1 + d)) : (subst (φ.substVarMap d) F).gates = F.gates + occ N F * φ.gates

Substituting φ for variable N adds φ.gates once per occurrence of N.

theorem Algebraic.Binary.Formula.occ_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) {w : ℕ} (hw : w < N) (F : Formula (N + 1 + d)) : occ w (subst (φ.substVarMap d) F) = occ w F + occ N F * occ w φ

Substituting φ for variable N adds the occurrences of w < N in φ once per occurrence of N.

theorem Algebraic.Binary.Formula.occ_subst_substVarMap_ge {N : ℕ} (φ : Formula N) (d : ℕ) {w : ℕ} (hw : N ≤ w) (F : Formula (N + 1 + d)) : occ w (subst (φ.substVarMap d) F) = occ (w + 1) F

Substituting for variable N shifts the occurrences of variables above N down by one.

theorem Algebraic.Binary.Formula.leavesIn_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (W : Finset (Fin (N + d))) (F : Formula (N + 1 + d)) : leavesIn W (subst (φ.substVarMap d) F) = leavesIn (liftBlock false W) F + occ N F * leavesIn {j : Fin N | Fin.castLE ⋯ j ∈ W} φ

The leaves of a substituted formula in W are the leaves of the original outside variable N plus the leaves of φ once per occurrence of N.

theorem Algebraic.Binary.Formula.leavesIn_subst_substVarMap_eq_zero_iff {N : ℕ} (φ : Formula N) (d : ℕ) (W : Finset (Fin (N + d))) (F : Formula (N + 1 + d)) : leavesIn W (subst (φ.substVarMap d) F) = 0 ↔ leavesIn (liftBlock (decide (leavesIn {j : Fin N | Fin.castLE ⋯ j ∈ W} φ ≠ 0)) W) F = 0

A substituted formula has no leaves in W iff the original has none in the block lifted by whether φ has leaves in W.

theorem Algebraic.Binary.Formula.sharedLeaves_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (F : Formula (N + 1 + d)) : (subst (φ.substVarMap d) F).sharedLeaves N = F.sharedLeaves (N + 1)

Substituting a formula on N variables for variable N shifts the shared leaves down by one.

theorem Algebraic.Binary.Formula.eval_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (F : Formula (N + 1 + d)) (y : Fin (N + d) → Bool) : (subst (φ.substVarMap d) F).eval y = F.eval (KW.insertVal y (φ.eval fun (j : Fin N) => y (Fin.castLE ⋯ j)))

Evaluating a substituted formula evaluates the original with φ's value inserted at N.

Subfunctions of a program with shared gates

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.last_notMem_castBlock {N : ℕ} (Y : Finset (Fin N)) : Fin.last N ∉ castBlock Y

castBlock Y never contains the new last variable.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.castSucc_mem_castBlock {N : ℕ} (Y : Finset (Fin N)) (i : Fin N) : i.castSucc ∈ castBlock Y ↔ i ∈ Y

A lifted old variable lies in castBlock Y iff it lies in Y.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.last_mem_snocBlock {N : ℕ} (Y : Finset (Fin N)) : Fin.last N ∈ snocBlock Y

snocBlock Y always contains the new last variable.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.castSucc_mem_snocBlock {N : ℕ} (Y : Finset (Fin N)) (i : Fin N) : i.castSucc ∈ snocBlock Y ↔ i ∈ Y

A lifted old variable lies in snocBlock Y iff it lies in Y.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.castSucc_mem_stepBlock {N : ℕ} (G : Binary.Formula N) (Y : Finset (Fin N)) (i : Fin N) : i.castSucc ∈ stepBlock G Y ↔ i ∈ Y

A lifted old variable lies in stepBlock G Y iff it lies in Y.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.last_mem_stepBlock {N : ℕ} (G : Binary.Formula N) (Y : Finset (Fin N)) : Fin.last N ∈ stepBlock G Y ↔ Binary.Formula.leavesIn Y G ≠ 0

The new last variable lies in stepBlock G Y iff G has a leaf in Y.

theorem Algebraic.Nechiporuk.SharedProgram.snocBlock_extendBlock {n N : ℕ} (hn : n ≤ N) (Y : Finset (Fin n)) : snocBlock (Binary.Formula.extendBlock N Y) = Binary.Formula.extendBlock (N + 1) Y

Adding the new last variable commutes with extending a block by all shared variables.

theorem Algebraic.Nechiporuk.SharedProgram.leavesIn_extendBlock {N k : ℕ} (P : SharedProgram N k) {n : ℕ} (_hn : n ≤ N) (Y : Finset (Fin n)) : P.leavesIn (Binary.Formula.extendBlock N Y) = inputLeavesIn Y P + P.sharedLeaves n

The block leaf count on an extended block is the input leaves in Y plus all shared leaves.

theorem Algebraic.Nechiporuk.SharedProgram.leavesIn_eq_inputLeavesIn_add_sharedLeaves {n k : ℕ} (P : SharedProgram n k) (Y : Finset (Fin n)) : P.leavesIn Y = inputLeavesIn Y P + P.sharedLeaves n

On a primary block, the block leaf count is the input leaves in Y plus all shared leaves.

theorem Algebraic.Nechiporuk.SharedProgram.sharedLeaves_eq_occ_add_sharedLeaves_succ (m : ℕ) {N k : ℕ} (P : SharedProgram N k) : P.sharedLeaves m = occ m P + P.sharedLeaves (m + 1)

The shared leaves from m on split into the occurrences of m and the shared leaves from m + 1 on.

theorem Algebraic.Nechiporuk.SharedProgram.activeLeavesIn_eq_inputLeavesIn_add_sum_occ {N k : ℕ} (P : SharedProgram N k) {n : ℕ} (_hn : n ≤ N) (Y₀ : Finset (Fin n)) (Y : Finset (Fin N)) : (∀ (i : Fin N) (hi : ↑i < n), i ∈ Y ↔ ⟨↑i, hi⟩ ∈ Y₀) → P.activeLeavesIn Y = (inputLeavesIn Y₀ P + ∑ i ∈ Y, if n ≤ ↑i then occ (↑i) P else 0) + P.activeSharedLeaves Y

The active leaves of P on Y split into input leaves in Y₀, occurrences of the shared variables in Y, and the active shared-variable leaves, when Y agrees with Y₀ below n.

theorem Algebraic.Nechiporuk.SharedProgram.activeLeavesIn_eq_inputLeavesIn_add_activeSharedLeaves {n k : ℕ} (P : SharedProgram n k) (Y : Finset (Fin n)) : P.activeLeavesIn Y = inputLeavesIn Y P + P.activeSharedLeaves Y

The active leaves of P on a primary block Y ⊆ Fin n equal P.inputLeavesIn Y plus P.activeSharedLeaves Y.

def Algebraic.Nechiporuk.SharedProgram.castBlockVal {N : ℕ} {Y : Finset (Fin N)} (y : ↥Y → Bool) (j : ↥(castBlock Y)) : Bool

Project a coordinate in castBlock Y to Y.

Equations

• Algebraic.Nechiporuk.SharedProgram.castBlockVal y j = y ⟨⟨↑↑j, ⋯⟩, ⋯⟩

def Algebraic.Nechiporuk.SharedProgram.snocComplVal {N : ℕ} {Y : Finset (Fin N)} (z : ↥Yᶜ → Bool) (b : Bool) (j : ↥(castBlock Y)ᶜ) : Bool

Extend an outside assignment z : ↥Yᶜ → Bool by b on Fin.last N.

Equations

• Algebraic.Nechiporuk.SharedProgram.snocComplVal z b j = if h : ↑↑j < N then z ⟨⟨↑↑j, h⟩, ⋯⟩ else b

theorem Algebraic.Nechiporuk.SharedProgram.glue_castBlock {N : ℕ} (Y : Finset (Fin N)) (y : ↥Y → Bool) (z : ↥Yᶜ → Bool) (b : Bool) : Fin.snoc (Cutwidth.glue Y y z) b = Cutwidth.glue (castBlock Y) (castBlockVal y) (snocComplVal z b)

Appending a value outside the block: gluing over Y and appending b equals gluing over castBlock Y with b among the outside coordinates.

def Algebraic.Nechiporuk.SharedProgram.uncastCompl {N : ℕ} {Y : Finset (Fin N)} (j : ↥(snocBlock Y)ᶜ) : ↥Yᶜ

Project a coordinate outside snocBlock Y to Yᶜ.

Equations

• Algebraic.Nechiporuk.SharedProgram.uncastCompl j = ⟨⟨↑↑j, ⋯⟩, ⋯⟩

def Algebraic.Nechiporuk.SharedProgram.snocBlockVal {N : ℕ} {Y : Finset (Fin N)} (y : ↥Y → Bool) (b : Bool) (j : ↥(snocBlock Y)) : Bool

Extend a block assignment y : ↥Y → Bool by the value b on Fin.last N.

Equations

• Algebraic.Nechiporuk.SharedProgram.snocBlockVal y b j = if h : ↑↑j < N then y ⟨⟨↑↑j, h⟩, ⋯⟩ else b

theorem Algebraic.Nechiporuk.SharedProgram.glue_snocBlock {N : ℕ} (Y : Finset (Fin N)) (y : ↥Y → Bool) (z : ↥Yᶜ → Bool) (b : Bool) : Fin.snoc (Cutwidth.glue Y y z) b = Cutwidth.glue (snocBlock Y) (snocBlockVal y b) (z ∘ uncastCompl)

Appending a value inside the block: gluing over Y and appending b equals gluing over snocBlock Y with b among the block coordinates.

theorem Algebraic.Nechiporuk.SharedProgram.card_subfunctions_share_le_of_leavesIn_eq_zero {N k : ℕ} (G : Binary.Formula N) (P : SharedProgram (N + 1) k) (Y : Finset (Fin N)) (hG : Binary.Formula.leavesIn Y G = 0) : (subfunctions (share G P).eval Y).card ≤ (subfunctions P.eval (castBlock Y)).card

If the shared formula G has no leaves in Y, then share G P has at most as many subfunctions on Y as P has on castBlock Y: the shared value is constant once the outside coordinates are fixed.

theorem Algebraic.Nechiporuk.SharedProgram.card_subfunctions_share_le_mul {N k : ℕ} (G : Binary.Formula N) (P : SharedProgram (N + 1) k) (Y : Finset (Fin N)) : (subfunctions (share G P).eval Y).card ≤ (subfunctions G.eval Y).card * (subfunctions P.eval (snocBlock Y)).card

The subfunctions of share G P on Y number at most the product of the subfunction counts of G on Y and of P on snocBlock Y.

Substitution of a variable in a SharedProgram

def Algebraic.Nechiporuk.SharedProgram.substVar {N : ℕ} (φ : Binary.Formula N) {d k : ℕ} : SharedProgram (N + 1 + d) k → SharedProgram (N + d) k

Substitute the formula φ for variable N throughout a program on N + 1 + d variables.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Nechiporuk.SharedProgram.substVar φ (Algebraic.Nechiporuk.SharedProgram.output F) = Algebraic.Nechiporuk.SharedProgram.output (Algebraic.Binary.Formula.subst (φ.substVarMap x✝) F)

theorem Algebraic.Nechiporuk.SharedProgram.eval_substVar {N : ℕ} (φ : Binary.Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) (y : Fin (N + d) → Bool) : (substVar φ P).eval y = P.eval (KW.insertVal y (φ.eval fun (j : Fin N) => y (Fin.castLE ⋯ j)))

Evaluating substVar φ P evaluates P with φ's value inserted at variable N.

theorem Algebraic.Nechiporuk.SharedProgram.gates_substVar {N : ℕ} (φ : Binary.Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : (substVar φ P).gates = P.gates + occ N P * φ.gates

Substituting φ adds φ.gates once per occurrence of variable N.

theorem Algebraic.Nechiporuk.SharedProgram.occ_substVar {N : ℕ} (φ : Binary.Formula N) {w : ℕ} (hw : w < N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : occ w (substVar φ P) = occ w P + occ N P * Binary.Formula.occ w φ

Substituting φ adds the occurrences of w < N in φ once per occurrence of variable N.

theorem Algebraic.Nechiporuk.SharedProgram.occ_substVar_ge {N : ℕ} (φ : Binary.Formula N) {w : ℕ} (hw : N ≤ w) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : occ w (substVar φ P) = occ (w + 1) P

Substituting for variable N shifts the occurrences of variables above N down by one.

theorem Algebraic.Nechiporuk.SharedProgram.sharedLeaves_substVar {N : ℕ} (φ : Binary.Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : (substVar φ P).sharedLeaves N = P.sharedLeaves (N + 1)

Substituting for variable N shifts the shared leaves down by one.

theorem Algebraic.Nechiporuk.SharedProgram.activeShared_substVar_aux {N : ℕ} (φ : Binary.Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) (W : Finset (Fin (N + d))) : (substVar φ P).activeShared W = P.activeShared (Binary.Formula.liftBlock (decide (Binary.Formula.leavesIn {j : Fin N | Fin.castLE ⋯ j ∈ W} φ ≠ 0)) W)

Substitution preserves active shared gates, measured on the lifted block.

theorem Algebraic.Nechiporuk.SharedProgram.activeShared_substVar {N k : ℕ} (φ : Binary.Formula N) (P : SharedProgram (N + 1) k) (Z : Finset (Fin N)) : (substVar φ P).activeShared Z = P.activeShared (stepBlock φ Z)

Substituting φ for the first shared variable preserves active shared gates once the block is advanced through φ.

theorem Algebraic.Nechiporuk.SharedProgram.activeSharedLeaves_substVar_aux {N : ℕ} (φ : Binary.Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) (W : Finset (Fin (N + d))) : (substVar φ P).activeSharedLeaves W = P.activeSharedLeaves (Binary.Formula.liftBlock (decide (Binary.Formula.leavesIn {j : Fin N | Fin.castLE ⋯ j ∈ W} φ ≠ 0)) W)

Substitution preserves active shared-variable leaves, measured on the lifted block.

theorem Algebraic.Nechiporuk.SharedProgram.activeSharedLeaves_substVar {N k : ℕ} (φ : Binary.Formula N) (P : SharedProgram (N + 1) k) (Z : Finset (Fin N)) : (substVar φ P).activeSharedLeaves Z = P.activeSharedLeaves (stepBlock φ Z)

Substituting φ for the first shared variable preserves active shared-variable leaves once the block is advanced through φ.

Shared fan-out and translation from binary circuits to SharedProgram

def Algebraic.Nechiporuk.sharedFanOutCount {σ : Signature} {n t : ℕ} (p : Program σ n t) (u : Fin t → ℕ) : ℕ

The total fan-out of the gates of p whose fan-out is at least two when gate g is read u g more times.

Equations

• Algebraic.Nechiporuk.sharedFanOutCount p u = ∑ g : Fin t with 2 ≤ Algebraic.KW.slotUses p g + u g, (Algebraic.KW.slotUses p g + u g)

theorem Algebraic.Nechiporuk.sharedFanOut_eq {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : sharedFanOut c = sharedFanOutCount c.program fun (g : Fin c.size) => {o : Fin m | c.outputs o = Wire.gate g}.card

sharedFanOut c is sharedFanOutCount of its program with the output reads as extra uses.

theorem Algebraic.Nechiporuk.sharedFanOutCount_gate {σ : Signature} {n t : ℕ} (p : Program σ n t) (line : Line σ n t) (u : Fin (t + 1) → ℕ) : sharedFanOutCount (p.gate line) u = (if 2 ≤ u (Fin.last t) then u (Fin.last t) else 0) + sharedFanOutCount p fun (g : Fin t) => u g.castSucc + KW.argUses line g

Peeling the last gate off a program: its shared fan-out is counted separately, and its reads move into the extra uses of the earlier gates.

theorem Algebraic.Nechiporuk.gateActive_gate_last {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (line : Line σ n t) : gateActive Y (p.gate line) (Fin.last t) = decide (∃ (a : Fin (σ.Arity line.op)), wireActive Y p (line.wires a) = true)

The last gate is active iff one of its argument wires is active.

@[simp]

theorem Algebraic.Nechiporuk.gateActive_gate_castSucc {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (line : Line σ n t) (g : Fin t) : gateActive Y (p.gate line) g.castSucc = gateActive Y p g

Appending a gate does not change whether an earlier gate is active.

def Algebraic.Nechiporuk.activeSharedCount {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (u : Fin t → ℕ) : ℕ

The number of gates of p active on Y whose fan-out is at least two when gate g is read u g more times.

Equations

• Algebraic.Nechiporuk.activeSharedCount Y p u = {g : Fin t | 2 ≤ Algebraic.KW.slotUses p g + u g ∧ Algebraic.Nechiporuk.gateActive Y p g = true}.card

def Algebraic.Nechiporuk.activeSharedFanOutCount {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (u : Fin t → ℕ) : ℕ

The total fan-out of the gates of p active on Y whose fan-out is at least two when gate g is read u g more times.

Equations

• Algebraic.Nechiporuk.activeSharedFanOutCount Y p u = ∑ g : Fin t with 2 ≤ Algebraic.KW.slotUses p g + u g ∧ Algebraic.Nechiporuk.gateActive Y p g = true, (Algebraic.KW.slotUses p g + u g)

theorem Algebraic.Nechiporuk.activeSharedGateCount_eq {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : activeSharedGateCount c Y = activeSharedCount Y c.program fun (g : Fin c.size) => {o : Fin m | c.outputs o = Wire.gate g}.card

activeSharedGateCount c Y is activeSharedCount of its program with the output reads as extra uses.

theorem Algebraic.Nechiporuk.activeSharedFanOut_eq {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : activeSharedFanOut c Y = activeSharedFanOutCount Y c.program fun (g : Fin c.size) => {o : Fin m | c.outputs o = Wire.gate g}.card

activeSharedFanOut c Y is activeSharedFanOutCount of its program with the output reads as extra uses.

theorem Algebraic.Nechiporuk.activeSharedCount_gate {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (line : Line σ n t) (u : Fin (t + 1) → ℕ) : activeSharedCount Y (p.gate line) u = (if 2 ≤ u (Fin.last t) ∧ gateActive Y (p.gate line) (Fin.last t) = true then 1 else 0) + activeSharedCount Y p fun (g : Fin t) => u g.castSucc + KW.argUses line g

Peeling the last gate off a program for activeSharedCount.

theorem Algebraic.Nechiporuk.activeSharedFanOutCount_gate {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (line : Line σ n t) (u : Fin (t + 1) → ℕ) : activeSharedFanOutCount Y (p.gate line) u = (if 2 ≤ u (Fin.last t) ∧ gateActive Y (p.gate line) (Fin.last t) = true then u (Fin.last t) else 0) + activeSharedFanOutCount Y p fun (g : Fin t) => u g.castSucc + KW.argUses line g

Peeling the last gate off a program for activeSharedFanOutCount.

def Algebraic.Nechiporuk.activeWires {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) : Finset (Fin (n + t))

The subset of Fin (n + t) consisting of wires of p active on Y.

Equations

• Algebraic.Nechiporuk.activeWires Y p = {i : Fin (n + t) | if h : ↑i < n then ⟨↑i, h⟩ ∈ Y else Algebraic.Nechiporuk.gateActive Y p ⟨↑i - n, ⋯⟩ = true}

@[simp]

theorem Algebraic.Nechiporuk.activeWires_empty {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) : activeWires Y Program.empty = Y

The active wires of the empty program are the block itself.

@[simp]

theorem Algebraic.Nechiporuk.index_mem_activeWires {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (w : Wire n t) : w.index ∈ activeWires Y p ↔ wireActive Y p w = true

A wire's index is an active wire iff the wire is active.

def Algebraic.Nechiporuk.lineFormula {n t : ℕ} (line : Line Binary.signature n t) : Binary.Formula (n + t)

The formula of one full-binary-basis gate over the earlier wires, numbered by Wire.index.

Equations

• Algebraic.Nechiporuk.lineFormula line = Algebraic.Binary.Formula.gate line.op (Algebraic.Binary.Formula.var (line.wires 0).index) (Algebraic.Binary.Formula.var (line.wires 1).index)

theorem Algebraic.Nechiporuk.leavesIn_lineFormula_activeWires_eq_zero_iff {n t : ℕ} (Y : Finset (Fin n)) (p : Program Binary.signature n t) (line : Line Binary.signature n t) : Binary.Formula.leavesIn (activeWires Y p) (lineFormula line) = 0 ↔ gateActive Y (p.gate line) (Fin.last t) = false

The formula of the last gate has no leaves among the active wires iff the gate is inactive.

theorem Algebraic.Nechiporuk.stepBlock_lineFormula_activeWires {n t : ℕ} (Y : Finset (Fin n)) (p : Program Binary.signature n t) (line : Line Binary.signature n t) : SharedProgram.stepBlock (lineFormula line) (activeWires Y p) = activeWires Y (p.gate line)

Advancing the active wires through the formula of a new gate gives the active wires of the extended program.

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

The values of the inputs and gates of a binary program, numbered by Wire.index.

Equations

• Algebraic.Nechiporuk.wireValues p x = Fin.append x (p.eval Algebraic.Binary.interpretation x)

theorem Algebraic.Nechiporuk.eval_lineFormula {n t : ℕ} (line : Line Binary.signature n t) (x : Fin n → Bool) (vals : Fin t → Bool) : (lineFormula line).eval (Fin.append x vals) = line.eval Binary.interpretation x vals

The formula of a gate evaluates as the gate.

theorem Algebraic.Nechiporuk.gates_lineFormula {n t : ℕ} (line : Line Binary.signature n t) : (lineFormula line).gates = 1

The formula of a gate has exactly one binary gate.

theorem Algebraic.Nechiporuk.sharedLeaves_lineFormula {n t : ℕ} (line : Line Binary.signature n t) : (lineFormula line).sharedLeaves (n + t) = 0

The formula of a gate reads no variables beyond the existing wires.

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

The formula of a gate reads gate g at most as often as the gate's arguments do.

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

Evaluating a program with an appended gate appends the gate's value.

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

The wire values of an extended program append the value of the new gate's formula.

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

The wire values of the empty program are the inputs.

theorem Algebraic.Nechiporuk.exists_sharedProgram_of_program {n : ℕ} (f : Cslib.BooleanFunction n) {t : ℕ} (p : Program Binary.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 + KW.sharedCount p u ∧ P.Computes f ∧ P.gates ≤ Q.gates + t ∧ P.sharedLeaves n ≤ Q.sharedLeaves (n + t) + sharedFanOutCount p u ∧ ∀ (Y : Finset (Fin n)), P.activeShared Y ≤ Q.activeShared (activeWires Y p) + activeSharedCount Y p u ∧ P.activeSharedLeaves Y ≤ Q.activeSharedLeaves (activeWires Y p) + activeSharedFanOutCount Y p u

Build a SharedProgram from the last gate of a full-binary-basis program down, simultaneously bounding both global and block-active shared gates and shared-variable leaves.

theorem Algebraic.Nechiporuk.Internal.gateActive_eq_true_iff {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (g : Fin t) : gateActive Y p g = true ↔ ∃ i ∈ Y, i ∈ p.wireSupport (Wire.gate g)

Gate g is active on Y iff its syntactic input support intersects Y.

theorem Algebraic.Nechiporuk.Internal.gateBlockSpan_le_card_wireSupport {σ : Signature} {n t B : ℕ} {Y : Fin B → Finset (Fin n)} (hdisj : Pairwise fun (i j : Fin B) => Disjoint (Y i) (Y j)) (p : Program σ n t) (g : Fin t) : gateBlockSpan Y p g ≤ (p.wireSupport (Wire.gate g)).card

Over pairwise disjoint blocks Y, the number of blocks on which gate g is active is at most the cardinality of its syntactic input support.

theorem Algebraic.Nechiporuk.Internal.sharedFanOut_le_two_mul_size_add_one {n : ℕ} (c : Circuit Binary.signature n 1) : sharedFanOut c ≤ 2 * c.size + 1

In any single-output circuit over Binary.signature, the total fan-out of all shared gates is at most 2 * c.size + 1.