Nechiporuk's formula and bounded-sharing circuit lower bounds for rectangle-free functions

Nechiporuk's method bounds the leaf size of a formula from below by the number of distinct subfunctions on the blocks of a partition of the inputs. A rectangle-free function with many accepting inputs has nearly the maximal number of subfunctions on every block whose size exceeds log₂ (8 K) (Nechiporuk.two_pow_card_compl_le), while a formula with l leaves in a block has at most 2 · 16 ^ l subfunctions there (Nechiporuk.card_subfunctions_le). Summing over n / b disjoint blocks of size b gives leaf size Ω(n² / b); with a polynomial threshold K ≤ n ^ c the blocks have logarithmic size, and every formula over the full binary basis computing the function has Ω(n² / log n) leaves.

The main formula statements are sum_le_of_computes for an arbitrary family of disjoint blocks, leaves_lower_bound for consecutive blocks of a given size, and the asymptotic eventually_sq_le_leaves.

Because a rectangle-free function has 2 ^ (n - |Y|) / (8 K) subfunctions on each block Y, its binary logarithm is Θ(n) per block. Decomposing a full-binary-basis circuit c : Circuit Binary.signature n 1 at its shared gates (exists_sharedProgram_of_circuit) yields both:

• Global bounded-sharing lower bounds (sum_le_size_of_computes, size_lower_bound, size_lower_bound', eventually_sq_le_size, isLittleO_size_of_rectangleFree) when total shared fan-out sharedFanOut c is sublinear in n. The asymptotic ones follow from their active-block counterparts, since every block sees at most sharedFanOut c active shared fan-out.
• Active-block bounded-sharing lower bounds (SharedProgram.block_bound_active, SharedProgram.sum_le_of_computes_active, sum_le_size_of_computes_active, size_lower_bound_active, size_lower_bound_active', eventually_sq_le_size_active, eventually_sq_le_size_of_gateBlockSpan_le, isLittleO_size_of_rectangleFree_active), where a shared gate only contributes on blocks Y that intersect its syntactic input cone (activeSharedGateCount c Y, activeSharedFanOut c Y). Summing activeSharedFanOut c (Y i) over blocks weights each shared gate by its gateBlockSpan rather than the total number of blocks (sum_activeSharedFanOut). If the input cone of every shared gate meets at most span of the logarithmic blocks, so that each shared gate depends on O(span · log n) inputs, the total shared fan-out may be superlinear, up to O(n² / (span · log n)), while Ω(n² / log n) gates are still required (eventually_sq_le_size_of_gateBlockSpan_le). This locality restriction is essential: shared gates whose cones meet many blocks are charged on each of them.
• Span-threshold tradeoffs without a total shared-fan-out budget (size_lower_bound_highSpanSharedFanOut, eventually_sq_le_size_of_highSpanSharedFanOut_le, eventually_sq_le_span_mul_size_of_gateBlockSpan_le, eventually_sq_le_size_of_card_wireSupport_le). Every single-output binary circuit satisfies sharedFanOut c ≤ 2 * c.size + 1 (sharedFanOut_le_two_mul_size_add_one), so the fan-out of shared gates active on at most d blocks, charged on each of those blocks, is absorbed into a factor d on the circuit size: (n - b)(n - 2 b - 1) ≤ 5 n · s + (5 d + 4) b · (2 · c.size + 1), where s bounds only highSpanSharedFanOut c (block n b) d, the fan-out of shared gates active on more than d blocks. This trades the budget on sharedFanOut for a loss of the factor d; it does not remove the locality restriction, since high-span shared gates still need the budget s. When every shared gate has block-span at most d n (for instance, syntactic input support of size at most d n), highSpanSharedFanOut vanishes and n² ≤ 16 (5 · d n + 4) (c + 3) log₂ n · (2 · cir.size + 1), that is, Ω(n² / (d n · log n)) gates are required, with no hypothesis on sharedFanOut cir.

theorem Algebraic.Nechiporuk.block_bound {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) {Y : Finset (Fin n)} (hY : 8 * K ≤ 2 ^ Y.card) (F : Binary.Formula n) (hF : F.Computes f) : n - Y.card ≤ Nat.log 2 (16 * K) + 4 * Binary.Formula.leavesIn Y F

On a block of size at least log₂ (8 K), a formula computing a rectangle-free function with many accepting inputs has at least (n - |Y| - log₂ (16 K)) / 4 leaves in the block.

theorem Algebraic.Nechiporuk.sum_le_of_computes {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) {k : ℕ} (Y : Fin k → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin k) => Disjoint (Y i) (Y j)) (hY : ∀ (i : Fin k), 8 * K ≤ 2 ^ (Y i).card) (F : Binary.Formula n) (hF : F.Computes f) : ∑ i : Fin k, (n - (Y i).card) ≤ k * Nat.log 2 (16 * K) + 4 * F.leaves

Nechiporuk's bound for rectangle-free functions. Over k pairwise disjoint blocks, each of size at least log₂ (8 K), every formula computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs has leaf size at least (Σ_i (n - |Y_i|) - k · log₂ (16 K)) / 4.

Consecutive blocks of a fixed size

def Algebraic.Nechiporuk.block (n b : ℕ) (i : Fin (n / b)) : Finset (Fin n)

The i-th block of b consecutive coordinates, for i < n / b.

Equations

• Algebraic.Nechiporuk.block n b i = Finset.image (fun (j : Fin b) => ⟨b * ↑i + ↑j, ⋯⟩) Finset.univ

theorem Algebraic.Nechiporuk.card_block {n b : ℕ} (i : Fin (n / b)) : (block n b i).card = b

theorem Algebraic.Nechiporuk.block_disjoint {n b : ℕ} (hb : 0 < b) : Pairwise fun (i j : Fin (n / b)) => Disjoint (block n b i) (block n b j)

theorem Algebraic.Nechiporuk.leaves_lower_bound {n : ℕ} {f : Cslib.BooleanFunction n} {K b : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (F : Binary.Formula n) (hF : F.Computes f) : n / b * (n - b) ≤ n / b * Nat.log 2 (16 * K) + 4 * F.leaves

Nechiporuk's bound with consecutive blocks of size b. With 8 K ≤ 2 ^ b, every formula computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies (n / b) · (n - b) ≤ (n / b) · log₂ (16 K) + 4 · leaves.

theorem Algebraic.Nechiporuk.leaves_lower_bound' {n : ℕ} {f : Cslib.BooleanFunction n} {K b : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (F : Binary.Formula n) (hF : F.Computes f) : (n - b) * (n - 2 * b - 1) ≤ 4 * b * F.leaves

A cleaner consequence: (n - b) (n - 2 b - 1) ≤ 4 b · leaves.

The asymptotic statement

theorem Algebraic.Nechiporuk.natLog_le_logb (m : ℕ) : ↑(Nat.log 2 m) ≤ Real.logb 2 ↑m

The natural binary logarithm is at most the real one.

def Algebraic.Nechiporuk.nechiporukBlockSize (c n : ℕ) : ℕ

The logarithmic block size 3 + c * (Nat.log 2 n + 1) used in Nechiporuk's asymptotic lower bounds for K n-rectangle-free functions with K n ≤ n ^ c.

Equations

• Algebraic.Nechiporuk.nechiporukBlockSize c n = 3 + c * (Nat.log 2 n + 1)

theorem Algebraic.Nechiporuk.eventually_sq_le_leaves (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Binary.Formula n), F.Computes (f n) → ↑n ^ 2 ≤ 64 * (↑c + 3) * Real.logb 2 ↑n * ↑F.leaves

Formula size Ω(n² / log n) for rectangle-free families. For a family that is K n-rectangle-free with K n ≤ n ^ c and at least 2 ^ (n - 2) accepting inputs, every formula over the full binary basis computing f n has at least n² / (64 (c + 3) log₂ n) leaves, for all large n.

Programs and circuits with shared gates

theorem Algebraic.Nechiporuk.SharedProgram.block_bound_active {n : ℕ} {f : Cslib.BooleanFunction n} {K k : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) {Y : Finset (Fin n)} (hY : 8 * K ≤ 2 ^ Y.card) (P : SharedProgram n k) (hP : P.Computes f) : n - Y.card ≤ Nat.log 2 (16 * K) + P.activeShared Y + 4 * P.activeSharedLeaves Y + 4 * inputLeavesIn Y P

Active-block Nechiporuk bound for programs with shared gates. On a block Y of size at least log₂ (8 K), a program P computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies n - |Y| ≤ log₂ (16 K) + P.activeShared Y + 4 · P.activeSharedLeaves Y + 4 · P.inputLeavesIn Y.

theorem Algebraic.Nechiporuk.SharedProgram.block_bound {n : ℕ} {f : Cslib.BooleanFunction n} {K k : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) {Y : Finset (Fin n)} (hY : 8 * K ≤ 2 ^ Y.card) (P : SharedProgram n k) (hP : P.Computes f) : n - Y.card ≤ Nat.log 2 (16 * K) + k + 4 * P.sharedLeaves n + 4 * inputLeavesIn Y P

On a block of size at least log₂ (8 K), a program with k shared gates computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies n - |Y| ≤ log₂ (16 K) + k + 4 · sharedLeaves + 4 · inputLeavesIn Y.

theorem Algebraic.Nechiporuk.SharedProgram.sum_le_of_computes_active {n : ℕ} {f : Cslib.BooleanFunction n} {K m k : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (Y : Fin m → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin m) => Disjoint (Y i) (Y j)) (hY : ∀ (i : Fin m), 8 * K ≤ 2 ^ (Y i).card) (P : SharedProgram n k) (hP : P.Computes f) : ∑ i : Fin m, (n - (Y i).card) ≤ m * Nat.log 2 (16 * K) + ∑ i : Fin m, (P.activeShared (Y i) + 4 * P.activeSharedLeaves (Y i)) + 4 * P.inputLeaves n

Active-block Nechiporuk sum bound for programs with shared gates. Over m pairwise disjoint blocks of size at least log₂ (8 K), every program P computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies `∑ i, (n - |Y i|) ≤ m · log₂ (16 K) + ∑ i, (P.activeShared (Y i) + 4 · P.activeSharedLeaves (Y i))

• 4 · P.inputLeaves n`.

theorem Algebraic.Nechiporuk.SharedProgram.sum_le_of_computes {n : ℕ} {f : Cslib.BooleanFunction n} {K m k : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (Y : Fin m → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin m) => Disjoint (Y i) (Y j)) (hY : ∀ (i : Fin m), 8 * K ≤ 2 ^ (Y i).card) (P : SharedProgram n k) (hP : P.Computes f) : ∑ i : Fin m, (n - (Y i).card) ≤ m * (Nat.log 2 (16 * K) + k + 4 * P.sharedLeaves n) + 4 * P.inputLeaves n

Nechiporuk's bound for programs with shared gates. Over m pairwise disjoint blocks, each of size at least log₂ (8 K), every program with k shared gates computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies ∑ i, (n - |Y i|) ≤ m · (log₂ (16 K) + k + 4 · sharedLeaves) + 4 · inputLeaves.

theorem Algebraic.Nechiporuk.sum_le_size_of_computes_active {n : ℕ} {f : Cslib.BooleanFunction n} {K m : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (Y : Fin m → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin m) => Disjoint (Y i) (Y j)) (hY : ∀ (i : Fin m), 8 * K ≤ 2 ^ (Y i).card) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : ∑ i : Fin m, (n - (Y i).card) ≤ m * Nat.log 2 (16 * K) + ∑ i : Fin m, (activeSharedGateCount c (Y i) + 4 * activeSharedFanOut c (Y i)) + 4 * (c.size + KW.sharedGateCount c + 1)

Active-block Nechiporuk bound for full-binary-basis circuits. Over m pairwise disjoint blocks of size at least log₂ (8 K), every single-output circuit c over Binary.signature computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies ∑ i, (n - |Y i|) ≤ m · log₂ (16 K) + ∑ i, (activeSharedGateCount c (Y i) + 4 · activeSharedFanOut c (Y i)) + 4 · (c.size + KW.sharedGateCount c + 1).

theorem Algebraic.Nechiporuk.sum_le_size_of_computes {n : ℕ} {f : Cslib.BooleanFunction n} {K m k s : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (Y : Fin m → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin m) => Disjoint (Y i) (Y j)) (hY : ∀ (i : Fin m), 8 * K ≤ 2 ^ (Y i).card) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (hk : KW.sharedGateCount c ≤ k) (hs : sharedFanOut c ≤ s) : ∑ i : Fin m, (n - (Y i).card) ≤ m * (Nat.log 2 (16 * K) + k + 4 * s) + 4 * (c.size + k + 1)

Nechiporuk's bound for full-binary-basis circuits with bounded sharing. Over m pairwise disjoint blocks, each of size at least log₂ (8 K), every single-output circuit c over Binary.signature computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs and with KW.sharedGateCount c ≤ k and sharedFanOut c ≤ s satisfies ∑ i, (n - |Y i|) ≤ m · (log₂ (16 K) + k + 4 s) + 4 · (c.size + k + 1).

theorem Algebraic.Nechiporuk.size_lower_bound_active {n : ℕ} {f : Cslib.BooleanFunction n} {K b : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : n / b * (n - b) ≤ n / b * Nat.log 2 (16 * K) + ∑ i : Fin (n / b), (activeSharedGateCount c (block n b i) + 4 * activeSharedFanOut c (block n b i)) + 4 * (c.size + KW.sharedGateCount c + 1)

Active-block Nechiporuk circuit bound with consecutive blocks of size b. With 8 K ≤ 2 ^ b, every single-output circuit c over Binary.signature computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies (n / b) · (n - b) ≤ (n / b) · log₂ (16 K) + ∑ i, (activeSharedGateCount c (block n b i) + 4 · activeSharedFanOut c (block n b i)) + 4 · (c.size + KW.sharedGateCount c + 1).

theorem Algebraic.Nechiporuk.size_lower_bound_active' {n : ℕ} {f : Cslib.BooleanFunction n} {K b : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : (n - b) * (n - 2 * b - 1) ≤ 5 * b * ∑ i : Fin (n / b), activeSharedFanOut c (block n b i) + 4 * b * (c.size + KW.sharedGateCount c + 1)

A multiplicative consequence of size_lower_bound_active: (n - b) · (n - 2 b - 1) ≤ 5 b · (∑ i, activeSharedFanOut c (block n b i)) + 4 b · (c.size + KW.sharedGateCount c + 1).

theorem Algebraic.Nechiporuk.size_lower_bound_highSpanSharedFanOut {n : ℕ} {f : Cslib.BooleanFunction n} {K b d s : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (hhigh : highSpanSharedFanOut c (block n b) d ≤ s) : (n - b) * (n - 2 * b - 1) ≤ 5 * n * s + (5 * d + 4) * b * (2 * c.size + 1)

High-span shared fan-out circuit bound with consecutive blocks of size b. Absorbing shared gates of block-span at most d into 2 * c.size + 1 via sharedFanOut_le_two_mul_size_add_one and sum_activeSharedFanOut_le_add_highSpanSharedFanOut yields (n - b) · (n - 2 b - 1) ≤ 5 n · s + (5 d + 4) b · (2 · c.size + 1) whenever highSpanSharedFanOut c (block n b) d ≤ s, with no bound on total sharedFanOut c.

theorem Algebraic.Nechiporuk.size_lower_bound {n : ℕ} {f : Cslib.BooleanFunction n} {K b k s : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (hk : KW.sharedGateCount c ≤ k) (hs : sharedFanOut c ≤ s) : n / b * (n - b) ≤ n / b * (Nat.log 2 (16 * K) + k + 4 * s) + 4 * (c.size + k + 1)

Nechiporuk's circuit bound with consecutive blocks of size b. With 8 K ≤ 2 ^ b, every single-output circuit c over Binary.signature computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs and with KW.sharedGateCount c ≤ k and sharedFanOut c ≤ s satisfies (n / b) · (n - b) ≤ (n / b) · (log₂ (16 K) + k + 4 s) + 4 · (c.size + k + 1).

theorem Algebraic.Nechiporuk.size_lower_bound' {n : ℕ} {f : Cslib.BooleanFunction n} {K b k s : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (c : Circuit Binary.signature n 1) (hc : c.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (hk : KW.sharedGateCount c ≤ k) (hs : sharedFanOut c ≤ s) : (n - b) * (n - 2 * b - 1 - k - 4 * s) ≤ 4 * b * (c.size + k + 1)

A multiplicative consequence of size_lower_bound: (n - b) · (n - 2 b - 1 - k - 4 s) ≤ 4 b · (c.size + k + 1).

theorem Algebraic.Nechiporuk.eventually_sq_le_size_active (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → 20 * nechiporukBlockSize c n * ∑ i : Fin (n / nechiporukBlockSize c n), activeSharedFanOut cir (block n (nechiporukBlockSize c n) i) ≤ n * n → ↑n ^ 2 ≤ 64 * (↑c + 3) * Real.logb 2 ↑n * (2 * ↑cir.size + 1)

Active-block Ω(n² / log n) circuit lower bound for rectangle-free families. For a family that is K n-rectangle-free with K n ≤ n ^ c and at least 2 ^ (n - 2) accepting inputs, every full-binary-basis circuit cir computing f n whose active shared fan-out summed across the n / b logarithmic blocks (b = nechiporukBlockSize c n) satisfies 20 b · (∑ i, activeSharedFanOut cir (block n b i)) ≤ n² (an O(n² / log n) total active shared fan-out budget) obeys n² ≤ 64 (c + 3) log₂ n · (2 · cir.size + 1) for all large n.

theorem Algebraic.Nechiporuk.eventually_sq_le_size_of_gateBlockSpan_le (f : (n : ℕ) → Cslib.BooleanFunction n) (K span s : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (hspan : ∀ᶠ (n : ℕ) in Filter.atTop, 40 * (c + 3) * Nat.log 2 n * span n * s n ≤ n * n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → sharedFanOut cir ≤ s n → (∀ (g : Fin cir.size), 2 ≤ KW.gateFanOut cir g → gateBlockSpan (block n (nechiporukBlockSize c n)) cir.program g ≤ span n) → ↑n ^ 2 ≤ 64 * (↑c + 3) * Real.logb 2 ↑n * (2 * ↑cir.size + 1)

Bounded-block-span Ω(n² / log n) circuit lower bound. Let b = nechiporukBlockSize c n = 3 + c (⌊log₂ n⌋ + 1) be the logarithmic Nechiporuk block size and suppose every shared gate of cir is active on at most span n of the n / b consecutive blocks block n b i. Then the syntactic input cone of each shared gate lies inside at most span n blocks together with the fewer than b trailing coordinates outside every block, so every shared gate depends on fewer than (span n + 1) · b = O(span n · log n) inputs. Under this locality restriction, if sharedFanOut cir ≤ s n and 40 (c + 3) log₂ n · span n · s n ≤ n², then n² ≤ 64 (c + 3) log₂ n · (2 · cir.size + 1) for all large n.

For span n = O(1) the total shared fan-out s n may thus be superlinear, up to Θ(n² / log n), but only for shared gates of logarithmic input-cone size; the hypothesis excludes shared gates whose cones meet many blocks, and the theorem says nothing about circuits with such gates beyond eventually_sq_le_size_active.

theorem Algebraic.Nechiporuk.eventually_sq_le_size_of_highSpanSharedFanOut_le (f : (n : ℕ) → Cslib.BooleanFunction n) (K d s : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (hs : ∀ᶠ (n : ℕ) in Filter.atTop, 20 * s n ≤ n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → highSpanSharedFanOut cir (block n (nechiporukBlockSize c n)) (d n) ≤ s n → ↑n ^ 2 ≤ 16 * (5 * ↑(d n) + 4) * (↑c + 3) * Real.logb 2 ↑n * (2 * ↑cir.size + 1)

Span-threshold tradeoff without a total shared-fan-out budget. For a K n-rectangle-free family with K n ≤ n ^ c and at least 2 ^ (n - 2) accepting inputs, if the fan-out of shared gates active on strictly more than d n logarithmic blocks is at most s n with 20 · s n ≤ n eventually, then every full-binary-basis circuit cir computing f n satisfies n² ≤ 16 (5 · d n + 4) (c + 3) log₂ n · (2 · cir.size + 1) for all large n, so cir has Ω(n² / ((d n + 1) log n)) gates. Shared gates of block-span at most d n need no fan-out budget; their fan-out is absorbed into the factor d n via sharedFanOut_le_two_mul_size_add_one.

theorem Algebraic.Nechiporuk.eventually_sq_le_span_mul_size_of_gateBlockSpan_le (f : (n : ℕ) → Cslib.BooleanFunction n) (K d : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (∀ (g : Fin cir.size), 2 ≤ KW.gateFanOut cir g → gateBlockSpan (block n (nechiporukBlockSize c n)) cir.program g ≤ d n) → ↑n ^ 2 ≤ 16 * (5 * ↑(d n) + 4) * (↑c + 3) * Real.logb 2 ↑n * (2 * ↑cir.size + 1)

Bounded-block-span circuit lower bound without a total shared-fan-out budget. If every shared gate of cir is active on at most d n of the logarithmic Nechiporuk blocks, then n² ≤ 16 (5 · d n + 4) (c + 3) log₂ n · (2 · cir.size + 1) for all large n, that is, Ω(n² / ((d n + 1) log n)) gates, with no bound on sharedFanOut cir. Compared with eventually_sq_le_size_of_gateBlockSpan_le, the budget on sharedFanOut is traded for the factor d n.

theorem Algebraic.Nechiporuk.eventually_sq_le_size_of_card_wireSupport_le (f : (n : ℕ) → Cslib.BooleanFunction n) (K d : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (∀ (g : Fin cir.size), 2 ≤ KW.gateFanOut cir g → (cir.program.wireSupport (Wire.gate g)).card ≤ d n) → ↑n ^ 2 ≤ 16 * (5 * ↑(d n) + 4) * (↑c + 3) * Real.logb 2 ↑n * (2 * ↑cir.size + 1)

Bounded-input-support circuit lower bound without a total shared-fan-out budget. If the syntactic input support cir.program.wireSupport (Wire.gate g) of every shared gate g has cardinality at most d n, then n² ≤ 16 (5 · d n + 4) (c + 3) log₂ n · (2 · cir.size + 1) for all large n, that is, Ω(n² / ((d n + 1) log n)) gates, with no bound on sharedFanOut cir.

theorem Algebraic.Nechiporuk.eventually_mul_le_size_of_rectangleFree_active (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (M : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → 20 * nechiporukBlockSize c n * ∑ i : Fin (n / nechiporukBlockSize c n), activeSharedFanOut cir (block n (nechiporukBlockSize c n) i) ≤ n * n → M * n ≤ cir.size

For any multiplier M, a rectangle-free family requires at least M · n gates in any full-binary-basis circuit whose active shared fan-out on the logarithmic blocks satisfies 20 b · (∑ i, activeSharedFanOut cir (block n b i)) ≤ n².

theorem Algebraic.Nechiporuk.isLittleO_size_of_rectangleFree_active (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (cir : (n : ℕ) → Circuit Binary.signature n 1) (hcir : ∀ (n : ℕ), (cir n).ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) (hact : ∀ᶠ (n : ℕ) in Filter.atTop, 20 * nechiporukBlockSize c n * ∑ i : Fin (n / nechiporukBlockSize c n), activeSharedFanOut (cir n) (block n (nechiporukBlockSize c n) i) ≤ n * n) : (fun (n : ℕ) => ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑(cir n).size

Superlinear circuit size for rectangle-free families under O(n² / log n) active-block shared fan-out. If cir n is a family of circuits over Binary.signature computing a K n-rectangle-free family f n (K n ≤ n ^ c, 2 ^ (n - 2) ≤ |(accepting (f n))|) whose active shared fan-out on the logarithmic blocks satisfies 20 b · (∑ i, activeSharedFanOut (cir n) (block n b i)) ≤ n² eventually, then (cir n).size grows faster than n.

theorem Algebraic.Nechiporuk.eventually_sq_le_size (f : (n : ℕ) → Cslib.BooleanFunction n) (K s : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (hs : ∀ᶠ (n : ℕ) in Filter.atTop, 20 * s n ≤ n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → sharedFanOut cir ≤ s n → ↑n ^ 2 ≤ 128 * (↑c + 3) * Real.logb 2 ↑n * (↑cir.size + ↑(s n) + 1)

Circuit size Ω(n² / log n) for rectangle-free families with bounded shared fan-out. For a family that is K n-rectangle-free with K n ≤ n ^ c and at least 2 ^ (n - 2) accepting inputs, every full-binary-basis circuit cir computing f n with sharedFanOut cir ≤ s n (where 20 · s n ≤ n eventually) satisfies n² ≤ 128 (c + 3) log₂ n · (cir.size + s n + 1) for all large n. Only the reuse of computed gate outputs is bounded: the size is unrestricted and inputs may be read any number of times, so s = 0 is the formula case, while general circuits (shared fan-out Θ(size)) are not covered.

theorem Algebraic.Nechiporuk.eventually_mul_le_size_of_rectangleFree (f : (n : ℕ) → Cslib.BooleanFunction n) (K s : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (hs : ∀ᶠ (n : ℕ) in Filter.atTop, 20 * s n ≤ n) (M : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (cir : Circuit Binary.signature n 1), (cir.ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → sharedFanOut cir ≤ s n → M * n ≤ cir.size

For any multiplier M, a rectangle-free family with 20 · s n ≤ n eventually requires at least M · n gates in any full-binary-basis circuit with sharedFanOut ≤ s n.

theorem Algebraic.Nechiporuk.isLittleO_size_of_rectangleFree (f : (n : ℕ) → Cslib.BooleanFunction n) (K s : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) (hs : (fun (n : ℕ) => ↑(s n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (cir : (n : ℕ) → Circuit Binary.signature n 1) (hcir : ∀ (n : ℕ), (cir n).ComputesWith Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) (hfan : ∀ (n : ℕ), sharedFanOut (cir n) ≤ s n) : (fun (n : ℕ) => ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑(cir n).size

Rectangle-free families need superlinear full-binary-basis circuits when sharedFanOut = o(n). If s n = o(n) and cir n is a family of circuits over Binary.signature computing a K n-rectangle-free family f n (K n ≤ n ^ c, 2 ^ (n - 2) ≤ |(accepting (f n))|) with sharedFanOut (cir n) ≤ s n, then (cir n).size grows faster than n.