check_virtual_crease_causal_width.py

"""Finite checks for the virtual-crease causal-width note.

This is a regression instrument, not a proof.  Coordinates are doubled:
q = 2c = t + p.  A lattice track may hold or advance by one q-unit per
input step.
"""

from __future__ import annotations

from functools import lru_cache
from itertools import combinations, product
from math import ceil
from typing import Iterable

Event = tuple[int, int]  # (time, doubled crease coordinate q)
Config = tuple[int, ...]


def precedes(left: Event, right: Event) -> bool:
    """Whether one lattice track can serve left and then right."""

    t1, q1 = left
    t2, q2 = right
    return t1 <= t2 and 0 <= q2 - q1 <= t2 - t1


def transformed_precedes(left: Event, right: Event) -> bool:
    """The same order after (t,q) -> (q,t-q)."""

    t1, q1 = left
    t2, q2 = right
    return q1 <= q2 and t1 - q1 <= t2 - q2


def minimum_chain_cover(events: Iterable[Event]) -> int:
    """Minimum chain cover via maximum matching in the transitive DAG."""

    points = sorted(set(events))
    size = len(points)
    match_right = [-1] * size

    def augment(left_index: int, seen: set[int]) -> bool:
        for right_index in range(size):
            if left_index == right_index:
                continue
            if not precedes(points[left_index], points[right_index]):
                continue
            # Distinct simultaneous points are incomparable.  Identical points
            # were removed by set().
            if points[left_index][0] == points[right_index][0]:
                continue
            if right_index in seen:
                continue
            seen.add(right_index)
            if match_right[right_index] == -1 or augment(
                match_right[right_index], seen
            ):
                match_right[right_index] = left_index
                return True
        return False

    matching = sum(augment(i, set()) for i in range(size))
    return size - matching


def maximum_antichain_bruteforce(events: Iterable[Event]) -> int:
    points = sorted(set(events))
    for width in range(len(points), -1, -1):
        for subset in combinations(points, width):
            if all(
                not precedes(a, b) and not precedes(b, a)
                for a, b in combinations(subset, 2)
            ):
                return width
    return 0


def formed_comb_events(
    period: int,
    candidates: int,
    *,
    tail_length: int = 0,
    first_split: int = 0,
) -> set[Event]:
    """Head/next-axis service events for one already formed comb."""

    if period < 1 or candidates < 2:
        raise ValueError("need a positive period and at least two candidates")
    events: set[Event] = set()
    offset = tail_length - 1
    for j in range(candidates - 1):
        time = first_split + j * period
        head_q = offset + j * period
        events.add((time, head_q))
        events.add((time, head_q + period))
    return events


def reachable(parent: Config, child: Config) -> bool:
    """Sorted noncrossing matching of labeled unit-speed tracks."""

    return len(parent) == len(child) and all(
        new - old in (0, 1) for old, new in zip(parent, child)
    )


def next_configs(config: Config) -> tuple[Config, ...]:
    return tuple(
        sorted(
            {
                tuple(sorted(old + step for old, step in zip(config, moves)))
                for moves in product((0, 1), repeat=len(config))
            }
        )
    )


def binary_late_fan_is_feasible(depth: int, tracks: int) -> bool:
    """Exact bounded search for leaf demand q = binary_value(history).

    The common root configuration is freely chosen.  No demand is made before
    the leaf.  The finite root search range is exact: a useful root track must
    start between min(target)-depth and max(target).
    """

    if depth < 0 or tracks < 0:
        raise ValueError
    targets = range(2**depth)
    root_values = range(-depth, max(targets, default=0) + 1)

    @lru_cache(maxsize=None)
    def feasible(prefix: tuple[int, ...], config: Config) -> bool:
        if len(prefix) == depth:
            target = sum(bit << (depth - 1 - i) for i, bit in enumerate(prefix))
            return target in config
        children = next_configs(config)
        return all(
            any(feasible(prefix + (bit,), child) for child in children)
            for bit in (0, 1)
        )

    for root in combinations(root_values, tracks):
        if feasible((), tuple(root)):
            return True
    return False


def exact_late_fan_demand(depth: int) -> int:
    for tracks in range(1, 2**depth + 1):
        if binary_late_fan_is_feasible(depth, tracks):
            return tracks
    raise AssertionError("one pre-positioned track per target must work")


def spaced_selector_capacity_checks(max_depth: int) -> int:
    """Check the load-bearing capacity lemma for Theorem 3.

    At selector depth r, targets are separated by r + 1.  A track's entire
    r-step reachable interval must therefore contain at most one target.
    Holding one track at each target supplies the matching upper bound.
    """

    cases = 0
    for depth in range(1, max_depth + 1):
        targets = tuple((depth + 1) * value for value in range(2**depth))
        for root in range(-depth, targets[-1] + 1):
            reachable_targets = [
                target for target in targets if root <= target <= root + depth
            ]
            assert len(reachable_targets) <= 1
            cases += 1

        # The matching upper-bound policy: one track holds at each target.
        assert len(set(targets)) == 2**depth
    return cases


def run_checks() -> dict[str, object]:
    # Coordinate-change identity.
    comparisons = 0
    for t1 in range(5):
        for t2 in range(5):
            for q1 in range(-3, 6):
                for q2 in range(-3, 6):
                    assert precedes((t1, q1), (t2, q2)) == transformed_precedes(
                        (t1, q1), (t2, q2)
                    )
                    comparisons += 1

    # Dilworth equality on every subset of a small event box.
    universe = [(t, q) for t in range(3) for q in range(3)]
    subsets = 0
    for mask in range(1 << len(universe)):
        events = [universe[i] for i in range(len(universe)) if mask & (1 << i)]
        assert minimum_chain_cover(events) == maximum_antichain_bruteforce(events)
        subsets += 1

    # Every formed comb in this finite range has exact width two.
    combs = 0
    for period in range(1, 7):
        for candidates in range(2, 10):
            events = formed_comb_events(period, candidates)
            assert minimum_chain_cover(events) == 2
            combs += 1

    # Exact small causal demands for the binary late-choice fan.
    exact = {depth: exact_late_fan_demand(depth) for depth in range(1, 5)}
    for depth, demand in exact.items():
        assert demand >= ceil((2**depth) / (depth + 1))
        assert demand <= 2**depth

    spaced_cases = spaced_selector_capacity_checks(10)

    return {
        "coordinate_comparisons": comparisons,
        "event_subsets": subsets,
        "formed_combs": combs,
        "packed_late_fan_exact_small": exact,
        "spaced_selector_capacity_cases": spaced_cases,
        "violations": 0,
    }


if __name__ == "__main__":
    print(run_checks())