Two-sided rectangle-freeness of the explicit family

A two-sided flat sumset disperser has both values on every rectangle with large sides: embed the first side as glue p 0 and the second as glue 0 q, whose sums are glue p q. The explicit family sourceReductionHardFamily is the balanced padding of an extractor with error 35/72 < 1/2, so it is eventually a two-sided disperser (Aggregate.family_eventually_sumsetDisperser), hence two-sided rectangle-free, at the threshold Aggregate.familyThreshold n = 2 ^ k(n) with k(n) = o(n).

theorem Algebraic.Threshold.twoSidedRectangleFree_of_flatSumsetDisperser_internal {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : Cutwidth.FlatSumsetDisperser f K) : TwoSidedRectangleFree f K

A two-sided flat sumset disperser is two-sided rectangle-free at the same threshold.

def Algebraic.Threshold.familyLogThreshold (n : ℕ) : ℕ

The binary logarithm of the rectangle threshold of the explicit family.

Equations

• Algebraic.Threshold.familyLogThreshold n = Algebraic.Cutwidth.Extractor.sourceReductionEntropy (n - 1) (Algebraic.Cutwidth.Extractor.sourceReductionFamilyScale (n - 1)) + 1

theorem Algebraic.Threshold.familyThreshold_eq_two_pow (n : ℕ) : Cutwidth.Aggregate.familyThreshold n = 2 ^ familyLogThreshold n

theorem Algebraic.Threshold.sourceReductionHardFamily_twoSidedRectangleFree_internal : ∀ᶠ (n : ℕ) in Filter.atTop, TwoSidedRectangleFree (Cutwidth.Extractor.sourceReductionHardFamily n) (Cutwidth.Aggregate.familyThreshold n)

The explicit family is eventually two-sided rectangle-free at familyThreshold n, from its sumset dispersion (Aggregate.family_eventually_sumsetDisperser).

theorem Algebraic.Threshold.eventually_two_mul_familyLogThreshold_add_four_le {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 * ↑(familyLogThreshold n) + 4 ≤ δ * ↑n

The logarithmic threshold is eventually below every positive multiple of n, with room for the additive constants of the capacity bounds.

theorem Algebraic.Threshold.lt_add_logb_of_two_pow_lt {n k K P : ℕ} (hK : K = 2 ^ k) (h : 2 ^ n < 4 * K ^ 2 * P) : ↑n < 2 * ↑k + 2 + Real.logb 2 ↑P

Binary logarithms of a capacity bound 2ⁿ < 4 K² P with K = 2 ^ k.