import json,math
SLUG='synthesis-oracle-limits'
def response(threshold,x):return int(x>=threshold)
def identify(target,active):
    candidates=list(range(17));sizes=[17];queries=[]
    while len(candidates)>1:
        if active:
            x=min(range(16),key=lambda x:(max(sum(response(t,x)==y for t in candidates) for y in [0,1]),x))
        else:x=len(queries)
        answer=response(target,x)
        candidates=[t for t in candidates if response(t,x)==answer]
        queries.append(x);sizes.append(len(candidates))
        assert target in candidates
    return candidates[0],queries,sizes
def optimum(n):
    dp=[0]*(n+1)
    for size in range(2,n+1):dp[size]=1+min(max(dp[k],dp[size-k]) for k in range(1,size))
    return dp

def run():
    results=[(identify(t,True),identify(t,False)) for t in range(17)]
    optimal=optimum(64)
    inputs=[(x,y) for x in range(8) for y in range(8)]
    weak=[sum(max(x,y)+c>=x and max(x,y)+c>=y for x,y in inputs) for c in range(5)]
    strong=[sum(max(x,y)+c>=x and max(x,y)+c>=y and max(x,y)+c in (x,y) for x,y in inputs) for c in range(5)]
    r11=results[11]
    checks=[dict(name='Both query strategies identify every finite target',passed=all(a[0]==t and b[0]==t for t,(a,b) in enumerate(results)),cases=17,detail='All 17 thresholds over inputs 0..15, including constant endpoint hypotheses.'),dict(name='Version spaces shrink and retain the target',passed=all(all(b<a for a,b in zip(r[2],r[2][1:])) for pair in results for r in pair),cases=34,detail='Target preservation asserted at every update; each query strictly reduces this class.'),dict(name='Decision-tree recurrence equals logarithmic lower bound',passed=all(optimal[n]==math.ceil(math.log2(n)) for n in range(1,65)),cases=64,detail='Dynamic recurrence independently considers every ordered split.'),dict(name='Balanced strategy meets optimal worst case',passed=max(len(pair[0][1]) for pair in results)==optimal[17]==5,cases=17,detail='The worked target needs four queries, but worst case is five.'),dict(name='Weak maximum specification permits every offset',passed=weak==[64]*5 and strong==[64,0,0,0,0],cases=320,detail='Exhaustive 64 input pairs for each of five offsets; mathematical integers.'),dict(name='Worked example query counts',passed=len(r11[0][1])==4 and len(r11[1][1])==12 and r11[0][2]==[17,9,4,2,1],cases=1,detail='Target threshold 11; ties resolved by smallest input.')]
    xs=list(range(17))
    return dict(slug=SLUG,checks=checks,figures=[dict(id='threshold-queries',title='Queries required to identify each threshold',x_label='Target threshold',y_label='Oracle queries',series=[dict(name='Balanced active queries',x=xs,y=[len(r[0][1]) for r in results]),dict(name='Sequential queries',x=xs,y=[len(r[1][1]) for r in results])],caption='Seventeen exact hypotheses; target 11 needs 4 versus 12 queries. Worst-case active depth is 5.',assumptions=['Deterministic exact I/O oracle','Cheap finite candidate evaluation','No query-generation cost'],kind='Constructed analytical model; not a measured benchmark'),dict(id='maximum-specification',title='An incomplete maximum specification admits unintended offsets',x_label='Offset c added to max(x,y)',y_label='Passing input pairs out of 64',series=[dict(name='Weak lower-bound constraints',x=list(range(5)),y=weak),dict(name='Strong lower-bound plus selector',x=list(range(5)),y=strong)],caption='Every nonnegative offset satisfies the weak specification; only offset zero equals one input on the modeled domain.',assumptions=['x,y in 0..7','Mathematical integer arithmetic','Candidate family max(x,y)+c'],kind='Constructed analytical model; not a measured benchmark')],result_summary=dict(target11_active_queries=r11[0][1],target11_sequential_count=len(r11[1][1]),target11_version_space_sizes=r11[0][2],optimal_worst_case_17=optimal[17],weak_pass_counts=weak,strong_pass_counts=strong))
if __name__=='__main__':print(json.dumps(run(),indent=2))