#!/usr/bin/env python3
"""Independent review of two quotient-result families.

This standard-library-only checker reconstructs the intersecting-core
decomposition and the two-occurrence shuffle witness without importing the
research implementations.
"""

from __future__ import annotations

import itertools
import json
from collections import Counter
from functools import lru_cache


def subsets(items):
    items = tuple(items)
    for mask in range(1 << len(items)):
        yield tuple(items[i] for i in range(len(items)) if mask >> i & 1)


def is_matching(family):
    used = 0
    for support in family:
        if used & support:
            return False
        used |= support
    return True


def disjointness_adjacency(family):
    adjacency = [0] * len(family)
    for i, left in enumerate(family):
        for j in range(i + 1, len(family)):
            if not left & family[j]:
                adjacency[i] |= 1 << j
                adjacency[j] |= 1 << i
    return adjacency


def minimum_vertex_cover(adjacency):
    @lru_cache(maxsize=None)
    def solve(active):
        for u, neighbors0 in enumerate(adjacency):
            neighbors = neighbors0 & active
            if active & (1 << u) and neighbors:
                vbit = neighbors & -neighbors
                left = (1 << u) | solve(active & ~(1 << u))
                right = vbit | solve(active & ~vbit)
                return left if left.bit_count() <= right.bit_count() else right
        return 0

    return solve((1 << len(adjacency)) - 1)


def matching_histogram(family):
    return Counter(len(choice) for choice in subsets(family) if is_matching(choice))


def factored_histogram(family, cover):
    exceptional = [s for i, s in enumerate(family) if cover >> i & 1]
    core = [s for i, s in enumerate(family) if not (cover >> i & 1)]
    assert all(a & b for i, a in enumerate(core) for b in core[i + 1 :])
    histogram = Counter()
    for choice in subsets(exceptional):
        if not is_matching(choice):
            continue
        histogram[len(choice)] += 1
        used = 0
        for support in choice:
            used |= support
        histogram[len(choice) + 1] += sum(not (used & support) for support in core)
    return histogram


def audit_intersecting_cores():
    universe = tuple(range(1, 16))  # all nonempty supports on four participants
    families = matching_states = strict_improvements = 0
    for size in range(8):
        for family in itertools.combinations(universe, size):
            cover = minimum_vertex_cover(disjointness_adjacency(family))
            direct = matching_histogram(family)
            assert direct == factored_histogram(family, cover)
            maximum_intersecting = len(family) - cover.bit_count()
            assert maximum_intersecting == max(
                len(choice)
                for choice in subsets(family)
                if all(a & b for i, a in enumerate(choice) for b in choice[i + 1 :])
            )
            degrees = [sum(bool(s & (1 << x)) for s in family) for x in range(4)]
            gamma = len(family) - max(degrees, default=0)
            assert cover.bit_count() <= gamma
            strict_improvements += cover.bit_count() < gamma
            families += 1
            matching_states += sum(direct.values())
    return {
        "families_of_size_at_most_7": families,
        "matching_states": matching_states,
        "strict_improvements_over_diversity": strict_improvements,
        "direct_vs_factored": "exact",
        "minimum_complement_equals_vertex_cover": "exact",
    }


def normalize(vector, q):
    for value in vector:
        if value % q:
            inverse = pow(value, -1, q)
            return tuple((entry * inverse) % q for entry in vector)
    raise ValueError("zero vector")


def audit_projective_planes():
    rows = []
    for q in (2, 3, 5):
        points = sorted({
            normalize(v, q)
            for v in itertools.product(range(q), repeat=3)
            if any(v)
        })
        lines = []
        for coefficients in points:
            line = frozenset(
                i for i, point in enumerate(points)
                if sum(a * b for a, b in zip(coefficients, point)) % q == 0
            )
            lines.append(line)
        assert len(points) == len(lines) == q * q + q + 1
        assert all(len(line) == q + 1 for line in lines)
        assert all(len(a & b) == 1 for i, a in enumerate(lines) for b in lines[i + 1 :])
        degrees = [sum(i in line for line in lines) for i in range(len(points))]
        assert set(degrees) == {q + 1}
        rows.append({"q": q, "supports": len(lines), "gamma": q * q, "kappa": 0})
    return rows


def quotient_edges(source, mapping):
    return {
        letter: {
            (mapping[start], mapping[end])
            for start, ends in transitions.items()
            for end in ends
        }
        for letter, transitions in source.items()
    }


def audit_two_occurrence_shuffle():
    # States 0,A,B,C are numbered 0,1,2,3; target eps,X,Y are 0,1,2.
    source = {
        "a": {0: {1}, 1: {1}, 2: {3}, 3: {3}},
        "b": {0: {2}, 1: {3}, 2: {2}, 3: {3}},
    }
    target = {
        "a": {(0, 1), (1, 1), (2, 1)},
        "b": {(0, 2), (1, 2), (2, 2)},
    }
    candidates = exact = 0
    witnesses = []
    for tail in itertools.product((0, 1, 2), repeat=3):
        mapping = (0,) + tail
        if set(mapping) != {0, 1, 2}:
            continue
        candidates += 1
        if quotient_edges(source, mapping) == target:
            exact += 1
            witnesses.append(mapping)
    assert candidates == 12 and exact == 0
    assert source["a"][3] == {3} and source["b"][3] == {3}
    assert all((state, state) not in target["a"] or (state, state) not in target["b"] for state in range(3))
    return {
        "source_states": 4,
        "target_states": 3,
        "surjective_initial_preserving_maps": candidates,
        "exact_quotient_maps": exact,
        "mixed_loop_source_state": 3,
        "target_mixed_loop_states": 0,
        "minimum_nonempty_operand_occurrences": 2,
        "witness_occurrences": 2,
    }


def main():
    result = {
        "schema": "fprd.result-review.kernel-minimal-shuffle.v1",
        "status": "pass_with_scope_corrections",
        "intersecting_core": audit_intersecting_cores(),
        "projective_plane_controls": audit_projective_planes(),
        "two_occurrence_shuffle": audit_two_occurrence_shuffle(),
        "scope": [
            "kappa is optimal only within the supplied intersecting-core decomposition",
            "the negative witness is occurrence-minimal among shuffles with two nonempty operands",
            "finite checks corroborate but do not replace the general proofs",
        ],
    }
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()