verify_destructor_separation.py

#!/usr/bin/env python3
"""Finite calibration for the destructor-separation obstruction."""

import itertools
import json
from pathlib import Path


def all_preorders(size):
    pairs = tuple(itertools.product(range(size), repeat=2))
    result = []
    for bits in range(1 << len(pairs)):
        relation = {(x, y) for index, (x, y) in enumerate(pairs) if bits & (1 << index)}
        if any((x, x) not in relation for x in range(size)):
            continue
        if any(
            (x, z) not in relation
            for x in range(size)
            for y in range(size)
            for z in range(size)
            if (x, y) in relation and (y, z) in relation
        ):
            continue
        result.append(frozenset(relation))
    return tuple(result)


def trace_classes(observation, destructors):
    classes = tuple(observation)
    while True:
        signatures = tuple(
            (observation[state], tuple(classes[action[state]] for action in destructors))
            for state in range(len(observation))
        )
        names = {}
        refined = tuple(names.setdefault(signature, len(names)) for signature in signatures)
        if refined == classes:
            return classes
        classes = refined


def main():
    preorder_count = systems = candidate_orders = comparable_pairs = 0
    quotient_checks = strict_collapse_systems = 0

    for size in range(1, 5):
        preorders = all_preorders(size)
        preorder_count += len(preorders)
        functions = tuple(itertools.product(range(size), repeat=size))
        destructor_arity = 2 if size <= 3 else 1
        for destructors in itertools.product(functions, repeat=destructor_arity):
            for observation in itertools.product(range(2), repeat=size):
                systems += 1
                classes = trace_classes(observation, destructors)
                if len(set(classes)) == size:
                    strict_collapse_systems += 1
                for relation in preorders:
                    if any(observation[x] != observation[y] for x, y in relation):
                        continue
                    if any(
                        (action[x], action[y]) not in relation
                        for action in destructors
                        for x, y in relation
                    ):
                        continue
                    candidate_orders += 1
                    for x, y in relation:
                        comparable_pairs += 1
                        assert classes[x] == classes[y]
                        quotient_checks += 1

    result = {
        "status": "pass",
        "scope": "all binary-observation systems through four states; two destructors through three states",
        "preorders": preorder_count,
        "observation_destructor_systems": systems,
        "observation_preserving_monotone_orders": candidate_orders,
        "comparable_pairs_checked": comparable_pairs,
        "quotient_containment_checks": quotient_checks,
        "fully_separating_systems": strict_collapse_systems,
        "does_not_verify": [
            "existence or nonexistence of a WQO using coarser scaffold observations",
            "monotonicity of whole scaffold input steps without monotone port probes",
            "the infinite theorem beyond the enumerated finite systems",
        ],
    }
    output = json.dumps(result, indent=2) + "\n"
    Path(__file__).with_name("destructor-separation-checker-output.json").write_text(output)
    print(output, end="")


if __name__ == "__main__":
    main()