check_publication_examples.py

#!/usr/bin/env python3
"""Independent finite checks of equations and examples; no unbounded certification."""
from fractions import Fraction as F
from itertools import product, combinations
from collections import deque
from functools import lru_cache
import json

counts = {}

def words(n, alphabet='01'):
    for k in range(n + 1):
        for t in product(alphabet, repeat=k):
            yield ''.join(t)

def epal(w):
    return len(w) % 2 == 0 and w == w[::-1]

@lru_cache(None)
def suffix(w, proper=False):
    start = 1 if proper and w else 0
    return next(w[i:] for i in range(start, len(w)+1) if epal(w[i:]))

def selected(p, a):
    for i in range(1, len(p)+1):
        if p[i-1] == a and epal(p[i:]):
            return p[i:], p[:i-1][::-1]
    return None

def rope(anchor, w):
    h = suffix(anchor, True)
    cells = []
    for a in w:
        anchor = a+anchor+a
        cells.append((a, suffix(anchor, True)))
    return h, tuple(cells)

def entry(p, a):
    sel = selected(p, a)
    return rope(a+sel[0]+a, sel[1]) if sel else rope('', a+p)

updates = 0
for w in words(12):
    p = suffix(w)
    left = w[:len(w)-len(p)][::-1]
    for a in '01':
        sel = selected(p, a)
        if left.startswith(a):
            nxt, ctx = a+p+a, left[1:]
        elif sel:
            nxt, ctx = a+sel[0]+a, sel[1]+left
        else:
            nxt, ctx = '', a+p+left
        assert nxt == suffix(w+a) and ctx[::-1]+nxt == w+a
        updates += 1
counts['palindrome_occurrence_updates'] = updates

recurrences = shadow = 0
palindromes = [w+w[::-1] for w in words(7) if w]
for p in palindromes:
    link = suffix(p, True)
    bridge = p[-len(link)-1]
    match = entry(p, bridge)
    for a in '01':
        if a != bridge:
            left = entry(link, a)
            expected = (left[0], left[1] + ((bridge, match[0]),) + match[1])
            assert entry(p, a) == expected, (p, a)
            recurrences += 1
    for w in words(5):
        if (not w or w[0] != bridge) and suffix(w[::-1]+link) == link:
            assert rope(p,w)[1] == rope(link,w)[1]
            shadow += 1
counts.update(palindrome_receipt_recurrences=recurrences, palindrome_shadow_cases=shadow)

# Persistent stack decoder is independent of list-operation semantics.
nodes = [(None,None)]
def decode(v):
    out=[]
    while v is not None and nodes[v][0] is not None:
        a,v=nodes[v];out.append(a)
    return tuple(out)
stacks = 0
for ops in product(('0','1','keep','pop'), repeat=7):
    top=0; plain=()
    for op in ops:
        val,tail=nodes[top]
        if op in ('0','1'):
            node=(op,top); plain=(op,)+plain
        elif op=='keep': node=(val,tail)
        else:
            node=nodes[tail] if tail is not None else (None,None)
            plain=plain[1:]
        nodes.append(node);top=len(nodes)-1
        assert decode(top)==plain
        stacks+=1
counts['persistent_stack_steps']=stacks

# Rational readout, inverse digit recovery and XOR subadditivity.
def E(digits,c):
    x=F(0)
    for d in reversed(digits):x=d+x/(c+x)
    return x
digits=list(product(range(4),repeat=3));norm_checks=0
for c in (F(1),F(3,2),F(2)):
    labels={a:E(a,c) for a in digits}
    assert len(set(labels.values()))==len(digits)
    for a,x in labels.items():
        for d in a:
            q=x.numerator//x.denominator;assert q==d
            x=c*(x-q)/(1-(x-q))
        assert x==0
        for b in digits:
            ab=tuple(u^v for u,v in zip(a,b))
            assert labels[ab]<=labels[a]+labels[b]
            norm_checks+=1
assert E((0,1),F(2))==F(1,3)
assert E((0,2),F(2))==F(1,2)
assert E((0,3),F(2))==F(3,5)
counts['metric_rational_subadditivity_pairs']=norm_checks
jumps=0
for m in range(1,129):
    v=(m & -m).bit_length()-1
    for q in range(1,65):
        assert ((m^q)==((m-1)^q)+1)==(q % (2**(v+1))==0)
        jumps+=1
counts['metric_boundary_cancellations']=jumps

# Legal carrier graph distances versus the asserted sum of coordinate changes.
pairs=0
for n in range(1,9):
    for m in range(1,n+1):
        tuples=[t+(n,) for t in combinations(range(1,n),m-1)]
        for start in tuples:
            dist={start:0};queue=deque([start])
            while queue:
                u=queue.popleft()
                for v in tuples:
                    if sum(abs(a-b) for a,b in zip(u,v))==1 and v not in dist:
                        dist[v]=dist[u]+1;queue.append(v)
            for end in tuples:
                assert dist[end]==sum(abs(a-b) for a,b in zip(start,end))
                pairs+=1
counts['carrier_graph_distance_pairs']=pairs

c=F(1,30);Q=242;k=34;t=172
assert k-(1+2*c*(1+2*Q))==F(2,3)
assert t-(1+5*k)==1 and Q-(1+2*k+t)==1
N=100
assert 16**15*40<N**10
assert 4*(N+N**69)<N**242
assert 4*N**241<N**242
assert 2*N**173<N**242
assert N**172>=2*N**34-1
assert 5*N**171<N**172 and 9*N**34<N**172
counts['gapcvp_exact_parameter_checks']=10

# The displayed hard/easy cluster answer table.
expected_h=['0000','1000','1010','0010','1100','0100','0110','1110']
expected_e=['0000','1000','0010','1010','0100','1100','0110','1110']
for i,(a,b,c) in enumerate(product((0,1),repeat=3)):
    assert ''.join(map(str,(a^b^c,a,b,0)))==expected_h[i]
    assert ''.join(map(str,(c,a,b,0)))==expected_e[i]
counts['residual_cluster_table_rows']=8

print(json.dumps({'status':'pass','scope':'Finite examples and identities only; no certification of the unbounded theorems or external implementations.','checks':counts},indent=2))