verify_correlated_caches.py

#!/usr/bin/env python3
"""Finite corroboration of correlated-root costs and persistent histories."""
import json
from itertools import product

# Expanded formal words model old roots X,Y,XY and fixed a,b,E.
base=frozenset(['','a','b','X','Y','XY'])
states={base}; rows=[]; min_joint=None
for k in range(3):
    exists=any({'Xa','Y','XaY'} <= s for s in states)
    if exists and min_joint is None:min_joint=k
    rows.append({'K':k,'available_word_sets':len(states),'joint_update_exists':exists})
    if k<2: states={s|{u+v} for s in states for u in s for v in s}
assert min_joint==2
assert 'XY' in base  # Cached query costs zero.
assert 'XY' != 'Xa'+'Y'  # Stale cache fails preservation.

# Immutable arena; branching explores calls made on retained versions.
class Arena:
    def __init__(self):
        self.nodes=[None,('a',),('b',)];self.words=['','a','b']
    def cat(self,x,y):
        self.nodes.append((x,y));self.words.append(self.words[x]+self.words[y])
        return len(self.nodes)-1

def append(ar,x,p,i,c):
    before=len(ar.nodes);xx=list(x);pp=list(p)
    xx[i]=ar.cat(x[i],c)
    if i==0: pp[0]=xx[0]
    else: pp[i]=ar.cat(p[i],c)
    for j in range(i+1,len(x)):pp[j]=ar.cat(pp[j-1],x[j])
    return tuple(xx),tuple(pp),len(ar.nodes)-before

def valid(ar,x,p):
    total=''
    for j in range(len(x)):
        total+=ar.words[x[j]]
        assert ar.words[p[j]]==total

histories=[]
for d in range(1,5):
    ar=Arena();visited=0
    def explore(x,p,depth):
        global visited
        valid(ar,x,p)
        if not depth:return
        old_nodes=tuple(ar.nodes)
        old_words=tuple(ar.words[k] for k in x+p)
        for i,c in product(range(d),(1,2)):
            xx,pp,cost=append(ar,x,p,i,c)
            assert cost==(d if i==0 else d-(i+1)+2)
            assert tuple(ar.nodes[:len(old_nodes)])==old_nodes
            assert tuple(ar.words[k] for k in x+p)==old_words
            visited+=1;explore(xx,pp,depth-1)
    explore((0,)*d,(0,)*d,4)
    # Symbolic distinct-output lower bound for all positions at this d.
    z=[f'X{j}' for j in range(d)]
    old={(),('a',),('b',)} | {(v,) for v in z} | {tuple(z[:j]) for j in range(2,d+1)}
    lower=[]
    for i in range(d):
        factors=[(v,) for v in z];factors[i]+=('a',)
        prefs=[sum(factors[:j],()) for j in range(2,d+1)]
        needed=set(factors+prefs)-old
        assert len(needed)==(d if i==0 else d-i+1)
        lower.append(len(needed))
    histories.append({'d':d,'append_calls_in_depth_four_tree':visited,'symbolic_lower_bounds_by_position':lower})

print(json.dumps({'scope':'Formal available-word sets for one two-parameter cache with K<=2; all binary-letter append histories through depth 4 for d=1..4, branching from retained versions; symbolic fresh-output counts for those dimensions. No proof-assistant verification or unbounded theorem check.','joint_template_search':rows,'joint_minimum':min_joint,'prefix_checks':histories},indent=2))