Rectangle covers from mergeable summaries

A summary whose fibres are closed under mixing the two sides of an input partition covers the accepted inputs by one rectangle per summary. This is the finite counting step used when special circuit gates are checked through their partial aggregates.

def Algebraic.Cutwidth.Aggregate.mix {n : ℕ} (U : Finset (Fin n)) (x y : Fin n → Bool) : Fin n → Bool

Replace the coordinates in U by those of x, retaining those of y elsewhere.

Equations

• Algebraic.Cutwidth.Aggregate.mix U x y = Algebraic.Cutwidth.glue U (fun (i : ↥U) => x ↑i) fun (i : ↥Uᶜ) => y ↑i

theorem Algebraic.Cutwidth.Aggregate.card_accepting_le_of_mixing {n K : ℕ} {f : Cslib.BooleanFunction n} (free : RectangleFree f K) (U : Finset (Fin n)) {T : Type u_1} [Fintype T] (key : (Fin n → Bool) → T) (closed : ∀ x ∈ accepting f, ∀ y ∈ accepting f, key x = key y → f (mix U x y) = true) : (accepting f).card ≤ Fintype.card T * (K - 1) * 2 ^ max U.card Uᶜ.card

A finite summary with mixing-closed accepting fibres gives a rectangle cover bound. Only one side's aggregate needs to be included in the summary.

theorem Algebraic.Cutwidth.Aggregate.min_card_lt_of_mixing {n K D : ℕ} {f : Cslib.BooleanFunction n} (free : RectangleFree f K) (dense : 2 ^ (n - 2) ≤ (accepting f).card) (U : Finset (Fin n)) {T : Type u_1} [Fintype T] (key : (Fin n → Bool) → T) (short : Fintype.card T ≤ 2 ^ D) (closed : ∀ x ∈ accepting f, ∀ y ∈ accepting f, key x = key y → f (mix U x y) = true) : min U.card Uᶜ.card < D + Nat.clog 2 K + 3

A dense rectangle-free function cannot have a balanced partition with a short mixing summary. The three-bit slack avoids rounding qualifications at small sizes.

theorem Algebraic.Cutwidth.Aggregate.exists_subset_sum_interval {ι : Type u_1} (weight : ι → ℕ) {S : Finset ι} {r : ℕ} (positive : 0 < r) (small : ∀ i ∈ S, weight i < r) (large : r ≤ ∑ i ∈ S, weight i) : ∃ T ⊆ S, r ≤ ∑ i ∈ T, weight i ∧ ∑ i ∈ T, weight i < 2 * r

Greedily collecting parts smaller than r first reaches r before 2r.

theorem Algebraic.Cutwidth.Aggregate.exists_large_part {ι : Type u_1} [Fintype ι] (weight : ι → ℕ) {n r : ℕ} (positive : 0 < r) (total : ∑ i : ι, weight i = n) (big : 3 * r ≤ n) (unbalanced : ∀ (S : Finset ι), min (∑ i ∈ S, weight i) (n - ∑ i ∈ S, weight i) < r) : ∃ (i : ι), n - r < weight i

If no union of parts is balanced, one part contains all but fewer than r items.