Restricting rectangle-free functions

Fixing coordinates preserves the rectangle threshold. Among the restrictions fixing all coordinates outside a set, one has at least the original acceptance density.

noncomputable def Algebraic.Cutwidth.subcubeInput {n m : ℕ} (U : Finset (Fin n)) (e : ↥U ≃ Fin m) (z : Fin n → Bool) (x : Fin m → Bool) : Fin n → Bool

Extend an assignment on U, reindexed by e, by the fixed outside assignment z.

Equations

• Algebraic.Cutwidth.subcubeInput U e z x j = if hj : j ∈ U then x (e ⟨j, hj⟩) else z j

noncomputable def Algebraic.Cutwidth.restriction {n m : ℕ} (f : Cslib.BooleanFunction n) (U : Finset (Fin n)) (e : ↥U ≃ Fin m) (z : Fin n → Bool) : Cslib.BooleanFunction m

A restriction with free coordinates U, reindexed by e.

Equations

• Algebraic.Cutwidth.restriction f U e z x = f (Algebraic.Cutwidth.subcubeInput U e z x)

@[simp]

theorem Algebraic.Cutwidth.subcubeInput_apply_symm {n m : ℕ} (U : Finset (Fin n)) (e : ↥U ≃ Fin m) (z : Fin n → Bool) (x : Fin m → Bool) (i : Fin m) : subcubeInput U e z x ↑(e.symm i) = x i

theorem Algebraic.Cutwidth.RectangleFree.restriction {n m : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : RectangleFree f K) (U : Finset (Fin n)) (e : ↥U ≃ Fin m) (z : Fin n → Bool) : RectangleFree (Cutwidth.restriction f U e z) K

A restriction cannot introduce a new large one-rectangle.

theorem Algebraic.Cutwidth.exists_card_accepting_le_card_restriction_mul {n m : ℕ} (f : Cslib.BooleanFunction n) (U : Finset (Fin n)) (e : ↥U ≃ Fin m) : ∃ (z : Fin n → Bool), (accepting f).card ≤ (accepting (restriction f U e z)).card * 2 ^ (n - U.card)

Some restriction has at least the original acceptance density, expressed without rational division. The fixed assignment is chosen by finite maximization.

theorem Algebraic.Cutwidth.exists_dense_restriction {n m : ℕ} {f : Cslib.BooleanFunction n} (U : Finset (Fin n)) (e : ↥U ≃ Fin m) (hm : 2 ≤ m) (hdense : 2 ^ (n - 2) ≤ (accepting f).card) : ∃ (z : Fin n → Bool), 2 ^ (m - 2) ≤ (accepting (restriction f U e z)).card

A one-quarter-dense function has a one-quarter-dense restriction to any set of at least two free coordinates.