Input-support components, fan-in-two splits, and block-excess bounds

This module proves two structural lower bounds for weighted threshold programs from the coordinate-split and median-cut rectangle lemmas in Cut.lean:

• C5 (lt_of_inputSupport_card_le_two, circuit_lt_of_inputSupport_card_le_two): when every gate has aggregated input support of size at most 2, the input-support graph on Fin n has at least n - |inputGates p| connected components that are trees (|V| = |E| + 1). Grouping L such components into U produces a coordinate split crossed by no gate with excess L, yielding n < (inputGates p).card + 2 * L for any two-sided K-rectangle-free function with K ≤ 2 ^ L.
• C6 (lt_of_blocks, circuit_lt_of_blocks): given a set F of freely-read inputs and a pairwise disjoint block partition 𝓑 of Fᶜ such that every gate's residual support outside F lies in a single block of 𝓑 and every block has excess |b| - e_b ≤ M, a subset-sum split (exists_subset_sum_ge) and exists_rectangle_of_cut_with_fixed yield n < F.card + (inputGates p).card + M + 2 * k.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.supportGraph: the graph on Fin n where two inputs are adjacent when some gate has nonzero aggregated weight on both.
• Cslib.Circuits.Boolean.WeightedThreshold.componentInputs, Cslib.Circuits.Boolean.WeightedThreshold.componentGates: the inputs and active gates in a connected component of supportGraph p.
• Cslib.Circuits.Boolean.WeightedThreshold.residualGates: gates whose residual input support outside F is nonempty and contained in a block b.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.sum_card_componentInputs, Cslib.Circuits.Boolean.WeightedThreshold.sum_card_componentGates, Cslib.Circuits.Boolean.WeightedThreshold.card_componentInputs_le: component counting for fan-in-two input supports.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_split_of_inputSupport_card_le_two: unsplit coordinate cut with prescribed excess L.
• Cslib.Circuits.Boolean.WeightedThreshold.lt_of_inputSupport_card_le_two, Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_inputSupport_card_le_two: the C5 fan-in-two component lower bound.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_subset_sum_ge: balanced subset-sum partition for bounded weights.
• Cslib.Circuits.Boolean.WeightedThreshold.lt_of_blocks, Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_blocks: the C6 block-excess lower bound.

References

• S. Schlesinger, Algebraic circuit formalizations in Complexitylib, Threshold/Internal/Components, SplitBound, and Excess

Input-support graph and connected components

def Cslib.Circuits.Boolean.WeightedThreshold.supportGraph {n g : ℕ} (p : Program signature n g) : SimpleGraph (Fin n)

The input-support graph of a weighted threshold program: two inputs are adjacent when some gate has nonzero aggregated weight on both.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.componentInputs {n g : ℕ} (p : Program signature n g) (c : (supportGraph p).ConnectedComponent) : Finset (Fin n)

The inputs belonging to a connected component of supportGraph p.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.componentGates {n g : ℕ} (p : Program signature n g) (c : (supportGraph p).ConnectedComponent) : Finset (Fin g)

The gates with nonempty aggregated input support inside a connected component of supportGraph p.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_componentInputs {n g : ℕ} (p : Program signature n g) {c : (supportGraph p).ConnectedComponent} {u : Fin n} : u ∈ componentInputs p c ↔ (supportGraph p).connectedComponentMk u = c

theorem Cslib.Circuits.Boolean.WeightedThreshold.coe_componentInputs {n g : ℕ} (p : Program signature n g) (c : (supportGraph p).ConnectedComponent) : ↑(componentInputs p c) = c.supp

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_componentGates {n g : ℕ} (p : Program signature n g) {c : (supportGraph p).ConnectedComponent} {j : Fin g} : j ∈ componentGates p c ↔ inputSupport p j ≠ ∅ ∧ inputSupport p j ⊆ componentInputs p c

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputSupport_subset_componentInputs {n g : ℕ} (p : Program signature n g) {j : Fin g} {u : Fin n} (hu : u ∈ inputSupport p j) : inputSupport p j ⊆ componentInputs p ((supportGraph p).connectedComponentMk u)

The input support of a gate lies in the connected component of any of its inputs.

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_card_componentInputs {n g : ℕ} (p : Program signature n g) : ∑ c : (supportGraph p).ConnectedComponent, (componentInputs p c).card = n

The connected components of supportGraph p partition the n inputs.

theorem Cslib.Circuits.Boolean.WeightedThreshold.pairwiseDisjoint_componentInputs {n g : ℕ} (p : Program signature n g) : (↑Finset.univ).PairwiseDisjoint (componentInputs p)

theorem Cslib.Circuits.Boolean.WeightedThreshold.pairwiseDisjoint_componentGates {n g : ℕ} (p : Program signature n g) : (↑Finset.univ).PairwiseDisjoint (componentGates p)

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputGates_eq_biUnion_componentGates {n g : ℕ} (p : Program signature n g) : inputGates p = Finset.univ.biUnion (componentGates p)

The input-reading gates are partitioned by the connected components of supportGraph p.

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_card_componentGates {n g : ℕ} (p : Program signature n g) : ∑ c : (supportGraph p).ConnectedComponent, (componentGates p c).card = (inputGates p).card

The sizes of componentGates p c sum to (inputGates p).card.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_componentInputs_le {n g : ℕ} (p : Program signature n g) (h2 : ∀ (j : Fin g), (inputSupport p j).card ≤ 2) (c : (supportGraph p).ConnectedComponent) : (componentInputs p c).card ≤ (componentGates p c).card + 1

When every gate has aggregated input support of size at most 2, every connected component of supportGraph p has at most one more input than active gates.

C5: Fan-in-two component split and lower bound

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_split_of_inputSupport_card_le_two {n g : ℕ} (p : Program signature n g) (h2 : ∀ (j : Fin g), (inputSupport p j).card ≤ 2) (L : ℕ) (hL : L + (inputGates p).card ≤ n) : ∃ (U : Finset (Fin n)), (∀ (j : Fin g), inputSupport p j ⊆ U ∨ inputSupport p j ⊆ Uᶜ) ∧ U.card = {j : Fin g | inputSupport p j ⊆ U ∧ inputSupport p j ≠ ∅}.card + L

When every gate of p has aggregated input support of size at most 2, for every L ≤ n - (inputGates p).card there is a coordinate split U that no gate crosses and whose size exceeds the number of active gates on U by L.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lt_of_inputSupport_card_le_two {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (h2 : ∀ (j : Fin g), (inputSupport p j).card ≤ 2) {L : ℕ} (hK : K ≤ 2 ^ L) : n < (inputGates p).card + 2 * L

C5: component bound for input fan-in two. If every gate of p has aggregated input support of size at most 2 and p computes a two-sided K-rectangle-free function f through readout with K ≤ 2 ^ L, then n < (inputGates p).card + 2 * L.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_inputSupport_card_le_two {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (h2 : ∀ (j : Fin c.size), (inputSupport c.program j).card ≤ 2) {L : ℕ} (hK : K ≤ 2 ^ L) : n < (inputGates c.program).card + 2 * L

The C5 fan-in-two component bound for a single-output weighted threshold circuit whose output selects a gate.

C6: Block-excess restriction and lower bound

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_subset_sum_ge {ι : Type u_1} [DecidableEq ι] (𝓑 : Finset ι) (φ : ι → ℕ) (M k : ℕ) (hφ : ∀ b ∈ 𝓑, φ b ≤ M) (htot : 2 * k + M ≤ ∑ b ∈ 𝓑, φ b) : ∃ 𝒢 ⊆ 𝓑, k ≤ ∑ b ∈ 𝒢, φ b ∧ k ≤ ∑ b ∈ 𝓑 \ 𝒢, φ b

Subset sum. Items of weight at most M with total weight at least 2 * k + M can be partitioned into 𝒢 ⊆ 𝓑 and 𝓑 \ 𝒢 each of weight at least k.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.residualGates {n g : ℕ} (p : Program signature n g) (F b : Finset (Fin n)) : Finset (Fin g)

The gates of p whose residual input support outside F is nonempty and contained in b.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_residualGates {n g : ℕ} (p : Program signature n g) (F b : Finset (Fin n)) (j : Fin g) : j ∈ residualGates p F b ↔ ¬inputSupport p j ⊆ F ∧ inputSupport p j \ F ⊆ b

theorem Cslib.Circuits.Boolean.WeightedThreshold.residualGates_subset_inputGates {n g : ℕ} (p : Program signature n g) (F b : Finset (Fin n)) : residualGates p F b ⊆ inputGates p

theorem Cslib.Circuits.Boolean.WeightedThreshold.disjoint_residualGates {n g : ℕ} (p : Program signature n g) (F : Finset (Fin n)) {b b' : Finset (Fin n)} (hbb' : Disjoint b b') : Disjoint (residualGates p F b) (residualGates p F b')

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_card_residualGates_le {n g : ℕ} (p : Program signature n g) (F : Finset (Fin n)) (𝓑 : Finset (Finset (Fin n))) (hdisj : (↑𝓑).PairwiseDisjoint id) : ∑ b ∈ 𝓑, (residualGates p F b).card ≤ (inputGates p).card

Over pairwise disjoint blocks 𝓑, the total number of residual gates is at most (inputGates p).card.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lt_of_blocks {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (F : Finset (Fin n)) (𝓑 : Finset (Finset (Fin n))) (hdisj : (↑𝓑).PairwiseDisjoint id) (hcover : ∀ i ∉ F, ∃ b ∈ 𝓑, i ∈ b) (hF : ∀ b ∈ 𝓑, Disjoint b F) (hblocks : ∀ (j : Fin g), inputSupport p j ⊆ F ∨ ∃ b ∈ 𝓑, inputSupport p j \ F ⊆ b) (M : ℕ) (hM : ∀ b ∈ 𝓑, b.card ≤ (residualGates p F b).card + M) {k : ℕ} (hK : K ≤ 2 ^ k) : n < F.card + (inputGates p).card + M + 2 * k

C6: the block-excess lower bound. Let F be a set of inputs and 𝓑 a family of pairwise disjoint blocks covering the inputs outside F, such that every gate reads inputs from F only or has its residual support outside F inside a single block of 𝓑. If every block b has excess |b| - e_b ≤ M, where e_b = (residualGates p F b).card, and p computes a two-sided K-rectangle-free function f through readout with K ≤ 2 ^ k, then n < F.card + (inputGates p).card + M + 2 * k.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_blocks {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (F : Finset (Fin n)) (𝓑 : Finset (Finset (Fin n))) (hdisj : (↑𝓑).PairwiseDisjoint id) (hcover : ∀ i ∉ F, ∃ b ∈ 𝓑, i ∈ b) (hF : ∀ b ∈ 𝓑, Disjoint b F) (hblocks : ∀ (j : Fin c.size), inputSupport c.program j ⊆ F ∨ ∃ b ∈ 𝓑, inputSupport c.program j \ F ⊆ b) (M : ℕ) (hM : ∀ b ∈ 𝓑, b.card ≤ (residualGates c.program F b).card + M) {k : ℕ} (hK : K ≤ 2 ^ k) : n < F.card + (inputGates c.program).card + M + 2 * k

The C6 block-excess bound for a single-output weighted threshold circuit whose output selects a gate.