Incidence layouts and support deficits

The incidence multigraph of a finite indexed support family has one vertex for each input and each support, and one edge for each support membership. A support meeting both sides of an input cut contributes an edge to every incidence-layout frontier inducing that cut.

For supports of size at most three and input incidence at most T, the existing connected multigraph layout bound combines with the support-deficit obstruction to give 2 * N < 3 * Q + max 3 T * log₂ (N + Q) + 2 * k + 1.

Main definitions

• Cslib.Circuits.Frontier.Incidence.graph: the incidence multigraph of a support family.
• Cslib.Circuits.Frontier.Incidence.inputPrefix: the input vertices in a layout prefix.

Main results

• Cslib.Circuits.Frontier.Incidence.maxDegreeLE: support and input-incidence degree bounds.
• Cslib.Circuits.Frontier.Incidence.card_crossing_le_width: crossing supports are bounded by incidence-layout width.
• Cslib.Circuits.Frontier.Incidence.two_mul_card_lt: the connected support-family bound.

def Cslib.Circuits.Frontier.Incidence.graph {ι : Type u_1} {κ : Type u_2} (S : κ → Finset ι) : Multigraph (ι ⊕ κ) { p : ι × κ // p.1 ∈ S p.2 }

The bipartite incidence multigraph, with an edge from each input to each support containing it. Distinct support indices remain distinct vertices, including repeated or empty supports.

theorem Cslib.Circuits.Frontier.Incidence.loopless {ι : Type u_1} {κ : Type u_2} (S : κ → Finset ι) : (graph S).Loopless

Every incidence edge joins the two different vertex classes.

@[simp]

theorem Cslib.Circuits.Frontier.Incidence.adj_inl_inr {ι : Type u_1} {κ : Type u_2} (S : κ → Finset ι) (i : ι) (j : κ) : (graph S).toSimpleGraph.Adj (Sum.inl i) (Sum.inr j) ↔ i ∈ S j

Adjacency between an input vertex and a support vertex is support membership.

@[simp]

theorem Cslib.Circuits.Frontier.Incidence.not_adj_inl_inl {ι : Type u_1} {κ : Type u_2} (S : κ → Finset ι) (i i' : ι) : ¬(graph S).toSimpleGraph.Adj (Sum.inl i) (Sum.inl i')

Two input vertices are never adjacent in an incidence graph.

@[simp]

theorem Cslib.Circuits.Frontier.Incidence.not_adj_inr_inr {ι : Type u_1} {κ : Type u_2} (S : κ → Finset ι) (j j' : κ) : ¬(graph S).toSimpleGraph.Adj (Sum.inr j) (Sum.inr j')

Two support vertices are never adjacent in an incidence graph.

theorem Cslib.Circuits.Frontier.Incidence.card_edges {ι : Type u_1} {κ : Type u_2} [Fintype κ] (S : κ → Finset ι) : Nat.card { p : ι × κ // p.1 ∈ S p.2 } = ∑ j : κ, (S j).card

The edge count of an incidence multigraph is the sum of the support sizes.

theorem Cslib.Circuits.Frontier.Incidence.ncard_incidence_inl {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [Fintype κ] (S : κ → Finset ι) (i : ι) : ((graph S).incidenceSet (Sum.inl i)).ncard = {j : κ | i ∈ S j}.card

Input-vertex degree is the number of supports containing that input.

theorem Cslib.Circuits.Frontier.Incidence.ncard_incidence_inr {ι : Type u_1} {κ : Type u_2} (S : κ → Finset ι) (j : κ) : ((graph S).incidenceSet (Sum.inr j)).ncard = (S j).card

Support-vertex degree is the size of that support.

theorem Cslib.Circuits.Frontier.Incidence.maxDegreeLE {ι : Type u_1} {κ : Type u_2} [Finite ι] [DecidableEq ι] [Fintype κ] (S : κ → Finset ι) {d T : ℕ} (hs : ∀ (j : κ), (S j).card ≤ d) (hT : ∀ (i : ι), {j : κ | i ∈ S j}.card ≤ T) : (graph S).MaxDegreeLE (max d T)

Bounds on support sizes and input incidences bound both classes of incidence-graph degrees.

def Cslib.Circuits.Frontier.Incidence.inputPrefix {ι : Type u_1} {κ : Type u_2} [Fintype ι] (π : Layout (ι ⊕ κ)) (t : ℕ) : Finset ι

The inputs occurring among the first t incidence-layout vertices.

@[simp]

theorem Cslib.Circuits.Frontier.Incidence.mem_inputPrefix {ι : Type u_1} {κ : Type u_2} [Fintype ι] (π : Layout (ι ⊕ κ)) (t : ℕ) (i : ι) : i ∈ inputPrefix π t ↔ ↑(π (Sum.inl i)) < t

An input belongs to the prefix exactly when its layout position is below t.

@[simp]

theorem Cslib.Circuits.Frontier.Incidence.inputPrefix_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] (π : Layout (ι ⊕ κ)) : inputPrefix π 0 = ∅

The empty layout prefix contains no inputs.

theorem Cslib.Circuits.Frontier.Incidence.inputPrefix_last {ι : Type u_1} {κ : Type u_2} [Fintype ι] (π : Layout (ι ⊕ κ)) : inputPrefix π (Nat.card (ι ⊕ κ)) = Finset.univ

The full layout prefix contains every input.

theorem Cslib.Circuits.Frontier.Incidence.inputPrefix_mono {ι : Type u_1} {κ : Type u_2} [Fintype ι] (π : Layout (ι ⊕ κ)) : Monotone (inputPrefix π)

Input prefixes grow with the layout position.

theorem Cslib.Circuits.Frontier.Incidence.card_inputPrefix_succ_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] (π : Layout (ι ⊕ κ)) (t : ℕ) : (inputPrefix π (t + 1)).card ≤ (inputPrefix π t).card + 1

Processing one layout vertex adds at most one input.

theorem Cslib.Circuits.Frontier.Incidence.card_crossing_le_width {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] (S : κ → Finset ι) (π : Layout (ι ⊕ κ)) (t : ℕ) : {j : κ | ¬Disjoint (S j) (inputPrefix π t) ∧ ¬Disjoint (S j) (inputPrefix π t)ᶜ}.card ≤ (graph S).width π

Each support crossing the input cut contributes a distinct incidence edge to the layout frontier, so the number of such supports is at most the layout width.

theorem Cslib.Circuits.Frontier.Incidence.two_mul_card_lt {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] (S : κ → Finset ι) {T k : ℕ} (hs : ∀ (j : κ), (S j).card ≤ 3) (hT : ∀ (i : ι), {j : κ | i ∈ S j}.card ≤ T) (hconn : (graph S).toSimpleGraph.Connected) (hcut : ∀ (U : Finset ι), U.card < {j : κ | ¬Disjoint (S j) U}.card + k ∨ Uᶜ.card < {j : κ | ¬Disjoint (S j) Uᶜ}.card + k) : 2 * Fintype.card ι < 3 * Fintype.card κ + max 3 T * Nat.log 2 (Fintype.card ι + Fintype.card κ) + 2 * k + 1

A connected family whose supports have size at most three satisfying the cut-deficit obstruction has twice as many inputs as at most three times as many supports, up to the degree-layout and rectangle-threshold terms.