quotient_arsenal_boundary_audit.py

#!/usr/bin/env python3
"""Independent finite checks for two Quotient Arsenal review units.

The script reconstructs the pinned Hurwitz support calculation and the
half-turn move-graph quotient directly from their definitions.  It uses no
project modules or archived verifier code.
"""

from __future__ import annotations

from collections import Counter, defaultdict
from itertools import combinations, combinations_with_replacement, product
import json


def mat_mul(a, b):
    return tuple(
        tuple(sum(a[i][k] * b[k][j] for k in range(2)) for j in range(2))
        for i in range(2)
    )


def mat_pow(a, n):
    out = ((1, 0), (0, 1))
    for _ in range(n):
        out = mat_mul(out, a)
    return out


def hurwitz_audit():
    points = range(1, 6)
    a_block = {1, 2, 5}
    u, v = 3, 4
    proper = [frozenset(s) for k in (2, 3, 4) for s in combinations(points, k)]
    assert len(proper) == 25

    def occupancy(s):
        return (len(s & a_block), int(u in s), int(v in s))

    def normalized_cross(s):
        a, b, c = occupancy(s)
        return (a * b, a * c, b * c)

    target = (3, 3, 1)
    solutions = []
    for triple in combinations_with_replacement(proper, 3):
        total = tuple(sum(normalized_cross(s)[i] for s in triple) for i in range(3))
        if total == target:
            solutions.append(triple)
    assert len(solutions) == 55

    type_counts = Counter()
    half_counts = Counter()
    for triple in solutions:
        occs = tuple(sorted(occupancy(s) for s in triple))
        bridges = [o for o in occs if o[1:] == (1, 1)]
        assert len(bridges) == 1
        r = bridges[0][0]
        type_counts[r] += 1
        h = 12 - sum(2 * o[0] * (o[0] - 1) for o in occs)
        half_counts[(r, h)] += 1
    assert type_counts == Counter({0: 1, 1: 27, 2: 27})
    assert set(half_counts) == {(0, -12), (1, 4), (2, 8)}

    x = ((1, 1), (0, 1))
    y = ((1, 0), (-1, 1))
    target_matrix = mat_pow(mat_mul(x, y), 6)
    solutions_8 = []
    for bits in product((0, 1), repeat=8):
        h = ((1, 0), (0, 1))
        word = []
        for bit in bits:
            letter = y if bit else x
            word.append("y" if bit else "x")
            h = mat_mul(h, letter)
        if mat_mul(mat_pow(x, 4), h) == target_matrix:
            solutions_8.append("".join(word))
    assert solutions_8 == ["yxxyyxxy"]

    return {
        "proper_supports": len(proper),
        "three_packet_multisets_tested": 2925,
        "cross_budget_solutions": len(solutions),
        "solutions_by_bridge_occupancy": {str(k): type_counts[k] for k in sorted(type_counts)},
        "forced_half_twists": {"0": -12, "1": 4, "2": 8},
        "positive_words_tested": 256,
        "shadow_solutions": solutions_8,
    }


KNIGHT_STEPS = ((1, 2), (1, -2), (-1, 2), (-1, -2), (2, 1), (2, -1), (-2, 1), (-2, -1))


def knight_graph(n):
    vertices = [(r, c) for r in range(n) for c in range(n)]
    adjacency = {v: set() for v in vertices}
    for r, c in vertices:
        for dr, dc in KNIGHT_STEPS:
            w = (r + dr, c + dc)
            if w in adjacency:
                adjacency[(r, c)].add(w)
    edges = {tuple(sorted((v, w))) for v in vertices for w in adjacency[v]}
    return vertices, adjacency, edges


def half_turn(n, v):
    return (n - 1 - v[0], n - 1 - v[1])


def orbit_data(n):
    vertices, adjacency, edges = knight_graph(n)
    vertex_orbits = []
    vertex_orbit_of = {}
    for v in vertices:
        if v in vertex_orbit_of:
            continue
        orb = tuple(sorted({v, half_turn(n, v)}))
        idx = len(vertex_orbits)
        vertex_orbits.append(orb)
        for x in orb:
            vertex_orbit_of[x] = idx

    edge_orbits = []
    edge_orbit_of = {}
    for e in sorted(edges):
        if e in edge_orbit_of:
            continue
        he = tuple(sorted((half_turn(n, e[0]), half_turn(n, e[1]))))
        orb = tuple(sorted({e, he}))
        idx = len(edge_orbits)
        edge_orbits.append(orb)
        for x in orb:
            edge_orbit_of[x] = idx
    return vertices, adjacency, edges, vertex_orbits, vertex_orbit_of, edge_orbits


def equitable_check(adjacency, orbits, orbit_of, horizon=4):
    size = len(orbits)
    b = [[0] * size for _ in range(size)]
    for i, orb in enumerate(orbits):
        rows = []
        for x in orb:
            row = [0] * size
            for y in adjacency[x]:
                row[orbit_of[y]] += 1
            rows.append(row)
        assert all(row == rows[0] for row in rows)
        b[i] = rows[0]

    matrix = [[int(i == j) for j in range(size)] for i in range(size)]
    direct = [[int(i == j) for j in range(size)] for i in range(size)]
    for _ in range(horizon + 1):
        assert matrix == direct
        matrix = [[sum(matrix[i][k] * b[k][j] for k in range(size)) for j in range(size)] for i in range(size)]
        direct = [[sum(direct[i][k] * b[k][j] for k in range(size)) for j in range(size)] for i in range(size)]
    return b


def six_board_quotient_cycles():
    n = 6
    _, _, _, orbits, orbit_of, edge_orbits = orbit_data(n)
    section = [orb[0] for orb in orbits]
    darts = defaultdict(list)
    for edge_id, edge_orbit in enumerate(edge_orbits):
        q0 = orbit_of[edge_orbit[0][0]]
        q1 = orbit_of[edge_orbit[0][1]]
        for source, target in ((q0, q1), (q1, q0)):
            s = section[source]
            candidates = [e[1] if e[0] == s else e[0] for e in edge_orbit if s in e]
            assert len(candidates) == 1
            t = candidates[0]
            voltage = int(t != section[target])
            assert t == (section[target] if voltage == 0 else half_turn(n, section[target]))
            darts[source].append((target, voltage, edge_id))

    found = {}
    start = 0

    def dfs(path, used, voltage):
        if len(found) == 2:
            return
        current = path[-1]
        if len(path) == len(orbits):
            for nxt, edge_voltage, edge_id in darts[current]:
                if nxt == start:
                    total = voltage ^ edge_voltage
                    found.setdefault(total, (path[:], edge_id))
            return
        for nxt, edge_voltage, _ in darts[current]:
            if nxt not in used:
                used.add(nxt)
                path.append(nxt)
                dfs(path, used, voltage ^ edge_voltage)
                path.pop()
                used.remove(nxt)

    dfs([start], {start}, 0)
    assert set(found) == {0, 1}
    return {"voltage_zero_components": 2, "voltage_one_lift_vertices": 36, "voltages_found": sorted(found)}


def move_graph_audit():
    expected = {4: (16, 24, 8, 12), 5: (25, 48, 13, 24), 6: (36, 80, 18, 40)}
    boards = {}
    for n in (4, 5, 6):
        vertices, adjacency, edges, orbits, orbit_of, edge_orbits = orbit_data(n)
        assert (len(vertices), len(edges), len(orbits), len(edge_orbits)) == expected[n]
        equitable_check(adjacency, orbits, orbit_of)
        boards[str(n)] = {
            "vertices": len(vertices),
            "edges": len(edges),
            "vertex_orbits": len(orbits),
            "edge_orbits": len(edge_orbits),
        }

    _, adjacency5, _, orbits5, orbit_of5, edge_orbits5 = orbit_data(5)
    center = (2, 2)
    center_orbit = orbit_of5[center]
    outgoing = []
    for edge_orbit in edge_orbits5:
        lifts = [e for e in edge_orbit if center in e]
        if lifts:
            outgoing.append(len(lifts))
    assert center_orbit < len(orbits5)
    assert sorted(outgoing) == [2, 2, 2, 2]
    assert len(adjacency5[center]) == 8

    c4_orbits = [((0, 1), (2, 3)), ((0, 3), (1, 2))]
    c4_voltages = []
    for edge_orbit in c4_orbits:
        terminal = next(b if a == 0 else a for a, b in edge_orbit if 0 in (a, b))
        c4_voltages.append(0 if terminal == 1 else 1)
    assert c4_voltages == [0, 1]

    return {
        "boards": boards,
        "equitable_horizons_checked": [0, 1, 2, 3, 4],
        "five_by_five_center_outgoing_dart_orbits": 4,
        "lifts_per_center_dart_orbit": outgoing,
        "c4_parallel_edge_voltages": c4_voltages,
        "six_by_six": six_board_quotient_cycles(),
    }


def main():
    result = {
        "status": "pass",
        "hurwitz_support_and_positivity": hurwitz_audit(),
        "move_graph_lifting_and_monodromy": move_graph_audit(),
    }
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()