#!/usr/bin/env python3
"""Independent finite review of the diversity kernel and two-block compiler.

The implementation intentionally does not import the research checkers.  It
reconstructs the combinatorics from the theorem statements and emits a compact
JSON certificate suitable for exact replay with Python's standard library.
"""

from __future__ import annotations

import itertools
import json
import random
from collections import Counter


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(edges):
    used = set()
    for edge in edges:
        if used.intersection(edge):
            return False
        used.update(edge)
    return True


def center_split(family, n):
    degrees = [sum(i in edge for edge in family) for i in range(n)]
    x = max(range(n), key=lambda i: (degrees[i], -i))
    hub = tuple(edge for edge in family if x in edge)
    exceptional = tuple(edge for edge in family if x not in edge)
    return x, hub, exceptional


def direct_matchings(family):
    return tuple(selection for selection in subsets(family) if is_matching(selection))


def factorized_matchings(family, n):
    _, hub, exceptional = center_split(family, n)
    result = set()
    for matching in direct_matchings(exceptional):
        result.add(frozenset(matching))
        occupied = set().union(*matching) if matching else set()
        for edge in hub:
            if occupied.isdisjoint(edge):
                result.add(frozenset((*matching, edge)))
    return result


def zeta_overhead(family, n):
    _, hub, exceptional = center_split(family, n)
    gamma = len(exceptional)
    full = (1 << gamma) - 1
    weights = [0] * (1 << gamma)
    for edge in hub:
        mask = sum((1 << j) for j, other in enumerate(exceptional) if not edge.isdisjoint(other))
        weights[mask] += 1
    zeta = weights[:]
    for bit in range(gamma):
        flag = 1 << bit
        for mask in range(1 << gamma):
            if mask & flag:
                zeta[mask] += zeta[mask ^ flag]
    answer = 0
    for selected in range(1 << gamma):
        chosen = tuple(exceptional[j] for j in range(gamma) if selected >> j & 1)
        if not is_matching(chosen):
            continue
        size = len(chosen)
        answer += max(size - 1, 0) + size * zeta[full ^ selected]
    return answer


def direct_overhead(family):
    return sum(max(len(matching) - 1, 0) for matching in direct_matchings(family))


def audit_diversity():
    families = 0
    matching_states = 0
    for n in (4, 5):
        universe = tuple(frozenset(edge) for edge in itertools.combinations(range(n), 2))
        for family in subsets(universe):
            direct = {frozenset(matching) for matching in direct_matchings(family)}
            factored = factorized_matchings(family, n)
            assert direct == factored
            assert direct_overhead(family) == zeta_overhead(family, n)
            families += 1
            matching_states += len(direct)

    rng = random.Random(20260901)
    hostile = 0
    universe = tuple(frozenset(edge) for edge in itertools.combinations(range(7), 3))
    for _ in range(250):
        family = tuple(edge for edge in universe if rng.random() < 0.12)
        if len(family) > 14:
            family = tuple(rng.sample(family, 14))
        assert direct_overhead(family) == zeta_overhead(family, 7)
        hostile += 1
    return {
        "complete_families": families,
        "complete_matching_states": matching_states,
        "deterministic_larger_controls": hostile,
        "factorization": "exact",
        "zeta_overhead": "exact",
    }


def successor_sets(code):
    result = {}
    for first, second in code:
        result.setdefault(first, set()).add(second)
    return {first: frozenset(seconds) for first, seconds in result.items()}


def cycle_adjacent(a, b, n):
    return (a - b) % n in (0, 1, n - 1)


def strong_square_independent(code, n):
    return all(
        not (cycle_adjacent(a, c, n) and cycle_adjacent(b, d, n))
        for (a, b), (c, d) in itertools.combinations(code, 2)
    )


def audit_reversible_compiler():
    code = frozenset({
        (0, 2), (0, 4), (1, 6), (2, 1), (2, 3),
        (3, 5), (4, 1), (4, 3), (5, 5), (6, 0),
    })
    fibres = successor_sets(code)
    distinct = set(fibres.values())
    assert len(fibres) == 7
    assert len(distinct) == 5
    assert fibres[2] == fibres[4] == frozenset({1, 3})
    assert fibres[3] == fibres[5] == frozenset({5})
    assert distinct == {
        frozenset({2, 4}), frozenset({6}), frozenset({1, 3}),
        frozenset({5}), frozenset({0}),
    }
    assert strong_square_independent(code, 7)
    assert all(left.isdisjoint(right) for left, right in itertools.combinations(distinct, 2))
    transitions = len(fibres) + sum(map(len, distinct))
    assert transitions == 14

    invalid_label_control = set(code)
    invalid_label_control.remove((6, 0))
    invalid_label_control.add((7, 0))
    assert not strong_square_independent(invalid_label_control, 7)
    return {
        "standard_c7_codewords": len(code),
        "unmerged_first_coordinate_fibres": len(fibres),
        "distinct_successor_sets": len(distinct),
        "quotient_states_including_root": 1 + len(distinct),
        "quotient_transitions": transitions,
        "strong_square_independent": True,
        "reversible": True,
        "out_of_alphabet_label_control_rejected": True,
    }


def main():
    certificate = {
        "schema": "fprd.result-review.diversity-reversible.v1",
        "status": "pass",
        "diversity_kernel": audit_diversity(),
        "reversible_c7_compiler": audit_reversible_compiler(),
        "scope": "finite corroboration; arbitrary-size statements use the published proofs",
    }
    print(json.dumps(certificate, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()