ithmove.py

Checks: FORGET: The quarantine theorem theorem.

Cited on: FORGET.

To run it: save ithmove.py, with quarantine.py beside it; standard library only.

"""ithmove.py -- does avoiding every position up to i hide the i-th move
on no dated fiber, the routes free to differ before it?

QUESTION. The quarantine theorem: in a world AVOIDING POSITION i (every
menu a route meets after its i-th move is prime to that move), no set
of routes of one age to one endpoint, SHARING THEIR FIRST i - 1 MOVES
and meeting two i-th moves, is flat for the i-th move at every beta.
diverge.py printed a lead past that: over a WHOLE dated fiber, prefixes
free, the i-th move was flat at every beta only in arms leaving some
position before i unavoided, never (0 of 1530) when every position up
to i is avoided; toy scale (ages 2 to 4, menus of 1 or 2, i <= 3). Is
the lead a law, and at what scale was it silent? A second, hand
question rides along: the theorem's sharpness was stated over SETS of
avoided positions; the open boundary asked about menus that avoid the
primes of some earlier moves and not all, which is a WINDOW per menu.

THE ARGUMENT (written before the engine).
  (A) THE READ. Flat for the i-th move at every beta, over a set F of
      routes to N at age t, means the class sums S_c = sum of 1/D_r over
      the routes of F with i-th move c agree for every two c met. With
      x_q = q^-beta independent (firstmove.py's (A)) this is an identity
      of rational functions in the x_q, so it holds at every point of
      any field where no D_r vanishes. Reading it modulo a prime P at a
      random point: a mismatch proves F not flat (a sound NO); agreement
      at every point drawn is a candidate, false with probability at
      most deg / P per point (Schwartz-Zippel), deg <= the sum of the
      D_r's total degrees, below 10^5 here (at most 729 routes, each D
      of degree at most 6 * 5) against P = 2^61 - 1; a point where some
      D_r vanishes is redrawn. A candidate is
      re-read at 16 points modulo 2^89 - 1 and printed as a specimen.
  (B) WHAT AVOIDING 1..i FORCES. Every menu after move k <= i is prime
      to m_k, so m_1, ..., m_i are pairwise coprime and each is prime
      to every other move of its route: each is a unitary divisor of N,
      and a prime p of an i-th move a is carried by no other move of a
      route of a's class. Two i-th moves a != b differ in their primes
      (p | a, p not dividing b), so every route of b's class carries p
      at another position, before i or after it.
  (C) WHERE THE KILL CAN FIRE. If every i-th move class of F holds one
      route, flat is a tie of each two, and two routes with different
      i-th moves first differ at a position k <= i, avoided: no tie
      (the theorem). So a flat F needs a class of two routes or more: a
      read is LIVE when F meets two i-th moves and some class holds two
      routes. Only live reads count toward the kill.
  (D) WHY THE THEOREM'S PROOF DOES NOT CARRY. The class of a is blind
      to x_p only after position i; the menus before it, met by routes
      that differ there, may offer multiples of p, so S_a moves with x_p
      too. The derivation's corner is a world whose early menus offer
      the primes of later i-th moves: the exhaustive coprime tables of
      quarantine.py (moves 2 to 6, state menus, every allowed menu
      nonempty) hold it at age 3, where the fiber (30, 3) meets every
      order of 2, 3, 5 that its menus allow and each class by the
      second or third move can hold two routes.
  (E) THE WINDOW FORM, by hand. Let a hypothesis give each length k a
      set S(k) of positions <= k, and admit the worlds whose menu after
      k moves is prime to the moves at the positions of S(k). THEOREM
      (by hand): the pairs splitting at j are quarantined in every
      admitted world iff j is in S(k) for every k >= j below the age.
      If so, the admitted worlds avoid position j: the theorem. If not,
      take k0 >= j with j not in S(k0), distinct primes q_1 .. q_(j-1),
      b, c, r_(j+1) .. r_(k0), and the world offering q_(k+1) after
      q_1 .. q_k (k < j - 1), then {b, c}, then r_(k+1) after k moves
      for j <= k < k0, then {b, c}. Its routes ..., b, r.., c and ...,
      c, r.., b reach one endpoint at age k0 + 1 with one D, a tie
      splitting at j; every menu but the last holds fresh primes, and
      the last, {b, c}, is prime to the moves at S(k0), which omits j.
      The last-move world is the window S(k) = {k}, at j = 1 and k0 = 2.
      Position sets are the windows S(k) = T restricted to k.

DESIGN. quarantine.py's engine (menus keyed by the route so far, drawn
at random, routes walked breadth first carrying the menus they pass).
Reads: every dated fiber, every position i of the arm's read set; a read
is LIVE as in (C), and LIVE reads are read by (A).
  LEAD ARMS (the lead's hypothesis):
    L2, L3: moves UL (quarantine.py's 7-smooth 2..36), menus of 1 to 3,
      avoiding positions 1..I (I = 2, 3) and free after, ages 5 and 6,
      read i = 2..I. 600 worlds each.
    LC: coprime route menus on UL, menus of 1 to 3, ages 3 and 4 (a
      coprime route on UL holds at most four moves), read i = 2..age.
      2000 worlds.
    EX: quarantine.exhaustive_worlds() (87,885 coprime state tables),
      ages 2 and 3, read i = 2..age. The derivation's corner (D).
  CONTROL ARMS (one position before i left unavoided), on L2's and L3's
    universe, sizes and ages, 600 worlds each: K2 avoids {2}, read
    i = 2; K3a avoids {2, 3}, read i = 2, 3; K3b avoids {1, 3}, read
    i = 3.
  i = 1 reads (the theorem's own case) are taken in L2, L3, LC and EX
    and counted apart.

CONTROLS, read first.
  C1 the hand worlds: W_2 (7, then {2, 3}, then {2, 3}) at (42, 3) and
     the world seed {2, 3}, menu(2) = menu(3) = {5}, menu(2, 5) =
     menu(3, 5) = {2, 3} at (30, 3) are flat for the third move, read
     by (A); W_2 avoids positions 1 and 3 and not 2, the other avoids
     2 and 3 and not 1.
  C2 the instrument: on every live read of at most 8 routes in the
     control arms, (A)'s verdict equals quarantine.first_move_robust on
     the routes shifted to start at i (exact), with flat and not-flat
     both met.
  C3 (E)'s construction: for every window family S(1), S(2), S(3)
     (64 families) and every j <= 3 and k0 in j..3 with j not in
     S(k0), the built world obeys its windows on every route and ties
     the pair splitting at j; and for every family with j in S(k) at
     every k >= j, nothing is built.

PREDICTIONS (frozen before the engine).
  P1 C1, C2, C3 as stated.
  P2 the control arms: live reads flat for the i-th move above 0 in
     K2, K3a and K3b together (the reader sees flatness at this scale
     when an earlier position is unavoided).
  P3 KILL: 0 live reads flat for the i-th move over L2, L3, LC and EX;
     live reads above 0 at i = 2 and at i = 3 in L2 and L3 together at
     age 5 or 6, and above 0 at i = 2 and i = 3 in EX.
  P4 0 flat among the i = 1 reads (the theorem; a count above 0 is a
     bug in the reader).
KILLS. P3's flat count above 0 is a fiber that hides its i-th move with
every position up to i avoided: the lead is false, read the specimen by
hand. If P2 reads 0, or P3's live bars miss, the scale cannot see the
question: the reach is named, nothing is verdicted.

CHANGES AFTER THE FREEZE: (1) to (3) at rehearsal before any verdict
was read, (4) and (5) after the run.
  (1) UL has four primes, so avoiding three positions leaves almost no
      route past age 4 (L3 read nothing): the three-position arms moved
      to U13, the 13-smooth numbers 2 to 40.
  (2) At ages 5 and 6 with menus of 3 the exact reader took 220 s at 5%
      scale and the control arms read no flat: every K and L arm now
      runs on U13 at ages 4 and 5 with menus of 1 or 2, 1000 worlds,
      and C2 reads live reads of at most 4 routes, plus C1's fibers.
  (3) P2 as frozen (K2, K3a, K3b) read 0: their cheap flats are
      single-route classes flattened by a tie at an unavoided split,
      which LIVE excludes, and no multi-route flat class was met there.
      Arms were added: lead arms L2s, L3s and control arms K2s, K3s on
      U5 (5-smooth to 12) at ages 3 and 4; KF (free state menus on the
      3-smooth UT); and EXF, every free state table on the moves 2 and 3
      with every menu nonempty, to age 4 (3^10 tables, the depth column
      among them); P2's check reads all control arms, the bars ages 4, 5.
  (4) After the run's audit: distinct live reads counted at i >= 2 only,
      EXF's flats printed by age, and a redraw at 2^89 - 1 when a D
      vanishes there (it had read as a NO).
  (5) After the run, since no control arm read a live flat at EX's age
      3: C4, a built control, the free state world {1: {4, 6},
      4: {3, 6}, 6: {2, 4}, 12: {2, 4}, 24: {2, 4}} on the moves 2 to
      6, avoiding neither position 1 nor 2, whose (48, 3) is live and
      flat for the third move (by hand: 12 and 24 offer one menu, so
      both class sums are (1/Psi_4 + 1/Psi_6) / (Psi_1 Psi_12)).

FINDINGS.
  P1 held: W_2 at (42, 3) and the seed-{2, 3} world at (30, 3) are flat
     for the third move, avoiding (1, 3) and (2, 3) and not 2 and 1; the
     reader equals the exact reader on 37790 of 37790 reads, 417 exact
     flat; (E)'s construction obeys its windows and ties at j in 192 of
     192 built worlds over the 64 window families, with 56 (family, j)
     quarantined and none built.
  P2 FAILED as frozen: K2, K3a, K3b read 0 live flats. Of the arms
     added, only EXF reads any, 441, every one at age 4 (63 at i = 2,
     171 at 3, 207 at 4) and on one fiber, (36, 4); its 3888 live reads
     at age 3 at i = 2 and at i = 3 hold none, and the random controls
     (K3a 46, K3b 57, K2s 33, K3s 34, KF 485 distinct live reads) none.
     No random control family matches EX at its age 3. C4, built after
     the run, shows only that the reader sees a live flat at age 3:
     (48, 3) at 4,3,4; 4,6,2; 6,2,4; 6,4,2 is live and flat for the
     third move, by the reader and exactly, one world outside EX's
     coprime family.
  P3 the kill's count: 0 of 55041 live reads flat for the i-th move
     with every position to i avoided, 9793 distinct (EX 9088, L2 81,
     L3 280, L2s 18, L3s 39, LC 287); EX 25152 at i = 2 and 29184 at
     i = 3; L2 + L3 102 and 108 at i = 2, ages 4 and 5, 36 and 115 at
     i = 3. By the frozen KILLS nothing is verdicted (P2); the random
     arms' silence is cheap, their controls reading no live flat.
  P4 held: 0 of 34431 i = 1 reads flat.
  The x_p limits at the i-th move's primes alone do not close the lead:
  as x_p grows the class sums concentrate on the routes of least
  x_p-degree, as it falls on those of greatest least-degree, and
  neither forces two classes apart. (E) is a hand proof; its check
  holds by construction and reads only that the built worlds are as
  written.

RUN RECORD. python ithmove.py: 9 of 9 checks, 6.1 s, peak commit 15.7
MB.
"""

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

import quarantine as Q

CHECKS = []
DISTINCT = defaultdict(set)
C1_EXACT = []
AGES = (4, 5)
U5 = (2, 3, 4, 5, 6, 8, 9, 10, 12)
UT = (2, 3, 4, 6, 8, 9)
LEAD = ("L2", "L3", "L2s", "L3s", "LC", "EX")
U13 = tuple(m for m in range(2, 41)
            if all(m % q for q in (17, 19, 23, 29, 31, 37)))
P1, P2 = (1 << 61) - 1, (1 << 89) - 1
_FAC = {}


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


def factor(n):
    if n not in _FAC:
        out, m, q = {}, n, 2
        while q * q <= m:
            while m % q == 0:
                out[q] = out.get(q, 0) + 1
                m //= q
            q += 1
        if m > 1:
            out[m] = out.get(m, 0) + 1
        _FAC[n] = out
    return _FAC[n]


class Reader:
    """(A): class sums of 1/D modulo P at random points of independent
    x_q, one dict of residues per point, drawn lazily per prime."""

    def __init__(self, rng, P, npts):
        self.rng, self.P = rng, P
        self.pts = [dict() for _ in range(npts)]
        self.psi = [dict() for _ in range(npts)]

    def x(self, k, q):
        pt = self.pts[k]
        if q not in pt:
            pt[q] = self.rng.randrange(1, self.P)
        return pt[q]

    def mono(self, k, m):
        v = 1
        for q, e in factor(m).items():
            v = v * pow(self.x(k, q), e, self.P) % self.P
        return v

    def Psi(self, k, mu):
        c = self.psi[k]
        if mu not in c:
            c[mu] = sum(self.mono(k, m) for m in mu) % self.P
        return c[mu]

    def flat(self, items, i):
        """None if some D vanishes at a point, else whether every class
        sum agrees at every point."""
        P = self.P
        for k in range(len(self.pts)):
            sums = defaultdict(int)
            for r, ms in items:
                d = 1
                for mu in ms:
                    d = d * self.Psi(k, mu) % P
                if d == 0:
                    return None
                sums[r[i - 1]] = (sums[r[i - 1]] + pow(d, P - 2, P)) % P
            if len(set(sums.values())) > 1:
                return False
        return True


def live(items, i):
    cls = defaultdict(int)
    for r, _ in items:
        cls[r[i - 1]] += 1
    return len(cls) >= 2 and max(cls.values()) >= 2


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


def avoids(menu, age, k):
    return all(gcd(m, r[k - 1]) == 1 for r, n, ms in Q.walk(menu, age)
               for mu in ms[k:] for m in mu)


def read_arm(name, worlds, ages, reads, rd, rd2, t, exact=False):
    """Every dated fiber of every world at every age; every i in
    reads(age); live reads by (A), candidates re-read by rd2."""
    for menu in worlds:
        t["worlds"] += 1
        for age in ages:
            for n, items in Q.fibers(menu, age).items():
                if len(items) < 2:
                    continue
                for i in reads(age):
                    if not live(items, i):
                        continue
                    f = rd.flat(items, i)
                    while f is None:
                        rd = Reader(rd.rng, rd.P, len(rd.pts))
                        f = rd.flat(items, i)
                    if f:
                        f2 = rd2.flat(items, i)
                        while f2 is None:
                            rd2 = Reader(rd2.rng, rd2.P, len(rd2.pts))
                            f2 = rd2.flat(items, i)
                        f = f2
                        if f and name in LEAD:
                            print(f"    SPECIMEN {name} i={i} age={age} "
                                  f"N={n}: {[r for r, _ in items]}")
                    key = "i=1" if i == 1 else f"i={i}"
                    if i >= 2:
                        DISTINCT[name].add((i, tuple(items)))
                    if f and name == "EXF":
                        t[f"flat i={i} age={age}"] += 1
                    t[f"live {key}"] += 1
                    t[f"live {key} age={age}"] += 1
                    t[f"flat {key}"] += f
                    if exact and len(items) <= 4:
                        e = Q.first_move_robust(
                            [(r[i - 1:], ms) for r, ms in items])
                        t["C2 read"] += 1
                        t["C2 agree"] += e == f
                        t["C2 exact flat"] += e
    return t


def window_world(j, k0):
    """(E)'s construction: (menu, age, the tied pair's endpoint)."""
    fresh = [11, 13, 17, 19, 23, 29, 31, 37]
    qs = tuple(fresh[:j - 1])
    b, c = fresh[j - 1], fresh[j]
    rs = tuple(fresh[j + 1:j + 1 + k0 - j])
    table = {qs[:k]: (qs[k],) for k in range(j - 1)}
    table[qs] = (b, c)
    for x in (b, c):
        for k in range(j, k0 + 1):
            pre = qs + (x,) + rs[:k - j]
            table[pre] = (rs[k - j],) if k < k0 else (b, c)
    end = b * c
    for q in qs + rs:
        end *= q
    return Q.by_prefix(table), k0 + 1, end


def obeys(menu, age, S):
    """Every menu met after k moves is prime to the moves at S[k]."""
    for r, n, ms in Q.walk(menu, age):
        for k, mu in enumerate(ms):
            for pos in S.get(k, ()):
                if any(gcd(m, r[pos - 1]) != 1 for m in mu):
                    return False
    return True


def controls(rd):
    print("CONTROLS")
    w2 = Q.by_prefix({(): (7,), (7,): (2, 3), (7, 2): (2, 3),
                      (7, 3): (2, 3)})
    h = Q.by_prefix({(): (2, 3), (2,): (5,), (3,): (5,), (2, 5): (2, 3),
                     (3, 5): (2, 3)})
    for name, menu, n, av, nav in (("W_2", w2, 42, (1, 3), 2),
                                   ("seed {2,3}", h, 30, (2, 3), 1)):
        items = Q.fibers(menu, 3)[n]
        e = Q.first_move_robust([(r[2:], ms) for r, ms in items])
        C1_EXACT.append((e == rd.flat(items, 3), e))
        check(f"C1 {name} at ({n}, 3): flat for the third move, avoids "
              f"{av}, not {nav}",
              rd.flat(items, 3) is True
              and all(avoids(menu, 3, k) for k in av)
              and not avoids(menu, 3, nav), f"{[r for r, _ in items]}")
    m48 = Q.by_state({1: (4, 6), 4: (3, 6), 6: (2, 4), 12: (2, 4),
                      24: (2, 4)})
    items = Q.fibers(m48, 3)[48]
    e = Q.first_move_robust([(r[2:], ms) for r, ms in items])
    C1_EXACT.append((e == rd.flat(items, 3), e))
    check("C4 the built age-3 control: a free state world on 2, 3, 4, 6 "
          "holds (48, 3) live and flat for the third move, read and exact",
          live(items, 3) and rd.flat(items, 3) is True and e
          and not avoids(m48, 3, 1) and not avoids(m48, 3, 2),
          f"{sorted(r for r, _ in items)}")
    subsets = [lambda k: [tuple(c) for s in range(k + 1)
                          for c in itertools.combinations(range(1, k + 1), s)]]
    fams = list(itertools.product(subsets[0](1), subsets[0](2),
                                  subsets[0](3)))
    built = ok = quarantined = 0
    for fam in fams:
        S = {1: fam[0], 2: fam[1], 3: fam[2]}
        for j in (1, 2, 3):
            ks = [k0 for k0 in range(j, 4) if j not in S[k0]]
            if not ks:
                quarantined += 1
            for k0 in ks:
                menu, age, end = window_world(j, k0)
                items = Q.fibers(menu, age).get(end, [])
                built += 1
                ok += (len(items) == 2 and obeys(menu, age, S)
                       and diverge_split(items) == j
                       and Q.dkey(Q.product(items[0][1]))
                       == Q.dkey(Q.product(items[1][1])))
    check(f"C3 (E)'s construction over {len(fams)} window families: "
          "every built world obeys its windows and ties a pair split at j",
          len(fams) == 64 and built > 0 and ok == built,
          f"{ok} of {built} built; {quarantined} (family, j) with j in "
          "every later window, none built")


def diverge_split(items):
    (r1, _), (r2, _) = items
    return next(k + 1 for k, (x, y) in enumerate(zip(r1, r2)) if x != y)


def main():
    t0 = time.time()
    scale = float(os.environ.get("ITH_SCALE", "1"))
    rng = random.Random(7)
    rd = Reader(random.Random(11), P1, 4)
    rd2 = Reader(random.Random(13), P2, 16)
    controls(rd)
    arms = [
        ("K2", U13, (2,), AGES, lambda a: (2,), 1000, True, (1, 2)),
        ("K3a", U13, (2, 3), AGES, lambda a: (2, 3), 1000, True, (1, 2)),
        ("K3b", U13, (1, 3), AGES, lambda a: (3,), 1000, True, (1, 2)),
        ("L2", U13, (1, 2), AGES, lambda a: (1, 2), 1000, False, (1, 2)),
        ("L3", U13, (1, 2, 3), AGES, lambda a: (1, 2, 3), 1000, False,
         (1, 2)),
        ("K2s", U5, (2,), (3, 4), lambda a: (2,), 3000, True, (1, 2)),
        ("K3s", U5, (1, 3), (3, 4), lambda a: (3,), 3000, True, (1, 2)),
        ("L2s", U5, (1, 2), (3, 4), lambda a: (1, 2), 3000, False, (1, 2)),
        ("L3s", U5, (1, 2, 3), (3, 4), lambda a: (1, 2, 3), 3000, False,
         (1, 2)),
        ("KF", UT, (), (3, 4), lambda a: range(2, a + 1), 3000, True,
         (1, 2), "state"),
        ("LC", Q.UL, None, (3, 4), lambda a: range(1, a + 1), 2000,
         False, (1, 3)),
    ]
    out = {}
    for name, uni, T, ages, reads, count, exact, sizes, *kd in arms:
        allowed = Q.coprime if T is None else avoid_set(T)
        keyed = kd[0] if kd else "prefix"
        worlds = (Q.random_world(rng, uni, allowed, keyed, sizes)
                  for _ in range(max(1, int(count * scale))))
        t = read_arm(name, worlds, ages, reads, rd, rd2, defaultdict(int),
                     exact)
        out[name] = dict(t)
        print(f"    {name} ({time.time() - t0:.0f} s): {out[name]}")
    states = [2 ** a * 3 ** b for a in range(4) for b in range(4 - a)]
    exf = (Q.by_state(dict(zip(states, ch))) for ch in itertools.product(
        ((2,), (3,), (2, 3)), repeat=len(states)))
    if scale < 1:
        exf = itertools.islice(exf, int(3 ** 10 * scale))
    t = read_arm("EXF", exf, (3, 4), lambda a: range(2, a + 1), rd, rd2,
                 defaultdict(int), exact=True)
    out["EXF"] = dict(t)
    print(f"    EXF ({time.time() - t0:.0f} s): {out['EXF']}")
    ex = Q.exhaustive_worlds()
    if scale < 1:
        ex = itertools.islice(ex, int(87885 * scale))
    t = read_arm("EX", ex, (2, 3), lambda a: range(1, a + 1), rd, rd2,
                 defaultdict(int))
    out["EX"] = dict(t)
    print(f"    EX ({time.time() - t0:.0f} s): {out['EX']}")
    ctl = [out[k] for k in ("K2", "K3a", "K3b", "K2s", "K3s", "KF",
                            "EXF")]
    c2 = sum(d.get("C2 read", 0) for d in ctl) + len(C1_EXACT)
    agree = sum(d.get("C2 agree", 0) for d in ctl) + sum(
        a for a, _ in C1_EXACT)
    eflat = sum(d.get("C2 exact flat", 0) for d in ctl) + sum(
        e for _, e in C1_EXACT)
    check("C2 the reader equals the exact reader on the control arms' "
          "live reads of at most 4 routes and C1's and C4's fibers, both "
          "verdicts "
          "met", c2 > 0 and agree == c2 and 0 < eflat < c2,
          f"{agree} of {c2} agree, {eflat} exact flat")
    kf = sum(v for d in ctl for k, v in d.items()
             if k.startswith("flat") and "age" not in k)
    check("P2 (widened past the freeze) some control arm sees flat live "
          "reads; the frozen K2, K3a, K3b read 0, and EXF's are at age 4",
          kf > 0, f"{kf}")
    lead = [out[k] for k in LEAD]
    kill = sum(v for d in lead for k, v in d.items()
               if k.startswith("flat i=") and k != "flat i=1")
    nlive = sum(v for d in lead for k, v in d.items()
                if k.startswith("live i=") and "age" not in k
                and k != "live i=1")
    check("P3 KILL (unverdicted, P2 failed as frozen): no live read flat "
          "for the i-th move with every position to i avoided", kill == 0, f"{kill} of {nlive}")
    bars = {f"L i={i} age {a}": out["L2"].get(f"live i={i} age={a}", 0)
            + out["L3"].get(f"live i={i} age={a}", 0)
            for i in (2, 3) for a in AGES}
    bars.update({f"EX i={i}": out["EX"].get(f"live i={i}", 0)
                 for i in (2, 3)})
    check("P3 live bars: i = 2 and 3 in L2+L3 at age 4 or 5, and in EX",
          all(bars[f"L i={i} age 4"] + bars[f"L i={i} age 5"] > 0
              for i in (2, 3))
          and bars["EX i=2"] > 0 and bars["EX i=3"] > 0, f"{bars}")
    print(f"    distinct live reads at i >= 2 (i, routes and menus): "
          f"{ {k: len(v) for k, v in DISTINCT.items()} }")
    one = sum(d.get("flat i=1", 0) for d in lead)
    check("P4 no i = 1 read flat", one == 0,
          f"{one} of {sum(d.get('live i=1', 0) for d in lead)}")
    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()