flush.py

"""
flush.py -- a redundant output alphabet on the trailing Ostrowski
numeration: which maps a bottom-up reader then computes, and what
reading the integers costs over reading their completion.

QUESTION. Fix an irrational alpha = [0; a_1, a_2, ...] with
denominators q_k, numerators p_k and remainders theta_k = q_k alpha -
p_k (theta_(-1) = -1), which alternate in sign and shrink. The INPUT is
the greedy Ostrowski string of n (ostrowski.py). The OUTPUT alphabet is
widened: digit e_k may run to a_(k+1) + s (position 0 to a_1 - 1 + s_0,
with s_0 <= s + 1) and the below-a-cap rule is dropped, so an integer
has several output strings. A reader at lookahead c writes e_t having
seen d_0 .. d_(t+c). Under the legal output, n -> m n walls on the
circle and floor(n/m) is no continuous circle map at all
(ostrowski.py). Which of
the two does redundancy cure? And a reader that must write a FINITE
string equal to m n (the INTEGER reader) against one that need only
write an infinite string coding the circle point m x (the COMPLETION
reader): what separates them?

THE ARGUMENT (written before this script).
  (1) THE RANGES. The real star of a string is sum e_k theta_k, a REAL:
      two strings of one integer can differ in it by an integer. The
      tails from level t fill the interval T_t between -sum over the
      negative theta_k of (cap_k)|theta_k| and the same over the
      positive ones, and by a_(k+1) theta_k = theta_(k+1) - theta_(k-1)
      its length is |theta_(t-1)| + |theta_t| + s S_t, S_t = sum_(k>=t)
      |theta_k| (level 0: 1 + E, E = s_0 alpha + s S_1). The TAIL LEMMA
      S_t <= |theta_(t-1)| + |theta_t| follows from |theta_(k-1)| >=
      |theta_k| + |theta_(k+1)|. The members e theta_t + T_(t+1),
      e = 0 .. cap_t, cover T_t, consecutive ones overlapping by
      ov_t = |theta_(t+1)| + s S_(t+1).
  (2) THE TEAR AT E = 0. At s = s_0 = 0, T_0 = [-alpha, 1 - alpha]
      exactly, so every string of N has as star the representative of
      N alpha mod 1 in (-alpha, 1 - alpha). The least string (0, a_2,
      0, a_4, ...) has star -alpha, the greatest (a_1 - 1, 0, a_3, 0,
      ...) has 1 - alpha, and star minus -alpha is a sum of
      non-negative terms (e_k - e^min_k) theta_k, so a string within
      eta of -alpha agrees with the least string wherever |theta_k|
      > eta, likewise at the top. They part at position t_0 - 1. The
      integers of any input tile about the non-cut (1 - alpha)/m have
      images on both sides of the cut -alpha, so x m commits no output
      tile past depth t_0 - 1 there, at any lookahead: dropping the
      rule alone buys nothing.
  (3) THE COMPLETION READER AT E > 0. Keep the interval J_t of
      targets the unseen input still allows, M + m (seen star + I) -
      sum_(k<t) e_k theta_k, I the closed interval between
      -theta_(t+c+1) and -theta_(t+c), of width w_t = m (|theta_(t+c)|
      + |theta_(t+c+1)|). An interval no longer than the overlap lies
      in one member, so the reader commits e_t with J_t inside
      e_t theta_t + T_(t+1) whenever w_t <= ov_t, and the next target
      interval lies inside the committed member because the tail
      intervals nest. The lift M exists once w_0 <= E. So x m reads on
      the completion at the least c_ov meeting both, finite at every
      irrational alpha once E > 0 since |theta_(k+2)| < |theta_k| / 2.
      This is the signed-digit cure of the reading lemma: a cover
      whose children overlap by a positive amount, on the circle.
  (4) THE FLOORS DO NOT FOLLOW. A depth-t output cylinder holds stars
      in an interval of length |T_t|. The integers of any input tile
      about a non-cut x have floor(n/m) alpha accumulating at m points
      1/m apart (ostrowski.py, the residue section), so once |T_t| <
      1/m no depth-t output tile holds them: floor division commits
      nothing from that depth on, anywhere, at any s.
  (5) THE GAME. Write the residual H_t = m sum_(k<=t) d_k q_k + omega
      - sum_(k<t) e_k q_k (the pre-read d_(t+1) .. d_(t+c) kept apart)
      as g q_t + h q_(t-1), and put sigma = g theta_t + h
      theta_(t-1): (g, h) is a lattice point, integers, and a step
      sends it to (h + m d_(t+1), g - e - a_(t+1) h), labelled by the
      local quotient. The lift M sits in the seed (m d_0 + omega, -M),
      and every branch carries the same H, so the state holds the SET of
      lifts still alive: the branches' sigma differ only by integers,
      the fibre of R over R/Z. A true branch (the lift a
      correct reader realizes) has sigma_t = (output tail star) - m
      (input tail star from t + 1), so |sigma_t| < (1 + s)|theta_(t-1)|
      + m |theta_t|, and |H_t| <= mu q_(t+1), mu = max(m, 1 + s).
      Inverting the unimodular frame with q_t |theta_(t-1)|,
      q_(t+1) |theta_t| and q_(t-1) |theta_(t-1)| at most 1 (equal only
      at q_0 |theta_(-1)|, where the sigma bound is strict) and
      q_(t+1) |theta_(t-1)| < a_(t+1) + 1:
          |g| < mu (A + 1) + 1 + s + m,   |h| < 1 + s + m + mu,
      A the largest quotient. Prune to that BOX and the pruning never
      removes a true branch, so a win of the pruned game is a real
      reader and a loss is a real loss, with no lookahead in the box.
      The INTEGER game adds the FLUSH: under zero input the reader must
      force the branch (0, 0) with nothing pending (H = 0). The SAFETY
      game drops it. c_int and c_saf are their least lookaheads.
  (6) THE COMPLETION READER IS THE SAFETY GAME: c_comp = c_saf at
      omega = 0. A safe play keeps the branch set non-empty; each
      branch has one parent, the box holds finitely many per state, so
      by Koenig one lineage runs forever, and its sigma_t -> 0 at the
      rate of the box times |theta_(t-1)|: the output codes m x + M, a
      completion reader. A completion reader's own lift gives a true
      branch, inside the box by (5), so it plays safe. So tracking the
      lifts costs nothing, the width of the box is irrelevant above
      (5)'s floor, and
      c_int - c_comp = c_int - c_saf is the price of the flush alone.
  (7) THE FLUSH FLOOR. If s >= (m - 1) a_(k+1) at every k >= 1, the
      digitwise reader e_0 = m d_0 mod a_1, e_1 = m d_1 + floor(m d_0 /
      a_1), e_k = m d_k fits the caps (d_0 >= 1 forces d_1 <= a_2 - 1),
      whatever s_0: c_int = 0. If (m - 1) a_(k+1) > s and m a_(k+1) <
      q_(k-1) for infinitely many k, no integer reader has c <= 1: a
      reader flushed on n writes the same prefix on n' = n + a_(k+1)
      q_k (k deep, a zero below it) through position k - c - 1, so it
      owes exactly m a_(k+1) q_k, from level k - c >= k - 1. Writing
      q_(k+j) = U_j q_k + V_j q_(k-1) with V_j >= 1, a string of value
      m a_(k+1) q_k from level k - 1 has q_k | Y, Y = e_(k-1) + sum
      e_(k+j) V_j, and Y >= q_k would force m a_(k+1) >= q_(k-1); so
      Y = 0 and the only string is e_k = m a_(k+1), over its cap
      a_(k+1) + s. So c_int
      is 0 or at least 2, never 1, at every periodic alpha.
  (8) THE UNIVERSAL READER. The step is labelled by the local quotient
      only, so over the alphabet {1, .., A} the game with the OPPONENT
      choosing each quotient is ONE finite game; a win is a reader
      that sees the quotients through a_(t+c+1) and nothing else of
      alpha, correct at every alpha with quotients <= A.
  (9) THE OWED INTEGER (added later). N_t = m sum_(k<=t+c) d_k q_k +
      omega - sum_(k<t) e_k q_k is what is owed if the input stops at
      t + c, the same at every branch: G q_t + H q_(t-1), (G, H) a
      branch's TENTATIVE pair, its pending digits absorbed. (a) At every
      irrational alpha, a play that stays in the box and never owes a
      negative integer ends under zero input: N_(t+1) = N_t - e_t q_t
      there, so e_t = 0 from some T on; then a step sends (g, h) to
      (h, g - a_(t+1) h) and keeps sigma, which the box squeezes below
      B_g |theta_t| + B_h |theta_(t-1)| -> 0, so the branches left are
      (0, 0), alpha irrational. Conversely N_t is the value of what the
      reader writes from t on, >= 0. (b) At a periodic alpha the sign
      is a function of the state: with theta'_k = q_k alpha' - p_k <
      0 (alpha' the conjugate) and zeta'_t = theta'_t/theta'_(t-1) =
      a_t + 1/zeta'_(t-1) > 1, by t mod p, a branch's TENTATIVE
      CONJUGATE u~ = G zeta'_t + H obeys N (alpha - alpha') = sigma~ -
      u~ theta'_(t-1), so u~ >= 0 is N >= 1, or N = 0 with sigma~ <=
      0, once |sigma~| < 1 on the box. A step sends u~ to u~/zeta'_t -
      e plus a non-negative input term, so under zero input u~ < 0
      persists and a winner's states all hold a branch with u~ >= 0;
      conversely, inside the safety game's set on such states, by Koenig
      a chain of branches with u~ >= 0 runs on under zero input, u~
      shrinking by zeta'_min over finitely many values to 0, which is
      (0, 0) with nothing pending. So c_int is the least lookahead of
      ONE safety game, and inside its set every safe move flushes. Over
      a quotient alphabet zeta' is not known to the state, (a) holds
      per play, and the engine keeps the attractor of (5).
  (10) THE CONE (added later). Write N_t =
      K q_(t+1) + L q_t and zeta_k = |theta_k/theta_(k-1)|. At (s, s_0) =
      (0, 1) every cap is a_(t+1), T_t over theta_t is [-1, a_(t+1) +
      zeta_(t+1)], and the member e holds J_t iff e is in [j+ - zeta_(t+1),
      j- + 1]; J_t over theta_t is L - K zeta_(t+1) + I, the ends of I of
      opposite signs. A step sends (K, L) to (L - e, K - a_(t+2)(L - e)),
      so the cone K, L >= 0 holds at t + 1 iff L - floor(K/a_(t+2)) <= e
      <= L, and at K >= 0 every integer of the window lies there: its top
      is at most L, its bottom at least L - floor(K/a_(t+2)) since (K + 1)
      zeta_(t+1) < floor(K/a_(t+2)) + 1. x_0 = N_0 - K_0/alpha lies
      strictly inside J_0, so inside (-1, 1/alpha): K_0 >= 0, and then
      L_0 >= 0 from x_0 = L_0 - K_0 zeta_1 > -1. So every overlap reader at the (0, 1)
      windows never owes a negative integer and, by (9a) with no box (the
      star held in T_t), ends: c_int <= c_ov(0, 1) wherever s_0 >= 1, at
      every irrational alpha, and c_ov(0, 1) <= 2 ceil(log2 m) + 2 by
      |theta_(k+2)| < |theta_k|/2.
  (11) THE SEAM (added later). At s_0 = 0, s >= 1 the level-0 window
      at the (0, 0) caps, [-1, a_1 - 1 + zeta_1] over alpha, has length
      1/alpha, the lift's shift, so J_0 lies in one lift of it or holds
      its seam -1. Inside: the s = 0 reader from level 0 (the cone lemma
      never used position 0's cap). Holding -1, |x_0 + 1| <= w_0/alpha:
      write e_0 = 0 and e_1 = a_2 + 1 (the one use of s = 1), then the s = 0
      reader from level 2. With sigma = x_0 + 1, x_1 = a_2 + zeta_2 -
      sigma/zeta_1 and x_2 = a_3 + zeta_3 - 1 + sigma/(zeta_1 zeta_2), so
      J_2 lies in [-1, a_3 + zeta_3] once w_0/alpha < zeta_1 zeta_2,
      that is w_0 < |theta_2|. The cone: M = N_0 + 1 has star sigma, and an
      integer M > 0 with |star| < 1 over theta_j has K >= 1 at level j
      (K = 0 gives |L| < 1; K <= -1 gives L >= a_(j+1), star > 1); the
      two moves leave K_1(M) - 1 and K_2(M) - 1, both >= 0, and L_2 >= 0
      as x_2 > -1. So the seam reader at c_sr, the least c with w_0 <
      |theta_2| and w_t <= |theta_(t+1)| at t >= 1, is an integer reader
      at (1, 0), hence at every (s, 0) with s >= 1, and c_sr <= 2
      ceil(log2 m) + 3. Equality w_0 = |theta_2| never occurs: m >= 2
      would divide the coprime q_2 and p_2.
  (12) THE CYLINDER BOUND (added later). Fix t >= 0 with |T_(t+1)| < 1
      and the inputs with d_0 .. d_(t+c) all 0: their stars are dense in
      I_j, j = t + c + 1, of length |theta_(t+c)| + |theta_(t+c+1)|, and
      over them a reader at lookahead c has written one e_0 .. e_t. A
      completion reader, or an integer reader of m n + omega (n = 0
      aside), puts each output star m x + omega alpha + M, M an integer,
      in one translate of T_(t+1); for each M the x allowed form a
      closed interval of length |T_(t+1)|/m < 1/m, the M's disjoint
      translates by 1/m, and a dense subset of I_j in finitely many of
      them puts I_j in one. So m |I_j| <= |T_(t+1)|: c_lo, the least c
      with w_t <= |T_(t+1)| at every t with |T_(t+1)| < 1, bounds c_comp
      and c_int below at every irrational alpha, s_0 never entering.
      Upward: |T_L| falls with L, |T_(t+3)| <= ov_t as |theta_(t+1)| >=
      |theta_(t+2)| + |theta_(t+3)|, |T_3| < E wherever E > 0, and
      w_t(c + K) = w_(t+K)(c); so c_ov <= c_lo + max(2, t_1), t_1 the
      least t with |T_(t+1)| < 1, and |T_(t+1)| <= |theta_(t-1)| +
      2s|theta_t| < (1 + 2s) 2^-floor(t/2) at t >= 1 gives t_1 <= max(1,
      2 ceil(log2(2s + 1))). At a purely periodic alpha w_t/|T_(t+1)|
      has the period, so the bar holds at every t and the gap is at most
      2, as wherever |T_3| < 1. Golden: c_lo is the least c with m phi^-c
      <= 1 + s, c_ov the least with m phi^-c <= s + min(phi^-2,
      s_0/phi).
  (13) THE PINNED ZERO CYLINDER (added later). At s = 0, T_L = I_L for
      L >= 1, its members e theta_L + I_(L+1), e = 0 .. a_(L+1). Fix t
      with |I_(t+1)| < 1 (t = 0 at a_1 = 1 aside, where |T_1| = 1), j =
      t + c + 1. By (12) the lift M is one integer over I_j, and a
      reader of x m (completion, or integers at omega = 0) writes there
      one e_0 .. e_t, sigma_t = N alpha - P, N = sum e_k q_k in 0 ..
      q_(t+1) + q_t - 1 at s = 0, s_0 = 1; so delta = M + P - N alpha
      has delta + m I_j inside I_(t+1), and delta is interior to it as
      0 is interior to I_j. For 0 < N < q_(t+1), |N alpha - K| >=
      |theta_t|; for N = q_(t+1) + N', N' < q_t, K - N alpha is -theta_
      (t+1) plus a point at distance 0 or >= |theta_(t-1)| = a_(t+1)
      |theta_t| + |theta_(t+1)| or 1: never interior. So N = 0, M = 0:
      the zero cylinder is written as zeros through level t at lift 0,
      and m I_j lies inside I_(t+1) (ONE LEVEL: R(t, c), R(t + 1, c) at
      c even, R(t, c + 1), R(t + 1, c - 1) at c odd, R(k, g) being m
      |theta_(k+g)| <= |theta_k|). TWO LEVELS: over C_0 = I_(j+1) and
      C_d = hull{(d - 1) theta_j - theta_(j+1), d theta_j -
      theta_(j+1)}, d = 1 .. a_(j+1), the reader has written e_(t+1), so
      m C_d lies in one member of T_(t+1). Z(c), both levels at every t,
      bars every reader at c; c_lo2 = 1 + the largest c with Z(c)
      failing. c_lo <= c_lo2, as m|I_j| <= |I_(t+1)| is c_lo's bar, and
      c_lo2 <= min(c_comp, c_int); by (6), c_lo2 <= c_saf wherever c_saf
      is defined. Z(c) holds once 2^floor((c - 1)/2) >= m, as R(k, g)
      does once 2^floor(g/2) >= m. At a constant quotient a, R reads m
      r^g <= 1, r the ratio, so the one-level bar is c_lo rounded up to
      even. The
      second level adds to the one-level bars at t and t + 1 only the
      SEAM BAR at c even: each overlap zone of T_(t+1) past the first
      (member 1 reaches 0) that the m C_d, d >= 1, straddle holds a seam
      between two of them. At a = 1 there is one zone, so golden's c_lo2
      is c_lo rounded up to even. With c_int <= c_ov(0, 1) <= c_lo + 2,
      c_int is c_lo2 + 0..2, and + 0..1 wherever c_lo2 > c_lo.
  (14) THE PINNED LIMIT (added later). Read (13)'s subtree L levels: at
      i = 0 .. L - 1 the target m X_i lies in the committed window W_i,
      X_0 = I_j, W_0 = I_(t+1); at i >= 1 the opponent picks d_(j+i-1),
      then the reader e_(t+i), X_i = sum_(k=j)^(j+i-1) d_k theta_k + R,
      W_i = sum_(k=t+1)^(t+i) e_k theta_k + I_(t+i+1), R = I_(j+i) after
      a digit 0 and R' = hull(-theta_(j+i), -theta_(j+i-1) -
      theta_(j+i)) after a digit >= 1. c_L, 1 + the largest c at which
      some pin level fails, is non-decreasing in L, c_1 the one-level bar
      and c_2 = c_lo2. Its limit is one membership: c_inf, 1 + the
      largest c at which some PINNED STATE P_t (the branch (0, 0), the
      quotients a_(t+1) .. a_(t+c+1), the pending digits 0) is outside
      the safety game's set W. A strategy surviving every L exists by
      Koenig (finite choices on both sides) and codes m x exactly on the
      subtree, so its lift-0 branch is a true branch and the box (5)
      keeps it: P_t wins. A safe play from P_t keeps a lineage, which by
      (6) codes m x + M, M = 0; by (13) no move at that lift but e = 0 is
      in a safe play, so its output star lies in every W_i. Every c from
      c_comp on passes every L, so lim c_L = c_inf, reached at a finite
      L. c_lo2 <= c_inf <= c_comp = c_saf: by (12) and (13) every
      completion reader writes the zero cylinder at lift 0, so its lift-0
      branch survives from P_t. c_zero, the same read off the
      unmodified game's initial state with d_0 .. d_c all 0, equals
      c_inf. At a purely periodic alpha P_p plays as that state with the
      lift 0 alone (the quotients and the source state repeat, and
      position 0's cap a_1 - 1 + s_0 is a_1 at s_0 = 1; only the
      position-0 flag differs), so P_p winning makes the zero state, its
      branches a superset, win; and a winning play from the zero state,
      the opponent playing zeros, writes zeros through t by (13),
      reaching a state that holds P_t's (0, 0), whose survivor has lift
      0 by (12) and (13) again, so that strategy followed from P_t never
      empties it (strategy transfer; monotonicity runs the other way).

PREDICTIONS (frozen before the engine ran).
  C1 CONTROLS, run first. (a) At every alpha the range T_0 has length
     1 + E and each overlap is ov_t as (1) says, the tail lemma holds
     at every level read. (b) The legal output (rule kept, s = s_0 =
     0) through the game: the identity at 0, n + 1 at 1, x 2 and x 3
     at no c <= LOOKCAP at all six periodic alphas (ostrowski.py's
     theorems); with the rule dropped, n + 1 at 0. (c) Every winning
     integer-game strategy of the grid and the band writes m n + omega
     under the caps and flushes for every n < N_CHECK, 0 bad (the
     legal output's are
     not certified). (d) The grid's c_int agrees at every
     cell with the table of an earlier, independent engine (lattice
     points of the quadratic field of alpha, a box derived otherwise),
     EARLIER below.
  P1 THE TEAR. Every string of every N < N_TEAR at s = s_0 = 0 has
     star the representative of N alpha mod 1; every string within
     eta of an end agrees with that end's extreme string where
     |theta_k| > eta; the extremes part at t_0 - 1. The game's
     (0, 0) column: x m reads at no c <= LOOKCAP. Kill: one string off.
  P2 THE COMPLETION READER. At every alpha (the six periodic ones,
     e - 2, and the band alphas) and every grid cell with E > 0, the
     overlap reader at c_ov never fails to find a member over
     N_PLAY random inputs to depth DEPTH, and |its star - (m x + M)|
     is at most |T_DEPTH|. c_ov printed at the grid's cells. Kill: a
     failure.
  P3 THE FLOORS. For m = 2, 3 and s = s_0 = 0..3, at the first depth
     t* with |T_t*| < 1/m, every input tile at depth t* + c (c = 0..3)
     holding at least 12 integers below N_FLOOR has a circular hull of
     floor(n/m) alpha longer than |T_t*|. Kill: a tile whose hull fits.
  P4 THE FLUSH FLOOR. (a) The digitwise reader is correct on n <
     N_CHECK at every cell with s >= (m - 1) a_max, s_0 = 0 included.
     (b) At one k of every phase, the first k >= 2 with
     m a_(k+1) < q_(k-1), value m a_(k+1) q_k has exactly one string
     from level k - 1, of any digit sizes. (c) Over the grid, c_int is 0
     exactly where s >= (m - 1) a_max and at least 2 elsewhere. Kill:
     a printed 1, or a 0 below the line.
  P5 THE COMPLETION READER IS THE SAFETY GAME. (a) The overlap
     reader's true branch, tracked in frame coordinates, never leaves
     the box at any cell of P2: the largest |g|/B_g and |h|/B_h
     printed beside it. (b)
     c_saf <= c_ov at every cell. (c) --full: c_saf at twice the box
     equals c_saf at the box at a sample of cells. (d) The band cells
     [4] x 2 at s = s_0 = 3, [5] x 2 at 3, [4] x 3 at 5 and bronze
     x 3 at 5: c_ov = 1, so c_comp <= 1, and c_int >= 2 by P4: a
     strict flush price at each (the check asks c_int = 2). Kill:
     c_saf above c_ov, a branch out of the box, or c_int <= 1 at a
     band cell.
  P6 THE UNIVERSAL READER. {1, 2}: x 2 at (1, 1) wins at 2 and not at
     1 (the default run). --full: {1, 2, 3} x 2 at (1, 1) at 2; {1, 2}
     x 3 at (1, 1) at exactly 3 and x 3 at (2, 2) at 2; every win
     certified at 12 random alphas over the alphabet and its constant
     ones; the flushing lineages of a win solved at twice the box stay
     inside the box ({1, 2}, x 2); every primitive {1, 2}-necklace of period <= 8
     reads x 3 at (1, 1) at c_int = 2, at every rotation. Not predicted: whether a
     periodic member reaches the class's 3. THE PIN (added later, a
     corollary): a win at 2 bounds c_int by 2 at every alpha of its
     class, and the flush floor bounds it below by 2 wherever
     (m - 1) a > s for a quotient a that recurs, since m a_(k+1) <
     q_(k-1) then holds at every deep k; so the grid's c_int is 2 at
     each grid alpha of a class won at 2 with such a quotient.
  P7 THE OWED INTEGER (frozen with (9), in an earlier script). At every
     grid cell and every c from 0 to c_int (to LOOKCAP where none), the
     safety game's set on the states with a branch of u~ >= 0 equals
     the integer game's; every flushed state has a branch with u~ = 0,
     and over the branches of tentative pair other than (0, 0) the
     least |u~| stays above 1e-7. CONTROL: the real side's ratio
     |theta_t/theta_(t-1)| in place of zeta' must move the set at some
     cell. Kill: a cell off, or a margin below 1e-7.
  P8 THE CONE (frozen with (10)). At the grid's alphas, e - 2 and (full)
     one random {1, 2, 3} alpha, the reader of (10), exact, least lift,
     at the (0, 1) windows and caps: (a) at c from c_ov(0, 1) (full: to
     + 2), least and greatest member, omega = 0 and m, every n < N_CHECK
     and the random greedy strings read to m n + omega and end, with no
     step of K < 0 or L < 0; (b) c_ov(0, 1) <= 2 ceil(log2 m) + 2 at
     every alpha and m, c_int <= c_ov(0, 1) at every grid cell. CONTROL,
     the known answer, read first: the reader at c_int - 1, where c_int
     >= 1, fails at every cell. CONTROL, one variable, the windows: the
     same reader, least member, on the (1, 1) windows and caps at that
     cell's c_ov(1, 1) must fail at some cell where c_ov(1, 1) >=
     c_int(1, 1) (predicted: at K = 0 the member L + 1 is allowed there).
     Kill: a failure or a negative coordinate in (a), or (b) off.
     (c) THE SEAM (frozen with (11), in an earlier script). The seam
     reader at the (0, 0) windows and the (1, 0) caps, at the same
     alphas and inputs, c_sr (full: and c_sr + 1), both members, omega
     = 0 and m: no failure, no step of K < 0 or L < 0, the seam taken at
     every cell; c_sr <= 2 ceil(log2 m) + 3, c_int(1, 0) <= c_sr at every
     grid cell. CONTROL, the known answer, read first: the seam reader
     at c_int(1, 0) - 1, where c_int(1, 0) >= 1, fails at every cell.
     PLANT: the seam's bar loosened to w_0 <= |theta_1| (c_pl, the s = 0
     bars alone) fails at some cell where c_pl < c_sr. Kill: a failure
     or a negative coordinate, a cell with the seam never taken, or a
     bound off.
  P9 THE CYLINDER BOUND (frozen with (12), in an earlier script; the
     gap bound, its t_1 clause and the wall settled after that script's
     first run: see the run record). c_lo's bars read from above, so that
     an exact tie passes, and c_ov's both ways, which must give one c_ov
     at every cell but the golden controls. CONTROLS, read first:
     c_lo and c_ov at golden x 2 .. x 9 equal (12)'s closed forms; the
     bar ov_t (too strict) puts c_lo above c_saf at some cell; the bar
     |T_t| (too lax) gives a gap of 3 at golden s = 0. Kill: c_lo above
     c_saf or c_int at a finite grid cell; c_ov - c_lo outside 0 .. 2 at
     a grid cell, or at e - 2 and P8's random alpha, where |T_3| < 1 is
     printed; a gap above max(2, t_1), or t_1 above its bound, at any
     cell read. THE WALL: on the family [1 x (N + 1), 10^8, ...], N = 2
     .. 7, s the least with |T_N| >= 1, m = 2 .. 4096 in powers of 2,
     the largest gap is max(2, t_1).
     (b) THE ZERO CYLINDER (frozen with (13), in an earlier script).
     Every hull tested from its definition, exactly, over t < 60 at the
     six periodic alpha (the ratios and quotients repeat), c < 30.
     CONTROLS, read first: the sub-cylinders tile I_j and the members'
     hull is I_L; golden x 2 .. x 9 is c_lo rounded up to even; silver
     x 4 has one-level bar 2 and c_lo2 3, the seam's bite. The pinning:
     every N < q_(t+1) + q_t enumerated at each level with q_(t+1) + q_t
     <= NPIN, N = 0 alone strictly inside. Printed beside it: the least
     c at which Z(c) holds against c_lo2, x 2 .. x 9 at the six alpha.
     Kill: c_lo2 above c_saf, c_saf above c_int or c_lo above c_lo2 at a
     grid cell at (0, 1); c_int - c_lo2 above 1 where c_lo2 > c_lo; at e
     - 2 and P8's random alpha, depth 110, c_lo2 outside c_lo .. c_ov(0,
     1).
     (c) THE PINNED LIMIT (frozen with (14), in an earlier script, at x
     2 .. x 5; x 6 .. x 9 after its first run; the grid control and the
     plant's limit arm added here). At the six alpha at (0, 1), x 2, x 3
     (full: x 2 .. x 9), t = 1 .. 2p (the geometry repeats with
     the period): c_L for L <= 10 (full: 14) read exactly at c up to
     c_saf + 1; c_inf from the pinned game and c_zero from the
     unmodified one at c up to c_saf. CONTROLS, read first: c_L at L =
     1 and 2 is the one-level bar and c_lo2; c_saf equals the grid's;
     c_inf = c_saf where c_lo2 = c_saf; at c_saf the pinned states' only
     winning move is 0. PLANT: R' read as d theta + I_(K+1) moves the L
     = 2 control at some cell and, at some cell of maps(), the limit.
     Predicted: c_L stops by L = 8; c_inf = c_saf at every cell (the
     hypothesis, credence 40%). Kill: K1, c_L or c_inf above c_saf at
     any cell; K2, lim c_L or c_zero off c_inf at any cell.

THE DESIGN. Exact rationals for everything metric (ostrowski.py's
Numeration, alpha replaced by a convergent past 10^60). One game engine
for every quotient source: a periodic alpha is the source cycling its
period, a class is the source offering every letter at every step. The
state holds the sorted branches, the pending quotients a_(t+1) ..
a_(t+c+1), the source's state, the pending digits, whether the last
input digit is 0, whether this is position 0, and whether the last
output digit is 0 (read only with the rule kept, but carried always,
so every printed state count includes it). Safety is a greatest fixed
point; the flush alternates it with the attractor of the flushed
states under zero input. The reader picks, among moves keeping every
reply winning, one of least rank toward the flush under zero replies:
a rank that falls at every zero step, set once per state, not always
the least distance. Default: the grid at golden, silver and
sqrt(3) - 1 for x 2 and x 3, the band cell [4] x 2, the {1, 2}
universal cell; `--full` runs everything above.

FINDINGS (entered after the run, from its prints; `--full`).
  F1 CONTROLS (C1, all green; (a) and (b) run first, (c) and (d) inside
     the grid). The ranges and overlaps agree
     with (1) to half the truncation bound at worst over seven alphas
     and six slacks. The legal output reads the identity at 0, n + 1 at
     1, and x 2, x 3 at no c <= 3 at all six periodic alphas; with the
     rule dropped n + 1 reads at 0. The strategy extracted from every
     win of the grid and the band is correct on every n < 1000. The
     grid's c_int agrees with EARLIER at all 144 cells.
  F2 THE TEAR (P1 lands). 8,321 strings of N < 300 at seven alphas: 0
     stars off, 0 disagreements with the extremes; the (0, 0) column
     reads at no c <= 3 everywhere.
  F3 THE OVERLAP READER (P2 lands). 36,000 runs to depth 40 at nine
     alphas, x 2 .. x 5, five slacks: 0 failures, every output star
     within |T_40| of m x + M. c_ov runs from 0 to 6 over the grid
     (golden x 5 at (0, 1) is 6).
  F4 THE FLOORS (P3 lands). 9,063 (tile, m, s, c) tests, m = 2, 3,
     s = s_0 = 0 .. 3, c = 0 .. 3: none fits; the least hull exceeds
     |T_t*| by 0.196.
  F5 THE FLUSH FLOOR (P4 lands). The digitwise reader is correct at
     every alpha and m = 2 .. 5 at s = (m - 1) a_max, s_0 = 0; the value
     m a_(k+1) q_k has one string from level k - 1 of any digit sizes at
     every phase, e_k = m a_(k+1), over its cap a_(k+1) + s when
     (m - 1) a_(k+1) > s, so there it has no
     capped string: P4(b) as frozen read "exactly one capped string",
     which was wrong, and it now reads as the check counts, strings of
     any digit sizes; over the
     grid c_int
     is 0 exactly where s >= (m - 1) a_max and 2 or more elsewhere.
     c_int - c_saf over the 120 finite cells: 0 at 91, 1 at 28, 2 at one
     (V1 x 3 at (3, 3), c_saf 0).
  F6 THE SAFETY GAME (P5 lands). The overlap reader's true branch uses
     at most 0.92 of B_g and 0.42 of B_h; c_saf <= c_ov at every cell;
     c_saf is unchanged at twice the box at four cells; at the four band
     cells c_ov = c_saf = 1 and c_int = 2, strategies 0 bad.
  F7 THE UNIVERSAL READER (P6 lands). x 2 at (1, 1) reads at exactly 2
     over {1, 2} (28,268 states) and {1, 2, 3} (225,747); x 3 at (1, 1)
     at exactly 3 over {1, 2} (246,554) and x 3 at (2, 2) at 2
     (87,131). Every win certified at 14 or 15 members on n < 500, 0
     bad; the
     flushing lineages at twice the box reach (4, 2) against (10, 6).
     All 472 purely periodic {1, 2} alphas of primitive period <= 8
     (every rotation of the 71 words) read x 3 at (1, 1) at 2: no
     periodic member of the class to that period needs the class's 3.
     The pin holds at all 11 (class, cell) pairs it prints, 8 distinct
     grid cells (x 2 at (1, 1): silver,
     bronze, [1, 2], [1, 1, 1, 2], [2, 1, 3, 1]; x 3 at (2, 2): silver,
     [1, 2], [1, 1, 1, 2]), each class's members listed per class.
  F8 THE OWED INTEGER (P7 lands). "cells off: 0 of 144": the two sets
     agree at all 490 (cell, c) compared, 135 of them non-empty (the
     120 winning c, and 15 losing ones that keep states but no initial
     one); "flushed states without a u~ = 0 branch: 0", the margin
     3.837e-02; the first clause holds by construction (a flushed state's
     (0, 0) branch with nothing pending has u~ = 0 exactly), so the
     margin is the read. The control moves the set at 116 of 144. The
     margin's
     population was narrowed after the first run, which struck only the
     literal (0, 0) branch with nothing pending and printed 0: a branch
     whose pending digits cancel it has tentative pair (0, 0), u~ = 0
     exactly.
  F9 THE CONE (P8 lands). "failures at c >= c_ov(0, 1): 0; steps with
     K < 0 or L < 0: 0" over eight alphas (the grid's six, e - 2, one
     random {1, 2, 3}), x 2 .. x 5, c from c_ov(0, 1) to + 2, every n <
     1000 and 100 random strings of length 60; the known answer "passes
     at 0 of 24 cells". c_ov(0, 1) is at most 4, 5, 5, 6 for m = 2 .. 5
     against the bound 4, 6, 6, 8, met at x 2 by four of the eight
     alphas; c_int <= c_ov(0, 1) at the 24 grid cells, equal at 18. The
     control, at the theorem's lookahead, omega = 0 and the least member,
     on the (1, 1) windows and caps (an integer reader exists there, by
     the caps): "fails at 27, a negative coordinate at 27 (by the lift
     at 27, by a member at 14), of 32 cells; n = 0 fails at 27, alone at
     13, its lift K_0 = -1 at 27". (c) The seam at c_sr and c_sr + 1:
     "seam failures at c >= c_sr: 0; steps with K < 0 or L < 0: 0;
     cells where the seam is never taken: 0 of 32" (64 to 1,904 seam
     reads a cell, of 8,800); "c_sr above 2 ceil(log2 m) + 3: 0 of 32;
     c_int(1, 0) above c_sr: 0", c_sr at most 5, 6, 6, 7 for m = 2 .. 5,
     the bound met at golden x 2 alone, 1 to 5 above c_int(1, 0) at the
     24 grid cells; the known answer "passes at 0 of 23 cells" (golden
     x 2 has c_int(1, 0) = 0); the plant "c_pl < c_sr at 21 cells, fails
     at 12, its failures {'no member at t = 2': 303}".
  F10 THE CYLINDER BOUND (P9 lands). Controls: "0 of 40 off"; the strict
     bar "puts c_lo above c_saf at 27 cells", the lax one "gaps [3, 3,
     3, 3]". "c_lo > c_saf at 0 cells, c_lo > c_int at 0"; "c_ov - c_lo
     over the grid: 0: 31, 1: 67, 2: 22"; "c_saf - c_lo: 0: 54, 1: 56, 2:
     10; c_lo = 0 and c_saf = 0 disagree at 0 cells"; "c_int - c_lo at s
     = 0: 1: 14, 2: 10". "ties (a bar met exactly, missed when summed to
     top): 6 cells, at s = (m - 1)a, a the constant quotient: 6". e - 2
     and the random
     alpha: "|T_3| < 1 at every slack: yes; c_ov - c_lo 0 to 2". The
     family: s 1, 3, 6, 11, 19, 32 and t_1 = N, the largest gap N, at
     c_lo 1 and c_ov N + 1, at x 4, 16, 64, 256, 512, 2048. "gap above
     max(2, t_1): 0; t_1 above max(1, 2 ceil(log2(2s + 1))): 0; c_ov
     with its bars read from above moves at 0 of 232 cells".
     (b) The zero cylinder (P9(b) lands). Controls: "0 faults over the
     six alpha"; golden "[2, 4, 4, 4, 4, 6, 6, 6]"; silver x 4 "one
     level 2, two levels 3". The pinning reads N = 0 alone at "[19, 11,
     8, 14, 16, 13]" levels; the least passing c differs from c_lo2 at
     "0 of 48". c_lo / one level / c_lo2 / c_saf / c_int, x 2 .. x 5:
       golden      2/2/2/3/3  3/4/4/5/5  3/4/4/5/5  4/4/4/6/6
       silver      1/2/2/2/2  2/2/2/3/3  2/2/3/3/3  2/2/2/4/4
       bronze      1/2/2/2/2  1/2/2/2/2  2/2/2/3/3  2/2/2/3/3
       sqrt(3) - 1 2/2/2/3/3  2/2/2/4/4  3/4/4/5/5  3/4/4/5/5
       V1          2/2/2/3/3  3/4/4/4/4  3/4/4/5/5  4/4/4/5/5
       V2          2/2/2/3/3  2/2/2/4/4  3/4/4/4/4  3/4/4/5/5
     "c_int - c_lo2: 0: 6, 1: 14, 2: 4; where c_lo2 > c_lo: 0: 6, 1: 6;
     where c_lo2 = c_lo: 1: 8, 2: 4; the seam bar moves c_lo2 at
     ['silver x4']"; c_saf = c_int at all 24. c_lo/c_lo2/c_ov at depth
     110, x 2 .. x 5: e - 2 "2/2/4, 3/4/4, 3/4/4, 3/4/4", random "2/2/4,
     3/4/5, 3/4/5, 4/4/5".
     (c) The pinned limit (P9(c) lands, but for one prediction).
     Controls: c_saf "0 of 24 off", L = 1 and 2 "0, 0 of 48 off", "0 of
     12 off", "0 states"; the plant moves the L = 2 control and the
     limit "at 8 of 48 cells and 1 of 24". "K1: ... 0 cells", "K2: ... 0
     disagreements". "c_L stops at L = [1, 2, 3, 4, 5, 6, 7, 9, 10] of
     14": the stop by L = 8 failed, the latest stops 9 and 10. "c_inf = c_saf at 48 of 48 cells; at c_saf - 1 every
     pre-read loses at 48 of 48". c_inf, x 2 .. x 9: golden 3 5 5 6 6 7
     7 7, silver 2 3 3 4 4 4 4 4, bronze 2 2 3 3 3 3 3 4, sqrt(3) - 1 3
     4 5 5 5 5 5 6, V1 3 4 5 5 6 6 6 6, V2 3 4 4 5 5 5 5 5.
  Checks that read less than they seem, kept as reads: C1's tail lemma is
     an equality at golden, so its margin there is the truncation's;
     C1 reads the overlaps at L < 30 and the lemma at L < 40, and its
     |T_0| and overlap tests (ov is |T_(L+1)| - |theta_L| by
     definition) fail only through a slip in Metric's caps, theta or
     truncation;
     P1's parting of the extremes fails only at a_2 = 0; P5(c)'s and
     EARLIER's comparisons pass on None against None, which the
     prints show; P9(b)'s sub-cylinders share their ends by
     construction, so only its hull = I_j clause reads the recurrence;
     P9(c) recomputes c_saf with the grid's own solver, failing only
     where the grid's search cap cut it short.

RUN RECORD. `--full` under a 512 MB watch, its last run below. Two
earlier full runs were killed at the ceiling while holding a twice-box
game beside the {1, 2, 3} and the x 3 cells; the twice-box lineage check
now runs at {1, 2}, x 2 only, and each game is freed before the next. A
print of the c_int - c_saf tally was added to the grid after the slate
froze. An independent audit then found P6's necklaces read at one
rotation each (71 of the 472 alphas) and P1's comparison stopping at a
string's own length; both now run whole, and every print above is the
whole run's. A later reading found the box's A taken over a_1 .. a_52,
past the quotients the track's times 0 .. 40 use (a_1 .. a_41); at e - 2
that inflated B_g, and with A over a_1 .. a_41 the branch's share of B_g
is 0.92, first printed as 0.77. The same reading split P6's unflushed
reads from its seed mismatches and asserted the (0, 0) column's safety
game too. A print of c_ov's range over the grid was added later, and P7
after it, and P8 after that, its control later moved from c_ov(1, 1)
to c_ov(0, 1) so that it differs from the reader in the windows and
caps alone; the run after: 36/36, 156.6 s, peak 311.5 MB. P8(c) came
from a lab script whose verdicts and c_sr matched (c)'s prints (its
inputs and random alpha drew from another seed); the run after: 40/40,
167.4 s, peak 312.9 MB. P9 came from a lab script whose prints it
matches at every count above but three that are new: the s = 0 tally,
the ties' count at s = (m - 1)a and c_ov's both-ways read beyond the
grid. That script's first run, its bars summed to top, put c_lo above
c_saf and above c_int at six cells each and its golden closed forms off
at 4 of 40, every miss a tie, which killed its frozen floor; with the
bars re-read from above (hence Metric's reading) the floor and gap-2
kills held, its kill on the family (a largest gap <= 2) did not fire,
and its frozen prediction that the gap exceeds 2 and grows with m
failed: the gap tracked N, not m. So c_ov <= c_lo + max(2, t_1) was
frozen after it, as a second pass, whose first print found t_1 <= 2
ceil(log2(2s + 1)) false at the 20 cells with s = 0 and a_1 = 1 (|T_1|
= 1 exactly), the bound becoming max(1, .); the wall's equality, the
largest gap max(2, t_1), is that pass's observation. The run after:
48/48, 169.0 s, peak 314.0 MB. A later audit found c_ov read from above
only on the grid; the print now covers every cell but the golden
controls, its plant (the above-read overlaps tripled) moving c_ov at 32
of the default run's 122 cells and failing
the check. The run after: 49/49, 168.2 s, peak 310.3 MB. P9(b) came from
a lab script whose prints it matches at every count; that script's
plant, the sub-cylinders read by length alone, equals the one-level bar
by construction and was dropped. Broken in a scratch copy, the pinning
read with its interval closed finds another N at every alpha, and the
members cut to member 0 fail four of P9(b)'s checks. The run after:
57/57, 219.6 s, peak 312.3 MB. P9(c) came from a lab script whose
prints it matches at every count but the plant's, its x 6 .. x 9
widening a second run there; that script first ran the subtree at every
c and t, and was refused at the ceiling, so the engine reads c <= c_saf
+ 1 and t = 1 .. 2p. Its plant ran at x 2 .. x 5 alone; here it runs
the L = 2 control at every cell and the limit at x 2 .. x 5, the limit
arm added after an audit found the first port's plant reaching L = 2
alone (64/64, 246.3 s, 346.9 MB). The run after: 64/64, 244.3 s, peak
347.5 MB.
"""

import os
import random
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from ostrowski import Numeration, e_minus_2  # noqa: E402

CHECKS = []
FULL = "--full" in sys.argv    # the record run; the default runs small
LOOKCAP = 3
N_CHECK = 1000 if FULL else 400
N_TEAR = 300 if FULL else 120
N_FLOOR = 60000 if FULL else 20000
N_PLAY, DEPTH = (200, 40) if FULL else (60, 30)
SEED = 20260924

PERIODIC = [("golden [1]", (1,)), ("silver [2]", (2,)),
            ("bronze [3]", (3,)), ("sqrt(3) - 1 [1, 2]", (1, 2)),
            ("V1 [1, 1, 1, 2]", (1, 1, 1, 2)),
            ("V2 [2, 1, 3, 1]", (2, 1, 3, 1))]
SLACKS = [(0, 0), (0, 1), (1, 0), (1, 1), (2, 2), (3, 3)]
# The integer reader's least lookahead over this grid as an earlier,
# independent engine printed it (lattice points of the quadratic field
# of alpha, its own box): rows x2..x5, columns SLACKS, None for no c up
# to its cap.
EARLIER = {
    "golden [1]": [[None, 3, 0, 0, 0, 0], [None, 5, 2, 2, 0, 0],
                   [None, 5, 3, 3, 2, 0], [None, 6, 3, 3, 2, 2]],
    "silver [2]": [[None, 2, 2, 2, 0, 0], [None, 3, 2, 2, 2, 2],
                   [None, 3, 3, 2, 2, 2], [None, 4, 3, 3, 2, 2]],
    "bronze [3]": [[None, 2, 2, 2, 2, 0], [None, 2, 2, 2, 2, 2],
                   [None, 3, 2, 2, 2, 2], [None, 3, 2, 2, 2, 2]],
    "sqrt(3) - 1 [1, 2]": [[None, 3, 2, 2, 0, 0], [None, 4, 2, 2, 2, 2],
                           [None, 5, 3, 3, 2, 2], [None, 5, 3, 3, 2, 2]],
    "V1 [1, 1, 1, 2]": [[None, 3, 2, 2, 0, 0], [None, 4, 2, 2, 2, 2],
                        [None, 5, 3, 3, 2, 2], [None, 5, 4, 4, 2, 2]],
    "V2 [2, 1, 3, 1]": [[None, 3, 2, 2, 2, 0], [None, 4, 2, 2, 2, 2],
                        [None, 4, 3, 3, 2, 2], [None, 5, 3, 3, 2, 2]],
}
BAND = [("[4]", (4,), 2, 3), ("[5]", (5,), 2, 3), ("[4]", (4,), 3, 5),
        ("bronze [3]", (3,), 3, 5)]


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


def numeration(name, period):
    reps = -(-200 // len(period))
    while True:
        quots = list(period) * reps
        try:
            return Numeration(name, quots)
        except AssertionError:
            reps += 1


# ------------------------------------------------------------ the metric

class Metric:
    """theta_k, the level ranges T_L and their overlaps at slack
    (s, s0), exactly: every real is held as its numerator over the
    convergent's denominator Q."""

    def __init__(self, w, s, s0, top):
        self.s, self.s0, self.top = s, s0, top
        self.Q, self.a = w.Q, w.a
        self.th = [A * w.Q + B * w.P
                   for A, B in (w.theta(k) for k in range(-1, top + 3))]

    def theta(self, k):
        return self.th[k + 1]

    def cap(self, k):
        return self.a[1] - 1 + self.s0 if k == 0 else self.a[k + 1] + self.s

    def S(self, L):
        return sum(abs(self.theta(k)) for k in range(L, self.top))

    def T(self, L):
        """(lo, hi) of the tails from level t, truncated at top."""
        lo = hi = 0
        for k in range(L, self.top):
            v = self.cap(k) * self.theta(k)
            if v < 0:
                lo += v
            else:
                hi += v
        return lo, hi

    def E(self, above=False):
        return (self.s0 * self.theta(0) + self.s * self.S(1)
                + (self.tail() if above else 0))

    def tail(self):
        """A bound on s S_top, the part E's sum to top drops, as
        |theta_(k+2)| < |theta_k|/2."""
        return 2 * self.s * (abs(self.theta(self.top))
                             + abs(self.theta(self.top + 1)))

    def Tlen(self, L, above=False):
        """|T_L| summed to top, or from above: the a-part's telescoped
        |theta_(top-1)| + |theta_top| and the tail added, so that an exact
        tie w = |T_L| passes."""
        lo, hi = self.T(L)
        if not above:
            return hi - lo
        return (hi - lo + abs(self.theta(self.top - 1))
                + abs(self.theta(self.top)) + self.tail())

    def ov(self, L, above=False):
        return self.Tlen(L + 1, above) - abs(self.theta(L))

    def width(self, L, c, m):
        return m * (abs(self.theta(L + c)) + abs(self.theta(L + c + 1)))


def c_overlap(met, m, depth, cmax=12, above=False):
    """The least c with w_0 <= E and w_t <= ov_t at every t < depth;
    None at E <= 0 or when no c <= cmax works. With above, the bars are
    read from above."""
    E = met.E(above)
    if E <= 0:
        return None
    ovs = [met.ov(L, above) for L in range(depth)]
    for c in range(cmax + 1):
        if met.width(0, c, m) <= E and all(
                met.width(L, c, m) <= ovs[L] for L in range(depth)):
            return c
    return None


# ------------------------------------------------------------ the game

class Source:
    """Where the quotients come from: a periodic alpha (the state is
    the index of the next quotient in the period) or a class (every
    letter of the alphabet at every step, one state)."""

    def __init__(self, period=None, alphabet=None):
        self.period, self.alphabet = period, alphabet
        self.A = max(period or alphabet)

    def start(self):
        return 0

    def nxt(self, st):
        if self.period:
            P = self.period
            return [(P[st], (st + 1) % len(P))]
        return [(a, 0) for a in self.alphabet]


class Game:
    """The residual game of n -> m n + omega at lookahead `look`, the
    output capped at a_(t+1) + s (position 0: a_1 - 1 + s0), in frame
    coordinates (argument (5)). rule=True keeps the below-a-cap rule
    on the output (the legal output; s = s0 = 0 only)."""

    def __init__(self, src, m, s, s0, look, omega=0, rule=False, scale=1):
        assert 0 <= omega <= m and s0 <= s + 1
        assert not rule or s == s0 == 0
        self.src, self.m, self.s, self.s0 = src, m, s, s0
        self.look, self.omega, self.rule = look, omega, rule
        mu = max(m, 1 + s)
        self.bx = scale * (mu * (src.A + 1) + 1 + s + m)
        self.by = scale * (1 + s + m + mu)
        self.K = 2 * self.by + 1
        self.build()

    def pack(self, x, y):
        return (x + self.bx) * self.K + (y + self.by)

    # a state: (branches, quots, srcst, digs, lastzero_in, pos0,
    # lastzero_out); quots = (a_(t+1) .. a_(t+c+1)), digs = (d_(t+1) ..
    # d_(t+c)).
    def cap_out(self, st):
        a1 = st[1][0]
        if st[5]:
            return a1 - 1 + self.s0
        if self.rule and not st[6]:
            return a1 - 1
        return a1 + self.s

    def replies(self, st):
        for a_new, src2 in self.src.nxt(st[2]):
            top = a_new if st[4] else a_new - 1
            for d_new in range(top + 1):
                yield a_new, src2, d_new

    def succ(self, st, e, a_new, src2, d_new):
        br, quots, digs = st[0], st[1], st[3]
        seq = digs + (d_new,)
        d1, a1, m = seq[0], quots[0], self.m
        bx, by, K = self.bx, self.by, self.K
        out = []
        for v in br:
            x, y = divmod(v, K)
            x -= bx
            y -= by
            X, Y = y + m * d1, x - e - a1 * y
            if -bx <= X <= bx and -by <= Y <= by:
                out.append((X + bx) * K + (Y + by))
        if not out:
            return None
        return (tuple(sorted(out)), quots[1:] + (a_new,), src2, seq[1:],
                d_new == 0, False, e == 0)

    def seed(self, d0):
        x = self.m * d0 + self.omega
        return tuple(sorted(self.pack(x, y)
                            for y in range(-self.by, self.by + 1)))

    def initial(self):
        """Every legal pre-read d_0 .. d_c with its quotients."""
        out, c = [], self.look

        def rec(quots, srcst, digs, lastzero):
            if len(quots) == c + 1:
                out.append((self.seed(digs[0]), quots, srcst, digs[1:],
                            lastzero, True, True))
                return
            k = len(quots)
            for a, src2 in self.src.nxt(srcst):
                top = a - 1 if k == 0 else (a if lastzero else a - 1)
                for d in range(top + 1):
                    rec(quots + (a,), src2, digs + (d,), d == 0)
        rec((), self.src.start(), (), True)
        return out

    def build(self):
        ids, states = {}, []
        self.init = []
        for st in self.initial():
            if st not in ids:
                ids[st] = len(states)
                states.append(st)
            self.init.append(ids[st])
        todo = list(range(len(states)))
        trans = [None] * len(states)
        while todo:
            i = todo.pop()
            st = states[i]
            moves = {}
            for e in range(self.cap_out(st) + 1):
                zs, nz = [], []
                for a_new, src2, d_new in self.replies(st):
                    st2 = self.succ(st, e, a_new, src2, d_new)
                    if st2 is None:
                        break
                    j = ids.get(st2)
                    if j is None:
                        j = ids[st2] = len(states)
                        states.append(st2)
                        trans.append(None)
                        todo.append(j)
                    (zs if d_new == 0 else nz).append(j)
                else:
                    moves[e] = (len(zs), tuple(zs + nz))
            trans[i] = moves
        self.trans, self.states, self.ids = trans, states, ids
        self.zero = self.pack(0, 0)

    def solve(self, flush):
        """The winning set: safety, alternated with the flush attractor
        when flush is True. Sets W and dist; returns whether every
        initial state wins."""
        W = set(range(len(self.states)))
        flushed = [self.zero in st[0] and not any(st[3])
                   for st in self.states]
        while True:
            changed = True
            while changed:
                changed = False
                for i in list(W):
                    if not any(all(j in W for j in succ)
                               for _nz, succ in self.trans[i].values()):
                        W.discard(i)
                        changed = True
            if not flush:
                self.W, self.dist = W, None
                break
            dist = {i: 0 for i in W if flushed[i]}
            grew = True
            while grew:
                grew = False
                for i in W:
                    if i in dist:
                        continue
                    best = None
                    for nz, succ in self.trans[i].values():
                        zs = succ[:nz]
                        if zs and all(j in W for j in succ) and all(
                                j in dist for j in zs):
                            v = 1 + max(dist[j] for j in zs)
                            best = v if best is None else min(best, v)
                    if best is not None:
                        dist[i] = best
                        grew = True
            if len(dist) == len(W):
                self.W, self.dist = W, dist
                break
            W = set(dist)
        self.wins = all(i in self.W for i in self.init)
        return self.wins

    def choose(self, i):
        best = None
        for e, (nz, succ) in self.trans[i].items():
            if all(j in self.W for j in succ):
                key = 0
                if self.dist is not None:
                    key = max(self.dist[j] for j in succ[:nz])
                if best is None or key < best[0]:
                    best = (key, e)
        return best[1]

    def start_state(self, d, quots):
        c = self.look
        for i in self.init:
            st = self.states[i]
            if st[1] == tuple(quots[:c + 1]) and st[3] == tuple(d[1:c + 1]) \
                    and st[0] == self.seed(d[0]):
                return i
        raise KeyError("no initial state for this pre-read")

    def read(self, digits, quots, extra=6):
        """Run the reader on a greedy string at the alpha whose
        quotients are quots (a_1, a_2, ...): (output, flushed, path),
        path holding (e, d_(t+1), a_(t+1)) per step."""
        c = self.look
        d = list(digits) + [0] * (c + extra + 2)
        i = self.start_state(d, quots)
        out, path = [], []
        for t in range(len(digits) + extra):
            e = self.choose(i)
            cur = self.states[i]
            a_new, d_new = quots[t + c + 1], d[t + c + 1]
            src2 = [s2 for a, s2 in self.src.nxt(cur[2]) if a == a_new][0]
            st2 = self.succ(cur, e, a_new, src2, d_new)
            path.append((e, (cur[3] + (d_new,))[0], cur[1][0]))
            out.append(e)
            i = self.ids[st2]
        st = self.states[i]
        return out, self.zero in st[0] and not any(st[3]), path


def least(src, m, s, s0, flush, lo=0, hi=LOOKCAP, omega=0, rule=False,
          scale=1):
    """The least lookahead in lo..hi at which the reader wins, with the
    winning game; (None, None) when none does."""
    for c in range(lo, hi + 1):
        g = Game(src, m, s, s0, c, omega, rule, scale)
        if g.solve(flush):
            return c, g
    return None, None


# ------------------------------------------------------------ helpers

def maps():
    return (2, 3, 4, 5) if FULL else (2, 3)


def legal_random(rnd, quots, length):
    """A random legal greedy string of the given length."""
    d, last = [], 0
    for k in range(length):
        cap = quots[0] - 1 if k == 0 else quots[k]
        top = cap if (k == 0 or last == 0) else cap - 1
        d.append(rnd.randint(0, top))
        last = d[-1]
    return d


def certify(g, w, m, s, s0, N, omega=0):
    """Run the reader of game g on every n < N at numeration w; the
    count of wrong values, broken caps or missing flushes."""
    bad = 0
    quots = w.a[1:]
    for n in range(N):
        out, flushed, _path = g.read(w.digits(n), quots)
        val = sum(e * w.q(k) for k, e in enumerate(out))
        caps = all(e <= (quots[0] - 1 + s0 if k == 0 else quots[k] + s)
                   for k, e in enumerate(out))
        if val != m * n + omega or not caps or not flushed:
            bad += 1
    return bad


def lineage(g, path):
    """The flushing branch's trajectory, rebuilt backward from (0, 0)
    through the recorded (e, d_(t+1), a_(t+1)): its largest |g|, |h|
    and its seed's g."""
    x = y = 0
    mx = my = 0
    for e, d1, a1 in reversed(path):
        y0 = x - g.m * d1
        x0 = y + e + a1 * y0
        x, y = x0, y0
        mx, my = max(mx, abs(x)), max(my, abs(y))
    return mx, my, x


# ------------------------------------------------------------ C1a ranges

def section_ranges():
    print("== C1a the ranges, the overlaps and the tail lemma")
    alist = [(n, p) for n, p in PERIODIC] + [("e - 2", None)]
    worst = 0
    for name, per in alist:
        w = numeration(name, per) if per else Numeration(name, e_minus_2(200))
        for s, s0 in SLACKS:
            met = Metric(w, s, s0, 120)
            lo, hi = met.T(0)
            tol = 4 * abs(met.theta(met.top - 1))
            dev = abs((hi - lo) - (met.Q + met.E()))
            ovdev = max(abs(met.ov(L) - abs(met.theta(L + 1))
                            - s * met.S(L + 1)) for L in range(30))
            lemma = min(abs(met.theta(L - 1)) + abs(met.theta(L))
                        - met.S(L) for L in range(40))
            worst = max(worst, float(dev / tol), float(ovdev / tol))
            if lemma < 0:
                worst = float("inf")
    check("|T_0| = 1 + E and ov_t = |theta_(t+1)| + s S_(t+1) to the "
          "truncation, the tail lemma at every level read",
          worst <= 1, f"worst deviation {worst:.2f} of the truncation bound")


# ------------------------------------------------------------ P1 the tear

def strings_of(w, N, s, s0, k=None):
    """Every string with e_j <= cap_j and sum e_j q_j = N."""
    if k is None:
        k = w.depth_of(N) if N else 0
    if k < 0:
        return [[]] if N == 0 else []
    cap = w.a[1] - 1 + s0 if k == 0 else w.a[k + 1] + s
    out = []
    for e in range(min(cap, N // w.q(k)) + 1):
        for rest in strings_of(w, N - e * w.q(k), s, s0, k - 1):
            out.append(rest + [e])
    return out


def section_tear():
    print("== P1 the tear at E = 0")
    alist = [(n, p) for n, p in PERIODIC] + [("e - 2", None)]
    total = off = disagree = 0
    part_ok = True
    for name, per in alist:
        w = numeration(name, per) if per else Numeration(name, e_minus_2(200))
        th = [w.value(w.theta(k)) for k in range(40)]
        alpha = th[0]
        lo_s = [0 if k % 2 == 0 else w.a[k + 1] for k in range(40)]
        hi_s = [(w.a[1] - 1 if k == 0 else w.a[k + 1]) if k % 2 == 0 else 0
                for k in range(40)]
        part = next(k for k in range(40) if lo_s[k] != hi_s[k])
        part_ok &= part == w.t0 - 1
        for N in range(N_TEAR):
            rep = N * alpha - ((N * alpha + alpha).numerator
                               // (N * alpha + alpha).denominator)
            for e in strings_of(w, N, 0, 0):
                e = e + [0] * (40 - len(e))
                total += 1
                star = sum(ek * th[k] for k, ek in enumerate(e))
                if star != rep:
                    off += 1
                for ext, gap in ((lo_s, star + alpha),
                                 (hi_s, 1 - alpha - star)):
                    for k, ek in enumerate(e):
                        if abs(th[k]) > gap and ek != ext[k]:
                            disagree += 1
    check("every string's star is the representative of N alpha mod 1",
          off == 0, f"{total} strings over N < {N_TEAR} at seven alphas, "
          f"{off} off")
    check("a string within eta of an end agrees with that end's extreme "
          "string wherever |theta_k| > eta", disagree == 0,
          f"{disagree} disagreements")
    check("the extreme strings part at position t_0 - 1", part_ok)


# ------------------------------------------------------ P2 and P5a

class Overlap:
    """The completion reader of argument (3) at lookahead c, in integer
    numerators over the convergent's denominator Q."""

    def __init__(self, w, m, s, s0, c, depth):
        self.m, self.c = m, c
        top = depth + c + 60
        self.th = [w.theta(k) for k in range(-1, top + 2)]
        self.th = [A * w.Q + B * w.P for A, B in self.th]
        self.Q = w.Q
        self.depth, self.top = depth, top
        self.cap = [w.a[1] - 1 + s0] + [w.a[k + 1] + s
                                        for k in range(1, top + 1)]
        self.T = []
        for L in range(depth + 2):
            lo = hi = 0
            for k in range(L, top):
                v = self.cap[k] * self.t(k)
                lo, hi = (lo + v, hi) if v < 0 else (lo, hi + v)
            self.T.append((lo, hi))

    def t(self, k):
        return self.th[k + 1]

    def interval(self, j):
        """The closed interval between -theta_j and -theta_(j-1)."""
        a, b = -self.t(j), -self.t(j - 1)
        return min(a, b), max(a, b)

    def run(self, d):
        """Read the legal string d (long enough); returns (ok, M, out,
        close), close whether |output star - (m x + M)| <= |T_depth|."""
        m, c, Q = self.m, self.c, self.Q
        seen = sum(d[k] * self.t(k) for k in range(c + 1))
        ilo, ihi = self.interval(c + 1)
        lo, hi = m * (seen + ilo), m * (seen + ihi)
        T0lo, T0hi = self.T[0]
        M = -((lo - T0lo) // Q)          # lo + M Q lands in [T0lo, T0lo + Q)
        lo, hi = lo + M * Q, hi + M * Q
        if not (T0lo <= lo and hi <= T0hi):
            return False, M, [], None
        committed = 0
        out = []
        for L in range(self.depth):
            base = M * Q + m * seen - committed     # M + m seen - committed
            ilo, ihi = self.interval(L + c + 1)
            jlo, jhi = base + m * ilo, base + m * ihi
            tl, th_ = self.T[L + 1]
            best = None
            for e in range(self.cap[L] + 1):
                off = e * self.t(L)
                if off + tl <= jlo and jhi <= off + th_:
                    margin = min(jlo - off - tl, off + th_ - jhi)
                    if best is None or margin > best[0]:
                        best = (margin, e)
            if best is None:
                return False, M, out, None
            e = best[1]
            out.append(e)
            committed += e * self.t(L)
            seen += d[L + c + 1] * self.t(L + c + 1)
        xstar = sum(d[k] * self.t(k) for k in range(len(d)))
        err = abs(committed - (m * xstar + M * Q))
        tl, th_ = self.T[self.depth]
        return True, M, out, err <= th_ - tl


def section_completion():
    print("== P2 the completion reader, and P5a its branch in the box")
    rnd = random.Random(SEED)
    alist = [(n, p) for n, p in PERIODIC] + [("e - 2", None)]
    if FULL:
        alist += [("[4]", (4,)), ("[5]", (5,))]
    fails = errs = outbox = runs = 0
    cov = {}
    worst = (0, 0)
    for name, per in alist:
        w = numeration(name, per) if per else Numeration(name, e_minus_2(200))
        quots = w.a[1:]
        A = max(quots[:DEPTH + 1])        # a_(t+1) at the track's times 0..DEPTH
        for m in maps():
            for s, s0 in SLACKS[1:]:
                met = Metric(w, s, s0, DEPTH + 60)
                c = c_overlap(met, m, DEPTH)
                cov[(name, m, s, s0)] = c
                rd = Overlap(w, m, s, s0, c, DEPTH)
                mu = max(m, 1 + s)
                bx, by = mu * (A + 1) + 1 + s + m, 1 + s + m + mu
                for _ in range(N_PLAY):
                    d = legal_random(rnd, quots, DEPTH + c + 4)
                    ok, M, out, close = rd.run(d)
                    runs += 1
                    if not ok:
                        fails += 1
                        continue
                    if not close:
                        errs += 1
                    mx, my = _track(m, out, d, M, quots)
                    worst = (max(worst[0], mx / bx), max(worst[1], my / by))
                    if mx > bx or my > by:
                        outbox += 1
    check("the overlap reader finds a member at every level", fails == 0,
          f"{runs} runs to depth {DEPTH}, {fails} failures")
    check("its output star lies within |T_depth| of m x + M", errs == 0,
          f"{errs} off")
    check("its true branch stays inside the box", outbox == 0,
          f"largest |g|/Bg {worst[0]:.2f}, |h|/Bh {worst[1]:.2f}")
    return cov


def _track(m, out, d, M, quots):
    x, y = m * d[0], -M
    mx, my = abs(x), abs(y)
    for t, e in enumerate(out):
        x, y = y + m * d[t + 1], x - e - quots[t] * y
        mx, my = max(mx, abs(x)), max(my, abs(y))
    return mx, my


# ------------------------------------------------------------ P3 floors

def section_floors():
    print("== P3 the floors at every slack")
    alist = PERIODIC if FULL else PERIODIC[:4]
    tiles = fits = 0
    least_excess = None
    for name, per in alist:
        w = numeration(name, per)
        keys = w.keys(N_FLOOR)
        for m in (2, 3):
            for s in range(4):
                met = Metric(w, s, s, 120)
                t = next(t for t in range(1, 60)
                         if m * (met.T(t)[1] - met.T(t)[0]) < met.Q)
                width = met.T(t)[1] - met.T(t)[0]
                for c in range(4):
                    if t + c >= len(keys):
                        break
                    groups = {}
                    for n, key in enumerate(keys[t + c]):
                        groups.setdefault(key, []).append(n)
                    for ns in groups.values():
                        if len(ns) < 12:
                            continue
                        pts = sorted((n // m) * w.P % w.Q for n in ns)
                        gaps = [b - a for a, b in zip(pts, pts[1:])]
                        gaps.append(pts[0] + w.Q - pts[-1])
                        hull = w.Q - max(gaps)
                        tiles += 1
                        ex = (hull - width) / w.Q
                        least_excess = ex if least_excess is None \
                            else min(least_excess, ex)
                        if hull <= width:
                            fits += 1
    check("floor(n/m): no input tile's images fit a depth-t* cylinder",
          fits == 0, f"{tiles} (tile, m, s, c) tests, m = 2, 3, s = s_0 "
          f"= 0..3, c = 0..3, least "
          f"hull less |T_t*| = {least_excess:.4f}")


# ------------------------------------------------------ C1b-d, P1, P4, P5b

def section_controls():
    print("== C1b the legal output through the game")
    ok = True
    for name, per in PERIODIC:
        src = Source(period=per)
        ident = least(src, 1, 0, 0, True, rule=True)[0]
        succ = least(src, 1, 0, 0, True, omega=1, rule=True)[0]
        x2 = least(src, 2, 0, 0, True, rule=True)[0]
        x3 = least(src, 3, 0, 0, True, rule=True)[0]
        free = least(src, 1, 0, 0, True, omega=1)[0]
        row = (ident, succ, x2, x3, free)
        ok &= row == (0, 1, None, None, 0)
        print(f"    {name:20s} id {ident}  n+1 {succ}  x2 {x2}  x3 {x3}"
              f"   n+1 rule dropped {free}")
    check("identity 0, n + 1 at 1, x 2 and x 3 at no c <= LOOKCAP; "
          "n + 1 at 0 once the rule is dropped", ok)


def section_grid(cov):
    print("== the grid: c_saf / c_int per (alpha, m, (s, s_0)), c_ov after")
    alist = PERIODIC if FULL else [PERIODIC[0], PERIODIC[1], PERIODIC[3]]
    bad = earlier_off = floor_off = saf_over = tear_off = 0
    grid = {}
    for name, per in alist:
        src = Source(period=per)
        w = numeration(name, per)
        A = max(per)
        print(f"  {name}")
        for m in maps():
            row = []
            for j, (s, s0) in enumerate(SLACKS):
                c_ov = cov.get((name, m, s, s0))
                hi = max(LOOKCAP, (c_ov or 0) + 1)
                c_saf, _g = least(src, m, s, s0, False, hi=hi)
                c_int, g = least(src, m, s, s0, True, lo=c_saf or 0, hi=hi) \
                    if c_saf is not None else (None, None)
                if g is not None:
                    bad += certify(g, w, m, s, s0, N_CHECK)
                grid[(name, m, s, s0)] = (c_saf, c_int)
                if c_int != EARLIER[name][m - 2][j]:
                    earlier_off += 1
                digitwise = s >= (m - 1) * A
                if (c_int == 0) != digitwise or c_int == 1:
                    floor_off += 1
                if (s, s0) == (0, 0) and c_saf is not None:   # no reader at all
                    tear_off += 1
                if c_ov is not None and (c_saf is None or c_saf > c_ov):
                    saf_over += 1
                row.append(f"{_fmt(c_saf)}/{_fmt(c_int)} {_fmt(c_ov)}")
            print(f"    x{m}  " + "   ".join(f"{r:7s}" for r in row))
    tally = {}
    for c_saf, c_int in grid.values():
        if c_saf is not None and c_int is not None:
            tally[c_int - c_saf] = tally.get(c_int - c_saf, 0) + 1
    print("  c_int - c_saf over the finite cells: " + ", ".join(
        f"{k}: {v}" for k, v in sorted(tally.items())))
    ovs = [cov[(name, m, s, s0)] for name, _ in alist for m in maps()
           for s, s0 in SLACKS if cov.get((name, m, s, s0)) is not None]
    print(f"  c_ov over the grid's cells with E > 0: {min(ovs)} to "
          f"{max(ovs)}")
    check("every winning strategy is correct on every n < N_CHECK",
          bad == 0, f"{bad} bad")
    check("c_int agrees with the earlier independent engine",
          earlier_off == 0, f"{earlier_off} cells off")
    check("the (0, 0) column: x m reads at no c <= LOOKCAP", tear_off == 0)
    check("c_int is 0 exactly where s >= (m - 1) a_max, else >= 2",
          floor_off == 0, f"{floor_off} cells off")
    check("c_saf <= c_ov at every cell with E > 0", saf_over == 0,
          f"{saf_over} cells over")
    return grid


def _fmt(c):
    return "-" if c is None else str(c)


def section_digitwise():
    print("== P4a,b the flush floor's two halves")
    bad = 0
    for name, per in PERIODIC:
        w = numeration(name, per)
        A = max(per)
        for m in maps():
            s = (m - 1) * A
            a1 = w.a[1]
            for n in range(N_CHECK):
                d = w.digits(n) + [0, 0]
                e = [m * dk for dk in d]
                e[0], carry = (m * d[0]) % a1, (m * d[0]) // a1
                e[1] += carry
                val = sum(ek * w.q(k) for k, ek in enumerate(e))
                caps = e[0] <= a1 - 1 and all(
                    e[k] <= w.a[k + 1] + s for k in range(1, len(e)))
                if val != m * n or not caps:
                    bad += 1
    check("the digitwise reader at s = (m - 1) a_max, s_0 = 0: correct",
          bad == 0, f"{bad} bad over n < {N_CHECK}")
    wrong = 0
    shown = []
    for name, per in PERIODIC:
        w = numeration(name, per)
        P = len(per)
        for m in maps():
            for phase in range(P):
                k = next(k for k in range(2, 200) if k % P == phase
                         and w.q(k - 1) > m * w.a[k + 1])
                N = m * w.a[k + 1]
                V = N * w.q(k)
                coins = [w.q(j) for j in range(k - 1, 200) if w.q(j) <= V]
                ways = [1] + [0] * V
                for q in coins:
                    for v in range(q, V + 1):
                        ways[v] += ways[v - q]
                if ways[V] != 1:
                    wrong += 1
                if len(shown) < 3:
                    shown.append(f"{name} x{m} k={k}: {V} = {N} q_{k}")
    check("m a_(k+1) q_k has exactly one string from level k - 1 (any "
          "digit sizes), e_k = m a_(k+1)", wrong == 0,
          f"{wrong} off; e.g. " + "; ".join(shown))


# ------------------------------------------------------------ P5c, P5d

def section_band():
    print("== P5d the band cells: c_ov = 1 < 2 <= c_int")
    ok = True
    cells = BAND if FULL else BAND[:1]
    for name, per, m, s in cells:
        w = numeration(name, per)
        met = Metric(w, s, s, DEPTH + 60)
        c_ov = c_overlap(met, m, DEPTH)
        src = Source(period=per)
        c_saf, _g = least(src, m, s, s, False, hi=3)
        c_int, g = least(src, m, s, s, True, hi=3)
        bad = certify(g, w, m, s, s, N_CHECK) if g else None
        print(f"    {name:12s} x{m} s = s_0 = {s}: c_ov {c_ov}  c_saf "
              f"{c_saf}  c_int {c_int}  states {len(g.states) if g else '-'}"
              f"  bad {bad}")
        ok &= (c_ov == 1 and c_saf is not None and c_saf <= 1
               and c_int == 2 and bad == 0)
    check("a strict flush price at every band cell", ok)
    if not FULL:
        return
    print("== P5c c_saf at twice the box")
    same = True
    for name, per, m, s, s0 in [("golden [1]", (1,), 3, 0, 1),
                                ("silver [2]", (2,), 2, 1, 1),
                                ("sqrt(3) - 1 [1, 2]", (1, 2), 3, 2, 2),
                                ("bronze [3]", (3,), 2, 2, 2)]:
        src = Source(period=per)
        one = least(src, m, s, s0, False, hi=6)[0]
        two = least(src, m, s, s0, False, hi=6, scale=2)[0]
        print(f"    {name:20s} x{m} ({s},{s0}): c_saf {one} at the box, "
              f"{two} at twice it")
        same &= one == two
    check("c_saf does not move when the box doubles", same)


# ------------------------------------------------------------ P7 the owed

def conj_ratios(per):
    """zeta'_t by t mod p: the fixed point of z -> a_t + 1/z run round
    the period, a_t = per[(t - 1) % p] (a_0 read as a_p)."""
    p, z = len(per), 1.0
    out = [0.0] * p
    for t in range(1, 400 * p + 1):
        z = per[(t - 1) % p] + 1 / z
        if t > 399 * p:
            out[t % p] = z
    return out


def real_ratios(per):
    """|theta_t/theta_(t-1)| = [0; a_(t+1), a_(t+2), ...] by t mod p,
    the control's transplant."""
    p = len(per)
    out = []
    for r in range(p):
        x = 0.0
        for k in range(400 * p, -1, -1):
            x = 1 / (per[(r + k) % p] + x)
        out.append(x)
    return out


def tentative(g, st, Z, conj=True):
    """Every branch of state st as (G, H, u~): (G, H) its tentative pair,
    the pending digits absorbed exactly, q_(t+j) = U_j q_t + V_j q_(t-1)
    by q_(k+1) = a_(k+1) q_k + q_(k-1); u~ by the product formula, Z the
    ratio by t mod p, checked against G Z_t + H when Z is zeta' (the
    identity needs Z_(t+1) = a_(t+1) + 1/Z_t, which the control's real
    ratio does not obey)."""
    c, p = g.look, len(Z)
    t = (st[2] - c - 1) % p
    prods, acc = [], Z[t]
    for j in range(1, c + 1):
        acc *= Z[(t + j) % p]
        prods.append(acc)
    pend = g.m * sum(d * pr for d, pr in zip(st[3], prods))
    (U0, V0), (U1, V1) = (0, 1), (1, 0)        # q_(t-1), q_t
    PG = PH = 0
    for j in range(1, c + 1):
        a = st[1][j - 1]                          # a_(t+j)
        (U0, V0), (U1, V1) = (U1, V1), (a * U1 + U0, a * V1 + V0)
        PG += g.m * st[3][j - 1] * U1
        PH += g.m * st[3][j - 1] * V1
    out = []
    for v in st[0]:
        x, y = divmod(v, g.K)
        x -= g.bx
        y -= g.by
        G, H = x + PG, y + PH
        u = x * Z[t] + y + pend
        assert not conj or abs(u - (G * Z[t] + H)) <= 1e-6 * (1 + abs(u))
        out.append((G, H, u))
    return out


def safe_within(g, good):
    """The safety game's greatest fixed point inside the states marked
    good."""
    W = {i for i in range(len(g.states)) if good[i]}
    changed = True
    while changed:
        changed = False
        for i in list(W):
            if not any(all(j in W for j in succ)
                       for _nz, succ in g.trans[i].values()):
                W.discard(i)
                changed = True
    return W


def section_owed(grid):
    print("== P7 the integer game is the safety game on u~ >= 0")
    off = ctrl_off = zero_bad = kept = compared = 0
    margin = float("inf")
    for name, per in PERIODIC:
        if not any(k[0] == name for k in grid):
            continue
        Zc, Zr = conj_ratios(per), real_ratios(per)
        print(f"    {name:20s} zeta' by t mod p: "
              + ", ".join(f"{z:.6f}" for z in Zc))
        src = Source(period=per)
        for m in maps():
            for s, s0 in SLACKS:
                c_int = grid[(name, m, s, s0)][1]
                cell_off = cell_ctrl = False
                for c in range((LOOKCAP if c_int is None else c_int) + 1):
                    g = Game(src, m, s, s0, c)
                    assert g.solve(True) == (c == c_int)
                    good, goodr = [], []
                    for st in g.states:
                        us = tentative(g, st, Zc)
                        if g.zero in st[0] and not any(st[3]) and not any(
                                G == 0 and H == 0 and abs(u) <= 1e-9
                                for G, H, u in us):
                            zero_bad += 1
                        margin = min([margin] + [abs(u) for G, H, u in us
                                                 if (G, H) != (0, 0)])
                        good.append(any(u >= -1e-9 for _G, _H, u in us))
                        goodr.append(any(u >= -1e-9 for _G, _H, u in
                                         tentative(g, st, Zr, False)))
                    cell_off |= safe_within(g, good) != g.W
                    cell_ctrl |= safe_within(g, goodr) != g.W
                    compared += 1
                    kept += len(g.W) > 0
                    del g
                off += cell_off
                ctrl_off += cell_ctrl
    cells = len(grid)
    print(f"    {compared} winning sets compared over {cells} cells, every "
          f"c to c_int (to LOOKCAP where none), {kept} non-empty")
    print(f"    cells off: {off} of {cells}; control (the real side's "
          f"ratio for zeta'): {ctrl_off} of {cells} off")
    print(f"    flushed states without a u~ = 0 branch: {zero_bad}; least "
          f"|u~| over branches of tentative pair not (0, 0): {margin:.3e}")
    check("W_int is the safety game's set on the states with a branch of "
          "u~ >= 0, at every cell and c", off == 0)
    check("every flushed state has a branch with u~ = 0; the float margin "
          "above 1e-7", zero_bad == 0 and margin > 1e-7)
    check("control: the real-side ratio moves the set at some cell",
          ctrl_off > 0)


# ------------------------------------------------------------ P8 the cone

class Cone:
    """Argument (3)'s reader as an integer reader of n -> m n + omega at
    lookahead c, windows and caps at slack (s, s0): the owed integer N
    and its star kept exactly (numerators over Q), its cone coordinates
    N = K q_(t+1) + L q_t read off them at every step. With seam, at
    the (0, 0) windows, a target J_0 holding its lift's seam -1 is read
    by (11)'s two moves, e_0 = 0 and e_1 = a_2 + 1, so the output lies
    under the (1, 0) caps by construction."""

    def __init__(self, w, m, s, s0, c, depth, seam=False):
        self.w, self.m, self.c, self.depth = w, m, c, depth
        self.seam_rule = seam
        top = depth + c + 60
        self.th = [w.q(k) * w.P - w.p(k) * w.Q for k in range(-1, top + 2)]
        self.cap = [w.a[1] - 1 + s0] + [w.a[k + 1] + s
                                        for k in range(1, top + 1)]
        lo = hi = 0
        self.T = [None] * (depth + 2)
        for k in range(top - 1, -1, -1):
            v = self.cap[k] * self.t(k)
            lo, hi = (lo + v, hi) if v < 0 else (lo, hi + v)
            if k < depth + 2:
                self.T[k] = (lo, hi)

    def t(self, k):
        return self.th[k + 1]

    def interval(self, j):
        a, b = -self.t(j), -self.t(j - 1)
        return min(a, b), max(a, b)

    def coords(self, t, N, sig):
        w = self.w
        X = (N * w.P - sig) // w.Q          # K p_(t+1) + L p_t, exactly
        D = w.q(t + 1) * w.p(t) - w.q(t) * w.p(t + 1)
        return ((N * w.p(t) - w.q(t) * X) // D,
                (w.q(t + 1) * X - w.p(t + 1) * N) // D)

    def read(self, d, omega, pick):
        """(ok, why, steps with K < 0 or L < 0): the least lift K_0, then
        the least or greatest member holding J_t, until N = 0 with the
        input absorbed and eight zero digits after; self.seam says
        whether the seam's moves were taken."""
        w, m, c, Q = self.w, self.m, self.c, self.w.Q
        n = sum(x * w.q(k) for k, x in enumerate(d))
        d = list(d) + [0] * (self.depth + c + 2)
        N = m * sum(d[k] * w.q(k) for k in range(c + 1)) + omega
        ilo, ihi = self.interval(c + 1)
        lo, hi = self.T[0]
        K0 = -((hi - N * w.P - m * ihi) // Q)
        sig = N * w.P - K0 * Q              # the star N alpha - K_0
        self.neg_at, self.K0 = None, K0
        self.seam = self.seam_rule and sig + m * ilo < lo
        if sig + m * (ihi if self.seam else ilo) < lo:
            return False, "no lift", 0
        out, neg, done = [], 0, None
        for t in range(self.depth):
            K, L = self.coords(t, N, sig)
            if (K < 0 or L < 0) and self.neg_at is None:
                self.neg_at = t
            neg += K < 0 or L < 0
            if done is None and N == 0 and sig == 0 \
                    and not any(d[t + c + 1:]):
                done = t
            if done is not None and t >= done + 8:
                break
            u = self.t(t)
            if self.seam and t < 2:
                e = 0 if t == 0 else w.a[2] + 1
            else:
                ilo, ihi = self.interval(t + c + 1)
                jlo, jhi = sig + m * ilo, sig + m * ihi
                tl, th = self.T[t + 1]
                if u > 0:
                    elo, ehi = -((th - jhi) // u), (jlo - tl) // u
                else:
                    elo, ehi = -((jlo - tl) // -u), (th - jhi) // -u
                elo, ehi = max(elo, 0), min(ehi, self.cap[t])
                if elo > ehi:
                    return False, f"no member at t = {t}", neg
                e = elo if pick == "least" else ehi
            out.append(e)
            N, sig = N - e * w.q(t), sig - e * u
            dd = d[t + c + 1]
            N, sig = N + m * dd * w.q(t + c + 1), sig + m * dd * self.t(t + c + 1)
        val = sum(e * w.q(k) for k, e in enumerate(out))
        if done is None or any(out[done:]) or val != m * n + omega:
            return False, "not ended" if done is None else "value", neg
        return True, "", neg


def cone_inputs(w, rnd):
    count, length = (100, 60) if FULL else (20, 40)
    quots = w.a[1:]
    return ([w.digits(n) for n in range(N_CHECK)]
            + [legal_random(rnd, quots, length) for _ in range(count)])


def cone_cell(w, m, s, s0, c, ins, omegas, picks, breaks=None, seam=False,
              whys=None):
    """(failures, negative-coordinate steps, the first failure, seam
    reads); breaks, if given, tallies the reads whose first negative
    step is the lift's (t = 0) or a member's, whys every failure's
    reason."""
    rd = Cone(w, m, s, s0, c, 110, seam)
    bad = neg = seams = 0
    first = None
    for omega in omegas:
        for pick in picks:
            for d in ins:
                ok, why, ng = rd.read(d, omega, pick)
                neg += ng
                seams += rd.seam
                if breaks is not None and rd.neg_at is not None:
                    breaks["lift" if rd.neg_at == 0 else "member"] += 1
                if not ok:
                    bad += 1
                    first = first or why
                    if whys is not None:
                        whys[why] = whys.get(why, 0) + 1
    return bad, neg, first, seams


def c_seam(w, m, strict, depth=110):
    """The least c with w_0 < |theta_2| (strict) or w_0 <= |theta_1|,
    and w_t <= |theta_(t+1)| at 1 <= t < depth: the seam reader's bars
    of (11), or with its own bar loosened to the s = 0 one."""
    def th(k):
        return abs(w.q(k) * w.P - w.p(k) * w.Q)

    def wid(t, c):
        return m * (th(t + c) + th(t + c + 1))
    for c in range(20):
        ok0 = wid(0, c) < th(2) if strict else wid(0, c) <= th(1)
        if ok0 and all(wid(t, c) <= th(t + 1) for t in range(1, depth)):
            return c
    return None


def section_cone(grid):
    print("== P8 the overlap reader at the s = 0 windows is an integer reader")
    rnd = random.Random(SEED + 2)
    names = sorted({k[0] for k in grid}, key=[n for n, _ in PERIODIC].index)
    alist = [(n, numeration(n, p)) for n, p in PERIODIC if n in names]
    alist.append(("e - 2", Numeration("e - 2", e_minus_2(200))))
    if FULL:
        alist.append(("random {1, 2, 3}", Numeration("random {1, 2, 3}", [
            rnd.choice((1, 2, 3)) for _ in range(200)])))
    known = known_pass = over = above = equal = cells = 0
    fails = negs = ctrl_fail = ctrl_neg = 0
    lift_cells = member_cells = zero_cells = only_zero = zero_k0 = 0
    sk = sk_pass = s_over = s_above = s_fail = s_neg = s_never = 0
    pl_cells = pl_bites = 0
    pl_whys = {}
    for name, w in alist:
        ins = cone_inputs(w, rnd)
        row, seam_row = [], []
        for m in maps():
            cells += 1
            c0 = c_overlap(Metric(w, 0, 1, 170), m, 110)
            over += c0 > 2 * (m - 1).bit_length() + 2
            c_int = grid.get((name, m, 0, 1), (None, None))[1]
            if c_int is not None:
                above += c_int > c0
                equal += c_int == c0
                if c_int >= 1:
                    known += 1
                    known_pass += cone_cell(w, m, 0, 1, c_int - 1, ins, (0,),
                                            ("least",))[0] == 0
            for c in range(c0, c0 + (3 if FULL else 1)):
                bad, neg, first, _ = cone_cell(w, m, 0, 1, c, ins, (0, m),
                                            ("least", "greatest"))
                fails += bad
                negs += neg
                if bad or neg:
                    print(f"    FAIL {name} x{m} c {c}: {bad} bad, {neg} "
                          f"negative steps, first {first}")
            br = {"lift": 0, "member": 0}
            bad, neg, first, _ = cone_cell(w, m, 1, 1, c0, ins, (0,),
                                        ("least",), br)
            ctrl_fail += bad > 0
            ctrl_neg += neg > 0
            rz = Cone(w, m, 1, 1, c0, 110)
            zero_bad = not rz.read(ins[0], 0, "least")[0]
            zero_cells += zero_bad
            only_zero += zero_bad and bad == 1
            zero_k0 += zero_bad and rz.K0 == -1
            lift_cells += br["lift"] > 0
            member_cells += br["member"] > 0
            row.append(f"x{m} c_ov {c0} c_int {_fmt(c_int)} | (1, 1): "
                       f"{bad} bad, breaks lift {br['lift']} member "
                       f"{br['member']}")
            csr, cpl = c_seam(w, m, True), c_seam(w, m, False)
            s_over += csr > 2 * (m - 1).bit_length() + 3
            ci = grid.get((name, m, 1, 0), (None, None))[1]
            if ci is not None:
                s_above += ci > csr
                if ci >= 1:
                    sk += 1
                    sk_pass += cone_cell(w, m, 0, 0, ci - 1, ins, (0,),
                                         ("least",), seam=True)[0] == 0
            taken = 0
            for c in range(csr, csr + (2 if FULL else 1)):
                bad, neg, first, seams = cone_cell(
                    w, m, 0, 0, c, ins, (0, m), ("least", "greatest"),
                    seam=True)
                s_fail += bad
                s_neg += neg
                taken += seams
                if bad or neg:
                    print(f"    SEAM FAIL {name} x{m} c {c}: {bad} bad, "
                          f"{neg} negative steps, first {first}")
            s_never += taken == 0
            seam_row.append(f"x{m} c_sr {csr} c_int(1, 0) {_fmt(ci)} seam "
                            f"{taken}")
            if cpl < csr:
                pl_cells += 1
                pl_bites += cone_cell(w, m, 0, 0, cpl, ins, (0,), ("least",),
                                      seam=True, whys=pl_whys)[0] > 0
        print(f"    {name:20s} " + "; ".join(row))
        print(f"    {'':20s} seam: " + "; ".join(seam_row))
    print(f"    known answer: the reader at c_int - 1 passes at {known_pass} "
          f"of {known} cells")
    print(f"    failures at c >= c_ov(0, 1): {fails}; steps with K < 0 or "
          f"L < 0: {negs}")
    print(f"    c_ov(0, 1) above 2 ceil(log2 m) + 2: {over} of {cells}; "
          f"c_int above c_ov(0, 1): {above}, equal at {equal}")
    print(f"    control, the (1, 1) windows at c_ov(0, 1): fails at "
          f"{ctrl_fail}, a negative coordinate at {ctrl_neg} (by the lift at "
          f"{lift_cells}, by a member at {member_cells}), of {cells} cells; "
          f"n = 0 fails at {zero_cells}, alone at {only_zero}, its lift "
          f"K_0 = -1 at {zero_k0}")
    check("known answer: the reader at c_int - 1 fails at every cell",
          known_pass == 0 and known > 0)
    check("the overlap reader at the (0, 1) windows reads every input and "
          "keeps K, L >= 0", fails == 0 and negs == 0)
    check("c_ov(0, 1) <= 2 ceil(log2 m) + 2 and c_int <= c_ov(0, 1)",
          over == 0 and above == 0)
    check("control: the (1, 1) windows at c_ov(0, 1) fail at some cell",
          ctrl_fail > 0)
    print(f"    seam, known answer: the seam reader at c_int(1, 0) - 1 "
          f"passes at {sk_pass} of {sk} cells")
    print(f"    seam failures at c >= c_sr: {s_fail}; steps with K < 0 or "
          f"L < 0: {s_neg}; cells where the seam is never taken: {s_never} "
          f"of {cells}")
    print(f"    c_sr above 2 ceil(log2 m) + 3: {s_over} of {cells}; "
          f"c_int(1, 0) above c_sr: {s_above}")
    print(f"    plant, the seam's bar loosened to w_0 <= |theta_1|: c_pl < "
          f"c_sr at {pl_cells} cells, fails at {pl_bites}, its failures "
          f"{dict(sorted(pl_whys.items()))}")
    check("seam known answer: the seam reader at c_int(1, 0) - 1 fails at "
          "every cell", sk_pass == 0 and sk > 0)
    check("the seam reader at (1, 0) reads every input, keeps K, L >= 0 and "
          "takes the seam at every cell",
          s_fail == 0 and s_neg == 0 and s_never == 0)
    check("c_sr <= 2 ceil(log2 m) + 3 and c_int(1, 0) <= c_sr",
          s_over == 0 and s_above == 0)
    check("plant: the seam reader at the loosened bar fails at some cell",
          pl_bites > 0)


# ------------------------------------------------------------ P9 the cylinder

def c_floor(met, m, depth, bar="T", above=True):
    """The least c with w_t <= the bar at every t < depth with |T_(t+1)|
    < 1, read from above unless above is False: bar "T" is (12)'s
    |T_(t+1)|, "ov" c_ov's ov_t (too strict, a plant), "up" the level
    above's |T_t| (too lax, a plant)."""
    ts = [t for t in range(depth) if met.Tlen(t + 1, above) < met.Q]
    bars = [met.ov(t, above) if bar == "ov" else
            met.Tlen(t if bar == "up" else t + 1, above) for t in ts]
    for c in range(41):
        if all(met.width(t, c, m) <= b for t, b in zip(ts, bars)):
            return c
    return None


def _tally(xs):
    return ", ".join(f"{g}: {xs.count(g)}" for g in sorted(set(xs)))


def section_cylinder(grid, cov):
    print("== P9 the cylinder bound c_lo: below c_saf and c_int, c_ov "
          "within max(2, t_1)")
    over = [0, 0]

    def t_one(met, depth, gap):
        t1 = next(t for t in range(depth) if met.Tlen(t + 1, True) < met.Q)
        over[0] += gap > max(2, t1)
        over[1] += t1 > max(1, 2 * (2 * met.s).bit_length())
        return t1

    phi = (1 + 5 ** 0.5) / 2
    w = numeration("golden [1]", (1,))
    off = 0
    for m in range(2, 10):
        for s, s0 in SLACKS[1:]:
            met = Metric(w, s, s0, 120)
            lo = next(c for c in range(40) if m * phi ** -c <= 1 + s + 1e-12)
            ov = next(c for c in range(40) if m * phi ** -c
                      <= s + min(phi ** -2, s0 / phi) + 1e-12)
            off += (c_floor(met, m, 60), c_overlap(met, m, 60)) != (lo, ov)
    check("control: c_lo and c_ov at golden x 2 .. x 9 equal their closed "
          "forms", off == 0, f"{off} of 40 off")

    x_saf = x_int = strict_over = ties = tie_const = moved = reads = 0
    zero_off = 0
    gaps, below, at_s0, up_gold = [], [], [], []
    for name, per in PERIODIC:
        if (name, 2, 0, 1) not in grid:
            continue
        w = numeration(name, per)
        for m in maps():
            for s, s0 in SLACKS[1:]:
                met = Metric(w, s, s0, 120)
                lo = c_floor(met, m, 60)
                tie = c_floor(met, m, 60, above=False) != lo
                ties += tie
                tie_const += tie and len(per) == 1 and s == (m - 1) * per[0]
                c_ov = cov[(name, m, s, s0)]
                moved += c_overlap(met, m, 60, above=True) != c_ov
                reads += 1
                c_saf, c_int = grid[(name, m, s, s0)]
                x_saf += c_saf is not None and lo > c_saf
                x_int += c_int is not None and lo > c_int
                strict_over += c_saf is not None and \
                    c_floor(met, m, 60, "ov") > c_saf
                if name.startswith("golden") and s == 0:
                    up_gold.append(c_ov - c_floor(met, m, 60, "up"))
                gaps.append(c_ov - lo)
                t_one(met, 60, c_ov - lo)
                if c_saf is not None:
                    below.append(c_saf - lo)
                    zero_off += (lo == 0) != (c_saf == 0)
                if s == 0 and c_int is not None:
                    at_s0.append(c_int - lo)
    print(f"    controls: the bar ov_t puts c_lo above c_saf at {strict_over} "
          f"cells; the bar |T_t| at golden s = 0 gives gaps {up_gold}")
    print(f"    ties (a bar met exactly, missed when summed to top): {ties} "
          f"cells, at s = (m - 1)a, a the constant quotient: {tie_const}")
    print(f"    c_lo > c_saf at {x_saf} cells, c_lo > c_int at {x_int}")
    print(f"    c_ov - c_lo over the grid: {_tally(gaps)}")
    print(f"    c_saf - c_lo: {_tally(below)}; c_lo = 0 and c_saf = 0 "
          f"disagree at {zero_off} cells")
    print(f"    c_int - c_lo at s = 0: {_tally(at_s0)}")
    check("control: the bar ov_t, too strict, puts c_lo above c_saf at some "
          "cell", strict_over > 0)
    check("control: the bar |T_t|, too lax, gives a gap of 3 at golden s = 0",
          3 in up_gold)
    check("c_lo <= c_saf and c_lo <= c_int at every finite grid cell",
          x_saf + x_int == 0)
    check("0 <= c_ov - c_lo <= 2 at every grid cell",
          min(gaps) >= 0 and max(gaps) <= 2)

    rnd = random.Random(SEED + 2)
    rq = [rnd.choice((1, 2, 3)) for _ in range(200)]    # P8's random alpha
    far = 0
    for name, w in (("e - 2", Numeration("e - 2", e_minus_2(200))),
                    ("random {1, 2, 3}", Numeration("random {1, 2, 3}", rq))):
        short = all(Metric(w, s, s0, 170).Tlen(3, True) < w.Q
                    for s, s0 in SLACKS[1:])
        g = []
        for m in maps():
            for s, s0 in SLACKS[1:]:
                met = Metric(w, s, s0, 170)
                c_ov = c_overlap(met, m, 110)
                moved += c_overlap(met, m, 110, above=True) != c_ov
                reads += 1
                g.append(c_ov - c_floor(met, m, 110))
                t_one(met, 110, g[-1])
        print(f"    {name}: |T_3| < 1 at every slack: {'yes' if short else 'no'}"
              f"; c_ov - c_lo {min(g)} to {max(g)}")
        far += not short or min(g) < 0 or max(g) > 2
    check("e - 2 and the random alpha: |T_3| < 1, 0 <= c_ov - c_lo <= 2",
          far == 0)

    H, meets = 10 ** 8, 0
    for N in range(2, 8):
        w = Numeration(f"fam{N}", [1] * (N + 1) + [H] * 60)
        s = next(s for s in range(1, 10 ** 4)
                 if Metric(w, s, 0, N + 50).Tlen(N) >= w.Q)
        best = None
        for e in range(1, 13):
            met = Metric(w, s, 1, N + 50)
            lo, ov = c_floor(met, 2 ** e, N + 40), \
                c_overlap(met, 2 ** e, N + 40, 40)
            moved += c_overlap(met, 2 ** e, N + 40, 40, True) != ov
            reads += 1
            t1 = t_one(met, N + 40, ov - lo)
            if best is None or ov - lo > best[0]:
                best = (ov - lo, 2 ** e, lo, ov)
        meets += best[0] == max(2, t1)
        print(f"    family N {N}: s {s}, t_1 {t1}; largest c_ov - c_lo "
              f"{best[0]} at x{best[1]} (c_lo {best[2]}, c_ov {best[3]})")
    print(f"    gap above max(2, t_1): {over[0]}; t_1 above max(1, 2 "
          f"ceil(log2(2s + 1))): {over[1]}; c_ov with its bars read from "
          f"above moves at {moved} of {reads} cells")
    check("c_ov - c_lo <= max(2, t_1), t_1 <= max(1, 2 ceil(log2(2s + 1))), "
          "at every cell read", over == [0, 0])
    check("the family [1 x (N + 1), 10^8, ...] meets max(2, t_1) at N = "
          "2 .. 7", meets == 6)
    check("c_ov's bars read from above move no c_ov at any cell read",
          moved == 0)


# ------------------------------------------------------------ P9(b) the pin

NPIN = 20000


def _hull(x, y):
    return (min(x, y), max(x, y))


def _inside(a, b):
    return b[0] <= a[0] and a[1] <= b[1]


def zero_cyl(met, L):
    """I_L, the stars of the inputs with d_0 .. d_(L-1) all 0."""
    return _hull(-met.theta(L), -met.theta(L - 1))


def sub_cyls(met, j):
    """I_j split by the digit d_j: C_0 = I_(j+1), then C_1 .. C_a."""
    th, th1 = met.theta(j), met.theta(j + 1)
    return [_hull(-th1, -th)] + [_hull((d - 1) * th - th1, d * th - th1)
                                 for d in range(1, met.a[j + 1] + 1)]


def members(met, L):
    lo, hi = zero_cyl(met, L + 1)
    return [(lo + e * met.theta(L), hi + e * met.theta(L))
            for e in range(met.cap(L) + 1)]


def pin_levels(met, depth):
    return [t for t in range(depth)
            if abs(met.theta(t)) + abs(met.theta(t + 1)) < met.Q]


def pin_bar(met, m, c, t, two):
    """Z(c) at level t, s = 0: m I_j inside I_(t+1), j = t + c + 1 (one
    level), and with two, each m C_d inside one member of T_(t+1)."""
    j = t + c + 1
    if not _inside((m * zero_cyl(met, j)[0], m * zero_cyl(met, j)[1]),
                   zero_cyl(met, t + 1)):
        return False
    mem = members(met, t + 1) if two else []
    return all(any(_inside((m * p[0], m * p[1]), q) for q in mem)
               for p in (sub_cyls(met, j) if two else []))


def c_lo2(met, m, two=True, depth=60, least_pass=False):
    """1 + the largest c below 30 at which Z(c) fails at some level read
    (Z(c) holds at every c from 30 on); with least_pass, the least c at
    which it holds."""
    ts = pin_levels(met, depth)
    ok = [all(pin_bar(met, m, c, t, two) for t in ts) for c in range(30)]
    assert ok[-1]
    return ok.index(True) if least_pass else \
        1 + max(c for c in range(30) if not ok[c])


def pinning(w, met):
    """The first level t at which some N != 0 below q_(t+1) + q_t has a
    K - N alpha strictly inside I_(t+1), or None; and the levels read."""
    read = 0
    for t in pin_levels(met, 60):
        top = w.q(t + 1) + w.q(t)
        if top > NPIN:
            break
        lo, hi = zero_cyl(met, t + 1)
        read += 1
        for N in range(1, top):
            base = (N * w.P) // w.Q
            if any(lo < K * w.Q - N * w.P < hi
                   for K in (base - 1, base, base + 1, base + 2)):
                return t, read
    return None, read


def section_pinned(grid):
    print("== P9(b) the pinned zero cylinder at (s, s_0) = (0, 1): c_lo2 "
          "between c_lo and c_saf")
    off = 0
    for name, per in PERIODIC:
        met = Metric(numeration(name, per), 0, 1, 120)
        for j in range(1, 90):
            ps = sorted(sub_cyls(met, j))
            off += (ps[0][0], ps[-1][1]) != zero_cyl(met, j)
            off += any(a[1] != b[0] for a, b in zip(ps, ps[1:]))
            ms = members(met, j)
            off += (min(q[0] for q in ms), max(q[1] for q in ms)) \
                != zero_cyl(met, j)
    check("control: the sub-cylinders tile I_j and the members' hull is "
          "I_L at j, L < 90", off == 0, f"{off} faults over the six alpha")
    phi = (1 + 5 ** 0.5) / 2
    gmet = Metric(numeration("golden [1]", (1,)), 0, 1, 120)
    got = [c_lo2(gmet, m) for m in range(2, 10)]
    lo = [next(c for c in range(40) if m * phi ** -c <= 1 + 1e-12)
          for m in range(2, 10)]
    check("control: golden x 2 .. x 9, c_lo2 is c_lo rounded up to even",
          got == [c + c % 2 for c in lo], f"{got}")
    smet = Metric(numeration("silver [2]", (2,)), 0, 1, 120)
    one, two = c_lo2(smet, 4, False), c_lo2(smet, 4)
    check("control: silver x 4, the seam bar lifts the one-level bar 2 to 3",
          (one, two) == (2, 3), f"one level {one}, two levels {two}")

    alone, mono = [], 0
    for name, per in PERIODIC:
        w = numeration(name, per)
        met = Metric(w, 0, 1, 120)
        bad, read = pinning(w, met)
        alone.append(read if bad is None else f"another N at t = {bad}")
        mono += sum(c_lo2(met, m) != c_lo2(met, m, least_pass=True)
                    for m in range(2, 10))
    print(f"    pinning, the levels with q_(t+1) + q_t <= {NPIN} read: "
          f"{alone}")
    check("pinning: N = 0 alone at every level read, at the six alpha",
          all(isinstance(r, int) for r in alone))
    check("Z(c) fails below c_lo2 and holds from it, x 2 .. x 9 at the six "
          "alpha", mono == 0, f"{mono} of 48 differ")

    x_lo = x_saf = x_int = x_gap = 0
    gaps, moves, lifted, flat = [], [], [], []
    for name, per in PERIODIC:
        if (name, 2, 0, 1) not in grid:
            continue
        met = Metric(numeration(name, per), 0, 1, 120)
        row = []
        for m in maps():
            lo, par, two = c_floor(met, m, 60), c_lo2(met, m, False), \
                c_lo2(met, m)
            c_saf, c_int = grid[(name, m, 0, 1)]
            x_lo += lo > two
            x_saf += two > c_saf
            x_int += c_saf > c_int
            gaps.append(c_int - two)
            if two > lo:
                lifted.append(c_int - two)
                x_gap += c_int - two > 1
            else:
                flat.append(c_int - two)
            if two != par:
                moves.append(f"{name.split()[0]} x{m}")
            row.append(f"x{m} {lo}/{par}/{two}/{c_saf}/{c_int}")
        print(f"    {name:20s} " + "  ".join(row))
    print(f"    (c_lo / one level / c_lo2 / c_saf / c_int) c_int - c_lo2: "
          f"{_tally(gaps)}; where c_lo2 > c_lo: {_tally(lifted)}; where "
          f"c_lo2 = c_lo: {_tally(flat)}; the seam bar moves c_lo2 at "
          f"{moves or 'none'}")
    check("c_lo <= c_lo2 <= c_saf <= c_int at every grid cell at (0, 1)",
          x_lo + x_saf + x_int == 0, f"{x_lo}, {x_saf}, {x_int} off")
    check("c_int - c_lo2 <= 1 wherever c_lo2 > c_lo", x_gap == 0)

    rnd = random.Random(SEED + 2)
    rq = [rnd.choice((1, 2, 3)) for _ in range(200)]    # P8's random alpha
    far = 0
    for name, w in (("e - 2", Numeration("e - 2", e_minus_2(200))),
                    ("random {1, 2, 3}", Numeration("random {1, 2, 3}", rq))):
        met = Metric(w, 0, 1, 170)
        row = []
        for m in maps():
            lo, two = c_floor(met, m, 110), c_lo2(met, m, depth=110)
            ov = c_overlap(met, m, 110)
            far += not lo <= two <= ov
            row.append(f"x{m} {lo}/{two}/{ov}")
        print(f"    {name:20s} c_lo/c_lo2/c_ov, depth 110  " + "  ".join(row))
    check("e - 2 and the random alpha: c_lo <= c_lo2 <= c_ov(0, 1)", far == 0)


# ------------------------------------------------------------ P9(c) the limit

def subtree_ok(met, m, c, t, L, plant=False):
    """The pinned subtree at level t, lookahead c, read L levels: the
    target m X_i inside the committed window W_i at i = 0 .. L - 1, the
    opponent's digit d_(j+i-1) then the reader's e_(t+i) at i >= 1.
    plant reads R' as d theta + I_(K+1)."""
    j = t + c + 1
    x0 = zero_cyl(met, j)
    if not _inside((m * x0[0], m * x0[1]), zero_cyl(met, t + 1)):
        return False
    if L == 1:
        return True
    memo = {}

    def win(i, rel, prevzero):
        # rel = m (sum d theta) - (sum e theta): the target's offset
        # against the window's
        key = (i, rel, prevzero)
        if key in memo:
            return memo[key]
        K = j + i - 1
        thK, thK1 = met.theta(K), met.theta(K + 1)
        top = met.a[K + 1] if prevzero else met.a[K + 1] - 1
        ok = True
        for d in range(top + 1):
            r = zero_cyl(met, K + 1) if d == 0 or plant else \
                _hull(-thK1, -thK - thK1)
            base = rel + m * d * thK
            lv = t + i
            win_lv = zero_cyl(met, lv + 1)
            if not any(_inside((base + m * r[0] - e * met.theta(lv),
                                base + m * r[1] - e * met.theta(lv)), win_lv)
                       and (i == L - 1 or win(i + 1, base - e * met.theta(lv),
                                              d == 0))
                       for e in range(met.cap(lv) + 1)):
                ok = False
                break
        memo[key] = ok
        return ok

    return win(1, 0, True)


def c_level(met, m, L, ts, top, plant=False):
    """1 + the largest c below top at which the L-level subtree fails at
    some level of ts, and whether it passes at top - 1."""
    ok = [all(subtree_ok(met, m, c, t, L, plant) for t in ts)
          for c in range(top)]
    return 1 + max([c for c in range(top) if not ok[c]], default=-1), ok[-1]


class PinGame(Game):
    """The game built from the pinned states P_t alone: the branch (0,
    0), the quotients a_(t+1) .. a_(t+c+1), the pending digits all 0."""

    def __init__(self, src, m, look, ts):
        self.ts = ts
        super().__init__(src, m, 0, 1, look)

    def initial(self):
        per, c = self.src.period, self.look
        p = len(per)
        return [((self.pack(0, 0),),
                 tuple(per[(k - 1) % p] for k in range(t + 1, t + c + 2)),
                 (t + c + 1) % p, (0,) * c, True, t == 0, True)
                for t in self.ts]


def section_pinlimit(grid):
    print("== P9(c) the pinned limit at (0, 1): c_L, c_inf and c_zero "
          "against c_saf")
    LMAX = 14 if FULL else 10
    wide = (6, 7, 8, 9) if FULL else ()
    cells = k1 = k2 = ctl1 = ctl2 = sand = nsand = movebad = 0
    gridoff = ngrid = planted = plim = nplim = hit = lose_all = 0
    stops = []
    for name, per in PERIODIC:
        met = Metric(numeration(name, per), 0, 1, 120)
        p = len(per)
        # the normalized geometry repeats with the period: two periods read
        ts = [t for t in pin_levels(met, 24) if 1 <= t <= 2 * p]
        src = Source(period=per)
        row = []
        for m in maps() + wide:
            zvec = pvec = ""
            saf = losing = None
            for c in range(13):
                g = Game(src, m, 0, 1, c)
                g.solve(False)
                zi = g.start_state([0] * (c + 2),
                                   [per[k % p] for k in range(c + 2)])
                zvec += "T" if zi in g.W else "F"
                wins = g.wins
                lost = sum(i not in g.W for i in g.init)
                total = len(g.init)
                del g
                pg = PinGame(src, m, c, list(range(1, 2 * p + 1)))
                pg.solve(False)
                pvec += "T" if all(i in pg.W for i in pg.init) else "F"
                if wins:
                    movebad += sum(
                        [e for e, (_nz, succ) in pg.trans[i].items()
                         if all(j in pg.W for j in succ)] != [0]
                        for i in pg.init)
                    del pg
                    saf = c
                    break
                del pg
                losing = (lost, total)
            cells += 1
            if (name, m, 0, 1) in grid:
                ngrid += 1
                gridoff += saf != grid[(name, m, 0, 1)][0]
            one, two = c_lo2(met, m, False), c_lo2(met, m)
            got = [c_level(met, m, L, ts, saf + 2) for L in range(1, LMAX + 1)]
            cs = [x for x, _ok in got]
            ctl1 += cs[0] != one
            ctl2 += cs[1] != two
            planted += c_level(met, m, 2, ts, 30, plant=True)[0] != two
            pin = 1 + max([c for c, v in enumerate(pvec) if v == "F"],
                          default=-1)
            if m in maps():
                nplim += 1
                plim += c_level(met, m, LMAX, ts, saf + 2,
                                plant=True)[0] != pin
            lim = cs[-1]
            stops.append(cs.index(lim) + 1)
            zero = 1 + max([c for c, v in enumerate(zvec) if v == "F"],
                           default=-1)
            k1 += (not all(ok for _x, ok in got) or max(cs) > saf
                   or pin > saf)
            k2 += (lim != pin) + (zero != pin)
            if two == saf:
                nsand += 1
                sand += pin != saf
            hit += pin == saf
            lose_all += losing is not None and losing[0] == losing[1]
            row.append(f"x{m} {lim}/{pin}/{saf}")
        print(f"    {name:20s} " + "  ".join(row))
    print(f"    (lim c_L / c_inf / c_saf) c_L stops at L = {sorted(set(stops))}"
          f" of {LMAX}; c_inf = c_saf at {hit} of {cells} cells; at c_saf - 1 "
          f"every pre-read loses at {lose_all} of {cells}")
    check("control: c_saf read here equals the grid's at (0, 1)",
          gridoff == 0, f"{gridoff} of {ngrid} off")
    check("control: L = 1 is the one-level bar and L = 2 is c_lo2",
          ctl1 + ctl2 == 0, f"{ctl1}, {ctl2} of {cells} off")
    check("control: c_inf = c_saf where c_lo2 = c_saf", sand == 0,
          f"{sand} of {nsand} off")
    check("control: at c_saf the pinned states' only winning move is 0",
          movebad == 0, f"{movebad} states")
    check("plant: R' read as d theta + I_(K+1) moves the L = 2 control "
          "and the limit off c_inf", planted > 0 and plim > 0,
          f"at {planted} of {cells} cells and {plim} of {nplim}")
    check("K1: c_L and c_inf at most c_saf", k1 == 0, f"{k1} cells")
    check("K2: lim c_L and c_zero equal c_inf", k2 == 0,
          f"{k2} disagreements")


# ------------------------------------------------------------ P6

def section_universal(grid):
    print("== P6 the universal reader")
    rnd = random.Random(SEED + 1)
    pins = []
    cells = [((1, 2), 2, 1, 1, 2)]
    if FULL:
        cells += [((1, 2, 3), 2, 1, 1, 2), ((1, 2), 3, 1, 1, 3),
                  ((1, 2), 3, 2, 2, 2)]
    for alph, m, s, s0, want in cells:
        src = Source(alphabet=alph)
        t0 = time.time()
        c, g = least(src, m, s, s0, True, hi=want)
        tag = "{" + ", ".join(map(str, alph)) + "}"
        print(f"    {tag:10s} x{m} ({s},{s0}): c_int {c}  states "
              f"{len(g.states) if g else '-'}  ({time.time() - t0:.0f} s)")
        check(f"{tag} x{m} at ({s}, {s0}) reads at exactly {want}",
              c == want)
        if c == 2:
            for name, per in PERIODIC:
                cell = grid.get((name, m, s, s0))
                if cell and set(per) <= set(alph) and (m - 1) * max(per) > s:
                    pins.append((name, m, s, s0, cell[1]))
        if g is None:
            continue
        alphas = [[a] * 400 for a in alph]
        alphas += [[rnd.choice(alph) for _ in range(400)] for _ in range(12)]
        bad = 0
        for quots in alphas:
            w = Numeration("class member", quots)
            bad += certify(g, w, m, s, s0, N_CHECK // 2)
        check(f"certified at {len(alphas)} members", bad == 0, f"{bad} bad")
        if (alph, m) == ((1, 2), 2):
            g2 = Game(src, m, s, s0, want, scale=2)
            won = g2.solve(True)
            mx = my = 0
            unflushed = seeds = 0
            for quots in alphas[:6]:       # the two constant alphas, four random
                w = Numeration("class member", quots)
                for n in range(N_CHECK // 4):
                    out, fl, path = g2.read(w.digits(n), quots)
                    if not fl:
                        unflushed += 1
                        continue
                    x_, y_, x0 = lineage(g2, path)
                    mx, my = max(mx, x_), max(my, y_)
                    seeds += x0 != m * w.digits(n)[0]
            check("at twice the box the flushing lineages stay in the box",
                  won and mx <= g.bx and my <= g.by and unflushed == seeds == 0,
                  f"largest |g|, |h| = {mx}, {my} against ({g.bx}, {g.by}), "
                  f"6 members, n < {N_CHECK // 4}, {unflushed} unflushed")
            del g2
        del g
    print(f"    the pin, grid alphas of a class won at 2 with a quotient "
          f"above s/(m - 1): {pins}")
    check("the pin: c_int is 2 at each of them",
          pins and all(c == 2 for *_, c in pins))
    if not FULL:
        return
    print("== P6 the periodic members of {1, 2} for x 3 at (1, 1)")
    necks = necklaces((1, 2), 8)
    off = []
    for per in necks:
        c, _g = least(Source(period=per), 3, 1, 1, True, hi=3)
        if c != 2:
            off.append((per, c))
    check("every purely periodic alpha of primitive period <= 8 reads "
          "at 2", not off, f"{len(necks)} alphas (every rotation of "
          f"{len(set(min(tuple(p[i:] + p[:i]) for i in range(len(p))) for p in necks))}"
          f" words), off: {off}")


def necklaces(alph, top):
    out = []
    for P in range(1, top + 1):
        seen = set()
        for k in range(len(alph) ** P):
            word = []
            for _ in range(P):
                k, r = divmod(k, len(alph))
                word.append(alph[r])
            rots = [tuple(word[i:] + word[:i]) for i in range(P)]
            if len(set(rots)) < P or min(rots) in seen:
                continue
            seen.add(min(rots))
            out.extend(rots)
    return out


# ------------------------------------------------------------ main

def main():
    t0 = time.time()
    section_ranges()
    section_controls()
    section_tear()
    cov = section_completion()
    section_floors()
    grid = section_grid(cov)
    section_digitwise()
    section_band()
    section_owed(grid)
    section_cone(grid)
    section_cylinder(grid, cov)
    section_pinned(grid)
    section_pinlimit(grid)
    section_universal(grid)
    n_ok = sum(CHECKS)
    print(f"\n{n_ok} of {len(CHECKS)} checks passed "
          f"({time.time() - t0:.1f} s{', full' if FULL else ''})")
    sys.exit(0 if n_ok == len(CHECKS) else 1)


if __name__ == "__main__":
    main()