verify_substitution_stable_restoration.py

#!/usr/bin/env python3
"""Construct selected finite stable summaries; no proof-assistant claim."""
from collections import deque
from itertools import permutations, product
from pathlib import Path
import json


class Group:
    def __init__(self, elements, identity, multiplication):
        self.elements = tuple(elements)
        self.identity = identity
        self.mul = multiplication
        self.inverse = {x: next(y for y in self.elements
                               if multiplication(x, y) == identity
                               and multiplication(y, x) == identity)
                        for x in self.elements}


def construct(group, alphabet, initial_evaluation, transforms, word_bound):
    positions = {a: i for i, a in enumerate(alphabet)}

    def evaluate(phi, word):
        value = group.identity
        for a in word:
            value = group.mul(value, phi[positions[a]])
        return value

    def substitute(word, h):
        return ''.join(h[a] for a in word)

    evaluations = [initial_evaluation]
    evaluation_set = {initial_evaluation}
    queue = deque(evaluations)
    while queue:
        phi = queue.popleft()
        for _, h, _ in transforms.values():
            child = tuple(evaluate(phi, h[a]) for a in alphabet)
            if child not in evaluation_set:
                evaluation_set.add(child)
                evaluations.append(child)
                queue.append(child)
    assert len(evaluations) <= len(group.elements) ** len(alphabet)
    evaluation_index = {phi: i for i, phi in enumerate(evaluations)}

    def summary(word):
        return tuple(evaluate(phi, word) for phi in evaluations)

    def push(state, a):
        return tuple(group.mul(value, phi[positions[a]])
                     for value, phi in zip(state, evaluations))

    def pop(state, a):
        return tuple(group.mul(value, group.inverse[phi[positions[a]]])
                     for value, phi in zip(state, evaluations))

    def boundary(state, data):
        u, h, v = data
        result = []
        for phi in evaluations:
            child = tuple(evaluate(phi, h[a]) for a in alphabet)
            index = evaluation_index[child]
            result.append(group.mul(group.mul(evaluate(phi, u), state[index]),
                                    evaluate(phi, v)))
        return tuple(result)

    initial = summary('')
    representatives = {initial: ''}
    queue = deque([initial])
    while queue:
        state = queue.popleft()
        for a in alphabet:
            nxt = push(state, a)
            if nxt not in representatives:
                representatives[nxt] = representatives[state] + a
                queue.append(nxt)

    inverse_entries = boundary_entries = 0
    for state, word in representatives.items():
        assert state == summary(word)
        for a in alphabet:
            assert pop(push(state, a), a) == state
            assert push(pop(state, a), a) == state
            assert pop(state, a) in representatives
            inverse_entries += 1
        for data in transforms.values():
            u, h, v = data
            nxt = boundary(state, data)
            assert nxt in representatives
            assert nxt == summary(u + substitute(word, h) + v)
            boundary_entries += 1

    # Independent word interpreter also checks collisions and legal undo.
    word_cases = 0
    for length in range(word_bound + 1):
        for letters in product(alphabet, repeat=length):
            word = ''.join(letters)
            state = summary(word)
            assert state in representatives
            if word:
                assert pop(state, word[-1]) == summary(word[:-1])
            for data in transforms.values():
                u, h, v = data
                assert boundary(state, data) == summary(u + substitute(word, h) + v)
            word_cases += 1

    return {
        'group_order': len(group.elements),
        'evaluation_orbit_size': len(evaluations),
        'reachable_summary_states': len(representatives),
        'all_push_inverse_entries_checked': inverse_entries,
        'all_boundary_entries_checked': boundary_entries,
        'transform_names': list(transforms),
        'raw_word_max_length': word_bound,
        'raw_words_checked': word_cases,
    }, summary


def horizon_check(r, word_bound, witness_max):
    modulus = 2 ** r

    def update(state, letter):
        n, bits = state
        bits = list(bits)
        if letter == 'a':
            for k in range(r + 1):
                if n % (2 ** k) == 0:
                    bits[k] ^= 1
        return ((n + 1) % modulus, tuple(bits))

    def undo(state, letter):
        n, bits = state
        n = (n - 1) % modulus
        bits = list(bits)
        if letter == 'a':
            for k in range(r + 1):
                if n % (2 ** k) == 0:
                    bits[k] ^= 1
        return (n, tuple(bits))

    table_entries = words = 0
    for n in range(modulus):
        for bits in product((0, 1), repeat=r + 1):
            state = (n, bits)
            for a in 'ab':
                assert undo(update(state, a), a) == state
                table_entries += 1
    for length in range(word_bound + 1):
        for letters in product('ab', repeat=length):
            word = ''.join(letters)
            state = (0, (0,) * (r + 1))
            for a in word:
                state = update(state, a)
            raw = word
            for k in range(r + 1):
                assert state[1][k] == raw.count('a') % 2
                raw = raw[::2]
            words += 1
    rows = []
    for j in range(witness_max + 1):
        raw = 'b' * (2 ** j) + 'a'
        observations = []
        for k in range(witness_max + 2):
            observations.append(raw.count('a') % 2)
            assert observations[-1] == int(k <= j)
            raw = raw[::2]
        rows.append(observations)
    return {'horizon': r, 'state_bound': modulus * 2 ** (r + 1),
            'all_append_inverse_entries': table_entries,
            'raw_word_max_length': word_bound, 'raw_words': words,
            'separating_family_max_j': witness_max,
            'separating_family_observations': rows,
            'scope': 'Finite corroboration only; no all-state-size impossibility proof.'}


def main():
    c2 = Group((0, 1), 0, lambda x, y: (x + y) % 2)
    identity = {'a': 'a', 'b': 'b'}
    swap = {'a': 'b', 'b': 'a'}
    fibonacci = {'a': 'ab', 'b': 'a'}
    erase_b = {'a': 'a', 'b': ''}
    transforms = {
        'swap': ('', swap, ''),
        'fibonacci': ('', fibonacci, ''),
        'erase_b': ('', erase_b, ''),
        'surround': ('ab', identity, 'a'),
    }
    minimal, _ = construct(c2, 'ab', (1, 0), {}, 6)
    refined, summary = construct(c2, 'ab', (1, 0), {'swap': transforms['swap']}, 9)
    expanded, _ = construct(c2, 'ab', (1, 0), transforms, 9)
    assert minimal['reachable_summary_states'] == 2
    assert refined['evaluation_orbit_size'] == 2
    assert refined['reachable_summary_states'] == 4
    assert len({summary(w) for w in ('', 'a', 'b', 'ab')}) == 4

    elements = tuple(permutations(range(3)))
    # Product is in reading order: first x, then y.
    s3 = Group(elements, (0, 1, 2), lambda x, y: tuple(y[x[i]] for i in range(3)))
    noncommutative, noncomm_summary = construct(
        s3, 'ab', ((1, 0, 2), (1, 2, 0)), transforms, 7)
    assert noncomm_summary('ab') != noncomm_summary('ba')

    # A minimal forward machine for ends-in-b fails the necessary test.
    last_b_updates = {'a': (0, 0), 'b': (1, 1)}
    assert any(len(set(update)) != 2 for update in last_b_updates.values())
    # Parity alone merges epsilon and b but swap separates their observations.
    assert ''.count('a') % 2 == 'b'.count('a') % 2
    assert ''.count('b') % 2 != 'b'.count('b') % 2
    result = {
        'scope': ('Finite evaluation-orbit construction and exhaustive checks of every '
                  'reachable table entry in the listed examples; independent raw-word '
                  'evaluation through the stated lengths. No proof assistant, infinite '
                  'word enumeration, nested-trace or scaffold generator is claimed.'),
        'parity_before_refinement': minimal,
        'parity_swap': refined,
        'parity_multiple_transforms': expanded,
        'noncommutative_S3': noncommutative,
        'four_observation_pairs_force_four_states': True,
        'last_b_minimal_machine_rejected': True,
        'decimation_horizons': horizon_check(3, 9, 9),
        'general_proof': 'Written finite-orbit and permutation argument in companion note.',
    }
    Path(__file__).with_name('substitution-stable-restoration-output.json').write_text(
        json.dumps(result, indent=2) + '\n')
    print(json.dumps(result, indent=2))


if __name__ == '__main__':
    main()