"""dambar.py -- the dam read at the prime powers: is the depth dam's B under the dam's own bar F, and where does F sit against the runs? QUESTION. The dam gives every run from the void that escapes under a nondecreasing f the bar f(tau(P)) >= P+ at every prime P, so f >= F, F(t) = max{P+ : tau(P) <= t}; the depth dam gives f >= B, B(t) the largest p(s) whose point, r^(e+1) at s = r^e odd or 2^(e+2) at s = 2^e, is at most t. Is B <= F, and where does F sit against the record run's envelope E and the two choosier runs' (choosy.py)? DESIGN. tau(P) from cgreedy.tau_table (every prime P <= 10^4); F(t) is fixed by the table where some tabled P has tau(P) > t. B, E and the arms' envelopes E_A, E_B as choosy.py builds them, t <= 10^4. (1) THE LEMMA, by hand: s = r^e, P the largest prime below p(s). On a state whose primes are all at most P no held prime is 1 mod s, so u_r <= e - 1 and the price at r is at most r^(u_r+2) <= r^(e+1) at an unheld odd r, r^max(1, u_r-a+2) <= r^e held at a, 2^(u_2+3) <= 2^(e+2) at 2. So tau(P) <= point(s), and F(point(s)) >= P+ = p(s): F >= B at every t. The depth dam from the void is the dam read at P = p(s)-. (2) Every escaping run's envelope is a nondecreasing slack it escapes under, so it is at least F wherever F is fixed. PREDICTIONS (frozen before the code). P1 (proved) tau(p(s)-) <= point(s) at every prime power s with p(s) <= 10^4, and F >= B at every t where F is fixed. P2 (forced) F <= E, F <= E_A, F <= E_B wherever F is fixed. P3 (a guess, 60%) F > B at every fixed t >= 100. P4 (a guess, 55%) min(E, E_B)/F > 2 at more than half the fixed t >= 100. THE PRINT. The least and median of min(E, E_B)/F over the fixed t >= 100, and "F MEETS A RUN" if min(E, E_B) = F at some fixed t >= 100, else "F BELOW EVERY RUN". CONTROLS, read first. C1 F(7) = 13 and F(13) = 23. C2 P2's test flags E lowered to F - 1 at one fixed t. C3 the lemma's test flags the point read one power low, r^e or 2^(e+1), at some s. (C3 was first frozen as tau read at p(s) itself instead of the prime below it; that flagged 0 of 304 s, so it broke nothing, and was replaced before any verdict printed.) FINDINGS (from the printed run; the controls passed first). P1 holds: tau(p(s)-) <= point(s) at all 304 prime powers s with p(s) <= 9973 (the point one power low fails at 115), and F >= B at all 1819 fixed t, 4..1822 (tau(9973) = 1823 ends the range). P2 holds on E, E_A and E_B. P3 holds: F > B at all 1723 fixed t >= 100, F/B largest 15.3249 at t = 503 (F 3019, B 197); F/t largest 6.9928 at t = 839. P4 holds: min(E, E_B)/F > 2 at 1327 of 1723. THE PRINT: least 1.0000, median 2.3458; F MEETS A RUN at t = 227 and 228, where E_B = F = 1583 (E 5449); below 100, printed with the second readings, E_B = F at 4..12 and 17..24 and E = E_A = F at 5 and 6. Readings added after the first run: min(E, E_B) <= 1.1 F at 2 of the 1723 t and <= 1.5 F at 10; E/F least 1.1026, median 3.7643, largest 6.9715; E_B/F least 1.0000, median 2.3458, largest 4.2057. So the depth dam is the dam read at the prime powers, and at each t where a run meets F (227 and 228, and those below 100) no pointwise bar from the void rises above F: the least envelope over escaping runs equals F there. RUN RECORD. First run: C3 as first frozen flagged nothing (0 of 304) and was replaced, before any verdict; 8/8, 2.9 s, 79.8 MB. With the readings: 8/8, 2.9 s, 79.0 MB. With the line below 100: 8/8, 2.9 s, 79.8 MB. From its shipped place: 8/8, 2.9 s, 79.2 MB. """ import os import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") import cgreedy # noqa: E402 import envelope as ev # noqa: E402 import choosy # noqa: E402 T = ev.T CHECKS = [] def check(name, ok, detail=""): CHECKS.append((name, bool(ok))) print(f" [{'PASS' if ok else 'FAIL'}] {name}" + (f" -- {detail}" if detail else "")) def f_table(tab): """F(t) on 4..T where the table fixes it, else None.""" tp = sorted(tab) out = [None] * (T + 1) j, last = 0, None for t in range(4, T + 1): while j < len(tp) and tab[tp[j]][0] <= t: last = tp[j] j += 1 if j < len(tp) and last is not None: out[t] = cgreedy.next_prime(last) return out def lemma_bad(tab, low=False): """The prime powers s, p(s) <= the table, with tau(P) > point(s), P the prime below p(s); low reads the point one power lower.""" tp = sorted(tab) bad, n = [], 0 for s, r, _ in ev.prime_powers(tp[-1]): ps = ev.p_of(s) if ps > tp[-1]: continue P = max(p for p in tp if p < ps) point = (4 * s if r == 2 else r * s) // (r if low else 1) n += 1 if tab[P][0] > point: bad.append((s, P, tab[P][0], point)) return bad, n def main(): t0 = time.time() tab = cgreedy.tau_table() F = f_table(tab) fixed = [t for t in range(4, T + 1) if F[t] is not None] B, _ = choosy.bars() epairs, _, _, _ = ev.record_run() E = ev.hull([(m, R) for m, R, _ in epairs]) env = {"E": E} for arm in ("A", "B"): pairs, _ = choosy.run(arm) env["E_" + arm] = ev.hull(pairs) def under(Ex): return [t for t in fixed if Ex[t] < F[t]] print("CONTROLS") check("C1 F(7) = 13 and F(13) = 23", F[7] == 13 and F[13] == 23, f"F(7) = {F[7]}, F(13) = {F[13]}") tp = fixed[len(fixed) // 2] plant = list(E) plant[tp] = F[tp] - 1 check("C2 P2's test flags E lowered to F - 1 at one fixed t", under(plant) == [tp], f"t = {tp}, F = {F[tp]}") cbad, cn = lemma_bad(tab, low=True) check("C3 the lemma's test flags the point read one power low", len(cbad) > 0, f"{len(cbad)} of {cn} s, first {cbad[:2]}") if not all(ok for _, ok in CHECKS): print("CONTROL FAILED: nothing below is read.") raise SystemExit(1) print("THE BARS") bad, n = lemma_bad(tab) check(f"P1 tau(p(s)-) <= point(s) at every prime power s with " f"p(s) <= {max(tab)}", not bad, f"{n} s, {len(bad)} off {bad[:3]}") fb = [t for t in fixed if F[t] < B[t]] check("P1 F >= B at every fixed t", not fb, f"{len(fixed)} fixed t, 4..{fixed[-1]}; {len(fb)} off {fb[:3]}") for name, Ex in env.items(): u = under(Ex) check(f"P2 F <= {name} at every fixed t", not u, f"{len(u)} off {u[:3]}") hi = [t for t in fixed if t >= 100] eq = [t for t in hi if F[t] == B[t]] print(f"P3 F > B at every fixed t >= 100: {not eq} " f"({len(eq)} of {len(hi)} t equal, first {eq[:5]})") ratio = sorted(min(E[t], env['E_B'][t]) / F[t] for t in hi) big = sum(x > 2 for x in ratio) print(f"P4 min(E, E_B)/F > 2 at more than half the fixed t >= 100: " f"{2 * big > len(ratio)} ({big} of {len(ratio)})") print("READINGS") for t in (16, 64, 100, 256, 1000, fixed[-1]): print(f" t = {t}: B {B[t]}, F {F[t]}, E {E[t]}, E_A " f"{env['E_A'][t]}, E_B {env['E_B'][t]}") tm = max(fixed, key=lambda t: F[t] / B[t] if B[t] else 0) print(f" largest F/B over the fixed t: {F[tm] / B[tm]:.4f} at t = {tm}" f" (F {F[tm]}, B {B[tm]})") tm = max(fixed, key=lambda t: F[t] / t) print(f" largest F/t: {F[tm] / tm:.4f} at t = {tm}") print(f" tau(max P) = {tab[max(tab)][0]}, the end of the fixed range") # added with the second readings: where each run meets F below 100 for name, Ex in env.items(): print(f" {name} = F at fixed t < 100: " f"{[t for t in fixed if t < 100 and Ex[t] == F[t]]}") # added after the first run: who meets F, and how near the rest come for t in (227, 228): print(f" t = {t}: F {F[t]}, E {E[t]}, E_A {env['E_A'][t]}, " f"E_B {env['E_B'][t]}") for c in (1.1, 1.5): n = sum(min(E[t], env['E_B'][t]) <= c * F[t] for t in hi) print(f" min(E, E_B) <= {c} F at {n} of the {len(hi)} fixed t >= 100") for name in ("E", "E_B"): r = sorted(env[name][t] / F[t] for t in hi) print(f" {name}/F over fixed t >= 100: least {r[0]:.4f}, median " f"{r[len(r) // 2]:.4f}, largest {r[-1]:.4f}") print("THE PRINT") meet = [t for t in hi if min(E[t], env['E_B'][t]) == F[t]] print(f" min(E, E_B)/F over fixed t >= 100: least {ratio[0]:.4f}, " f"median {ratio[len(ratio) // 2]:.4f}") print(" " + (f"F MEETS A RUN at {meet[:5]}" if meet else "F BELOW EVERY RUN")) print(f"{sum(ok for _, ok in CHECKS)}/{len(CHECKS)} checks passed, " f"{time.time() - t0:.1f} s") raise SystemExit(0 if all(ok for _, ok in CHECKS) else 1) if __name__ == "__main__": main()