Functions with two rectangle-free fibers

Bias strictly below 1 / 2 excludes monochromatic rectangles of positive size. Applying the probabilistic existence theorem for rectangle bias with bias 1 / 4 and threshold 16 (n + 1) therefore gives Boolean functions whose two fibers are rectangle-free at that threshold.

This proves nonvacuity of the two-sided rectangle hypothesis used by the threshold-circuit lower bounds. The existence statement is nonconstructive and asserts no evaluation-time bound.

Main results

• Cslib.Circuits.Frontier.RectangleBias.rectangleFree: bias below one half implies rectangle-freeness.
• Cslib.Circuits.Frontier.RectangleBias.rectangleFree_compl: the complementary set is rectangle-free as well.
• Cslib.Circuits.Frontier.exists_twoSided_rectangleFree: both fibers can be 16 (n + 1)-rectangle-free for every input length n.

References

The probabilistic existence argument is in Complexity.Computability.Circuit.Frontier.Witness; see Alon and Spencer, The Probabilistic Method.

theorem Cslib.Circuits.Frontier.RectangleBias.rectangleFree {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] {S : Set (ι → U)} {K : ℕ} {b : ℝ} (hS : RectangleBias S K b) (hb : b < 1 / 2) (hK : 0 < K) : RectangleFree S K

A set with bias strictly below one half on large rectangles contains no such rectangle.

theorem Cslib.Circuits.Frontier.RectangleBias.rectangleFree_compl {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] {S : Set (ι → U)} {K : ℕ} {b : ℝ} (hS : RectangleBias S K b) (hb : b < 1 / 2) (hK : 0 < K) : RectangleFree Sᶜ K

The complement of a set with bias strictly below one half also contains no large rectangle.

theorem Cslib.Circuits.Frontier.exists_twoSided_rectangleFree (n : ℕ) : ∃ (f : BooleanFunction n), ∀ (a : Bool), RectangleFree {x : Fin n → Bool | f x = a} (16 * (n + 1))

For every input length, there is a Boolean function whose two fibers are 16 (n + 1)-rectangle-free. This is nonconstructive; no evaluation-time bound is asserted.