#!/usr/bin/env python3
"""Finite certificates for the zero-error information unit, standard library only.
Prints JSON; enumerates small graphs and uses exact fractions except labelled
trigonometric/entropy numerical checks. It does not compute general capacities.
"""
import math,cmath,json,itertools
from fractions import Fraction as F
checks=[]
def eq(name,a,b):
    assert a==b,(name,a,b);checks.append(dict(name=name,value=str(a),expected=str(b),status='pass'))
def near(name,a,b,tol=1e-11):
    assert abs(a-b)<=tol,(name,a,b);checks.append(dict(name=name,value=a,expected=b,tolerance=tol,status='pass'))
def fact(name,**kw):checks.append(dict(name=name,status='pass',**kw))
def edge(i,j):return (i-j)%5 in[1,4]
def strong(x,y):return x!=y and all(a==b or edge(a,b) for a,b in zip(x,y))
def alpha(vertices,adj):
    masks=[sum(1<<j for j,y in enumerate(vertices) if adj(x,y)) for x in vertices];best=0;calls=0
    def search(candidates,size):
        nonlocal best,calls;calls+=1
        if size+candidates.bit_count()<=best:return
        if not candidates:best=max(best,size);return
        bit=candidates&-candidates;v=bit.bit_length()-1
        search(candidates&~masks[v]&~bit,size+1);search(candidates^bit,size)
    search((1<<len(vertices))-1,0);return best,calls
verts=list(range(5));supp=[{i,(i+1)%5} for i in verts]
assert all((bool(supp[i]&supp[j])==edge(i,j)) for i in verts for j in verts if i!=j)
fact('C5 channel support induces exactly cycle edges')
eq('C5 one-letter alpha',alpha(verts,edge)[0],2)
words=list(itertools.product(range(5),repeat=2));code=[(i,2*i%5) for i in verts]
assert all(not strong(x,y) for x,y in itertools.combinations(code,2));fact('five-word code pairwise independence',pairs=10)
outs=[set(itertools.product(supp[i],supp[j])) for i,j in code]
assert all(not(a&b) for a,b in itertools.combinations(outs,2));eq('five codewords disjoint possible outputs',len(set().union(*outs)),20)
a,calls=alpha(words,strong);eq('C5 strong-square exact alpha',a,5);fact('exact branch search audit',recursive_calls=calls)
colors={(i,j):(j-2*i)%5 for i,j in words};assert all(colors[x]!=colors[y] for x,y in itertools.combinations(words,2) if strong(x,y));eq('five-color class sizes',[list(colors.values()).count(i) for i in verts],[5]*5)
eq('complete square edges checked',sum(strong(x,y) for x,y in itertools.combinations(words,2)),100)
# Explicit theta geometry and primal SDP certificate.
a=1/math.sqrt(5);t=(math.sqrt(5)-1)/2
U=[(math.sqrt(1-a)*math.cos(2*math.pi*i/5),math.sqrt(1-a)*math.sin(2*math.pi*i/5),math.sqrt(a)) for i in verts]
dot=lambda x,y:sum(a*b for a,b in zip(x,y))
for i in verts:
    assert abs(dot(U[i],U[i])-1)<1e-12
    for j in verts:
        expected=1 if i==j else (t if edge(i,j) else 0)
        assert abs(dot(U[i],U[j])-expected)<1e-12
fact('C5 all25 Gram entries and nonedge zeros',cases=25)
near('theta handle upper bound',1/U[0][2]**2,math.sqrt(5))
X=[[(1 if i==j else(t if not edge(i,j) else 0))/5 for j in verts] for i in verts]
near('SDP trace',sum(X[i][i] for i in verts),1);near('SDP objective',sum(map(sum,X)),math.sqrt(5))
eigs=[]
for k in verts:
    z=[cmath.exp(2j*math.pi*k*j/5) for j in verts];lam=(1+2*t*math.cos(4*math.pi*k/5))/5;eigs.append(lam)
    assert max(abs(sum(X[i][j]*z[j] for j in verts)-lam*z[i]) for i in verts)<1e-12
assert min(eigs)>-1e-12;fact('SDP Fourier eigenvector/PSD check',eigenvalues=eigs)
XX=[[X[i][ii]*X[j][jj] for ii,jj in words] for i,j in words]
assert all(XX[k][l]==0 for k,x in enumerate(words) for l,y in enumerate(words) if strong(x,y));near('tensor SDP objective',sum(map(sum,XX)),5)
# Exact primal/dual fractional-cover certificates.
edges=[{i,(i+1)%5} for i in verts];zw=[F(1,2)]*5;ww=[F(1,2)]*5
assert all(sum(zw[k] for k,e in enumerate(edges) if i in e)==1 for i in verts)
assert all(sum(ww[i] for i in e)==1 for e in edges)
eq('fractional cover and packing agreement',(sum(zw),sum(ww)),(F(5,2),F(5,2)))
# Source path support and decoding, including full block support for n=1..4.
pairs=[('a',0),('b',0),('b',1),('c',1)];enc={'a':0,'b':1,'c':0};dec={(0,0):'a',(0,1):'c',(1,0):'b',(1,1):'b'}
assert all(dec[enc[x],y]==x for x,y in pairs);fact('source path exact decoding',cases=4)
for n in range(1,5):
    for seq in itertools.product(pairs,repeat=n):
        assert tuple(dec[enc[x],y] for x,y in seq)==tuple(x for x,y in seq)
fact('source path block decoding',cases=sum(4**n for n in range(1,5)))
def entropy(ps):return -sum(float(p)*math.log2(float(p)) for p in ps if p)
h=lambda p:entropy([p,1-p])
near('path graph entropy',h(F(1,4)),.8112781244591328)
near('rare-event conditional entropy',h(F(1,50)),.14144054254182067)
near('C5 graph entropy',math.log2(5)-1,1.3219280948873622)
near('C5 deterministic coloring entropy',entropy([F(2,5),F(2,5),F(1,5)]),1.5219280948873621)
q=[F(1,2),F(1,2)];qp=[F(3,4),F(1,4)];KL=sum(float(x)*math.log2(float(x/y)) for x,y in zip(qp,q));near('reference versus true marginal KL correction',entropy(qp)+KL,1)
# Function-computation example, exact probabilities then entropy.
P={('a',0):F(3,8),('a',1):F(1,8),('b',0):F(3,16),('b',1):F(1,16),('c',0):F(1,16),('c',1):F(3,16)}
eq('function distribution mass',sum(P.values()),F(1))
px={x:sum(P[x,y] for y in [0,1]) for x in 'abc'};py={y:sum(P[x,y] for x in 'abc') for y in [0,1]}
eq('function X marginal',px,{'a':F(1,2),'b':F(1,4),'c':F(1,4)});eq('function Y marginal',py,{0:F(5,8),1:F(3,8)})
f=lambda x,y:int(x=='c')^y
fedges={(x,z) for x,z in itertools.combinations('abc',2) if any(P[x,y]*P[z,y]>0 and f(x,y)!=f(z,y) for y in [0,1])}
eq('function graph edges',sorted(fedges),[('a','c'),('b','c')])
assert all((int(x=='c')^y)==f(x,y) for x,y in P);fact('function two-label zero-error decoder',cases=6)
HZ=sum(float(py[y])*h(P['c',y]/py[y]) for y in [0,1]);HX=sum(float(py[y])*entropy([P[x,y]/py[y] for x in 'abc']) for y in [0,1]);near('conditional graph entropy',HZ,.6681222459933006);near('full conditional entropy',HX,1.3568441215341678)
# Feedback candidate-count recursion, all possible outputs bounded.
def counts(M):
    q,r=divmod(M,5);return [q+int(i<r) for i in range(5)]
def survivors(M):
    c=counts(M);return [c[y]+c[(y-1)%5] for y in range(5)]
def worst(M):return max(survivors(M))
assert all(worst(M)<=F(2,5)*M+5 for M in range(1001));assert all(worst(M)<=worst(M+1) for M in range(1000));fact('balanced partition rounding and monotonicity',cases=1001)
eq('feedback 25->10->4',(worst(25),worst(10)),(10,4))
M=5**20//2**20;seq=[M]
for _ in range(20):seq.append(worst(seq[-1]))
eq('finite feedback initial messages',M,90949470);eq('finite feedback after20 uses',seq[-1],2);near('finite feedback rate21uses',math.log2(M)/21,1.2589791378540438)
assert math.log2(M)/21>math.log2(math.sqrt(5));fact('finite feedback strictly beats no-feedback capacity',sequence=seq)
# Complete triangle graph still has packing3/2; isolated vertex changes applicability.
triangle=[{0,1},{1,2},{2,0}];assert all(sum(F(1,2) for _ in e)==1 for e in triangle)
eq('triangle hypergraph packing',3*F(1,2),F(3,2))
eq('triangle plus isolated pair-hyperedge packing',3*F(1,2)+1,F(5,2));eq('triangle plus isolated full-hyperedge packing',F(1)+1,F(2))
# Source one-shot vs joint label packing: ceil(log2 5^k) without float rounding.
def bits(m):return (m-1).bit_length()
eq('two blocks joint colors versus separate rounding',(bits(5**2),2*bits(5)),(5,6))
print(json.dumps(dict(status='pass',check_count=len(checks),checks=checks,scope='Finite graph and arithmetic certificates verify worked examples. General asymptotic claims rely on the complete article proofs and cited coding theorem; floating checks do not replace PSD proof.'),ensure_ascii=False,indent=2))