Programs with shared gates over the full binary basis

A SharedProgram over Binary.Formula on n inputs with k shared gates consists of k intermediate formulas over the full binary basis together with one output formula, where each formula may read the primary inputs and all previously computed shared values.

Fixing the coordinates outside a block Y ⊆ Fin n turns each of the k + 1 formulas into a subfunction of the coordinates in Y together with the active shared variables:

• If a shared formula G has no leaves in the current block (G.leavesIn Y = 0), then by Formula.eval_eq_of_leavesIn_eq_zero its value is constant once the outside coordinates are fixed, so its output wire is placed outside the block (castBlock Y) and contributes 0 to both the shared-gate count and the shared-leaf count on Y.
• If G.leavesIn Y ≠ 0, its output wire is included in the active block (snocBlock Y), contributing 1 active shared gate and P.occ N active shared-variable leaves.

Applying Nechiporuk's counting lemma (Nechiporuk.card_subfunctions_le) to the active formulas yields |(subfunctions P.eval Y)| ≤ 2 ^ (P.activeShared Y + 1) · 16 ^ (P.inputLeavesIn Y + P.activeSharedLeaves Y) (SharedProgram.card_subfunctions_le_activeSharedLeaves), which in turn implies the global bound |(subfunctions P.eval Y)| ≤ 2 ^ (k + 1) · 16 ^ (P.inputLeavesIn Y + P.sharedLeaves n) (SharedProgram.card_subfunctions_le_inputLeavesIn).

Every single-output circuit c over Binary.signature decomposes from its last gate down into a SharedProgram with k ≤ KW.sharedGateCount c shared gates, at most c.size binary gates, at most sharedFanOut c total shared-variable leaves, and on every block Y ⊆ Fin n, at most activeSharedGateCount c Y active shared gates and activeSharedFanOut c Y active shared-variable leaves (exists_sharedProgram_of_circuit). Summed over a family of blocks, the active shared fan-out weights each shared gate by the number of blocks its syntactic input cone meets (sum_activeSharedFanOut, sum_activeSharedFanOut_le_of_gateBlockSpan_le, sum_activeSharedFanOut_le_add_highSpanSharedFanOut). Moreover, wireActive and gateActive coincide with having syntactic input support (Program.wireSupport) meeting Y (wireActive_eq_true_iff, gateActive_eq_true_iff), so over pairwise disjoint blocks a gate's block-span never exceeds the cardinality of its input support (gateBlockSpan_le_card_wireSupport), and in any single-output binary circuit sharedFanOut c ≤ 2 * c.size + 1 (sharedFanOut_le_two_mul_size_add_one).

The definitions live in Complexitylib.Algebraic.LowerBound.Nechiporuk.Sharing.Defs and the proof internals in Complexitylib.Algebraic.LowerBound.Nechiporuk.Sharing.Internal.

theorem Algebraic.Nechiporuk.SharedProgram.inputLeaves_le_gates (m : ℕ) {N k : ℕ} (P : SharedProgram N k) : P.inputLeaves m ≤ P.gates + k + 1

The input leaves of a program with k shared gates number at most gates + k + 1.

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

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

theorem Algebraic.Nechiporuk.SharedProgram.activeShared_le {N k : ℕ} (P : SharedProgram N k) (Y : Finset (Fin N)) : P.activeShared Y ≤ k

At most k of the k shared gates of a program are active on any block.

theorem Algebraic.Nechiporuk.SharedProgram.activeSharedLeaves_le_sharedLeaves {N k : ℕ} (P : SharedProgram N k) (Y : Finset (Fin N)) : P.activeSharedLeaves Y ≤ P.sharedLeaves N

The shared-variable leaves reading active shared gates are among all shared-variable leaves.

theorem Algebraic.Nechiporuk.SharedProgram.card_subfunctions_le_active {N k : ℕ} (P : SharedProgram N k) (Y : Finset (Fin N)) : (subfunctions P.eval Y).card ≤ 2 ^ (P.activeShared Y + 1) * 16 ^ P.activeLeavesIn Y

Sharpened Nechiporuk counting lemma for programs with shared gates. A program P has at most 2 ^ (P.activeShared Y + 1) · 16 ^ (P.activeLeavesIn Y) subfunctions on Y: shared gates with no leaves in the current active block contribute neither to the exponent of 2 nor to the active leaf count.

theorem Algebraic.Nechiporuk.SharedProgram.card_subfunctions_le_activeSharedLeaves {n k : ℕ} (P : SharedProgram n k) (Y : Finset (Fin n)) : (subfunctions P.eval Y).card ≤ 2 ^ (P.activeShared Y + 1) * 16 ^ (inputLeavesIn Y P + P.activeSharedLeaves Y)

A program P has at most 2 ^ (P.activeShared Y + 1) · 16 ^ (P.inputLeavesIn Y + P.activeSharedLeaves Y) subfunctions on a primary block Y ⊆ Fin n.

theorem Algebraic.Nechiporuk.SharedProgram.card_subfunctions_le {N k : ℕ} (P : SharedProgram N k) (Y : Finset (Fin N)) : (subfunctions P.eval Y).card ≤ 2 ^ (k + 1) * 16 ^ P.leavesIn Y

Nechiporuk's counting lemma for programs with shared gates. A program with k shared gates has at most 2 ^ (k + 1) · 16 ^ (P.leavesIn Y) subfunctions on Y.

theorem Algebraic.Nechiporuk.SharedProgram.card_subfunctions_le_inputLeavesIn {n k : ℕ} (P : SharedProgram n k) (Y : Finset (Fin n)) : (subfunctions P.eval Y).card ≤ 2 ^ (k + 1) * 16 ^ (inputLeavesIn Y P + P.sharedLeaves n)

A program with k shared gates has at most 2 ^ (k + 1) · 16 ^ (P.inputLeavesIn Y + P.sharedLeaves n) subfunctions on Y.

Shared fan-out and translation from binary circuits to SharedProgram

theorem Algebraic.Nechiporuk.sharedGateCount_le_sharedFanOut {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : KW.sharedGateCount c ≤ sharedFanOut c

Every shared gate has fan-out at least two, so there are at most sharedFanOut c of them.

theorem Algebraic.Nechiporuk.sharedGateCount_le_size {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : KW.sharedGateCount c ≤ c.size

A circuit has at most c.size shared gates.

theorem Algebraic.Nechiporuk.activeSharedGateCount_le_sharedGateCount {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : activeSharedGateCount c Y ≤ KW.sharedGateCount c

The shared gates active on a block are among all shared gates.

theorem Algebraic.Nechiporuk.activeSharedFanOut_le_sharedFanOut {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : activeSharedFanOut c Y ≤ sharedFanOut c

The fan-out of the shared gates active on a block is at most the total shared fan-out.

theorem Algebraic.Nechiporuk.activeSharedGateCount_le_activeSharedFanOut {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : activeSharedGateCount c Y ≤ activeSharedFanOut c Y

Each active shared gate has fan-out at least two, so it contributes at least one to activeSharedFanOut c Y.

theorem Algebraic.Nechiporuk.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.wireActive_eq_true_iff {σ : Signature} {n t : ℕ} (Y : Finset (Fin n)) (p : Program σ n t) (w : Wire n t) : wireActive Y p w = true ↔ ∃ i ∈ Y, i ∈ p.wireSupport w

Wire w is active on Y iff its syntactic input support intersects Y.

theorem Algebraic.Nechiporuk.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.gateBlockSpan_le {σ : Signature} {n t B : ℕ} (Y : Fin B → Finset (Fin n)) (p : Program σ n t) (g : Fin t) : gateBlockSpan Y p g ≤ B

A gate is active on at most all B blocks.

theorem Algebraic.Nechiporuk.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: each binary gate reads two wires and the circuit reads one output wire.

theorem Algebraic.Nechiporuk.sum_activeSharedGateCount {σ : Signature} {n m B : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) : ∑ i : Fin B, activeSharedGateCount c (Y i) = ∑ g : Fin c.size with 2 ≤ KW.gateFanOut c g, gateBlockSpan Y c.program g

Summing activeSharedGateCount over a family of blocks equals summing the block-spans of all shared gates.

theorem Algebraic.Nechiporuk.sum_activeSharedFanOut {σ : Signature} {n m B : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) : ∑ i : Fin B, activeSharedFanOut c (Y i) = ∑ g : Fin c.size with 2 ≤ KW.gateFanOut c g, KW.gateFanOut c g * gateBlockSpan Y c.program g

Summing activeSharedFanOut over a family of blocks equals summing KW.gateFanOut c g * gateBlockSpan Y c.program g over all shared gates g.

theorem Algebraic.Nechiporuk.sum_activeSharedFanOut_le_of_gateBlockSpan_le {σ : Signature} {n m B s : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) (hs : ∀ (g : Fin c.size), 2 ≤ KW.gateFanOut c g → gateBlockSpan Y c.program g ≤ s) : ∑ i : Fin B, activeSharedFanOut c (Y i) ≤ s * sharedFanOut c

If every shared gate of c is active on at most s blocks of Y, then the sum of activeSharedFanOut c (Y i) over all blocks is at most s * sharedFanOut c.

theorem Algebraic.Nechiporuk.sum_activeSharedFanOut_le {σ : Signature} {n m B : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) : ∑ i : Fin B, activeSharedFanOut c (Y i) ≤ B * sharedFanOut c

Over B blocks, the active shared fan-out sums to at most B * sharedFanOut c.

theorem Algebraic.Nechiporuk.highSpanSharedFanOut_eq_zero_of_gateBlockSpan_le {σ : Signature} {n m B d : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) (hd : ∀ (g : Fin c.size), 2 ≤ KW.gateFanOut c g → gateBlockSpan Y c.program g ≤ d) : highSpanSharedFanOut c Y d = 0

When every shared gate of c is active on at most d blocks of Y, highSpanSharedFanOut c Y d vanishes.

theorem Algebraic.Nechiporuk.highSpanSharedFanOut_eq_zero_of_card_wireSupport_le {σ : Signature} {n m B d : ℕ} (c : Circuit σ n m) {Y : Fin B → Finset (Fin n)} (hdisj : Pairwise fun (i j : Fin B) => Disjoint (Y i) (Y j)) (hd : ∀ (g : Fin c.size), 2 ≤ KW.gateFanOut c g → (c.program.wireSupport (Wire.gate g)).card ≤ d) : highSpanSharedFanOut c Y d = 0

Over pairwise disjoint blocks Y, if the syntactic input support of every shared gate has size at most d, then highSpanSharedFanOut c Y d vanishes.

theorem Algebraic.Nechiporuk.sum_activeSharedFanOut_le_add_highSpanSharedFanOut {σ : Signature} {n m B : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) (d : ℕ) : ∑ i : Fin B, activeSharedFanOut c (Y i) ≤ d * sharedFanOut c + B * highSpanSharedFanOut c Y d

Splitting ∑ i, activeSharedFanOut c (Y i) at block-span threshold d: shared gates active on at most d blocks contribute at most d * sharedFanOut c, while shared gates active on strictly more than d blocks are active on at most B blocks and contribute at most B * highSpanSharedFanOut c Y d.

theorem Algebraic.Nechiporuk.exists_sharedProgram_of_circuit {n : ℕ} (c : Circuit Binary.signature n 1) {f : Cslib.BooleanFunction n} (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : ∃ (k : ℕ) (P : SharedProgram n k), k ≤ KW.sharedGateCount c ∧ P.Computes f ∧ P.gates ≤ c.size ∧ P.sharedLeaves n ≤ sharedFanOut c ∧ ∀ (Y : Finset (Fin n)), P.activeShared Y ≤ activeSharedGateCount c Y ∧ P.activeSharedLeaves Y ≤ activeSharedFanOut c Y

Full-binary-basis circuits as programs with shared gates. Every single-output circuit c over Binary.signature computing f yields a SharedProgram computing f with at most KW.sharedGateCount c shared gates, at most c.size binary gates, at most sharedFanOut c shared-variable leaves, and on every block Y ⊆ Fin n, at most activeSharedGateCount c Y active shared gates and activeSharedFanOut c Y active shared-variable leaves.