verify_shared_level_selection.py

#!/usr/bin/env python3
"""Finite checks only: prescribed markers and indexed ternary templates."""
import json
from itertools import product

marker_cases=[]
for L in range(1,5):
    alphabet=('a','b','X','Y')
    words=[p for n in range(L+1) for p in product(alphabet,repeat=n)]
    for lengths in ((L+5,L+5),(3**(L+1),3**(L+2))):
        codes={v:'b'+'a'*(L+i+1)+'b'*(N-L-i-2)
               for i,(v,N) in enumerate(zip(('X','Y'),lengths),1)}
        assert tuple(map(len,codes.values()))==lengths
        decoded=[''.join(codes.get(c,c) for c in w) for w in words]
        assert len(set(decoded))==len(words)
        marker_cases.append({'L':L,'lengths':lengths,'formal_words':len(words)})

# All ordered templates through two G allocations over a,b,X,Y.
# Ranks are affine pairs (coefficient of ell, offset).
base=[(0,0),(0,0),(1,0),(1,1)]
def types(template,ell=None):
    ranks=base[:]
    if ell is not None:ranks=[a*ell+b for a,b in ranks]
    for children in template:
        rs=[ranks[i] for i in children]
        if not(rs[0]==rs[1]==rs[2]):return None
        r=rs[0]
        ranks.append((r[0],r[1]+1) if ell is None else r+1)
    return ranks

templates=[()];tested=0;accidental=0
for K in range(3):
    for t in templates:
        high=types(t,K+1);symbolic=types(t)
        if high is not None:
            assert symbolic is not None
            for ell in range(5):
                assert types(t,ell)==[a*ell+b for a,b in symbolic]
            for j,r in enumerate(high):
                for d in range(4):
                    if r==K+1+d:assert symbolic[j]==(1,d)
        if types(t,0) is not None and symbolic is None:accidental+=1
        tested+=1
    if K<2:
        templates=[t+(children,) for t in templates
                   for children in product(range(4+K),repeat=3)]

# Supplied roots for a fixed singleton domain; no uniform zero-node answer.
values={x:["a"+x,"ba"] for x in 'ab'}
assert all(x+'a' in values[x] for x in 'ab')
assert not any(all(values[x][i]==x+'a' for x in 'ab') for i in range(2))
for ell in range(10):
    assert 2*3**ell not in [3**j for j in range(12)]
    assert 3*3**ell==3**(ell+1)
print(json.dumps({'scope':'All formal words through length 4 over a,b,X,Y for two prescribed-length choices per bound; all ordered ternary templates over a,b,X(rank ell),Y(rank ell+1) through two allocations, symbolic vs concrete ranks ell=0..4; singleton selection and residual-length controls. No proof-assistant or unrestricted synthesis verification.','marker_cases':marker_cases,'templates_checked':tested,'accidental_level_zero_typings':accidental},indent=2))