verify_paired_retraction_pumping.py

#!/usr/bin/env python3
"""Finite calibration for the paired-retraction pumping theorem."""

import itertools
import json
from pathlib import Path


def maps(size):
    return tuple(itertools.product(range(size), repeat=size))


def apply_power(function, state, exponent):
    for _ in range(exponent):
        state = function[state]
    return state


def orbit(function, initial):
    result = []
    state = initial
    while state not in result:
        result.append(state)
        state = function[state]
    return tuple(result)


def main():
    function_triples = valid_certificates = orbit_law_checks = 0
    pumped_endpoint_checks = suffix_checks = 0

    for size in range(1, 4):
        functions = maps(size)
        for forward in functions:
            for middle in functions:
                for retract in functions:
                    function_triples += 1
                    for initial in range(size):
                        points = orbit(forward, initial)
                        law_holds = True
                        for parameter in points:
                            lhs = retract[middle[forward[parameter]]]
                            rhs = middle[parameter]
                            orbit_law_checks += 1
                            if lhs != rhs:
                                law_holds = False
                        if not law_holds:
                            continue

                        valid_certificates += 1
                        baseline = middle[initial]
                        for copies in range(9):
                            parameter = apply_power(forward, initial, copies)
                            endpoint = apply_power(retract, middle[parameter], copies)
                            assert endpoint == baseline
                            pumped_endpoint_checks += 1
                            for suffix in functions:
                                assert suffix[endpoint] == suffix[baseline]
                                suffix_checks += 1

    # Checking the cancellation law only at the initial parameter is not
    # enough. It holds at 0, but the two-copy sandwich ends at 2.
    forward = (1, 2, 2)
    middle = (0, 1, 2)
    retract = (0, 0, 2)
    assert retract[middle[forward[0]]] == middle[0]
    two_copy_parameter = apply_power(forward, 0, 2)
    two_copy_endpoint = apply_power(retract, middle[two_copy_parameter], 2)
    assert two_copy_endpoint == 2 != middle[0]

    result = {
        "status": "pass",
        "scope": "all transformation triples on carrier sets through size three",
        "function_triples": function_triples,
        "valid_orbit_certificates": valid_certificates,
        "orbit_law_checks": orbit_law_checks,
        "pumped_endpoint_checks": pumped_endpoint_checks,
        "arbitrary_suffix_checks": suffix_checks,
        "base_only_counterexample": {
            "forward": forward,
            "middle": middle,
            "retract": retract,
            "one_copy_law_holds": True,
            "two_copy_endpoint": two_copy_endpoint,
            "baseline_endpoint": middle[0],
        },
        "does_not_verify": [
            "recurrence of a paired-retraction certificate in every long run",
            "a finite parameterization for unrestricted scaffolding automata",
            "the infinite theorem beyond the enumerated finite carriers",
        ],
    }
    output = json.dumps(result, indent=2) + "\n"
    Path(__file__).with_name("paired-retraction-checker-output.json").write_text(output)
    print(output, end="")


if __name__ == "__main__":
    main()