gap.py

"""gap.py -- the depths between each rank's band scan and its certificate:
does the champion attain the least height at every one, ranks 5..10?

QUESTION. band.py reads ranks 5..10 to J_hi + 12, J_hi its last failing
depth; bandend.py and dualtail.py make the champion (1 + x)^(r-1)(x - 1)^J
the unique least-height vector at every depth from J_c = 47, 57, 97, 108,
157, 170. Between them stand J = 43..46, 46..56, 71..96, 73..107, 101..156
and 119..169, 183 depths no computation reads. Does the champion attain
h(J + r, J) at each? If so, J_hi(r) and J_ch(r) = J_hi(r) + 1 are settled:
no rank of 5..10 fails past J_hi.

THE ENGINE. band.py's cell: flatten.least_height, band.py's per-rank ph
and the champion's height, the code band.py's scan ran. Its soundness
re-derived at these sizes: enumerate_min's Gram-Schmidt data are Python
int/int divisions, correctly rounded however large (heights near 6e44 at
rank 10, J = 169), so its float error is relative about 1e-14 against
a squared-radius slack of relative 1e-9. The scan runs from J_hi itself,
band.py's last failure, to J_c - 1, so it reads band.py's twelve clean
depths again beside the gap.

PREDICTION (frozen before the engine). PG1 the champion attains h at all
183 gap depths.
KILL. KG a depth J_hi + 1 .. J_c - 1 at a rank where the champion misses
h: J_ch moves past the last one, and J_hi with it where also h < ph.
KB band.py's bugs (a witness of the wrong length or height, not cleared;
h > ph; the champion below h).
CONTROL (positive, read first). At J = J_hi(r) the same code reports
h < ph, the champion missing h, at all six ranks.

FINDINGS.
  (1) The control holds: J_hi fails at ranks 5..10.
  (2) PG1 holds, KG misses, KB 0: the champion attains h at every depth
      J_hi + 1 .. J_c - 1, 255 depths, the 183 of the gap among them.
      With dualtail.py's certificate and tail, at ranks 5..10 the champion
      attains h at every depth past J_hi = 30, 33, 58, 60, 88, 106, and
      no cell of those ranks fails past it.

RUN RECORD. Timed first, one cell per rank at the gap's deep end: 0.00 s
each, 68 nodes at rank 10, J = 169. The scan: 2.5 s, peak 9.2 MB under a
512 MB guard, KB 0.
"""
import os
import sys
import time

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

# bandend.py's FINDINGS (3): the certificate holds from J_c through JMAX
JC = {5: 47, 6: 57, 7: 97, 8: 108, 9: 157, 10: 170}


def gap():
    """band.py's cell at every depth J_hi .. J_c - 1, ranks 5..10: J_hi
    must fail (the control), and the champion attain h past it."""
    out = {}
    kb = 0
    for r in range(5, 11):
        cof = cofactors(r)
        miss, n = [], 0
        h, p, c, b = cell(r, JHI[r], cof)
        kb += b
        ctl = h < p
        for J in range(JHI[r] + 1, JC[r]):
            h, p, c, b = cell(r, J, cof)
            kb += b
            n += 1
            if c != h:
                miss.append((J, h < p))
        out[r] = (ctl, n, miss)
        print("  r = %2d  J_hi = %3d fails: %s; J = %d..%d, %d depths, "
              "of them %d past J_hi + 12; champion misses h at %s"
              % (r, JHI[r], ctl, JHI[r] + 1, JC[r] - 1, n,
                 max(0, JC[r] - JHI[r] - 13), miss), flush=True)
    print("KB %d" % kb)
    return out, kb


def main():
    t0 = time.time()
    gp, kb = gap()
    ctl = all(gp[r][0] for r in gp)
    kg = [r for r in gp if gp[r][2]]
    print("control: J_hi fails at every rank 5..10: %s" % ctl)
    print("PG1/KG ranks with a depth in J_hi + 1..J_c - 1 where the champion "
          "misses h: %s: %s" % (kg, "fires" if kg else "misses"))
    print("%.1f s" % (time.time() - t0))
    return not ctl or kb or kg


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