#!/usr/bin/env python3
"""Exact finite certificates for tableaux, Jacobi--Trudi and word RSK.
Only Python's standard library is used. No checks depend on assert or float.
Run with --output FILE; no author-workspace paths are required.
"""
from argparse import ArgumentParser
from collections import Counter
from fractions import Fraction as F
from functools import lru_cache
from itertools import combinations_with_replacement, permutations, product
from math import factorial, prod
import json
from pathlib import Path

COUNTS = Counter()

def check(ok, section, message):
    COUNTS[section] += 1
    if not ok:
        raise ValueError(f'{section}: {message}')

@lru_cache(None)
def partitions(n, bound=None):
    if not n:
        return ((),)
    bound = n if bound is None else min(bound, n)
    return tuple((a,) + b for a in range(bound, 0, -1)
                 for b in partitions(n-a, a))

def shape(T):
    return tuple(map(len, T))

def frozen(T):
    return tuple(map(tuple, T))

def cells(lam):
    return [(i,j) for i,a in enumerate(lam) for j in range(a)]

def valid(T, standard=False):
    lam = shape(T)
    if any(a < b for a,b in zip(lam, lam[1:])) or any(not a for a in lam):
        return False
    for i,j in cells(lam):
        if j and T[i][j-1] > T[i][j]:
            return False
        if i and T[i-1][j] >= T[i][j]:
            return False
    return not standard or sorted(sum((list(r) for r in T), [])) == list(range(1,sum(lam)+1))

@lru_cache(None)
def tableaux(lam, m):
    positions = cells(lam)
    rows = [[0]*a for a in lam]
    out = []
    def visit(k):
        if k == len(positions):
            out.append(frozen(rows)); return
        i,j = positions[k]
        lo = max(1, rows[i][j-1] if j else 1, rows[i-1][j]+1 if i else 1)
        for value in range(lo, m+1):
            rows[i][j] = value; visit(k+1)
    visit(0)
    return tuple(out)

@lru_cache(None)
def standard_tables(lam):
    n = sum(lam)
    if not n:
        return ((),)
    out = []
    for i,a in enumerate(lam):
        if i+1 < len(lam) and lam[i+1] == a:
            continue
        smaller = list(lam); smaller[i] -= 1; smaller = tuple(x for x in smaller if x)
        for T in standard_tables(smaller):
            rows = [list(r) for r in T]
            if i == len(rows): rows.append([])
            rows[i].append(n); out.append(frozen(rows))
    return tuple(out)

@lru_cache(None)
def corner_count(lam):
    if not lam: return 1
    total = 0
    for i,a in enumerate(lam):
        if i+1 == len(lam) or a > lam[i+1]:
            mu = list(lam); mu[i] -= 1
            total += corner_count(tuple(x for x in mu if x))
    return total

@lru_cache(None)
def strip_count(lam, m):
    if not lam: return 1
    if not m: return 0
    bounds = [(lam[i+1] if i+1 < len(lam) else 0, a) for i,a in enumerate(lam)]
    return sum(strip_count(tuple(x for x in mu if x),m-1)
               for mu in product(*(range(lo,hi+1) for lo,hi in bounds)))

def hooks(lam):
    return [[a-j+sum(b>j for b in lam[i+1:]) for j in range(a)] for i,a in enumerate(lam)]

def hook_counts(lam,m):
    denominator = prod(sum(hooks(lam), []))
    return F(factorial(sum(lam)),denominator), F(prod(m+j-i for i,j in cells(lam)),denominator)

def determinant(matrix):
    a = [list(map(F,row)) for row in matrix]; value = F(1); n=len(a)
    for k in range(n):
        pivot = next((i for i in range(k,n) if a[i][k]),None)
        if pivot is None: return F(0)
        if pivot != k: a[pivot],a[k] = a[k],a[pivot]; value = -value
        value *= a[k][k]
        for i in range(k+1,n):
            ratio = a[i][k]/a[k][k]
            for j in range(k+1,n): a[i][j] -= ratio*a[k][j]
            a[i][k] = F(0)
    return value

def jt(lam, xs):
    if not lam: return F(1)
    K = lam[0]+len(lam)-1; h = [F(1)]+[F(0)]*K
    for x in xs:
        for k in range(1,K+1): h[k] += x*h[k-1]
    return determinant([[h[d] if (d:=a-i+j)>=0 else F(0)
                         for j in range(len(lam))] for i,a in enumerate(lam)])

def content(T,m):
    return tuple(sum(row.count(k) for row in T) for k in range(1,m+1))

def insert(word, record_trace=False):
    """Core tables use O(N) slots; optional complete snapshots use O(N**2)."""
    P=[];Q=[]; trace=[]
    for k,value in enumerate(word,1):
        x=value; bumps=[] if record_trace else None; i=0
        while True:
            if i==len(P): P.append([]);Q.append([])
            j=next((j for j,y in enumerate(P[i]) if y>x),len(P[i]))
            if j==len(P[i]):
                P[i].append(x);Q[i].append(k)
                if record_trace: bumps.append([i+1,j+1,x,None])
                break
            old=P[i][j];P[i][j]=x
            if record_trace: bumps.append([i+1,j+1,x,old])
            x=old;i+=1
        if record_trace:
            trace.append({'time':k,'letter':value,'rows':frozen(P),'new_cell':[i+1,j+1],'bumps':bumps})
    return frozen(P),frozen(Q),trace

def inverse(P,Q):
    if shape(P)!=shape(Q) or not valid(P) or not valid(Q,True):
        raise ValueError('invalid same-shape tableau pair')
    P=[list(r) for r in P];Q=[list(r) for r in Q]; back=[]
    for k in range(sum(shape(P)),0,-1):
        i=next(i for i,row in enumerate(Q) if k in row)
        if Q[i][-1]!=k: raise ValueError('recording label not at corner')
        Q[i].pop();x=P[i].pop()
        if not P[i]: P.pop();Q.pop()
        for row in reversed(P[:i]):
            choices=[j for j,y in enumerate(row) if y<x]
            if not choices: raise ValueError('reverse insertion has no candidate')
            j=choices[-1];x,row[j]=row[j],x
        back.append(x)
    return tuple(reversed(back))

def longest_weak(word):
    best=[]
    for i,x in enumerate(word):
        best.append(1+max((best[j] for j in range(i) if word[j]<=x),default=0))
    return max(best,default=0)

def paths(A,B):
    x,y=A; u,v=B
    if x>u or y>v: return ()
    if A==B: return ((A,),)
    out=[]
    if x<u: out.extend((A,)+tail for tail in paths((x+1,y),B))
    if y<v: out.extend((A,)+tail for tail in paths((x,y+1),B))
    return tuple(out)

def path_weight(family,m):
    exponent=[0]*m
    for path in family:
        for a,b in zip(path,path[1:]):
            if a[0]!=b[0]: exponent[a[1]-1]+=1
    return tuple(exponent)

def swap_tail(family):
    incidence={}
    for i,path in enumerate(family):
        for v in path: incidence.setdefault(v,[]).append(i)
    shared=[v for v,ids in incidence.items() if len(ids)>=2]
    if not shared: return None
    v=min(shared,key=lambda z:(sum(z),z[0]));i,j=incidence[v][:2]
    a=family[i].index(v);b=family[j].index(v);new=list(family)
    new[i]=family[i][:a]+family[j][b:];new[j]=family[j][:b]+family[i][a:]
    return tuple(new)

def sign(perm):
    return (-1)**sum(perm[i]>perm[j] for i in range(len(perm)) for j in range(i+1,len(perm)))

def verify():
    COUNTS.clear()
    for n in range(12):
        for lam in partitions(n):
            f,_=hook_counts(lam,0)
            check(f==corner_count(lam),'hook_and_factorial','corner recursion')
            mat=[[F(1,factorial(d)) if (d:=a-i+j)>=0 else F(0)
                  for j in range(len(lam))] for i,a in enumerate(lam)]
            check(factorial(n)*determinant(mat)==f,'hook_and_factorial','factorial determinant')
            for padding in range(4):
                padded=lam+(0,)*padding;r=len(padded);ell=[a+r-i-1 for i,a in enumerate(padded)]
                for i,a in enumerate(padded):
                    actual={a-j+sum(b>j for b in padded[i+1:]) for j in range(a)}
                    expected=set(range(1,ell[i]+1))-{ell[i]-ell[j] for j in range(i+1,r)}
                    check(actual==expected,'hook_and_factorial','row-complement including zero rows')
    for n in range(8):
        for lam in partitions(n):
            for m in range(4):
                Ts=tableaux(lam,m);_,g=hook_counts(lam,m)
                check(g==len(Ts)==strip_count(lam,m)==jt(lam,[1]*m),'tableaux_and_jt','four counts')
                for T in Ts:
                    check(valid(T),'tableaux_and_jt','enumerated rows/columns')
                    chain=[tuple(sum(v<=k for v in row) for row in T) for k in range(m+1)]
                    for old,new in zip(chain,chain[1:]):
                        check(all(new[i]>=old[i]>=(new[i+1] if i+1<len(new) else 0) for i in range(len(new))),
                              'tableaux_and_jt','horizontal interlacing')
                    recovered=tuple(tuple(next(k for k,mu in enumerate(chain) if mu[i]>j) for j in range(a)) for i,a in enumerate(lam))
                    check(recovered==T,'tableaux_and_jt','chain inverse')
                points=[tuple(F(x) for x in range(1,m+1)),tuple(F((-1)**i*(i+1),2) for i in range(m)),(F(0),)*m]
                for xs in points:
                    weighted=sum((prod(xs[v-1] for row in T for v in row) for T in Ts),F(0))
                    check(jt(lam,xs)==weighted,'tableaux_and_jt','weighted evaluation')
                    if len(lam)<=m and m:
                        ell=list(lam)+( [0]*(m-len(lam)) );ell=[a+m-i-1 for i,a in enumerate(ell)]
                        if len(set(xs))==m:
                            numerator=determinant([[x**e for e in ell] for x in xs])
                            denominator=determinant([[x**(m-j-1) for j in range(m)] for x in xs])
                            check(numerator==weighted*denominator,'tableaux_and_jt','alternant bridge')
    lgv_examples=0
    for lam in [(),(1,),(2,),(1,1),(2,1),(2,2),(3,1),(1,1,1),(2,1,1)]:
        for m in range(1,4):
            r=len(lam);A=[(-j-1,1) for j in range(r)];B=[(a-i-1,m) for i,a in enumerate(lam)]
            signed=Counter();survivors=Counter()
            for perm in permutations(range(r)):
                for family in product(*(paths(A[j],B[perm[j]]) for j in range(r))):
                    lgv_examples+=1;weight=path_weight(family,m);signed[weight]+=sign(perm)
                    paired=swap_tail(family)
                    if paired is not None:
                        check(swap_tail(paired)==family and paired!=family,'path_involution','fixed-point-free involution')
                        newperm=tuple(B.index(path[-1]) for path in paired)
                        check(sign(newperm)==-sign(perm) and path_weight(paired,m)==weight,'path_involution','sign and weight')
                    else:
                        check(perm==tuple(range(r)),'path_involution','only identity endpoints survive')
                        T=tuple(tuple(a[1] for a,b in zip(path,path[1:]) if a[0]!=b[0]) for path in family)
                        check(valid(T) and shape(T)==lam,'path_involution','survivor is exactly a tableau')
                        survivors[weight]+=1
            check(all(value>=0 for value in signed.values()),'path_involution','no negative coefficient hidden by cancellation')
            signed=+signed
            expected=Counter(content(T,m) for T in tableaux(lam,m))
            check(signed==survivors==expected,'path_involution','complete signed cancellation')
    shape_counts=Counter();content_counts=Counter();image_pairs=set()
    for n in range(8):
        for word in product(range(1,4),repeat=n):
            P,Q,_=insert(word)
            check(valid(P) and valid(Q,True) and shape(P)==shape(Q),'word_bijection','valid output')
            check(inverse(P,Q)==word,'word_bijection','word round trip')
            check((len(P[0]) if P else 0)==longest_weak(word),'word_bijection','independent quadratic subsequence DP')
            check(content(P,3)==tuple(word.count(k) for k in range(1,4)),'word_bijection','content preserved')
            if n==7:
                shape_counts[shape(P)]+=1
                if shape(P)==(4,2,1): content_counts[content(P,3)]+=1;image_pairs.add((P,Q))
    for n in range(7):
        total=0
        for lam in partitions(n):
            Ps=tableaux(lam,3);Qs=standard_tables(lam)
            check(len(Qs)==corner_count(lam),'word_bijection','independently generated recording tables')
            for P in Ps:
                for Q in Qs:
                    w=inverse(P,Q);P2,Q2,_=insert(w)
                    check((P2,Q2)==(P,Q),'word_bijection','arbitrary legal pair round trip');total+=1
        check(total==3**n,'word_bijection','all independent pair counts')
    for n in range(8):
        counts=Counter()
        for word in permutations(range(1,n+1)):
            P,Q,_=insert(word);counts[shape(P)]+=1
            check(valid(P,True) and inverse(P,Q)==word,'permutations','standard pair and inverse')
        check(sum(corner_count(lam)**2 for lam in partitions(n))==factorial(n),'permutations','sum of squares')
        for lam in partitions(n):check(counts[lam]==corner_count(lam)**2,'permutations','each permutation fibre')
    main=(4,2,1);Ps=tableaux(main,3);Qs=standard_tables(main)
    check(len(image_pairs)==len(Ps)*len(Qs)==525,'main_fibre','complete pair coverage')
    check(content_counts[(3,2,2)]==70,'main_fibre','specified content')
    P,Q,trace=insert((1,3,2,3,2,1,3), record_trace=True)
    core=insert((1,3,2,3,2,1,3))
    check(core==(P,Q,[]) and len(trace)==7,'main_fibre','optional trace changes storage, not the pair')
    fixed_content=[T for T in Ps if content(T,3)==(3,2,2)]
    inverse_examples=[{'P':T,'Q':Q,'word':inverse(T,Q)} for T in fixed_content]
    check(insert((1,3,2))[0]==insert((3,1,2))[0] and insert((1,3,2))[1]!=insert((3,1,2))[1],'boundaries','P alone is not injective')
    check(not valid(((1,),(1,))) and longest_weak((1,1))==2,'boundaries','greater-or-equal collision fails')
    check(corner_count((3,2,1,1))==35 and not tableaux((3,2,1,1),3),'boundaries','transpose changes finite alphabet feasibility')
    check(hook_counts((3,2,1,1),4)==(F(35),F(20)) and strip_count((3,2,1,1),4)==20,'boundaries','four-letter transpose migration')
    check([row['word'] for row in inverse_examples]==[(1,3,1,3,2,1,2),(1,2,1,3,2,1,3)],'main_fibre','two specified inverse words')
    for n in range(6):
        for lam in partitions(n):
            positions=cells(lam);labels={};label=1
            for i in reversed(range(len(lam))):
                for j in range(lam[i]):labels[i,j]=label;label+=1
            for T in tableaux(lam,3):
                sigma={c:3-T[c[0]][c[1]] for c in positions}
                for a in positions:
                    for b in positions:
                        if a!=b and a[0]<=b[0] and a[1]<=b[1]:
                            check(sigma[a]>=sigma[b] and (labels[a]<labels[b] or sigma[a]>sigma[b]),'poset_bridge','all comparable-pair antitone conditions')
    event_count=sum(a<b and a<c and b<d for a,b,c,d in permutations(range(4)))
    check(F(event_count,24)==F(1,8)!=F(1,3)*F(1,2),'boundaries','hook events are dependent')
    check(jt((1,1),[F(1),F(1)])==1,'boundaries','coincident-variable polynomial value')
    return {'status':'PASS','arithmetic':'Python standard library, exact integers and Fraction',
            'checks':sum(COUNTS.values()),'section_checks':dict(sorted(COUNTS.items())),
            'lgv_path_families':lgv_examples,'main_shape':[4,2,1],
            'standard_count':35,'semistandard_count_three_letters':15,'word_fibre_count':525,
            'shape_distribution':[{'shape':lam,'standard':corner_count(lam),'semistandard':len(tableaux(lam,3)),'words':shape_counts[lam]} for lam in partitions(7) if len(lam)<=3],
            'tableau_content_distribution':[{'content':a,'tableaux':k,'words':content_counts[a]} for a,k in sorted(Counter(content(T,3) for T in Ps).items())],
            'insertion_trace':trace,'final_P':P,'final_Q':Q,'fixed_content_inverse_examples':inverse_examples,
            'specified_content_total_words':factorial(7)//(factorial(3)*factorial(2)**2),
            'scope':'Finite exact audits supplement, and do not replace, the general proofs in the four articles.'}

def main():
    parser=ArgumentParser(description=__doc__);parser.add_argument('--output',type=Path);args=parser.parse_args()
    result=verify();text=json.dumps(result,ensure_ascii=False,indent=2)+'\n'
    if args.output:args.output.parent.mkdir(parents=True,exist_ok=True);args.output.write_text(text)
    else:print(text,end='')

if __name__=='__main__':main()