check_sparse_completion_independent.py

#!/usr/bin/env python3
"""Independent finite controls for sparse completion certificates.

No imports from the primary audit. Aggregate normalized FIFO debt is charged
only to later target bits. This is finite semantic evidence, not an execution
of native dictionaries, persistent queues, old-top packing, or trie updates.
"""
from itertools import permutations, product
import json


def mixed_prefixes(words, lo, hi):
    universe = {''.join(bits) for n in range(lo, hi + 1)
                for bits in product('01', repeat=n)}
    mixed = set()
    for depth in range(hi + 1):
        for bits in product('01', repeat=depth):
            prefix = ''.join(bits)
            region = {w for w in universe if w.startswith(prefix)}
            if region & words and region - words:
                mixed.add(prefix)
    return mixed


def residuals(words):
    prefixes = {w[:i] for w in words for i in range(len(w) + 1)}
    return {frozenset(w[len(p):] for w in words if w.startswith(p))
            for p in prefixes}


def main():
    histories = prefix_checks = passing_prefixes = 0
    words = ('0', '1', '00', '01', '10', '11', '000', '001')
    for order in permutations(words):
        seen, released = set(), set()
        debt = 0
        for word in order:
            debt = max(0, debt - 4 * len(word))
            pair = word[:-1]
            if pair not in released:
                released.add(pair)
                debt += len(word) + 1
            seen.add(word)
            if all(p + '0' in seen and p + '1' in seen for p in released):
                passing_prefixes += 1
                assert debt == 0
            prefix_checks += 1
        histories += 1
    assert (histories, prefix_checks, passing_prefixes) == (40320, 322560, 55296)

    mixed_controls = 0
    for lo in (2, 4):
        hi = 2 * lo - 1
        comb = {'0' * (n - 1) + b for n in range(lo, hi + 1) for b in '01'}
        mixed = mixed_prefixes(comb, lo, hi)
        expected = {'0' * d for d in range(2 * lo - 2)}
        expected |= {'0' * (n - 1) + '1' for n in range(lo, 2 * lo - 1)}
        assert mixed == expected
        assert len(mixed) == 3 * lo - 3
        full = {''.join(bits) for bits in product('01', repeat=lo)}
        full |= {'0' * (hi - 1) + b for b in '01'}
        count = len(mixed_prefixes(full, lo, hi))
        if lo >= 4:
            assert count >= 2 ** (lo + 1) - 1
        else:
            # At L=2 the long pair fills its entire depth-L region.
            assert count == 6
        mixed_controls += 2

    join_controls = 0
    for n in range(2, 33):
        x = {'0' * (n - 1) + b for b in '01'}
        y = {'0' * (n - 2) + '1' + b for b in '01'}
        incoming = residuals(x) | residuals(y)
        forced = {frozenset(w[d:] for w in x | y) for d in range(n - 1)}
        assert len(forced) == n - 1
        assert not forced & incoming
        assert all(len(language) == 4 for language in forced)
        join_controls += 1
    print(json.dumps(dict(histories=histories, prefix_checks=prefix_checks,
                         passing_prefixes=passing_prefixes,
                         mixed_controls=mixed_controls,
                         join_controls=join_controls), sort_keys=True))


if __name__ == '__main__':
    main()