#!/usr/bin/env python3
"""Exact checks and a figure for the crossing decomposition in Hexagon 2610.00577v1.

Run from any directory:
    uv run --with matplotlib python "content/codes/2026 Fall/sat_crossing_checks.py"

Identity and matrix-rank checks use only Python integers and rational arithmetic.
The figure is expository; this is not an implementation of the SAT algorithm.
"""

from collections import Counter
from fractions import Fraction
from itertools import product
import json
from pathlib import Path


def sigma(p, q):
    """Equation (27), with the three coordinates read from low to high bit."""
    a = [(p >> i) & 1 for i in range(3)]
    b = [(q >> i) & 1 for i in range(3)]
    exponent = sum(a[i] * b[j] for i in range(3) for j in range(i, 3))
    exponent += b[0] * a[1] * a[2] + a[0] * b[1] * a[2] + a[0] * a[1] * b[2]
    return -1 if exponent % 2 else 1


def pieces(x, y, u, v):
    crossing = int(x == v and y == u)
    parity = int(x ^ y ^ u ^ v == 0)
    row = parity * sigma(x, y) * sigma(v, u)
    column = parity * sigma(x, u) * sigma(v, y)
    return crossing, row, column


def rational_rank(matrix):
    """Gaussian elimination over Q, without floating-point tolerances."""
    rows = [list(map(Fraction, row)) for row in matrix]
    rank = 0
    for column in range(len(rows[0])):
        pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None)
        if pivot is None:
            continue
        rows[rank], rows[pivot] = rows[pivot], rows[rank]
        divisor = rows[rank][column]
        rows[rank] = [value / divisor for value in rows[rank]]
        for i in range(rank + 1, len(rows)):
            multiplier = rows[i][column]
            if multiplier:
                rows[i] = [a - multiplier * b for a, b in zip(rows[i], rows[rank])]
        rank += 1
        if rank == len(rows):
            break
    return rank


def check():
    patterns = Counter()
    for x, y, u, v in product(range(8), repeat=4):
        crossing, row, column = pieces(x, y, u, v)
        assert row + column == 2 * crossing, (x, y, u, v)
        patterns[crossing, row, column] += 1
    assert sum(patterns.values()) == 4096

    # The grouped two-block polynomial depends only on these triples. Checking
    # all pattern pairs covers every pair of blocks, with multiplicities below.
    covered = 0
    for (a, multiplicity_a), (b, multiplicity_b) in product(patterns.items(), repeat=2):
        x1, r1, c1 = a
        x2, r2, c2 = b
        grouped = (r1 * r2, r1 * c2 + c1 * r2, c1 * c2)
        assert sum(grouped) == 4 * x1 * x2
        covered += multiplicity_a * multiplicity_b
    assert covered == 4096**2

    pairs = list(product(range(8), repeat=2))
    ranks = {}
    for index, name in enumerate(("X", "R", "C")):
        row_matrix = [[pieces(x, y, u, v)[index] for u, v in pairs] for x, y in pairs]
        col_matrix = [[pieces(x, y, u, v)[index] for y, v in pairs] for x, u in pairs]
        ranks[name] = [rational_rank(row_matrix), rational_rank(col_matrix)]
    assert ranks == {"X": [64, 64], "R": [8, 64], "C": [64, 8]}, ranks
    cancellations = sum(count for (x, r, c), count in patterns.items() if x == 0 and r and c)
    assert cancellations == 448
    return {
        "one_block_inputs": 4096,
        "nonzero_cancellations": cancellations,
        "two_block_inputs_covered": covered,
        "distinct_two_block_patterns": len(patterns) ** 2,
        "exact_ranks_row_column": ranks,
    }


def draw():
    import matplotlib

    matplotlib.use("Agg")
    import matplotlib.pyplot as plt
    from matplotlib.patches import FancyBboxPatch

    plt.rcParams.update({
        "svg.fonttype": "none",
        "svg.hashsalt": "latent-seminar-sat-crossing-v1",
        "font.family": "DejaVu Sans",
    })
    fig, axes = plt.subplots(3, 1, figsize=(5.2, 8.2))
    fig.patch.set_facecolor("#eff1f5")
    ink, blue, red = "#4c4f69", "#1e66f5", "#d20f39"
    points = {"x": (0.27, 0.68), "y": (0.73, 0.68), "u": (0.27, 0.22), "v": (0.73, 0.22)}
    titles = [
        ("Crossing X", "6 bits by rows; 6 bits by columns"),
        ("Piece R", "3 bits by rows; 6 bits by columns"),
        ("Piece C", "6 bits by rows; 3 bits by columns"),
    ]
    for index, (ax, (title, subtitle)) in enumerate(zip(axes, titles)):
        ax.set(xlim=(0, 1), ylim=(0, 1))
        ax.axis("off")
        ax.text(0.5, 0.97, title, ha="center", va="top", fontsize=17, color=ink, weight="bold")
        if index == 0:
            for a, b in (("x", "v"), ("y", "u")):
                ax.plot([points[a][0], points[b][0]], [points[a][1], points[b][1]], color=ink, lw=2)
        elif index == 1:
            for bottom, color in ((0.55, blue), (0.09, red)):
                ax.add_patch(FancyBboxPatch((0.13, bottom), 0.74, 0.26, boxstyle="round,pad=0.015",
                                            facecolor=color, edgecolor=color, alpha=0.12))
            ax.plot([0.5, 0.5], [0.37, 0.53], color=ink, lw=2)
            ax.text(0.56, 0.45, "b", color=ink, fontsize=17, va="center", style="italic")
        else:
            for left, color in ((0.15, blue), (0.61, red)):
                ax.add_patch(FancyBboxPatch((left, 0.09), 0.24, 0.72, boxstyle="round,pad=0.015",
                                            facecolor=color, edgecolor=color, alpha=0.12))
            ax.plot([0.41, 0.59], [0.45, 0.45], color=ink, lw=2)
            ax.text(0.5, 0.53, "b", color=ink, fontsize=17, ha="center", style="italic")
        for label, (x, y) in points.items():
            ax.scatter([x], [y], s=470, facecolors="#eff1f5", edgecolors=ink, linewidths=1.6, zorder=3)
            ax.text(x, y, label, ha="center", va="center", fontsize=17, color=ink, zorder=4, style="italic")
        ax.text(0.5, -0.03, subtitle, ha="center", va="top", fontsize=12.5, color=ink)
    fig.subplots_adjust(left=0.03, right=0.97, top=0.98, bottom=0.05, hspace=0.34)
    output = Path(__file__).resolve().parents[2] / "images" / "2026 Fall" / "sat-crossing-decomposition.svg"
    output.parent.mkdir(parents=True, exist_ok=True)
    fig.savefig(output, facecolor=fig.get_facecolor(), metadata={"Date": None, "Title": "Signed crossing decomposition: 2X = R + C"})
    plt.close(fig)
    output.write_text("\n".join(line.rstrip() for line in output.read_text().splitlines()) + "\n")
    return str(output)


if __name__ == "__main__":
    result = check()
    result["figure"] = draw()
    print(json.dumps(result, indent=2))