#!/usr/bin/env python3
"""Independent boundary audit for FPRD-SH-T19--T23, C10, and C11.

This checker is intentionally smaller than the preserved source programs. It
uses direct subset enumeration and explicit product-state exploration to test
the two reviewed theorem families, including the parameter boundaries omitted
from the original public T22 statement.
"""

from __future__ import annotations

import itertools
import json
import math
from collections import Counter, defaultdict, deque


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 & (1 << i))


def uniform_sets(n: int, r: int):
    return tuple(frozenset(x) for x in itertools.combinations(range(n), r))


def intersecting(family) -> bool:
    return all(a & b for a, b in itertools.combinations(family, 2))


def core(family):
    if not family:
        return frozenset()
    return frozenset.intersection(*family)


def disjoint_pairs(family) -> int:
    return sum(not (a & b) for a, b in itertools.combinations(family, 2))


def spectral_bound_holds(n: int, r: int, family) -> bool:
    assert 1 <= r and 2 * r <= n
    total = math.comb(n, r)
    degree = math.comb(n - r, r)
    tau = math.comb(n - r - 1, r - 1)
    alpha = math.comb(n - 1, r - 1)
    m = len(family)
    return 2 * total * disjoint_pairs(family) >= (degree + tau) * m * (m - alpha)


def audit_uniform_boundaries():
    audited = 0
    for n, r in ((4, 2), (5, 2), (6, 3)):
        universe = uniform_sets(n, r)
        alpha = math.comb(n - 1, r - 1)
        for family in subsets(universe):
            audited += 1
            assert spectral_bound_holds(n, r, family)
            if intersecting(family):
                assert len(family) <= alpha
                if n > 2 * r and len(family) == alpha:
                    assert core(family)
                if n > 2 * r and r >= 2 and not core(family):
                    hm = alpha - math.comb(n - r - 1, r - 1) + 1
                    assert len(family) <= hm

    # Below the EKR range KG_{n,r} is edgeless: the full family is valid.
    below = uniform_sets(5, 3)
    assert intersecting(below)
    assert disjoint_pairs(below) == 0
    assert len(below) == 10 > math.comb(4, 2)

    # At n=2r every set has one disjoint partner, its complement.
    critical = uniform_sets(6, 3)
    complement_pairs = {
        frozenset((a, frozenset(range(6)) - a)) for a in critical
    }
    assert len(complement_pairs) == math.comb(6, 3) // 2

    # The Hilton--Milner empty-core clause needs r>=2.
    singletons = uniform_sets(3, 1)
    empty_core_intersecting = [f for f in subsets(singletons) if intersecting(f) and not core(f)]
    assert max(map(len, empty_core_intersecting), default=0) == 0

    # Independently generate the two equality types for (n,r)=(7,3).
    n, r = 7, 3
    universe = uniform_sets(n, r)
    hm_families = set()
    for x in range(n):
        for a in universe:
            if x not in a:
                fam = frozenset({a} | {b for b in universe if x in b and a & b})
                assert len(fam) == 13 and intersecting(fam) and not core(fam)
                hm_families.add(fam)
    exceptional = set()
    for a in universe:
        fam = frozenset(b for b in universe if len(a & b) >= 2)
        assert len(fam) == 13 and intersecting(fam) and not core(fam)
        exceptional.add(fam)
    assert len(hm_families) == 140
    assert len(exceptional) == 35
    assert hm_families.isdisjoint(exceptional)

    return {
        "in_range_families_checked": audited,
        "below_threshold_counterexample": {
            "n": 5,
            "r": 3,
            "full_family_size": len(below),
            "misapplied_ekr_ceiling": math.comb(4, 2),
            "disjoint_pairs": 0,
        },
        "critical_complement_pairs_n6_r3": len(complement_pairs),
        "r1_maximum_empty_core_intersecting_size": 0,
        "n7_r3_standard_hilton_milner_families": len(hm_families),
        "n7_r3_exceptional_families": len(exceptional),
    }


def xcc_consistent(signatures, chosen) -> bool:
    participant_colors = defaultdict(set)
    for i in chosen:
        letter, support = signatures[i]
        for participant in support:
            participant_colors[participant].add(letter)
    return all(len(colors) <= 1 for colors in participant_colors.values())


def compatible(signatures, chosen) -> bool:
    return all(
        a == b or s.isdisjoint(t)
        for (a, s), (b, t) in itertools.combinations((signatures[i] for i in chosen), 2)
    )


def graph_edges(n: int):
    return tuple(itertools.combinations(range(n), 2))


def matchings(edges):
    return tuple(
        chosen
        for chosen in subsets(edges)
        if len(set().union(*(set(e) for e in chosen))) == 2 * len(chosen)
    )


def product_states(n: int, edges):
    start = (None,) * n
    queue = deque([start])
    seen = {start}
    incoming = defaultdict(set)
    while queue:
        state = queue.popleft()
        for edge_id, (u, v) in enumerate(edges):
            if state[u] is not None or state[v] is not None:
                continue
            target = list(state)
            target[u] = target[v] = edge_id
            target = tuple(target)
            incoming[target].add(edge_id)
            if target not in seen:
                seen.add(target)
                queue.append(target)
    return seen, incoming


def audit_xcc_and_matchings():
    supports = tuple(
        frozenset(i for i in range(3) if mask & (1 << i))
        for mask in range(1, 8)
    )
    signatures = tuple((letter, support) for letter in ("a", "b") for support in supports)
    compatible_count = 0
    for chosen in subsets(range(len(signatures))):
        assert xcc_consistent(signatures, chosen) == compatible(signatures, chosen)
        compatible_count += compatible(signatures, chosen)

    graph_count = 0
    state_count = 0
    for n in range(1, 6):
        universe = graph_edges(n)
        for edges in subsets(universe):
            graph_count += 1
            ms = matchings(edges)
            states, incoming = product_states(n, edges)
            assert len(states) == len(ms)
            hist = Counter(len(m) for m in ms)
            observed = Counter(len(labels) for labels in incoming.values())
            assert observed == Counter({k: v for k, v in hist.items() if k})
            delta = sum(max(k - 1, 0) * count for k, count in hist.items())
            assert delta == sum(max(len(labels) - 1, 0) for labels in incoming.values())

            extension = edges + ((n, n + 1),)
            z = len(ms)
            h_hist = Counter(len(m) for m in matchings(extension))
            h_delta = sum(max(k - 1, 0) * count for k, count in h_hist.items())
            assert z == 1 + h_delta - 2 * delta
            state_count += len(states)

    return {
        "xcc_subsets_checked": 1 << len(signatures),
        "xcc_compatible_subsets": compatible_count,
        "exhaustive_graphs_checked": graph_count,
        "matching_product_states_checked": state_count,
    }


def main():
    report = {
        "status": "pass",
        "uniform_support_review": audit_uniform_boundaries(),
        "xcc_matching_review": audit_xcc_and_matchings(),
        "verified_claims": [
            "corrected EKR/Hilton--Milner parameter ranges",
            "Kneser spectral receipt on 1 <= r <= n/2",
            "XCC color compatibility bijection",
            "one-shot product/matching bijection",
            "weighted overhead formula",
            "isolated-edge recovery identity",
        ],
    }
    print(json.dumps(report, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()