#!/usr/bin/env python3
"""Stage 3 preliminary check (throwaway; superseded by Stage C oracles).

1. Verifies the explicit isomorphism psi: P(n,k) -> P(n,l) when k*l == 1 (mod n),
   gcd(k,n) = 1, defined by psi(v_{jk}) = u_j, psi(u_{jk}) = v_j, and the
   complement identification P(n,l) = P(n,n-l), for all 11 <= n <= 60 and
   all l with 5*l == +-1 (mod n).  Lists the cases where the partner l' =
   min(l, n-l) is <= 4 (values then follow from the k = 2,3,4 literature).
2. Replays the planned 12-vertex forcing order for S = {u_0..u_11} in P(n,5),
   n >= 13, step by step (each force must be legal at the moment it is applied).
"""
from math import gcd

def P(n, k):
    adj = {}
    def add(a, b):
        if a == b:
            raise ValueError("self loop")
        adj.setdefault(a, set()).add(b); adj.setdefault(b, set()).add(a)
    for i in range(n):
        add(('u', i), ('u', (i + 1) % n)); add(('u', i), ('v', i)); add(('v', i), ('v', (i + k) % n))
    return adj

def edges(adj):
    return {frozenset((a, b)) for a in adj for b in adj[a]}

def is_iso_map(adj1, adj2, phi):
    if len(set(phi.values())) != len(adj1) or len(adj1) != len(adj2):
        return False
    return {frozenset((phi[a], phi[b])) for e in edges(adj1) for a, b in [tuple(e)]} == edges(adj2)

print("== isomorphisms P(n,5) ~ P(n,l), 5*l == +-1 (mod n) ==")
small_partner = []
for n in range(11, 61):
    if gcd(5, n) != 1:
        print(f"n={n}: gcd(n,5)=5, inner subgraph is 5 cycles of length {n//5}; no inversion of 5 mod n")
        continue
    l = pow(5, -1, n)            # 5*l == 1 (mod n)
    for ll, sign in ((l, '+1'), ((-l) % n, '-1')):
        if not (ll >= 1 and n > 2 * ll):
            ll_c = n - ll
        else:
            ll_c = ll
        # explicit map P(n,5) -> P(n,l) for 5*l == 1
        A = P(n, 5)
        B = P(n, l)
        phi = {}
        for j in range(n):
            phi[('v', (j * 5) % n)] = ('u', j)
            phi[('u', (j * 5) % n)] = ('v', j)
        ok = is_iso_map(A, B, phi)
        # complement identification: P(n,l) ~ P(n,n-l) via v_i -> v_{-i}, u_i -> u_{-i}
        C = P(n, (n - l) % n) if 0 < (n - l) % n else None
        ok2 = C is not None and is_iso_map(B, C, {('u', i): ('u', (-i) % n) for i in range(n)} | {('v', i): ('v', (-i) % n) for i in range(n)})
        break
    partner = min(l, n - l)
    tag = ""
    if partner <= 4:
        tag = f"  <-- partner k'={partner}: value known from literature"
        small_partner.append((n, partner))
    print(f"n={n}: 5^-1={l}, partner k'={partner}, explicit map ok={ok}, complement map ok={ok2}{tag}")
print("small partners:", small_partner)

print("\n== replay of the 12-vertex forcing order, S={u_0..u_11}, P(n,5) ==")
def legal_force(adj, black, src, tgt):
    white = [w for w in adj[src] if w not in black]
    return src in black and white == [tgt]

for n in range(13, 41):
    adj = P(n, 5)
    black = {('u', i) for i in range(12)}
    seq = [(('u', i), ('v', i)) for i in range(1, 11)] + [(('v', 5), ('v', 0)), (('v', 6), ('v', 11))]
    for j in range(12, n):
        seq += [(('u', j - 1), ('u', j)), (('v', j - 5), ('v', j))]
    ok = True
    for s, t in seq:
        if not legal_force(adj, black, s, t):
            ok = False; print(f"n={n}: ILLEGAL force {s}->{t}"); break
        black.add(t)
    print(f"n={n}: forces={len(seq)}, all legal={ok}, all black={len(black) == 2 * n}")