check_unary_guards.py

#!/usr/bin/env python3
"""Finite audit for Run 10's unary guard and terminal claims.

The exhaustive component checks small unary histories.  It is a falsifier for
the local claims, not a proof of the parameter-uniform coherence theorem.  The
general argument and its dependency boundary are recorded in run-10.md.
"""

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


MISSING = "M"
SELF = "S"
EPSILON = "E"
ZERO = "0"
DESCRIPTORS = (MISSING, SELF, EPSILON, ZERO)
BASE_LABEL = -1


def histories(length, labels):
    rows = tuple(product(labels, DESCRIPTORS))
    return product(rows, repeat=length)


def replay(history):
    edges = [None]
    for node, (_, descriptor) in enumerate(history, start=1):
        if descriptor == MISSING:
            endpoint = None
        elif descriptor == SELF:
            endpoint = node
        elif descriptor == EPSILON:
            endpoint = node - 1
        else:
            endpoint = edges[node - 1]
        edges.append(endpoint)
    return tuple(edges)


def rooted_figure(history, root=None):
    edges = replay(history)
    node = len(history) if root is None else root
    word = []
    while node is not None:
        word.append(BASE_LABEL if node == 0 else history[node - 1][0])
        endpoint = edges[node]
        if endpoint == node:
            while len(word) >= 2 and word[-2] == word[-1]:
                word.pop()
            return tuple(word), SELF
        node = endpoint
    return tuple(word), MISSING


def strong_trace(history):
    return tuple(rooted_figure(history[:length]) for length in range(1, len(history) + 1))


def terminal_kind(history):
    edges = replay(history)
    node = len(history)
    while True:
        if node == 0:
            return "base"
        endpoint = edges[node]
        if endpoint is None:
            return "missing"
        if endpoint == node:
            return "recursive"
        node = endpoint


def causal_support(history):
    edges = replay(history)
    node = len(history)
    labels = set()
    descriptors = set()
    while node is not None and node > 0:
        labels.add(node - 1)
        descriptors.add(node - 1)
        endpoint = edges[node]
        if endpoint == node:
            break
        node = endpoint
    work = list(descriptors)
    while work:
        index = work.pop()
        if history[index][1] != ZERO or index == 0:
            continue
        predecessor = index - 1
        if predecessor not in descriptors:
            descriptors.add(predecessor)
            work.append(predecessor)
    return frozenset(labels), frozenset(descriptors)


def changed_descriptor(history, index, descriptor):
    target = list(history)
    target[index] = (target[index][0], descriptor)
    return tuple(target)


def audit_history(history, labels, totals):
    edges = replay(history)
    source_trace = strong_trace(history)
    source_figure = rooted_figure(history)
    source_terminal = terminal_kind(history)
    label_support, descriptor_support = causal_support(history)
    totals["histories"] += 1
    totals[f"terminal_{source_terminal}"] += 1

    # D uses physical endpoint equality, not behavioral equality alone.
    for index, (_, descriptor) in enumerate(history):
        for alternate in DESCRIPTORS:
            if alternate == descriptor:
                continue
            target = changed_descriptor(history, index, alternate)
            if replay(target)[index + 1] != edges[index + 1]:
                continue
            assert strong_trace(target) == source_trace
            assert terminal_kind(target) == source_terminal
            totals["detours"] += 1

    # A is the strong-trace-preserving replacement by fresh SELF.  Its
    # elementary guard additionally requires the old target itself to loop.
    for index, (_, descriptor) in enumerate(history):
        if descriptor == SELF:
            continue
        target = changed_descriptor(history, index, SELF)
        if strong_trace(target) != source_trace:
            continue
        old_target = edges[index + 1]
        if old_target is None or old_target == index + 1:
            continue
        if edges[old_target] == old_target:
            assert rooted_figure(history, old_target)[1] == SELF
            assert terminal_kind(target) == source_terminal
            totals["literal_absorptions"] += 1
        elif rooted_figure(history, old_target)[1] == SELF:
            totals["behavioral_recursive_but_not_literal"] += 1

    # T cannot use the unlabelled base as its lower candidate carrier: left
    # starts at one, so x is always an actual labelled row.
    for left in range(1, len(history) - 1):
        pair = history[left][1], history[left + 1][1]
        if pair not in ((EPSILON, ZERO), (ZERO, EPSILON)):
            continue
        if history[left - 1][0] != history[left][0]:
            continue
        target = list(history)
        target[left] = (target[left][0], pair[1])
        target[left + 1] = (target[left + 1][0], pair[0])
        target = tuple(target)
        assert left >= 1
        assert rooted_figure(target) == source_figure
        assert terminal_kind(target) == source_terminal
        totals["temporal_slides"] += 1
        if strong_trace(target) != source_trace:
            totals["slides_changing_prefix_trace"] += 1

    # G changes only unsupported coordinates and preserves replay support.
    for index, (label, descriptor) in enumerate(history):
        if index not in label_support:
            for alternate in labels:
                if alternate == label:
                    continue
                target = list(history)
                target[index] = (alternate, descriptor)
                target = tuple(target)
                assert causal_support(target) == (label_support, descriptor_support)
                assert rooted_figure(target) == source_figure
                assert terminal_kind(target) == source_terminal
                totals["garbage_label_changes"] += 1
        if index not in descriptor_support:
            for alternate in DESCRIPTORS:
                if alternate == descriptor:
                    continue
                target = changed_descriptor(history, index, alternate)
                assert causal_support(target) == (label_support, descriptor_support)
                assert rooted_figure(target) == source_figure
                assert terminal_kind(target) == source_terminal
                totals["garbage_descriptor_changes"] += 1


def carrier_rectangles():
    checks = 0
    for n in range(1, 13):
        for m in range(1, n + 1):
            ordinary = tuple(product(range(n - m + 1), repeat=m - 1))
            weak_ordinary = sum(all(row[i] <= row[i + 1] for i in range(len(row) - 1)) for row in ordinary)
            assert weak_ordinary == comb(n - 1, m - 1)
            checks += 1
            if m <= n - 1:
                recursive = tuple(product(range(n - m), repeat=m - 1))
                weak_recursive = sum(all(row[i] <= row[i + 1] for i in range(len(row) - 1)) for row in recursive)
                assert weak_recursive == comb(n - 2, m - 1)
                checks += 1
    return {
        "parameter_pairs": checks,
        "ordinary_first_retained_time": 1,
        "recursive_first_retained_time": 2,
        "recursive_zero_carrier_case_is_singleton": True,
    }


def statement_markers():
    root = Path(__file__).resolve().parents[2]
    objects = root / "research-artifacts/scaffold-proof-review/history/objects"
    unary = (objects / "f125f710bd20360eaa12313d69da99c080c014ea4cd4b60d6d7cac897c6d463f.txt").read_text()
    causal = (objects / "2b0910f423c0a56136a7d1c293c57ff5f6361ee40bf5d777aa4d1da7aaaae716.txt").read_text()
    checks = {
        "unlabelled_base_explicit": "distinguished unlabelled base at" in unary,
        "literal_guard_explicit": "Literal physical self-looping matters" in unary,
        "temporal_label_guard_explicit": "candidate carrier labels agree" in unary,
        "causal_support_explicit": "least replay-closed" in unary,
        "three_terminal_cases_explicit": "ordinary missing or base terminal" in unary and "recursive terminal" in unary,
        "recursive_time_one_exclusion_explicit": "time $1$ is unavailable" in unary,
        "causal_full_behavior_present": "equal unfoldings" in causal and "bisimilar" in causal,
    }
    assert all(checks.values())
    return checks


totals = Counter()
for labels, maximum in (((0,), 8), ((0, 1), 5)):
    for length in range(1, maximum + 1):
        for history in histories(length, labels):
            audit_history(history, labels, totals)

assert totals["literal_absorptions"] > 0
assert totals["behavioral_recursive_but_not_literal"] > 0
assert totals["temporal_slides"] > 0
assert totals["slides_changing_prefix_trace"] > 0

result = {
    "status": "pass",
    "exhaustive_small_histories": dict(sorted(totals.items())),
    "carrier_rectangles": carrier_rectangles(),
    "statement_markers": statement_markers(),
    "proved_boundary": {
        "D_uses_physical_endpoint_equality": True,
        "A_requires_a_literal_old_self_loop": True,
        "G_uses_replay_closed_causal_irrelevance": True,
        "T_uses_equal_labelled_carriers_and_may_change_prefixes": True,
        "T_cannot_cross_the_unlabelled_base": True,
        "terminal_kind_is_preserved_by_every_move": True,
        "recursive_termination_reserves_one_extra_time_row": True,
        "full_behavior_not_same_radius_identity_is_inherited": True,
    },
    "scope": "Finite falsification plus exact source markers; the uniform coherence proof is argued in Run 10 and the paper.",
}

print(json.dumps(result, indent=2, sort_keys=True))