#!/usr/bin/env python3
"""Exhaustive labelled binary-DFA diagnostics for the degree-transport lemma.

Runs without third-party libraries. Enumerates every pair of maps for n<=4,
filters strong connectivity and synchronization by an independent pair BFS,
then computes the maximum corank reachable in <=n-1 letters by subset BFS.
Finite verification is a diagnostic, not a proof of the universal theorem.
"""

from collections import deque
from itertools import combinations, product
import argparse
import json
from pathlib import Path


def strongly_connected(generators, n):
    for q in range(n):
        seen = {q}
        todo = [q]
        for x in todo:
            for g in generators:
                y = g[x]
                if y not in seen:
                    seen.add(y)
                    todo.append(y)
        if len(seen) < n:
            return False
    return True


def pair_distances(generators, n, pairs, pair_index):
    reverse = [[] for _ in pairs]
    distances = [None] * len(pairs)
    todo = deque()
    for i, (x, y) in enumerate(pairs):
        for g in generators:
            gx, gy = g[x], g[y]
            if gx == gy:
                if distances[i] is None:
                    distances[i] = 1
                    todo.append(i)
            else:
                target = pair_index[tuple(sorted((gx, gy)))]
                reverse[target].append(i)
    while todo:
        j = todo.popleft()
        for i in reverse[j]:
            if distances[i] is None:
                distances[i] = distances[j] + 1
                todo.append(i)
    return distances


def cheap_corank(generators, n):
    initial = (1 << n) - 1
    seen = {initial}
    todo = deque([(initial, 0)])
    largest = 0
    while todo:
        subset, length = todo.popleft()
        largest = max(largest, n - subset.bit_count())
        if length == n - 1:
            continue
        for g in generators:
            image = 0
            for q in range(n):
                if subset >> q & 1:
                    image |= 1 << g[q]
            if image not in seen:
                seen.add(image)
                todo.append((image, length + 1))
    return largest


def verify(n):
    pairs = list(combinations(range(n), 2))
    pair_index = {pair: i for i, pair in enumerate(pairs)}
    functions = list(product(range(n), repeat=n))
    tested = horizons = 0
    for a in functions:
        for b in functions:
            generators = (a, b)
            if not strongly_connected(generators, n):
                continue
            distances = pair_distances(generators, n, pairs, pair_index)
            if any(distance is None for distance in distances):
                continue
            # A complete DFA synchronizes iff every pair can be merged.
            tested += 1
            largest = cheap_corank(generators, n)

            def degrees(t):
                values = [0] * n
                for (x, y), distance in zip(pairs, distances):
                    if distance <= t:
                        values[x] += 1
                        values[y] += 1
                return values

            for t in range(max(distances) + 1):
                bound = max(degrees(t)) - min(degrees(t + n - 1))
                assert largest >= bound, {
                    "n": n, "a": a, "b": b, "D": largest,
                    "t": t, "claimed_lower_bound": bound,
                }
                horizons += 1
    return {
        "n": n,
        "strongly_connected_synchronizing_binary_automata": tested,
        "transport_horizons_checked": horizons,
        "counterexamples": 0,
    }


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--max-n", type=int, default=4)
    parser.add_argument("--output", type=Path)
    args = parser.parse_args()
    if args.max_n < 2 or args.max_n > 4:
        parser.error("Use 2<=--max-n<=4; n=5 has 9,765,625 labelled map pairs.")
    results = []
    for n in range(2, args.max_n + 1):
        result = verify(n)
        print(json.dumps(result), flush=True)
        results.append(result)
    if args.output:
        args.output.write_text(json.dumps(results, indent=2) + "\n")


if __name__ == "__main__":
    main()