verify_selection_obstructions.py

#!/usr/bin/env python3
"""Bounded obstruction-duality audit for FPRD-T171."""

from __future__ import annotations

import itertools
import json
import math
from collections import Counter
from pathlib import Path


MAX_HORIZON = 3
SELECTORS = (0, 1)  # constant-tag selectors for a unary observed alphabet
FAMILIES = {
    1: ((0,), (1,)),
    2: ((0,), (1,), (0, 1)),
}


def tagged_offsets():
    result = {}
    cursor = 0
    for length in range(MAX_HORIZON + 1):
        for tags in itertools.product((0, 1), repeat=length):
            result[(length, tags)] = cursor
            cursor += 1
    return result, cursor


OFFSETS, TAGGED_WORDS = tagged_offsets()


def accepts(mask, length, tags):
    return bool(mask & (1 << OFFSETS[(length, tags)]))


def projected_accepts(mask, length):
    return any(
        accepts(mask, length, tags)
        for tags in itertools.product((0, 1), repeat=length)
    )


def family_covers_word(mask, family, length):
    if not projected_accepts(mask, length):
        return True
    return any(accepts(mask, length, (tag,) * length) for tag in family)


def minimum_obstructions(mask, families):
    accepted = tuple(
        length
        for length in range(MAX_HORIZON + 1)
        if projected_accepts(mask, length)
    )
    failures = {
        length: frozenset(
            index
            for index, family in enumerate(families)
            if not family_covers_word(mask, family, length)
        )
        for length in accepted
    }
    universe = frozenset(range(len(families)))

    candidates = []
    for size in range(len(accepted) + 1):
        for words in itertools.combinations(accepted, size):
            covered = frozenset().union(*(failures[w] for w in words)) if words else frozenset()
            if covered == universe:
                candidates.append(words)
    if not candidates:
        return None, None
    minimum_cardinality = min(candidates, key=lambda words: (len(words), max(words, default=0), words))
    minimum_radius = min(candidates, key=lambda words: (max(words, default=0), len(words), words))
    return minimum_cardinality, minimum_radius


def first_escape(mask, families):
    for horizon in range(MAX_HORIZON + 1):
        if not any(
            all(family_covers_word(mask, family, length) for length in range(horizon + 1))
            for family in families
        ):
            return horizon
    return None


def mealy_count(max_states, input_letters, fiber_sizes):
    fiber_product = math.prod(fiber_sizes)
    return sum(
        states ** (states * input_letters) * fiber_product**states
        for states in range(1, max_states + 1)
    )


def family_bound(machine_count, max_family_size):
    return sum(
        math.comb(machine_count, size)
        for size in range(1, min(max_family_size, machine_count) + 1)
    )


def audit():
    relation_count = 1 << TAGGED_WORDS
    obstruction_instances = 0
    exact_radius_checks = 0
    cardinality_bound_checks = 0
    duality_checks = 0
    size_distribution = Counter()

    for mask in range(relation_count):
        for budget, families in FAMILIES.items():
            witness, radius_witness = minimum_obstructions(mask, families)
            escape = first_escape(mask, families)
            assert (witness is None) == (escape is None)
            duality_checks += 1

            if witness is not None:
                obstruction_instances += 1
                assert len(witness) <= len(families)
                cardinality_bound_checks += 1
                assert max(radius_witness, default=0) == escape
                exact_radius_checks += 1
                size_distribution[len(witness)] += 1

    return {
        "relations": relation_count,
        "tagged_words": TAGGED_WORDS,
        "duality_checks": duality_checks,
        "obstruction_instances": obstruction_instances,
        "cardinality_bound_checks": cardinality_bound_checks,
        "exact_escape_radius_checks": exact_radius_checks,
        "obstruction_size_distribution": dict(sorted(size_distribution.items())),
    }


def main():
    unary_s1 = mealy_count(1, 1, (2,))
    unary_s2 = mealy_count(2, 1, (2,))
    binary_s2 = mealy_count(2, 2, (2, 2))
    assert (unary_s1, unary_s2, binary_s2) == (2, 18, 260)
    assert family_bound(unary_s2, 2) == 171
    assert family_bound(binary_s2, 2) == 33930

    output = {
        "status": "pass",
        "scope": "finite truncated failure-set duality and obstruction-radius audit",
        "model": {
            "observed_alphabet": "unary",
            "hidden_tags": 2,
            "selector_states": 1,
            "selector_budgets": [1, 2],
            "max_horizon": MAX_HORIZON,
        },
        **audit(),
        "labeled_selector_counts": {
            "unary_at_most_one_state": unary_s1,
            "unary_at_most_two_states": unary_s2,
            "binary_at_most_two_states": binary_s2,
        },
        "two_selector_family_bounds": {
            "unary_at_most_two_states": family_bound(unary_s2, 2),
            "binary_at_most_two_states": family_bound(binary_s2, 2),
        },
        "theorem_identity": "escape length = minimum obstruction radius",
        "does_not_verify": [
            "computability of obstruction suites for arbitrary languages",
            "tightness of the labeled-machine cardinality bound",
            "word-length bounds for the Kim-Park visible lift",
            "FPRD-T168's imported external separation premise",
        ],
    }
    Path(__file__).with_name("checker-output.json").write_text(
        json.dumps(output, indent=2) + "\n", encoding="utf-8"
    )
    print(json.dumps(output, indent=2))


if __name__ == "__main__":
    main()