"""Counterexample to Conjecture 5.5 (transcribed from
`constant_heawood_counterexample.tikz`).

This script:
  (1) builds H from the edge list transcribed from the .tikz file;
  (2) verifies H is simple, cubic, planar;
  (3) verifies the colour assignment is a proper 3-edge-colouring;
  (4) computes h_φ at every vertex via the CW rotation around each
      vertex using the planar coordinates given in the .tikz file
      (rather than Sage's combinatorial embedding, which may pick a
      different rotation system);
  (5) identifies the {a,b}-, {a,c}-, {b,c}-Kempe cycles of φ;
  (6) reports whether h_φ is constant on each Kempe cycle;
  (7) saves a PNG of the planar drawing with edges coloured red /
      blue / green at the same positions as the .tikz file.

Convention:
  colour 0 = red   = "a",
  colour 1 = blue  = "b",
  colour 2 = green = "c".

Run with: sage experiments/counterexample_conj_5_5.py
"""
import math
import os

from sage.all import Graph

HERE = os.path.dirname(os.path.abspath(__file__))
OUT_PNG = os.path.join(HERE, '..', 'figures',
                       'no-two-constant-kempe-counterexample.png')

RED, BLUE, GREEN = 0, 1, 2
COLOUR_NAME = {RED: 'red', BLUE: 'blue', GREEN: 'green'}

# Vertex positions transcribed verbatim from
# constant_heawood_counterexample.tikz.
POS = {
    0: (-4.0,  4.5),
    1: ( 0.0,  4.0),
    2: ( 4.5,  4.5),
    3: ( 4.0,  0.0),
    4: ( 4.5, -4.0),
    5: ( 0.0, -4.0),
    6: (-4.0, -4.0),
    7: (-4.0,  0.0),
    8: (-2.5,  1.5),
    9: (-2.0,  2.0),
    10: (-1.5,  2.5),
    11: (-1.0,  3.0),
    12: (-0.5,  3.5),
    13: (-3.0,  1.0),
    14: (-3.5,  0.5),
    15: ( 0.5,  4.5),
    16: ( 0.5, -3.5),
    17: ( 1.0, -3.0),
    18: ( 1.5, -2.5),
    19: ( 2.0, -2.0),
    20: ( 2.5, -1.5),
    21: ( 3.0, -1.0),
    22: ( 3.5, -0.5),
    23: ( 4.5,  0.5),
    24: (-3.5,  1.25),
    25: (-2.5,  2.25),
    26: (-1.5,  3.25),
    27: (-0.5,  4.25),
    28: (-2.0,  0.0),
    29: ( 0.0, -2.0),
    30: ( 2.0,  0.0),
    31: ( 0.0,  2.0),
    32: (-1.0,  1.0),
    33: ( 1.0,  3.0),
    34: ( 1.0, -1.0),
    35: ( 3.0,  1.0),
    36: ( 1.25, -3.5),
    37: ( 2.25, -2.5),
    38: ( 3.25, -1.5),
    39: ( 4.25, -0.5),
}

# Edges with colours, transcribed from the .tikz edgelayer in order.
# Two edges (6-4 and 0-2) are drawn bent in TikZ and represent the
# "outer-face" green arcs; their straight-line geometry in POS would
# pass through the interior, but the embedding treats them as edges of
# the outer face (i.e. they leave each endpoint pointing away from the
# interior). We model this by overriding the angle at vertices 0, 2,
# 6, 4 for these two edges (see CW_ANGLE_OVERRIDE below).
EDGES = [
    # blue (4)
    (0, 15, BLUE), (2, 23, BLUE), (5, 4, BLUE), (7, 6, BLUE),
    # red (outer 4)
    (0, 7, RED), (15, 2, RED), (23, 4, RED), (5, 6, RED),
    # red (interior-segments group 1)
    (14, 13, RED), (8, 9, RED), (10, 11, RED), (12, 1, RED),
    (16, 17, RED), (18, 19, RED), (20, 21, RED), (22, 3, RED),
    # green (outer "spokes" connecting outer frame to inner parallelograms)
    (7, 14, GREEN), (13, 8, GREEN), (9, 10, GREEN), (11, 12, GREEN),
    (1, 15, GREEN), (5, 16, GREEN), (17, 18, GREEN), (19, 20, GREEN),
    (21, 22, GREEN), (3, 23, GREEN),
    # green outer-face arcs
    (6, 4, GREEN),   # bottom arc (bent in tikz: out=-135, in=-45)
    (0, 2, GREEN),   # top arc (bent in tikz: bend left=45)
    # inner upper-left "trapezoid" connecting 14, 8, 10, 12 to 24..27
    (24, 14, BLUE), (25, 8, BLUE), (26, 10, BLUE), (27, 12, BLUE),
    (24, 25, RED), (26, 27, RED),
    (25, 26, GREEN),
    (24, 27, GREEN),  # bent
    # mid-layer edges connecting outer-frame intermediate vertices to
    # the inner "diamond" of 28-35
    (13, 28, BLUE), (9, 32, BLUE), (11, 31, BLUE), (1, 33, BLUE),
    (29, 17, BLUE), (34, 19, BLUE), (30, 21, BLUE), (35, 3, BLUE),
    # lower-right "trapezoid"
    (16, 36, BLUE), (18, 37, BLUE), (20, 38, BLUE), (22, 39, BLUE),
    (36, 37, RED), (38, 39, RED),
    (38, 37, GREEN),
    (36, 39, GREEN),  # bent
    # inner diamond edges (red rungs)
    (28, 32, RED), (31, 33, RED), (30, 35, RED), (29, 34, RED),
    # inner diamond edges (green rungs)
    (32, 34, GREEN), (28, 29, GREEN), (31, 30, GREEN), (33, 35, GREEN),
]

# For the two outer-face green arcs (and the bent edges 24-27 and
# 36-39), override the angle used in the CW-rotation computation so
# that the cyclic order around each endpoint matches the planar
# embedding actually drawn in tikz rather than the straight-line
# geometry.
#
# Convention: angle is measured in degrees, counterclockwise from
# +x axis. The override gives the direction the edge LEAVES the
# endpoint along the tikz-drawn curve, not toward the other endpoint
# of the straight line.
#
# - 0->2 green arc bends "left" over the top; from 0 it leaves
#   roughly upward (north), and from 2 it arrives from the upper-left
#   (so 2's local angle is also roughly upward).
# - 6->4 green arc bends "around the bottom"; from 6 it leaves
#   roughly downward (south), and from 4 it leaves roughly downward.
# - 24->27 green arc bends "left" above the upper-left ladder
#   (in=-135, out=-45 conceptually).
# - 36->39 green arc bends "right" below the lower-right ladder.
CW_ANGLE_OVERRIDE = {
    (0, 2):   90.0,   # at 0, edge to 2 leaves upward
    (2, 0):   90.0,   # at 2, edge to 0 leaves upward
    (6, 4):  -90.0,   # at 6, edge to 4 leaves downward
    (4, 6):  -90.0,   # at 4, edge to 6 leaves downward
    (24, 27): 135.0,  # at 24, edge to 27 leaves upper-left
    (27, 24): 135.0,  # at 27, edge to 24 leaves upper-left
    (36, 39): -45.0,  # at 36, edge to 39 leaves lower-right
    (39, 36): -45.0,  # at 39, edge to 36 leaves lower-right
}


def angle_at(v, u):
    """Direction (degrees) from v toward u in the planar drawing,
    honouring CW_ANGLE_OVERRIDE for bent edges."""
    if (v, u) in CW_ANGLE_OVERRIDE:
        return CW_ANGLE_OVERRIDE[(v, u)]
    (vx, vy) = POS[v]
    (ux, uy) = POS[u]
    return math.degrees(math.atan2(uy - vy, ux - vx))


def build_graph(edges):
    G = Graph(multiedges=False, loops=False)
    for u, v, _ in edges:
        G.add_edge(u, v)
    return G


def edge_colour_map(edges):
    return {frozenset((u, v)): c for u, v, c in edges}


def is_proper_3_edge_colouring(G, col):
    for v in G.vertex_iterator():
        cols = sorted(col[frozenset((v, u))] for u in G.neighbors(v))
        if cols != [RED, BLUE, GREEN]:
            return False, v, cols
    return True, None, None


def cw_neighbours(G, v):
    """List of v's neighbours in CW order from the planar coordinates
    (CW = decreasing polar angle)."""
    nbrs = list(G.neighbors(v))
    nbrs.sort(key=lambda u: -angle_at(v, u))
    return nbrs


def heawood_numbers(G, col):
    h = {}
    for v in G.vertex_iterator():
        nbrs = cw_neighbours(G, v)
        cols = [col[frozenset((v, u))] for u in nbrs]
        i0 = cols.index(RED)
        rot = cols[i0:] + cols[:i0]
        if rot == [RED, BLUE, GREEN]:
            h[v] = +1
        elif rot == [RED, GREEN, BLUE]:
            h[v] = -1
        else:
            raise RuntimeError(f"bad rotation at {v}: {cols}")
    return h


def kempe_cycle(G, col, start_edge, two_colours):
    target = set(two_colours)
    u0, v0 = start_edge
    walk = [u0, v0]
    while True:
        cur, prev = walk[-1], walk[-2]
        nxt = None
        for u in G.neighbors(cur):
            if u == prev:
                continue
            if col[frozenset((cur, u))] in target:
                nxt = u
                break
        if nxt is None:
            raise RuntimeError(f"Kempe walk stuck at {cur}")
        if nxt == walk[0] and cur == walk[-2]:
            # safety; shouldn't trigger in normal walks
            break
        walk.append(nxt)
        if walk[-1] == walk[0] and len(walk) > 2:
            return walk[:-1]


def report(name, cycle, h, two_colours):
    h_vals = [h[v] for v in cycle]
    plus = sum(1 for x in h_vals if x == +1)
    minus = sum(1 for x in h_vals if x == -1)
    const = (plus == 0 or minus == 0)
    a, b = two_colours
    print(f"  {name} (colours {{ {COLOUR_NAME[a]}, {COLOUR_NAME[b]} }}):")
    print(f"    length  = {len(cycle)}")
    print(f"    vertices= {cycle}")
    print(f"    h_φ     = {h_vals}")
    print(f"    +/-     = {plus} (+1) / {minus} (-1)")
    print(f"    const?  {'YES' if const else 'no'}")
    return const


# Bent edges, matching the tikz embedding. For each, we give a "rad"
# value (positive => arc bulges to the LEFT of the directed edge u->v
# in matplotlib's connectionstyle convention).
BENT_EDGES = {
    # In matplotlib's arc3, positive rad bulges to the RIGHT of the
    # directed edge from posA to posB. We pick signs so the bulge
    # matches the tikz drawing.
    frozenset((0, 2)):   ('arc', (0, 2), -0.30),   # 0→2 rightward, bulge up   (left of dir)
    frozenset((6, 4)):   ('arc', (6, 4), +0.30),   # 6→4 rightward, bulge down (right of dir)
    frozenset((24, 27)): ('arc', (24, 27), -0.30), # 24→27 up-right, bulge up-left ("bend left")
    frozenset((36, 39)): ('arc', (36, 39), +0.30), # 36→39 up-right, bulge down-right ("bend right")
}


def draw_png(G, col, out_path):
    import matplotlib
    matplotlib.use('Agg')
    import matplotlib.pyplot as plt
    from matplotlib.patches import FancyArrowPatch

    os.makedirs(os.path.dirname(out_path), exist_ok=True)
    fig, ax = plt.subplots(figsize=(10, 10), dpi=160)
    ax.set_aspect('equal')
    ax.axis('off')

    # Draw edges first so vertices sit on top
    for e in G.edge_iterator(labels=False):
        u, v = e
        c = COLOUR_NAME[col[frozenset(e)]]
        if frozenset(e) in BENT_EDGES:
            _, (a, b), rad = BENT_EDGES[frozenset(e)]
            # Orient so the rad sign matches the (a -> b) direction
            if (u, v) != (a, b):
                rad = -rad
            arc = FancyArrowPatch(
                POS[u], POS[v],
                arrowstyle='-',
                connectionstyle=f'arc3,rad={rad}',
                color=c, linewidth=2.5,
                shrinkA=0, shrinkB=0,
            )
            ax.add_patch(arc)
        else:
            (x1, y1), (x2, y2) = POS[u], POS[v]
            ax.plot([x1, x2], [y1, y2], color=c, linewidth=2.5,
                    solid_capstyle='round')

    # Draw vertices
    for v, (x, y) in POS.items():
        ax.plot(x, y, 'o', markersize=16,
                markerfacecolor='lightgrey',
                markeredgecolor='black', markeredgewidth=1.0)
        ax.text(x, y, str(v), ha='center', va='center', fontsize=8)

    # Set bounds with padding (the top arc goes well above 4.5)
    xs = [p[0] for p in POS.values()]
    ys = [p[1] for p in POS.values()]
    pad = 1.5
    ax.set_xlim(min(xs) - pad, max(xs) + pad)
    ax.set_ylim(min(ys) - pad, max(ys) + pad)

    fig.tight_layout()
    fig.savefig(out_path, dpi=160, bbox_inches='tight')
    plt.close(fig)
    print(f"\nWrote: {out_path}")


def main():
    print("Loading edges from transcribed tikz...")
    G = build_graph(EDGES)
    col = edge_colour_map(EDGES)
    print(f"  |V(H)| = {G.order()}, |E(H)| = {G.size()}")
    print(f"  canonical graph6 = {G.canonical_label().graph6_string()}")
    print(f"  girth = {G.girth()}, |Aut| = {G.automorphism_group().order()}, "
          f"hamiltonian = {G.is_hamiltonian()}")

    degs = sorted(set(G.degree()))
    print(f"  degree set = {degs}")
    if degs != [3]:
        print("  !! NOT CUBIC"); draw_png(G, col, OUT_PNG); return
    print("  cubic ✓")

    is_planar = G.is_planar(set_embedding=True)
    print(f"  planar (by Sage)? {is_planar}")
    if not is_planar:
        print("  !! NOT PLANAR"); draw_png(G, col, OUT_PNG); return

    ok, bad, cols = is_proper_3_edge_colouring(G, col)
    if not ok:
        print(f"  !! NOT a proper 3-edge-colouring: {bad} has {cols}")
        draw_png(G, col, OUT_PNG); return
    print("  proper 3-edge-colouring ✓")

    h = heawood_numbers(G, col)
    print("\nHeawood numbers per vertex (using tikz coordinates):")
    for v in sorted(h):
        print(f"  h_φ({v:2d}) = {h[v]:+d}")

    print("\nGlobal Heawood sums:")
    plus = sum(1 for v in h if h[v] == +1)
    minus = sum(1 for v in h if h[v] == -1)
    print(f"  total: {plus} (+1) / {minus} (-1), sum = {plus - minus}")

    # Try all three Kempe-cycle pairs and identify the ones sharing an
    # edge. We pick an edge of each colour and trace each cycle.
    print("\nAll three Kempe-cycle types through some shared edge:")
    # find an edge of each colour
    edge_by_color = {}
    for u, v, c in EDGES:
        if c not in edge_by_color:
            edge_by_color[c] = (u, v)

    for a in (RED, BLUE, GREEN):
        b, c = [x for x in (RED, BLUE, GREEN) if x != a]
        e_a = edge_by_color[a]
        Kab = kempe_cycle(G, col, e_a, (a, b))
        Kac = kempe_cycle(G, col, e_a, (a, c))
        print(f"\n-- shared edge: colour-{COLOUR_NAME[a]} edge {e_a}")
        const_ab = report(f"K_{{a,b}}={{{COLOUR_NAME[a]},{COLOUR_NAME[b]}}}",
                          Kab, h, (a, b))
        const_ac = report(f"K_{{a,c}}={{{COLOUR_NAME[a]},{COLOUR_NAME[c]}}}",
                          Kac, h, (a, c))
        if const_ab and const_ac:
            print(f"  ** counterexample with a={COLOUR_NAME[a]} **")

    draw_png(G, col, OUT_PNG)


if __name__ == '__main__':
    main()