Splits aligned with gates of support at most two

A program whose gates each read at most two inputs defines the support graph on the inputs: two inputs are adjacent when some gate reads both. Every gate with nonempty support lies inside a single connected component. A component with v inputs is connected, so it contains at least v - 1 edges; distinct edges come from distinct gates of support exactly two inside the component, so the component carries at least v - 1 input-reading gates. Summing over the components, the number of components with exactly v - 1 gates ("tree components") is at least n - |inputGates|. Taking L tree components for the side U of a split gives |U| = (number of gates with nonempty support inside U) + L, and no gate straddles the split.

The main result is exists_split_of_support_card_le_two_internal.

theorem Algebraic.Threshold.Program.inputWeight_ne_zero_iff {n s : ℕ} (C : Program n s) (j : Fin s) : C.inputWeight j ≠ 0 ↔ C.support j ≠ ∅

def Algebraic.Threshold.Program.supportGraph {n s : ℕ} (C : Program n s) : SimpleGraph (Fin n)

The support graph of a program: two inputs are adjacent when some gate reads both.

Equations

• C.supportGraph = { Adj := fun (u v : Fin n) => u ≠ v ∧ ∃ (j : Fin s), u ∈ C.support j ∧ v ∈ C.support j, symm := ⋯, loopless := ⋯ }

noncomputable def Algebraic.Threshold.Program.componentInputs {n s : ℕ} (C : Program n s) (c : C.supportGraph.ConnectedComponent) : Finset (Fin n)

The inputs of a connected component of the support graph, as a finset.

Equations

• C.componentInputs c = {u : Fin n | C.supportGraph.connectedComponentMk u = c}

noncomputable def Algebraic.Threshold.Program.componentGates {n s : ℕ} (C : Program n s) (c : C.supportGraph.ConnectedComponent) : Finset (Fin s)

The gates with nonempty support inside a connected component of the support graph.

Equations

• C.componentGates c = {j : Fin s | C.support j ≠ ∅ ∧ C.support j ⊆ C.componentInputs c}

theorem Algebraic.Threshold.Program.mem_componentInputs {n s : ℕ} (C : Program n s) {c : C.supportGraph.ConnectedComponent} {u : Fin n} : u ∈ C.componentInputs c ↔ C.supportGraph.connectedComponentMk u = c

theorem Algebraic.Threshold.Program.coe_componentInputs {n s : ℕ} (C : Program n s) (c : C.supportGraph.ConnectedComponent) : ↑(C.componentInputs c) = c.supp

theorem Algebraic.Threshold.Program.mem_componentGates {n s : ℕ} (C : Program n s) {c : C.supportGraph.ConnectedComponent} {j : Fin s} : j ∈ C.componentGates c ↔ C.support j ≠ ∅ ∧ C.support j ⊆ C.componentInputs c

theorem Algebraic.Threshold.Program.support_subset_componentInputs {n s : ℕ} (C : Program n s) {j : Fin s} {u : Fin n} (hu : u ∈ C.support j) : C.support j ⊆ C.componentInputs (C.supportGraph.connectedComponentMk u)

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

theorem Algebraic.Threshold.Program.sum_card_componentInputs {n s : ℕ} (C : Program n s) : ∑ c : C.supportGraph.ConnectedComponent, (C.componentInputs c).card = n

(F1) The components partition the inputs.

theorem Algebraic.Threshold.Program.pairwiseDisjoint_componentInputs {n s : ℕ} (C : Program n s) : (↑Finset.univ).PairwiseDisjoint C.componentInputs

theorem Algebraic.Threshold.Program.pairwiseDisjoint_componentGates {n s : ℕ} (C : Program n s) : (↑Finset.univ).PairwiseDisjoint C.componentGates

theorem Algebraic.Threshold.Program.inputGates_eq_biUnion_componentGates {n s : ℕ} (C : Program n s) : C.inputGates = Finset.univ.biUnion C.componentGates

(F2) The input-reading gates are partitioned by the components.

theorem Algebraic.Threshold.Program.sum_card_componentGates {n s : ℕ} (C : Program n s) : ∑ c : C.supportGraph.ConnectedComponent, (C.componentGates c).card = C.inputGates.card

theorem Algebraic.Threshold.Program.exists_gate_of_edge {n s : ℕ} (C : Program n s) (h2 : ∀ (j : Fin s), (C.support j).card ≤ 2) (c : C.supportGraph.ConnectedComponent) (e : Sym2 ↑c.supp) (he : e ∈ c.toSimpleGraph.edgeSet) : ∃ j ∈ C.componentGates c, ∀ (u : Fin n), u ∈ C.support j ↔ u ∈ Sym2.map Subtype.val e

When every gate reads at most two inputs, every edge of a component is the support of a gate of the component.

theorem Algebraic.Threshold.Program.card_componentInputs_le {n s : ℕ} (C : Program n s) (h2 : ∀ (j : Fin s), (C.support j).card ≤ 2) (c : C.supportGraph.ConnectedComponent) : (C.componentInputs c).card ≤ (C.componentGates c).card + 1

(F3) A component with v inputs carries at least v - 1 gates: it is connected, so it has at least v - 1 edges, and distinct edges come from distinct gates.

theorem Algebraic.Threshold.Program.exists_split_of_support_card_le_two_internal {n s : ℕ} (C : Program n s) (h2 : ∀ (j : Fin s), (C.support j).card ≤ 2) (L : ℕ) (hL : L + C.inputGates.card ≤ n) : ∃ (U : Finset (Fin n)), (∀ (j : Fin s), C.support j ⊆ U ∨ C.support j ⊆ Uᶜ) ∧ U.card = {j : Fin s | C.support j ⊆ U ∧ C.support j ≠ ∅}.card + L

A program whose gates each read at most two inputs admits, for every L ≤ n - |inputGates|, a split U of the inputs that no gate straddles, with |U| exceeding the number of gates reading inputs inside U by exactly L.