Quantitative forbidden-intersection bound by widening (source code)

= Quantitative forbidden-intersection bound by widening
{title2=$\rho\leq\max\{e^{-g\ell+D^2n/4},e^{-gn+(2g+h)\ell}\}$}

Let two <set families> on $n$ coordinates forbid cross-intersection size $\ell$, and let $\rho$ be their density product. For $0<\delta\leq1/10$, put $g=\log(1+\delta)$, $h=-\log(1-\delta-2\delta^2)$, and $D=g+h$. Repeated <forbidden-intersection density increments> terminate when one endpoint of the forbidden interval reaches zero or the remaining dimension. In the first case, if $v$ steps widened the interval, the <cross-intersection bound from cube separation> gives $\log\rho\leq-g\ell+Dv-v^2/n\leq-g\ell+D^2n/4$. In the second case, at least $n-\ell$ steps occurred and at most $\ell$ widened, giving $\log\rho\leq-gn+(2g+h)\ell$. For a single <set family> take the square of its density. Choosing $\delta=1/50$ proves $|\mathcal A|\leq1.999^n$ for forbidden intersections $n/4$ and $\lfloor n/8\rfloor$, with small dimensions handled directly.