Proof of the one-dimensional capacity theorem

Fix a split U with |U| = a and process the blocks of a decomposition in order, keeping a rectangle P × Q on which the current history is a function of the second side q alone.

• A one-dimensional block with T ≥ 1 changes is Ψ_q(α(p)) on the rectangle, where ⟨w, glue p q⟩ = α(p) + β(q). The sorted-group lemma with 2T groups keeps a group of ⌊|P| / 2T⌋ elements of P and at least half of Q.
• A summary block with V values keeps the largest fiber of σ, of ⌊|P| / V⌋ elements.

At the end the output is a function of q on P × Q; keep a majority value on at least half of Q. Choosing a = ⌈log₂ (K Dₚ)⌉, where Dₚ is the product of the first-side factors, both sides have at least K elements whenever 4 K² · cost ≤ 2ⁿ, contradicting two-sided rectangle-freeness.

theorem Algebraic.Threshold.weightedSum_glue {n : ℕ} (w : Fin n → ℝ) (U : Finset (Fin n)) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) : weightedSum w (Cutwidth.glue U p q) = weightedSum w (Cutwidth.glue U p fun (x : ↥Uᶜ) => false) + weightedSum w (Cutwidth.glue U (fun (x : ↥U) => false) q)

The weighted sum of a glued input splits into the two sides.

def Algebraic.Threshold.BlockKind.pcost : BlockKind → ℕ

The factor by which a block shrinks the first side.

Equations

• (Algebraic.Threshold.BlockKind.oneDim T).pcost = if T = 0 then 1 else 2 * T
• (Algebraic.Threshold.BlockKind.summary V).pcost = V

def Algebraic.Threshold.BlockKind.qcost : BlockKind → ℕ

The factor by which a block shrinks the second side.

Equations

• (Algebraic.Threshold.BlockKind.oneDim T).qcost = if T = 0 then 1 else 2
• (Algebraic.Threshold.BlockKind.summary V).qcost = 1

theorem Algebraic.Threshold.BlockKind.cost_eq_mul (κ : BlockKind) : κ.cost = κ.pcost * κ.qcost

theorem Algebraic.Threshold.BlockKind.qcost_pos (κ : BlockKind) : 0 < κ.qcost

theorem Algebraic.Threshold.BlockKind.pcost_pos_of_step {n : ℕ} {H : Type u_1} {κ : BlockKind} {prev next : (Fin n → Bool) → H} (h : κ.Step prev next) : 0 < κ.pcost

def Algebraic.Threshold.Reachable {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} (D : BlockDecomposition f H) (U : Finset (Fin n)) (i NP NQ : ℕ) : Prop

After the first i blocks, some rectangle with sides of at least NP and NQ elements has the history determined by the second side.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Threshold.reachable_zero {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} (D : BlockDecomposition f H) (U : Finset (Fin n)) : Reachable D U 0 (2 ^ U.card) (2 ^ Uᶜ.card)

theorem Algebraic.Threshold.reachable_succ {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} (D : BlockDecomposition f H) (U : Finset (Fin n)) {i NP NQ : ℕ} (hi : i < D.length) (h : Reachable D U i NP NQ) : Reachable D U (i + 1) (NP / (D.kind i).pcost) (NQ / (D.kind i).qcost)

theorem Algebraic.Threshold.reachable_le {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} (D : BlockDecomposition f H) (U : Finset (Fin n)) (i : ℕ) : i ≤ D.length → Reachable D U i (2 ^ U.card / ∏ j ∈ Finset.range i, (D.kind j).pcost) (2 ^ Uᶜ.card / ∏ j ∈ Finset.range i, (D.kind j).qcost)

theorem Algebraic.Threshold.not_reachable {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} {K : ℕ} (hf : TwoSidedRectangleFree f K) (D : BlockDecomposition f H) (U : Finset (Fin n)) {NP NQ : ℕ} (h : Reachable D U D.length NP NQ) (hP : K ≤ NP) (hQ : 2 * K ≤ NQ) : False

theorem Algebraic.Threshold.two_pow_lt_mul_cost_internal {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} {K : ℕ} (hf : TwoSidedRectangleFree f K) (D : BlockDecomposition f H) : 2 ^ n < 4 * K ^ 2 * D.cost

Theorem U (one-dimensional capacity). If f is two-sided K-rectangle-free, every block decomposition of f has 2ⁿ < 4 K² · cost.