check_conditioned_profiles.py

#!/usr/bin/env python3
"""Finite falsification checks for terminal-marker residual profiles.

Run beside the original check_tree_witness.py. No external packages.
The asymptotic theorem rests on the accompanying proof, not these checks.
"""
from collections import Counter
from itertools import product
from random import Random
import json
from check_tree_witness import encoded_word, semantic_accept


def bits(k):
    return map(''.join, product('01', repeat=k))


def rank(rows):
    pivots = {}
    for row in rows:
        x = int(row or '0', 2)
        while x:
            p = x.bit_length() - 1
            if p in pivots:
                x ^= pivots[p]
            else:
                pivots[p] = x
                break
    return len(pivots)


def construct(n, rows):
    assert len(rows) == n*n and all(len(a) == n for a in rows)
    N = 1 << (n*n-1).bit_length()
    G = 1 << n.bit_length()
    H = ['0'*(n+1) for _ in range(N*G)]
    E = H.copy()
    for i in range(N):
        H[i] = (rows[i] if i < n*n else '0'*n) + '1'
        E[i] = '0'*n + '1'
        for j in range(n):
            H[i+N*(j+1)] = E[i+N*(j+1)] = '0'*j+'1'+'0'*(n-j)
    return H, E


def cylinders(m):
    h = m.bit_length()-1
    for k in range(h+1):
        for r in bits(k):
            yield r, [i for i in range(m) if format(i, f'0{h}b')[::-1].startswith(r)]


def algebra_audit(n, A):
    H, E = construct(n, A)
    d = n+1
    for j in range(d+1):
        assert rank([a[:j] for a in H]) == rank([a[:j] for a in E]) == j
    checks = 0
    for r, indices in cylinders(len(H)):
        for j in range(d+1):
            assert rank([H[i][j:] for i in indices]) == rank([E[i][j:] for i in indices]), (n,A,j,r)
            checks += 1
    return checks


def semantic_audit(n, A):
    H, E = construct(n, A)
    d = n+1
    # Reuse independently evaluated complete words when forming residual sets.
    answers = []
    for M in (H, E):
        answers.append({y: [semantic_accept(encoded_word(M,y,i)) for i in range(len(M))] for y in bits(d)})
    checks = 0
    for r, indices in cylinders(len(H)):
        for j in range(d+1):
            expected_count = 1 << rank([H[i][j:] for i in indices])
            expected_fiber = (1 << (d-j)) // expected_count
            for v in bits(j):
                histograms = []
                for table in answers:
                    counts = Counter(tuple(table[v+z][i] for i in indices) for z in bits(d-j))
                    assert len(counts) == expected_count
                    assert set(counts.values()) == {expected_fiber}
                    histograms.append(sorted(counts.values()))
                assert histograms[0] == histograms[1]
                checks += 1
    for i in range(n*n):
        for x in bits(n):
            assert answers[0][x+'0'][i] == bool(sum(int(a)*int(b) for a,b in zip(A[i],x)) % 2)
    return checks


def main():
    count = 0
    matrices = 0
    for n in (1,2):
        for A in product(list(bits(n)), repeat=n*n):
            count += algebra_audit(n, A)
            matrices += 1
    rng = Random(20260905)
    for n in (3,4,6):
        for _ in range(3):
            A = [''.join(rng.choice('01') for _ in range(n)) for i in range(n*n)]
            count += algebra_audit(n, A)
            matrices += 1
    semantic_cases = sum(semantic_audit(n,A) for n,A in [
        (1,['0']), (1,['1']), (2,['00','00','00','00']),
        (2,['00','01','10','11']), (3,['101','011','111','000','001','100','110','010','101'])
    ])
    # The theorem does not claim equality of actual residuals or arbitrary conditioning.
    H,E = construct(1,['1'])
    assert semantic_accept(encoded_word(H,'10',0))
    assert not semantic_accept(encoded_word(E,'10',0))
    print(json.dumps({'status':'passed','matrices':matrices,
        'exhaustive_n1_and_n2_matrices':258,
        'cylinder_suffix_rank_checks':count,
        'semantic_conditioned_histograms':semantic_cases,
        'limitation_counterexample':'n=1, A=[1], update 10, row 0 has different acceptance',
        'scope':'Finite corroboration; no lower bound or universal unambiguity proved by enumeration.'},indent=2))


if __name__ == '__main__':
    main()