"""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)