#!/usr/bin/env python3
"""
Verify the Subgraph Lattice Theorem against all Test 2b data.

THEOREM: If G is a spanning subgraph of H (same vertex set, E(G) ⊆ E(H)),
         then p_𝔾(G) ≤ p_𝔾(H).

For every pair of graphs at the same n, check:
  1. Is E(G) ⊆ E(H)?  (spanning subgraph relation)
  2. If so, does p_𝔾(G) ≤ p_𝔾(H)?

Also flag all incomparable pairs (neither edge set contains the other).
"""

import sys
sys.path.insert(0, ".")
from test2b_fixed_n_topology import (
    make_path, make_cycle, make_star, make_complete, make_wheel,
    make_complete_bipartite, make_ladder, make_prism, make_friendship,
    make_book, make_petersen, count_connected_partitions
)

FAMILIES = [
    ("P_n (path)", make_path),
    ("S_n (star)", make_star),
    ("C_n (cycle)", make_cycle),
    ("W_n (wheel)", make_wheel),
    ("K_{2,n-2}", make_complete_bipartite),
    ("Fan_n", make_book),
    ("Ladder_n", make_ladder),
    ("Prism_n", make_prism),
    ("Friendship_n", make_friendship),
    ("K_n (complete)", make_complete),
]

def canonical_edges(G):
    """Return frozenset of edges as sorted tuples for comparison."""
    return frozenset(tuple(sorted(e)) for e in G.edges())

def main():
    print("=" * 72)
    print("  Subgraph Lattice Theorem — Verification")
    print("  Checking: E(G) ⊆ E(H) ⟹ p_𝔾(G) ≤ p_𝔾(H)")
    print("=" * 72)

    violations = []
    confirmations = 0
    incomparable_count = 0
    total_pairs = 0

    for n in range(4, 11):
        # Build all graphs at this n
        graphs = []
        for name, constructor in FAMILIES:
            if name == "Petersen" and n != 10:
                continue
            G = constructor(n)
            if G is None:
                continue
            if G.number_of_nodes() != n:
                continue
            pG = count_connected_partitions(G)
            edges = canonical_edges(G)
            graphs.append((name, G, edges, pG))

        # Add Petersen at n=10
        if n == 10:
            G = make_petersen()
            pG = count_connected_partitions(G)
            edges = canonical_edges(G)
            graphs.append(("Petersen", G, edges, pG))

        print(f"\n  n = {n}: {len(graphs)} graphs")

        # Check all pairs
        for i in range(len(graphs)):
            for j in range(len(graphs)):
                if i == j:
                    continue
                total_pairs += 1
                name_i, _, edges_i, pG_i = graphs[i]
                name_j, _, edges_j, pG_j = graphs[j]

                if edges_i <= edges_j:
                    # G_i is a spanning subgraph of G_j
                    if pG_i <= pG_j:
                        confirmations += 1
                    else:
                        violations.append((n, name_i, pG_i, name_j, pG_j,
                                         len(edges_i), len(edges_j)))
                        print(f"    *** VIOLATION: {name_i}(p={pG_i}) > "
                              f"{name_j}(p={pG_j}) but E(G_i) ⊆ E(G_j)")
                elif edges_j <= edges_i:
                    pass  # counted in reverse direction
                else:
                    incomparable_count += 1

        # Print containment chains for this n
        print(f"    Containment chains at n={n}:")
        for i in range(len(graphs)):
            for j in range(i + 1, len(graphs)):
                name_i, _, edges_i, pG_i = graphs[i]
                name_j, _, edges_j, pG_j = graphs[j]
                if edges_i < edges_j:
                    symbol = "✓" if pG_i <= pG_j else "✗ VIOLATION"
                    print(f"      {name_i}(p={pG_i:>6}, m={len(edges_i):>2}) "
                          f"⊂ {name_j}(p={pG_j:>6}, m={len(edges_j):>2})  {symbol}")
                elif edges_j < edges_i:
                    symbol = "✓" if pG_j <= pG_i else "✗ VIOLATION"
                    print(f"      {name_j}(p={pG_j:>6}, m={len(edges_j):>2}) "
                          f"⊂ {name_i}(p={pG_i:>6}, m={len(edges_i):>2})  {symbol}")

    print(f"\n{'=' * 72}")
    print(f"  RESULTS")
    print(f"{'=' * 72}")
    print(f"  Total ordered pairs checked:    {total_pairs}")
    print(f"  Comparable (E(G) ⊆ E(H)):      {confirmations}")
    print(f"  Incomparable pairs:             {incomparable_count}")
    print(f"  VIOLATIONS:                     {len(violations)}")

    if violations:
        print(f"\n  *** THEOREM FAILS. {len(violations)} violation(s):")
        for v in violations:
            n, g1, p1, g2, p2, m1, m2 = v
            print(f"      n={n}: {g1}(p={p1}, m={m1}) > {g2}(p={p2}, m={m2})")
    else:
        print(f"\n  ✓ THEOREM CONFIRMED on all {confirmations} comparable pairs.")
        print(f"    (Plus {incomparable_count} incomparable pairs where the")
        print(f"     theorem makes no prediction.)")

    # Also show the κ-counterexamples and confirm they're incomparable
    print(f"\n{'=' * 72}")
    print(f"  κ-COUNTEREXAMPLES — confirming incomparability")
    print(f"{'=' * 72}")
    counterexample_pairs = [
        (7, "Friendship_n", "C_n (cycle)"),
        (9, "Friendship_n", "C_n (cycle)"),
        (9, "K_{2,n-2}", "W_n (wheel)"),
        (10, "K_{2,n-2}", "W_n (wheel)"),
    ]

    for n_target, name_a, name_b in counterexample_pairs:
        # Rebuild the specific graphs
        for name, constructor in FAMILIES:
            G = constructor(n_target)
            if G is not None and name == name_a:
                ga, ea = G, canonical_edges(G)
            if G is not None and name == name_b:
                gb, eb = G, canonical_edges(G)

        a_sub_b = ea <= eb
        b_sub_a = eb <= ea
        if not a_sub_b and not b_sub_a:
            status = "INCOMPARABLE ✓"
        elif a_sub_b:
            status = f"{name_a} ⊆ {name_b}"
        else:
            status = f"{name_b} ⊆ {name_a}"

        only_a = ea - eb
        only_b = eb - ea
        print(f"  n={n_target}: {name_a} vs {name_b}: {status}")
        print(f"    Edges only in {name_a}: {len(only_a)}  "
              f"Edges only in {name_b}: {len(only_b)}")


if __name__ == "__main__":
    main()