verify_uniform_selection.py

#!/usr/bin/env python3
"""Finite controls only; see the note for unrestricted proofs."""
import json
from itertools import product
# All available formal-word sets through two Cat records (including sharing).
base=frozenset(['','a','b','X','Y'])
states={base}
minima={w:0 for w in base}
counts=[]
for k in range(3):
    for s in states:
        for w in s: minima.setdefault(w,k)
    counts.append(len(states))
    if k<2: states={s|{x+y} for s in states for x in s for y in s}
assert [minima[x] for x in ['X','XX','XYX']]==[0,1,2]
assert 'XXYY' not in minima and minima['XYXY']==2
L=max(map(len,minima))
codes={'X':'b'+'a'*(L+2)+'b','Y':'b'+'a'*(L+3)+'b'}
def sub(w):return ''.join(codes.get(c,c) for c in w)
assert len({sub(w) for w in minima})==len(minima)
# Canonical radius views retain aliasing by canonical first-encounter IDs.
def heap(n,which):
    h=[('E',()),('a',()),('b',()),('c',())]
    h.append(('Cat',(1,2 if which=='b' else 3)))
    p=4
    for _ in range(n):h.append(('Cat',(0,p)));p=len(h)-1
    return h,[p,0,1,2,3]
def view(h,roots,r):
    paths={():None}; ids={};queue=[]
    for x in roots:
        if x not in ids:ids[x]=len(ids);queue.append((x,0))
    out=[]
    for x,d in queue:
        tag,ch=h[x];edges=[]
        if d<r:
            for y in ch:
                if y not in ids:ids[y]=len(ids);queue.append((y,d+1))
                edges.append(ids[y])
        head='a' if tag=='Cat' else tag
        out.append((ids[x],tag,head,tuple(edges)))
    return tuple(ids[x] for x in roots),out
def word(h,x):
    tag,ch=h[x]
    return '' if tag=='E' else (word(h,ch[0])+word(h,ch[1]) if ch else tag)
for r in range(9):
    hb,rb=heap(r+1,'b');hc,rc=heap(r+1,'c')
    assert view(hb,rb,r)==view(hc,rc,r)
    assert word(hb,rb[0])=='ab' and word(hc,rc[0])=='ac'
    assert word(hb,2)=='b' and word(hc,3)=='c'
# Unary and correlated-domain controls for formal identity.
for x,y in product(range(4),repeat=2):
    X,Y='a'*x,'a'*y
    assert X+X+Y+Y==(X+Y)*2
print(json.dumps({'scope':'Finite template enumeration for m=2, Sigma={a,b}, K<=2; marker injection on enumerated words; paired rope views for r=0..8. No proof-assistant verification or unbounded theorem check.','available_word_set_counts':counts,'distinct_formal_outputs':len(minima),'allocation_threshold_controls':{x:minima[x] for x in ['X','XX','XYX']},'paired_view_radii':list(range(9))},indent=2))