verify_selection_spectrum.py

#!/usr/bin/env python3
"""Bounded audit for FPRD-T169's nested selector-family identities."""

from __future__ import annotations

import itertools
import json
from pathlib import Path


MAX_HORIZON = 3
SELECTORS = (0, 1)  # one-state selectors on a unary observed alphabet
FAMILIES = {
    1: ((0,), (1,)),
    2: ((0,), (1,), (0, 1)),
}


def offsets():
    """Bit offsets for all tagged unary words through MAX_HORIZON."""
    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 = 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_through(mask, family, horizon):
    for length in range(horizon + 1):
        selected = any(accepts(mask, length, (tag,) * length) for tag in family)
        if selected != projected_accepts(mask, length):
            return False
    return True


def candidate_sets(mask, budget):
    return tuple(
        frozenset(
            family
            for family in FAMILIES[budget]
            if family_covers_through(mask, family, horizon)
        )
        for horizon in range(MAX_HORIZON + 1)
    )


def audit():
    relation_count = 1 << TAGGED_WORDS
    nested_checks = 0
    intersection_checks = 0
    upward_checks = 0
    finite_escape_checks = 0
    strict_escape_examples = 0

    for mask in range(relation_count):
        by_budget = {budget: candidate_sets(mask, budget) for budget in FAMILIES}

        for budget, horizons in by_budget.items():
            for left, right in zip(horizons, horizons[1:]):
                assert right <= left
                nested_checks += 1

            assert set.intersection(*(set(item) for item in horizons)) == set(
                horizons[-1]
            )
            intersection_checks += 1

            if not horizons[-1]:
                first_failure = next(i for i, item in enumerate(horizons) if not item)
                assert all(not item for item in horizons[first_failure:])
                finite_escape_checks += 1
                if first_failure > 0:
                    strict_escape_examples += 1

        for horizon in range(MAX_HORIZON + 1):
            feasible_one = bool(by_budget[1][horizon])
            feasible_two = bool(by_budget[2][horizon])
            assert not feasible_one or feasible_two
            upward_checks += 1

    return {
        "relations": relation_count,
        "tagged_words": TAGGED_WORDS,
        "nested_candidate_set_checks": nested_checks,
        "finite_intersection_checks": intersection_checks,
        "resource_upward_checks": upward_checks,
        "finite_escape_checks": finite_escape_checks,
        "strict_positive_escape_examples": strict_escape_examples,
    }


def labeled_mealy_count(states, input_letters, output_choices):
    return (states * output_choices) ** (states * input_letters)


def main():
    counts = audit()
    assert labeled_mealy_count(1, 1, 2) == 2
    assert labeled_mealy_count(2, 1, 2) == 16
    assert labeled_mealy_count(2, 2, 2) == 256

    output = {
        "status": "pass",
        "scope": (
            "finite truncated audit of nested selector-family sets, resource "
            "upward closure, and finite escape"
        ),
        "model": {
            "observed_alphabet": "unary",
            "hidden_tags": 2,
            "selector_states": 1,
            "max_horizon": MAX_HORIZON,
            "selector_budgets": [1, 2],
        },
        **counts,
        "labeled_mealy_counts": {
            "unary_input_one_state": 2,
            "unary_input_two_states": 16,
            "binary_input_two_states": 256,
        },
        "theorem_identity": "Sel(A,pi) = intersection_n Sel_n(A,pi)",
        "does_not_verify": [
            "the infinite compactness theorem beyond the finite model",
            "computability or a closed-form bound for the escape modulus",
            "FPRD-T91's visible-lift construction",
            "the persistent-stack compiler",
            "Kim-Park Theorem 4.19 or its Lean artifact",
        ],
    }
    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()