#!/usr/bin/env python3
"""Finite covering and Schreier certificates; Python standard library only.
Positive edge (v,s) is distinct from reverse traversal of any other edge.
Words use signed 1-based generator numbers; all equalities use free reduction.
Run: python foundations-covering-certificates.py [--output PATH]
"""
from collections import deque
from itertools import permutations,product
from pathlib import Path
import argparse,json

def verify(condition,message):
    """Execute mathematical verification in normal and optimized Python."""
    if not condition:raise AssertionError(message)

def reduce_word(word):
    out=[]
    for a in word:
        if out and out[-1]==-a:out.pop()
        else:out.append(a)
    return tuple(out)
def inverse_word(word):return tuple(-a for a in reversed(word))
def compose(p,q):return tuple(p[q[i]] for i in range(len(p)))
def inverse_perm(p):
    out=[0]*len(p)
    for i,v in enumerate(p):out[v]=i
    return tuple(out)
def conjugate(c,p):return compose(c,compose(p,inverse_perm(c)))
def show_word(word):
    return ''.join(chr(96+a) if a>0 else chr(64-a) for a in word) or '1'

class Cover:
    def __init__(self,n,tables):
        if type(n) is not int or n<1:raise ValueError('positive vertex count required')
        self.n=n;self.tables=tuple(tuple(p) for p in tables);self.r=len(self.tables)
        for p in self.tables:
            if len(p)!=n:raise ValueError('each generator must have one image per vertex')
            seen=[False]*n
            for a in p:
                if type(a) is not int or not 0<=a<n or seen[a]:
                    raise ValueError('each generator must be a permutation of all vertices')
                seen[a]=True
        self.inverses=tuple(inverse_perm(p) for p in self.tables)
    def step(self,v,a):
        if type(a) is not int or a==0 or abs(a)>self.r:raise ValueError('unknown generator')
        return (self.tables if a>0 else self.inverses)[abs(a)-1][v]
    def read(self,word,start=0):
        if type(start) is not int or not 0<=start<self.n:raise ValueError('invalid start vertex')
        for a in word:start=self.step(start,a)
        return start
    def orbit(self,start):
        seen={start};todo=[start]
        while todo:
            v=todo.pop()
            for a in range(1,self.r+1):
                for letter in [a,-a]:
                    w=self.step(v,letter)
                    if w not in seen:seen.add(w);todo.append(w)
        return seen
    def tree(self):
        seen={0};todo=deque([0]);edges=[]
        while todo:
            v=todo.popleft()
            for a in range(1,self.r+1):
                for letter in [a,-a]:
                    w=self.step(v,letter)
                    if w not in seen:
                        seen.add(w);todo.append(w);edges.append((v,a-1) if letter>0 else (w,a-1))
        if len(seen)!=self.n:raise ValueError('connected cover required for one based subgroup certificate')
        return tuple(edges)
    def certificate(self,tree=None):
        tree=self.tree() if tree is None else tuple(tree)
        if len(tree)!=self.n-1 or len(set(tree))!=len(tree):raise ValueError('tree needs n-1 distinct positive edges')
        parent=list(range(self.n))
        def root(v):
            while parent[v]!=v:v=parent[v]
            return v
        adj=[[] for _ in range(self.n)]
        for v,a in tree:
            if not (0<=v<self.n and 0<=a<self.r):raise ValueError('invalid edge id')
            w=self.tables[a][v];rv,rw=root(v),root(w)
            if rv==rw:raise ValueError('tree contains a loop or cycle')
            parent[rv]=rw;adj[v].append((w,a+1));adj[w].append((v,-a-1))
        if len({root(v) for v in range(self.n)})!=1:raise ValueError('tree must span all vertices')
        words={0:()};todo=deque([0])
        while todo:
            v=todo.popleft()
            for w,a in adj[v]:
                if w not in words:words[w]=words[v]+(a,);todo.append(w)
        basis=[];edge_to_basis={};tree_set=set(tree)
        for v,a in product(range(self.n),range(self.r)):
            if (v,a) in tree_set:continue
            w=self.tables[a][v];word=reduce_word(words[v]+(a+1,)+inverse_word(words[w]))
            verify(word and self.read(word)==0, 'certificate certificate or invariant failed: word and self.read(word)==0')
            basis.append(word);edge_to_basis[v,a]=len(basis)
        verify(len(basis)==1+self.n*(self.r-1), 'certificate certificate or invariant failed: len(basis)==1+self.n*(self.r-1)')
        return {'tree':tree,'tree_words':tuple(words[v] for v in range(self.n)),'basis':tuple(basis),'edge_to_basis':edge_to_basis}
    def rewrite(self,word,cert):
        vertex=0;out=[]
        for a in word:
            after=self.step(vertex,a)
            edge=(vertex,a-1) if a>0 else (after,-a-1)
            c=cert['edge_to_basis'].get(edge)
            if c is not None:
                letter=c if a>0 else -c
                if out and out[-1]==-letter:out.pop()
                else:out.append(letter)
            vertex=after
        return tuple(out),vertex,cert['tree_words'][vertex]
    def expand(self,basis_word,cert):
        out=()
        for a in basis_word:
            w=cert['basis'][abs(a)-1]
            out=reduce_word(out+(w if a>0 else inverse_word(w)))
        return out
    def deck(self):
        return tuple(c for c in permutations(range(self.n)) if all(compose(c,p)==compose(p,c) for p in self.tables))

def group_generated(tables,n):
    identity=tuple(range(n));seen={identity};todo=[identity]
    while todo:
        p=todo.pop()
        for q in tables:
            t=compose(q,p)
            if t not in seen:seen.add(t);todo.append(t)
    return seen

def all_words(r,max_length):
    letters=tuple(range(1,r+1))+tuple(range(-1,-r-1,-1))
    for k in range(max_length+1):yield from product(letters,repeat=k)

def check_rewrite(C,cert,word):
    out,end,residual=C.rewrite(word,cert)
    verify(C.read(word)==end, 'check_rewrite certificate or invariant failed: C.read(word)==end')
    verify(reduce_word(word)==reduce_word(C.expand(out,cert)+residual), 'check_rewrite certificate or invariant failed: reduce_word(word)==reduce_word(C.expand(out,cert)+residual)')
    verify(C.read(C.expand(out,cert))==0, 'check_rewrite certificate or invariant failed: C.read(C.expand(out,cert))==0')
    verify((end==0)==(residual==()), 'check_rewrite certificate or invariant failed: (end==0)==(residual==())')
    return out,end,residual

def main():
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--output',type=Path,default=Path(__file__).with_name('foundations-covering-results.json'))
    args=parser.parse_args()
    C=Cover(3,[(1,0,2),(1,2,0)]);cert=C.certificate([(0,1),(1,1)])
    verify(cert['tree_words']==((),(2,),(2,2)), "main certificate or invariant failed: cert['tree_words']==((),(2,),(2,2))")
    verify(cert['basis']==((1,-2),(2,1),(2,2,1,-2,-2),(2,2,2)), "main certificate or invariant failed: cert['basis']==((1,-2),(2,1),(2,2,1,-2,-2),(2,2,2))")
    ex={}
    for w in [(2,2,1,1,2),(1,1),(1,2),(2,1)]:
        out,end,residual=check_rewrite(C,cert,w)
        ex[show_word(w)]={'basis_word':out,'end_vertex':end+1,'remaining_tree_word':show_word(residual)}
    verify(ex['bbaab']['basis_word']==(3,3,4), "main certificate or invariant failed: ex['bbaab']['basis_word']==(3,3,4)")
    verify(ex['aa']['basis_word']==(1,2), "main certificate or invariant failed: ex['aa']['basis_word']==(1,2)")
    verify(ex['ab']['basis_word']==(1,) and ex['ab']['remaining_tree_word']=='bb', "main certificate or invariant failed: ex['ab']['basis_word']==(1,) and ex['ab']['remaining_tree_word']=='bb'")
    count=0
    for w in all_words(2,8):check_rewrite(C,cert,w);count+=1
    inverse_tests=0
    for w in all_words(4,4):
        out,end,residual=C.rewrite(C.expand(w,cert),cert)
        verify(end==0 and residual==() and out==reduce_word(w), 'main certificate or invariant failed: end==0 and residual==() and out==reduce_word(w)');inverse_tests+=1
    image=group_generated(C.tables,C.n);H={p for p in image if p[0]==0}
    normalizer={p for p in image if {conjugate(p,h) for h in H}==H}
    verify(len(image)==6 and len(H)==2 and len(normalizer)==2 and len(C.deck())==1, 'main certificate or invariant failed: len(image)==6 and len(H)==2 and len(normalizer)==2 and len(C.deck())==1')
    # Same unbased cover, different chosen-point subgroup.
    Cprime=Cover(3,[(1,0,2),(2,0,1)])
    intertwiners=[p for p in permutations(range(3)) if all(conjugate(p,a)==b for a,b in zip(C.tables,Cprime.tables))]
    verify(intertwiners==[(1,0,2)] and Cprime.read((2,1))!=0, 'main certificate or invariant failed: intertwiners==[(1,0,2)] and Cprime.read((2,1))!=0')
    # Structural transfer to four sheets and a regular cyclic monodromy image.
    D=Cover(4,[(1,2,3,0),(2,3,0,1)]);d=D.certificate([(0,0),(1,0),(2,0)])
    verify(tuple(map(show_word,d['basis']))==('bAA','abAAA','aab','aaaa','aaabA'), "main certificate or invariant failed: tuple(map(show_word,d['basis']))==('bAA','abAAA','aab','aaaa','aaabA')")
    verify(len(D.deck())==4 and len(group_generated(D.tables,D.n))==4, 'main certificate or invariant failed: len(D.deck())==4 and len(group_generated(D.tables,D.n))==4')
    verify(check_rewrite(D,d,(2,2))[0]==(1,3), 'main certificate or invariant failed: check_rewrite(D,d,(2,2))[0]==(1,3)')
    verify(check_rewrite(D,d,(1,2,1))[0]==(2,4), 'main certificate or invariant failed: check_rewrite(D,d,(1,2,1))[0]==(2,4)')
    # Exhaust all labelled 2-generator connected covers through four vertices.
    rows=[];small_words=tuple(all_words(2,3));rewrite_cases=0
    for n in range(1,5):
        P=tuple(permutations(range(n)));transitive=[];decks=[]
        for a,b in product(P,repeat=2):
            E=Cover(n,[a,b])
            if len(E.orbit(0))!=n:continue
            transitive.append((a,b));e=E.certificate();deck=E.deck();decks.append(len(deck))
            verify(n%len(deck)==0 and len({p[0] for p in deck})==len(deck), 'main certificate or invariant failed: n%len(deck)==0 and len({p[0] for p in deck})==len(deck)')
            verify(len(e['basis'])==n+1, "main certificate or invariant failed: len(e['basis'])==n+1")
            for w in small_words:check_rewrite(E,e,w);rewrite_cases+=1
        def classes(renamings):
            unseen=set(transitive);out=[]
            while unseen:
                pair=min(unseen);orbit={(conjugate(c,pair[0]),conjugate(c,pair[1])) for c in renamings}
                verify(orbit<=set(transitive), 'classes certificate or invariant failed: orbit<=set(transitive)')
                out.append(pair);unseen-=orbit
            return out
        based=classes([c for c in P if c[0]==0]);unbased=classes(P)
        sizes=sorted(len(Cover(n,p).deck()) for p in unbased)
        rows.append({'sheets':n,'labelled_transitive_pairs':len(transitive),'based_isomorphism_classes':len(based),'unbased_isomorphism_classes':len(unbased),'deck_orders_by_unbased_class':sizes})
    verify([(r['labelled_transitive_pairs'],r['based_isomorphism_classes'],r['unbased_isomorphism_classes']) for r in rows]==[(1,1,1),(3,3,3),(26,13,7),(426,71,26)], "main certificate or invariant failed: [(r['labelled_transitive_pairs'],r['based_isomorphism_classes'],r['unbased_isomorphism_classes']) for r in rows]==[(1,1,1),(3,3,3),(26,13,7),(426,71,26)]")
    # Empty free basis and r=0 bookkeeping.
    empty=Cover(1,[]);e=empty.certificate();verify(e['basis']==() and check_rewrite(empty,e,())==((),0,()), "main certificate or invariant failed: e['basis']==() and check_rewrite(empty,e,())==((),0,())")
    failures=0
    bad=[lambda:Cover(0,[]),lambda:Cover(2,[(1,1)]),lambda:Cover(2,[(0,)]),lambda:Cover(2,[(0,2)]),lambda:Cover(2,[]).certificate(),lambda:Cover(3,[(0,1,2)]).certificate(),lambda:C.certificate([(0,0),(1,0)]),lambda:C.certificate([(2,0),(0,1)]),lambda:C.certificate([(0,1)]),lambda:C.certificate([(0,1),(0,1)]),lambda:C.read([0]),lambda:C.read([3])]
    for f in bad:
        try:f()
        except ValueError:failures+=1
        else:raise AssertionError('damaged input was accepted')
    result={'status':'PASS','word_encoding':'a,b,... positive generators; uppercase inverse letters; 1 empty word. Vertices in result are 1-based.','three_sheet':{'tables_1_based':[[x+1 for x in p] for p in C.tables],'tree_positive_edges_1_based':[[v+1,a+1] for v,a in cert['tree']],'basis':list(map(show_word,cert['basis'])),'word_examples':ex,'monodromy_image_order':len(image),'image_stabilizer_order':len(H),'image_normalizer_order':len(normalizer),'deck_order':len(C.deck()),'unbased_relabelling_to_reversed_b':[2,1,3]},'four_sheet':{'tables_1_based':[[x+1 for x in p] for p in D.tables],'basis':list(map(show_word,d['basis'])),'b_squared_rewrite':[1,3],'aba_rewrite':[2,4],'deck_order':len(D.deck())},'enumeration':rows,'checks':{'three_sheet_original_words_length_at_most_8':count,'free_basis_words_length_at_most_4':inverse_tests,'small_cover_word_rewrites':rewrite_cases,'damaged_inputs_rejected':failures,'empty_basis_case':True}}
    args.output.parent.mkdir(parents=True,exist_ok=True);args.output.write_text(json.dumps(result,ensure_ascii=False,indent=2)+'\n');print(json.dumps(result,ensure_ascii=False,indent=2))

if __name__=='__main__':main()