bandgrowth.py

"""bandgrowth.py -- where does the band of failing depths end at ranks
11..14, and does its last failing depth J_hi grow like the square of the
rank?

QUESTION. band.py reads ranks 11..14 only to their first failure, J_lo =
14, 15, 10, 19. At ranks 5..10 the band ends at J_hi = 30, 33, 58, 60,
88, 106, J_hi / r^2 between 0.92 and 1.20. Where does it end at ranks
11..14?

THE ARMS.
  (C) bandend.py's certificate at every depth r - 1 .. JMAX = 500: J_c,
      the least depth from which every depth through JMAX is certified
      (the champion the only minimiser up to sign), and per order s the
      last uncertified depth + 1. Exact, in integers.
  (E) band.py's cell (flatten.least_height, ph_rank, the champion's
      height) at every depth 2 .. J_c - 1: the failures (h < ph), J_hi
      the last, and whether the champion attains h past it.
No tail past JMAX is run, so the reading is "no failure past J_hi through
JMAX", not "at every depth".

BY HAND. A failure is exact: band.py's cell rechecks the witness in
integers (length, height, clears), so a failure printed is proved
whatever the enumeration's floats do. The floats can only hide a failure
(a missed shorter vector reads as the champion attaining h), never invent
one; J_hi is a lower bound from witnesses, its upper side carried by the
enumeration's slack at the clean depths and by (C) past J_c. The float
wall (squared heights near 1e308, J near 510) lies past every J_c read.

PREDICTIONS (frozen before the engine; TRANSPLANTS from the six ranks
5..10, J_hi / r^2 = 1.20, 0.92, 1.18, 0.94, 1.09, 1.06 and J_c / r^2 =
1.88, 1.58, 1.98, 1.69, 1.94, 1.70).
  PH1 the champion attains h at every depth J_hi + 1 .. J_c - 1.
  PH2 J_hi / r^2 in [0.85, 1.30] at each rank 11..14.
  PH3 J_c / r^2 in [1.8, 2.1] at ranks 11, 13 and [1.5, 1.8] at 12, 14;
      every J_c below 400.
  PH4 the certificate's binding order is s = r - 3.
KILLS. K1 a rank whose champion misses h at a depth J_hi + 1 .. J_c - 1.
K2 a rank with J_hi / r^2 outside [0.85, 1.30]. PH3, PH4 read, not gated.
CONTROLS, read first. C1 (E)'s first failures J_lo = 14, 15, 10, 19
(band.py F3). C2 (C) at rank 10 through 500 gives J_c = 170 (bandend.py
FINDINGS (3)). C3 KB, band.py's bug flags, 0. (The cell at J_hi fails
by construction, so it controls nothing.)

RESOURCE NOTE. Timed first, one cell per rank: (E) 0.30 s at rank 14,
J = 300; (C) 0.06 s at rank 14, J = 500. Estimate about 5 minutes.

FINDINGS (copied from the printed output).
  (1) Controls: C1 first failures [14, 15, 10, 19]; C2 J_c = 170 at rank
      10; C3 KB 0.
  (2) J_hi = 122, 152, 168, 195 and J_c = 227, 241, 305, 319 at ranks
      11..14; the champion attains h at every depth J_hi + 1 .. J_c - 1
      (K1 misses), and the certificate holds at every depth J_c .. 500,
      so no cell of ranks 11..14 fails past J_hi through J = 500.
  (3) J_hi / r^2 = 1.008, 1.056, 0.994, 0.995 (PH2 holds, K2 misses);
      J_c / r^2 = 1.876, 1.674, 1.805, 1.628 (PH3 holds, the odd ranks
      above the even); the binding order is s = r - 3 at all four (PH4).
  (4) Unpredicted: near its end the band fails at alternate depths, as
      band.py's F5 already shows at ranks 7, 9, 10 (holes 55, 57; 87;
      105). Rank 13 is clean at 157, 159, ..., 167 and fails at 156,
      158, ..., 168; rank 14 is clean at 190, 192, 194 and fails at 189,
      191, 193, 195. The other holes of ranks 11..14 sit at the band's
      low edge (ranks 11, 12 have none past 29).
  (5) Read: 101, 125, 139, 170 failing depths; holes 8, 13, 20, 7.

RUN RECORD. 135.1 s, peak commit 14.6 MB under a 512 MB guard. Its exit
code is red on C1, C2, C3, K1 or K2.
"""
import os
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
import bandend  # noqa: E402
from band import cell, cofactors  # noqa: E402

RANKS = (11, 12, 13, 14)
JMAX = 500
JLO = {11: 14, 12: 15, 13: 10, 14: 19}  # band.py's F3


def certificate(r):
    bandend.JMAX[r] = JMAX
    jc, by_s, _, _ = bandend.scan(r)
    return jc, by_s


def enumerate_to(r, jc):
    cof = cofactors(r)
    fails, att, kb = [], {}, 0
    for J in range(2, jc):
        h, p, c, b = cell(r, J, cof)
        kb += b
        if h < p:
            fails.append(J)
        att[J] = c == h
    return fails, att, kb


def main():
    t0 = time.time()
    jc10, _ = certificate(10)
    c2 = jc10 == 170
    print("C2 the certificate at rank 10 through %d: J_c = %d (%s)  [%.1f s]"
          % (JMAX, jc10, c2, time.time() - t0), flush=True)
    rows = {}
    kb = 0
    for r in RANKS:
        jc, by_s = certificate(r)
        bind = max(by_s, key=lambda s: by_s[s])
        print("  r = %d  (C) J_c = %d, J_c/r^2 = %.3f; per order s, last "
              "uncertified + 1: %s; binding s = %d = r - %d  [%.1f s]"
              % (r, jc, jc / r ** 2, by_s, bind, r - bind, time.time() - t0),
              flush=True)
        fails, att, b = enumerate_to(r, jc)
        kb += b
        jhi = fails[-1]
        miss = [J for J in range(jhi + 1, jc) if not att[J]]
        holes = [J for J in range(fails[0], jhi + 1) if J not in fails]
        print("  r = %d  (E) J_lo = %d, J_hi = %d, J_hi/r^2 = %.3f, %d "
              "failing depths, %d holes %s; past J_hi through J_c - 1 = %d "
              "the champion misses h at %s  [%.1f s]"
              % (r, fails[0], jhi, jhi / r ** 2, len(fails), len(holes),
                 holes, jc - 1, miss, time.time() - t0), flush=True)
        rows[r] = (jc, bind, fails, jhi, miss, att)
    c1 = all(rows[r][2][0] == JLO[r] for r in RANKS)
    print("C1 first failures %s (%s)" % ([rows[r][2][0] for r in RANKS], c1))
    print("C3 KB %d" % kb)
    k1 = [r for r in RANKS if rows[r][4]]
    k2 = [r for r in RANKS if not 0.85 <= rows[r][3] / r ** 2 <= 1.30]
    ph3 = [r for r in RANKS if not ((1.8 if r % 2 else 1.5) <= rows[r][0] /
                                    r ** 2 <= (2.1 if r % 2 else 1.8)
                                    and rows[r][0] < 400)]
    ph4 = [r for r in RANKS if rows[r][1] != r - 3]
    print("PH1/K1 ranks where the champion misses h past J_hi: %s (K1 %s)"
          % (k1, "fires" if k1 else "misses"))
    print("PH2/K2 ranks with J_hi/r^2 outside [0.85, 1.30]: %s (K2 %s)"
          % (k2, "fires" if k2 else "misses"))
    print("PH3 ranks off their J_c band: %s" % ph3)
    print("PH4 ranks whose binding order is not r - 3: %s" % ph4)
    print("J_hi through %d: %s; J_c: %s"
          % (JMAX, [rows[r][3] for r in RANKS], [rows[r][0] for r in RANKS]))
    print("%.1f s" % (time.time() - t0))
    return not (c1 and c2) or kb or k1 or k2


if __name__ == "__main__":
    sys.exit(1 if main() else 0)