Incidence bounds without connectedness

The hereditary obstruction on two disjoint coordinate sets controls the sum of the positive excesses of the connected components. This removes connectedness from the incidence bound. The component estimate reuses the connected incidence theorem and its multigraph layout bound.

Main results

• Cslib.Circuits.Frontier.Incidence.card_lt_of_partition: the total cardinality bound from the largest positive excess of a partition containing every support.
• Cslib.Circuits.Frontier.Incidence.two_mul_card_lt_of_partition: the combined estimate from uniform bounds on every part's excess.
• Cslib.Circuits.Frontier.Incidence.two_mul_card_lt_of_disjoint: the rank-three incidence bound for support families whose incidence graph may be disconnected.

theorem Cslib.Circuits.Frontier.Incidence.card_lt_of_partition {ι : Type u_1} {κ : Type u_2} {γ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [Finite γ] [DecidableEq γ] (S : κ → Finset ι) (a : ι → γ) (b : κ → γ) (hpart : ∀ (j : κ), ∀ i ∈ S j, a i = b j) {M k : ℕ} (hM : ∀ (c : γ), {i : ι | a i = c}.card ≤ {j : κ | b j = c}.card + M) (hdisj : ∀ (U V : Finset ι), Disjoint U V → U.card < {j : κ | ¬Disjoint (S j) U}.card + k ∨ V.card < {j : κ | ¬Disjoint (S j) V}.card + k) : Fintype.card ι < Fintype.card κ + M + 2 * k

A hereditary obstruction to two disjoint sets with excess at least k bounds the total coordinate count in terms of the largest positive excess of a partition. Each support must lie in the part assigned to its index.

theorem Cslib.Circuits.Frontier.Incidence.two_mul_card_lt_of_partition {ι : Type u_1} {κ : Type u_2} {γ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [Finite γ] [DecidableEq γ] (S : κ → Finset ι) (a : ι → γ) (b : κ → γ) (hpart : ∀ (j : κ), ∀ i ∈ S j, a i = b j) {L k : ℕ} (hlocal : ∀ (c : γ), 2 * {i : ι | a i = c}.card < 3 * {j : κ | b j = c}.card + L + 2 * k + 1) (hdisj : ∀ (U V : Finset ι), Disjoint U V → U.card < {j : κ | ¬Disjoint (S j) U}.card + k ∨ V.card < {j : κ | ¬Disjoint (S j) V}.card + k) : 2 * Fintype.card ι < 3 * Fintype.card κ + L + 6 * k + 1

Uniform bounds on the excess of every part combine without multiplying the additive term by the number of parts. The obstruction must hold for arbitrary disjoint coordinate sets.

theorem Cslib.Circuits.Frontier.Incidence.two_mul_card_lt_of_disjoint {ι : 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) (hdisj : ∀ (U V : Finset ι), Disjoint U V → U.card < {j : κ | ¬Disjoint (S j) U}.card + k ∨ V.card < {j : κ | ¬Disjoint (S j) V}.card + k) : 2 * Fintype.card ι < 3 * Fintype.card κ + max 3 T * Nat.log 2 (Fintype.card ι + Fintype.card κ) + 6 * k + 1

The rank-three incidence bound for an arbitrary support family. It suffices that every two disjoint coordinate sets have one side whose cardinality is smaller than its number of touching supports plus k. No connectedness assumption is needed.