"""diverge.py -- where the quarantine stops: two routes split at position
i, and which later menus keep them from tying.

QUESTION. The quarantine theorem: in a coprime grown world no two
routes of a dated fiber tie (carry equal posteriors at every beta), and
in a FIRST-COPRIME world (every menu after the first move prime to it)
no set of routes meeting two first moves is flat for the first move at
every beta. A last-move world (menus prime to the last move only) ties
2,3,5 and 3,2,5; a first-coprime world ties a,b,c and a,c,b. Where does
the quarantine stop, for menus that avoid the primes of some earlier
moves and not all? Positions are counted 1, 2, ... along a route; a
world AVOIDS POSITION i when every menu a route meets after its i-th
move is prime to that move.

THE ARGUMENT (written before the engine).
  (A) THE SHARED PREFIX CANCELS. Let two distinct routes r, r' of one
      dated fiber (endpoint N, age t) first differ at position i, with
      i-th moves a != b, from the state s their shared prefix reaches.
      Menus are functions of the route so far, so the prefix passes the
      same states and menus, s's included; those Psi cancel from both
      D (the formal Dirichlet polynomials being a domain), leaving D'
      and D'', the products of the Psi of the menus met after position
      i. With x_q = q^-beta independent (firstmove.py's (A)), r and r'
      tie iff D' = D'' as polynomials in the x_q.
  (B) THE PAIR CONDITION Q. Say a prime p SEPARATES the pair when p
      divides one i-th move, say a, not the other, and every menu r
      meets after position i is prime to p. Then N/s = a times r's later
      moves, all prime to p, so v_p(N/s) = v_p(a) >= 1; N/s = b times
      r''s later moves and p does not divide b, so some later move of r'
      carries p, its menu's Psi holds that monomial with coefficient 1,
      and D'' has positive x_p-degree, D' degree 0. Coefficients being
      nonnegative, 1/D'' -> 0 as x_p grows while 1/D' stays: no tie,
      and the cleared difference, a nonzero finite sum of exponentials
      in beta, vanishes at finitely many beta.
  (C) A WORLD AVOIDING POSITION i quarantines every pair splitting at
      i. Each route's later moves are prime to its own i-th move, so a
      and b are unitary divisors of N/s; a != b, so they differ in their
      primes, and a prime of one absent from the other separates (B).
      THEOREM (to be ruled). In a world avoiding the positions of a set
      T, no two routes of a dated fiber that first differ at a position
      of T tie, at any age; menus may depend on the route so far.
      Coprime is T = every position, the state being the product of the
      moves; the route quarantine is its case, the first-move theorem
      its class form at i = 1.
  (D) CLASS FORM. Fix a prefix of length i - 1; the routes of a fiber
      extending it, grouped by their i-th move, meeting two i-th moves
      or more, in a world avoiding position i: no grouping is flat for
      the i-th move at every beta. The same proof: the prefix's Psi are
      a common factor of every D, the class of a is blind to x_p, every
      route of the class of b takes p later.
  (E) SHARPNESS, by hand. For each j >= 1 the world W_j: distinct primes
      q_1 .. q_(j-1) and b, c coprime to each other and to them;
      menu(q_1 .. q_k) = {q_(k+1)} for k < j - 1, the seed's menu
      {q_1} (or {b, c} at j = 1), menu(q_1 .. q_(j-1)) = {b, c}, and
      menu(q_1 .. q_(j-1), b) = menu(q_1 .. q_(j-1), c) = {b, c}. The
      routes ..., b, c and ..., c, b reach one endpoint at age j + 1
      with one D: a tie splitting at j. W_j avoids every position but j:
      after position i < j the menus are later q's and {b, c}, prime to
      q_i; position j + 1 is last. So no hypothesis on positions alone
      does better than (C): the pairs splitting at j are quarantined in
      every world avoiding T iff j is in T. TRANSPLANT from the first-move
      case: the separating prime there came from FIRST-COPRIME; here
      from avoidance at the split, re-derived in (C).
  (F) Q IS NOT NECESSARY pair by pair: a pair can fail Q and still not
      tie (most do); the iff of (E) is at the level of position sets.

DESIGN. quarantine.py's engine: menus keyed by the route so far, drawn
at random as 1 or 2 elements of the allowed moves, routes walked
breadth first carrying the menus they pass, D an exact integer
Dirichlet polynomial. ARMS: for every subset T of {1, 2, 3}, the menu
at a prefix allows m iff gcd(m, i-th move) = 1 for every i in T at or
before the prefix's length; on two universes, US = {2, 3, 4, 5, 6, 8,
9, 10, 12, 15} (quarantine.py's) and the tie-rich 3-smooth UT = {2, 3,
4, 6, 8, 9}; 1000 worlds per arm, seeds fixed per arm; dated fibers of
age 2, 3 and 4. The singleton arms {1}, {2}, {3} are the derivation's
corner: one position avoided, every other free to recycle. For every
pair of distinct routes of a fiber: the split position i, the tie
(formal D equal), Q (B), and AVOID, both routes' later menus prime to
their own i-th move. For every fiber, prefix and i: the class form (D)
on groupings whose every route has AVOID at i, read by
quarantine.first_move_robust on the routes shifted to start at i.

CONTROLS, read first.
  C1 W_1, W_2 and W_3 of (E) (primes 7, 11 and b, c = 2, 3) tie one
     pair splitting at j = 1, 2, 3, fail Q at it, and avoid every
     position but j (read over their routes) and not j.
  C2 the kill can fire: Q_NEXT, Q with "every later menu" cut to the
     next menu only, holds at the tied pair 2,3,5 and 3,2,5 of
     quarantine.py's last-move world, so a kill on Q_NEXT fires there;
     its count over the arms is printed.
  C3 the tuned world's pair 2,3 and 3,2 at (6, 2) (flat at beta = 1
     only) has Q and does not tie.
  C4 the class reader: the depth column's (36, 4) is flat for the first
     move (quarantine.first_move_robust) and its routes fail AVOID at
     position 1.

PREDICTIONS (frozen before the engine).
  P1 C1 to C4 as stated.
  P2 KILL 1: 0 tied pairs with Q over all arms, the pairs with Q above
     0 in every arm (where the kill can fire).
  P3 every tie splits at a position outside its arm's T; the arm
     T = {1, 2, 3} ties no pair; the arm T = {} on UT ties pairs
     splitting at each of 1, 2 and 3.
  P4 KILL 2 (class form): 0 groupings with AVOID flat for the i-th move
     at every beta, groupings read above 0.
  P5 pairs failing Q and not tied above 0 in the arm T = {} on US.
KILLS. P2's or P4's count above 0 is a pair or grouping the argument
misreads: the theorem is wrong as stated until it is read by hand. If
P3's control at T = {} misses a position, the arms cannot see ties
splitting there and the reach is named, nothing killed.
UNFROZEN PRINT, a lead and no verdict: the i-th move as a datum over a
whole fiber, prefixes free, in arms avoiding position i: fibers flat
for it at every beta, counted.

FINDINGS.
  P1 held: W_1, W_2, W_3 tie (2,3)/(3,2), (7,2,3)/(7,3,2) and
     (7,11,2,3)/(7,11,3,2), fail Q, and avoid every position but their
     split; the last-move pair has Q_NEXT and not Q; the tuned pair has
     Q and no tie; the depth column's (36, 4) is flat for the first
     move with every route failing AVOID at 1.
  P2 held, KILL 1 missed: 0 tied pairs with Q of 3097 pairs with Q,
     over 8744 pairs in 16 arms, Q above 0 in every arm. The weakened
     Q_NEXT ties 6 of the 943 tied pairs: a next-menu hypothesis would
     have fired the kill.
  P3 held: 0 ties split inside their arm's T; the arms T = {1, 2, 3}
     tie no pair; UT at T = {} ties pairs splitting at 1, 2 and 3 (5, 2,
     4). Ties by split over the arms: 16 at 1, 465 at 2, 462 at 3, all
     outside T. US at T = {} ties no pair at all; the tie-rich
     universe carries the control.
  P4 held, KILL 2 missed: 0 of 2386 AVOID groupings flat for the i-th
     move at every beta.
  P5 held: 199 pairs of US at T = {} fail Q and do not tie (4704 over
     the arms): Q is sufficient, not necessary, pair by pair.
  The verifier is the argument (A)..(E), by hand; the arms read that
  the argument's steps meet no counterexample on these populations
  (toy scale: ages 2 to 4, menus of 1 or 2 moves, 16,000 worlds).
  LEAD (unfrozen, broken down by i after the first run): the i-th move
  over a whole fiber, prefixes free, is flat at every beta at 140 of
  4949 reads in arms avoiding i, 3 at i = 2 and 137 at i = 3, every
  one in an arm leaving some position before i unavoided; with every
  position up to i avoided, 0 of 1530 (856 at i = 1, the first-move
  theorem's case, 557 at i = 2, 117 at i = 3). A fiber that is exactly
  one pair tied at an earlier split, with different i-th moves, is flat
  for the i-th move by hand (W_2 at i = 3 is one). UT at
  T = {1, 3} prints 105 flat reads and 105 ties split at 2, tallied
  apart: that they are the same fibers is not read.
  Pattern, not proved: avoiding every position up to i hides the i-th
  move on no fiber.

RUN RECORD. python diverge.py: 12 of 12 checks, 0.7 s, peak commit
8.3 MB. The LEAD's breakdown by i and its specimen print were added
after the first run; no frozen check changed.
"""

import itertools
import random
import sys
import time
from collections import defaultdict
from math import gcd

import quarantine as Q

CHECKS = []
UT = (2, 3, 4, 6, 8, 9)


def check(name, ok, detail=""):
    CHECKS.append(bool(ok))
    print(f"  [{'PASS' if ok else 'FAIL'}] {name}" + (f": {detail}" if detail
                                                      else ""))


def primes(n):
    out, q = [], 2
    while q * q <= n:
        if n % q == 0:
            out.append(q)
            while n % q == 0:
                n //= q
        q += 1
    return out + ([n] if n > 1 else [])


def split(r1, r2):
    """1-indexed position of the first differing move."""
    for k, (x, y) in enumerate(zip(r1, r2)):
        if x != y:
            return k + 1
    raise ValueError("routes do not differ")


def avoid(r, ms, i):
    """Every menu the route meets after its i-th move is prime to it.
    ms[k] is the menu met before move k + 1, so ms[i:] come after move i."""
    return all(gcd(m, r[i - 1]) == 1 for mu in ms[i:] for m in mu)


def separates(p, ms, i, nxt=False):
    menus = ms[i:i + 1] if nxt else ms[i:]
    return all(m % p for mu in menus for m in mu)


def q_pair(a, b, i, nxt=False):
    """(B)'s Q: a prime of one i-th move, not of the other, avoided by
    every later menu of its own route (Q_NEXT: by the next menu only)."""
    (r1, m1), (r2, m2) = a, b
    x, y = r1[i - 1], r2[i - 1]
    return any(separates(p, m1, i, nxt) for p in primes(x) if y % p) \
        or any(separates(p, m2, i, nxt) for p in primes(y) if x % p)


def tied(a, b):
    return Q.dkey(Q.product(a[1])) == Q.dkey(Q.product(b[1]))


def world_avoids(menu, age, i):
    return all(avoid(r, ms, i) for r, n, ms in Q.walk(menu, age))


def w_world(j):
    """(E)'s W_j with q = 7, 11 and b, c = 2, 3: (menu, age, endpoint)."""
    qs = (7, 11)[:j - 1]
    table = {qs[:k]: (qs[k],) for k in range(len(qs))}
    table[qs] = (2, 3)
    table[qs + (2,)] = table[qs + (3,)] = (2, 3)
    end = 6
    for q in qs:
        end *= q
    return Q.by_prefix(table), j + 1, end


def make_allowed(T):
    def allowed(m, n, prefix):
        return all(gcd(m, prefix[i - 1]) == 1 for i in T if i <= len(prefix))
    return allowed


def read_arm(menus, ages, T):
    t = defaultdict(int)
    for menu in menus:
        for age in ages:
            for items in Q.fibers(menu, age).values():
                if len(items) < 2:
                    continue
                for a, b in itertools.combinations(items, 2):
                    i = split(a[0], b[0])
                    t["pairs"] += 1
                    q = q_pair(a, b, i)
                    t["Q pairs"] += q
                    if tied(a, b):
                        t["ties"] += 1
                        t[f"tie@{i}"] += 1
                        t["KILL1 tie with Q"] += q
                        t["tie with Q_NEXT"] += q_pair(a, b, i, nxt=True)
                    elif not q:
                        t["no Q, no tie"] += 1
                for i in range(1, age + 1):
                    groups = defaultdict(list)
                    for r, ms in items:
                        groups[r[:i - 1]].append((r, ms))
                    for g in groups.values():
                        if len({r[i - 1] for r, _ in g}) < 2 or \
                                not all(avoid(r, ms, i) for r, ms in g):
                            continue
                        t["class read"] += 1
                        t["KILL2 class flat"] += Q.first_move_robust(
                            [(r[i - 1:], ms) for r, ms in g])
                    if i in T and len({r[i - 1] for r, _ in items}) >= 2:
                        pre = set(range(1, i + 1)) <= set(T)
                        f = Q.first_move_robust(
                            [(r[i - 1:], ms) for r, ms in items])
                        t["LEAD read"] += 1
                        t["LEAD flat"] += f
                        t[f"LEAD read@{i}" + ("+" if pre else "")] += 1
                        t[f"LEAD flat@{i}" + ("+" if pre else "")] += f
                        if f and pre:
                            print(f"    SPECIMEN i={i} T={T}: "
                                  f"{[r for r, _ in items]}")
    return dict(t)


def controls():
    print("CONTROLS")
    for j in (1, 2, 3):
        menu, age, end = w_world(j)
        items = Q.fibers(menu, age)[end]
        a, b = items
        others = all(world_avoids(menu, age, i)
                     for i in range(1, age + 1) if i != j)
        check(f"C1 W_{j}: one tied pair splitting at {j}, Q fails, avoids "
              f"every position but {j}",
              len(items) == 2 and tied(a, b) and split(a[0], b[0]) == j
              and not q_pair(a, b, j) and others
              and not world_avoids(menu, age, j),
              f"{[r for r, _ in items]}")
    a, b = Q.fibers(Q.LAST, 3)[30]
    check("C2 last-move (30, 3): tied, split 1, Q_NEXT holds, Q fails",
          tied(a, b) and split(a[0], b[0]) == 1
          and q_pair(a, b, 1, nxt=True) and not q_pair(a, b, 1))
    a, b = Q.fibers(Q.TUNED, 2)[6]
    check("C3 tuned (6, 2): Q holds, no tie",
          q_pair(a, b, split(a[0], b[0])) and not tied(a, b))
    depth = Q.fibers(lambda p, n: (2, 3), 4)[36]
    check("C4 depth column (36, 4): flat for the first move, every route "
          "fails AVOID at 1", Q.first_move_robust(depth)
          and not any(avoid(r, ms, 1) for r, ms in depth))


def main():
    t0 = time.time()
    controls()
    subsets = [T for k in range(4)
               for T in itertools.combinations((1, 2, 3), k)]
    out = {}
    seed = 0
    for uname, uni in (("US", Q.US), ("UT", UT)):
        for T in subsets:
            rng = random.Random(100 + seed)
            seed += 1
            allowed = make_allowed(T)
            menus = (Q.random_world(rng, uni, allowed, "prefix", (1, 2))
                     for _ in range(1000))
            out[(uname, T)] = read_arm(menus, (2, 3, 4), T)
            print(f"    {uname} T={T}: {out[(uname, T)]}")
    tot = defaultdict(int)
    for d in out.values():
        for k, v in d.items():
            tot[k] += v
    print(f"    TOTAL: {dict(tot)}")
    print(f"    C2 over the arms: ties with Q_NEXT {tot['tie with Q_NEXT']}"
          f" of {tot['ties']} ties")
    check("P2 KILL 1: no tied pair with Q; Q pairs above 0 in every arm",
          tot["KILL1 tie with Q"] == 0
          and all(d.get("Q pairs", 0) > 0 for d in out.values()),
          f"{tot['KILL1 tie with Q']} of {tot['Q pairs']} Q pairs")
    inside = sum(d.get(f"tie@{i}", 0) for (u, T), d in out.items()
                 for i in T)
    check("P3 every tie splits outside its arm's T", inside == 0,
          f"{inside} inside")
    full = sum(out[(u, (1, 2, 3))].get("ties", 0) for u in ("US", "UT"))
    check("P3 the arms T = {1, 2, 3} tie no pair", full == 0, f"{full}")
    free = out[("UT", ())]
    got = [free.get(f"tie@{i}", 0) for i in (1, 2, 3)]
    check("P3 control: UT T = {} ties pairs splitting at 1, 2 and 3",
          all(g > 0 for g in got), f"{got}")
    check("P4 KILL 2: no AVOID grouping flat for the i-th move",
          tot["KILL2 class flat"] == 0 and tot["class read"] > 0,
          f"{tot['KILL2 class flat']} of {tot['class read']}")
    nq = out[("US", ())].get("no Q, no tie", 0)
    check("P5 US T = {}: pairs failing Q and not tied above 0", nq > 0,
          f"{nq}")
    print(f"    LEAD (unfrozen): the i-th move over whole fibers in arms "
          f"avoiding i: {tot['LEAD flat']} flat of {tot['LEAD read']}; "
          f"by i, + when every position to i is avoided: "
          f"{ {k: v for k, v in sorted(tot.items()) if '@' in k and 'LEAD' in k} }")
    print(f"{sum(CHECKS)}/{len(CHECKS)} checks passed, "
          f"{time.time() - t0:.1f} s")
    sys.exit(0 if all(CHECKS) else 1)


if __name__ == "__main__":
    main()