"""pointwise.py -- is the dam's bar F the least envelope at every t?

QUESTION. L(t), the least E_run(t) over runs escaping from the void,
E_run(t) the largest move a run takes from a state with tide <= t.
Every escape pays F (the dam's bar), so L >= F. Is L(t) = F(t) at
every t >= 4?

DESIGN. F from fwide.py's widened tau table, fixed on 4..10^4, cut into
its steps [t1, t2] (F constant, Q = F(t2)). Per step: the witness H,
cgreedy.feasible(t2 + 1, Q) with the primes of [t2 + 1, Q], a state on
the primes <= Q with tide > t2; cut to N_s-minimal by counts (s the
primes <= t2), then by one greedy pass, checked tide-minimal, to H';
seat H' from the void
one prime at a time, increasing and then decreasing.
(i) A small prime is one <= t. Its price reads only lambda's part at
the primes <= t and the exponents at small primes. On a state M with
tide > t >= 4, a small odd r held at a has price r^max(1, v - a + 2)
> r, so v_r(lambda) >= a, above r's own part a - 1; 2 held at b prices
2^max(1, v + 3 - b) > 4, so v_2 >= b, above its own part. So lambda's
small part is that of N' = lcm(q - 1), q over M's held odd primes, and
the squarefree odd state on them prices every prime <= t at least as M
does, and every larger prime at least itself: tide > t.
(ii) Tide-minimal is irredundant: if (p - 1)'s small part divides the
others' lcm, dropping p keeps lambda's small part, and p, if small,
prices p^(v+2) > p^(v+1) unheld. So in ANY order each seat p has p - 1
not dividing the lambda before it: a raising move at its price p <= Q.
(iii) From any state, a new odd prime seated at exponent 1 that raises
lambda lowers no price, and its own becomes at least itself, at least
the tide; the tide-led rule (the least prime = 1 mod the tide prime's
unborn power, an open r itself) raises the tide's price at every move but an open r's
first, so the tide grows without bound and the run escapes.
(iv) Q = F(t) lies in H', and in the state of every run attaining L(t)
when its tide first passes t: the primes below Q carry tide <= t.
So L(t) = F(t) at every t >= 4, by (i)-(iii); this script checks the
construction at every step.

PREDICTIONS (frozen before the code).
P1 (proved) every step, H' increasing: each move raises lambda, each
   is <= Q, the final tide > t2.
P2 (proved, (ii); minimality checked) the same, H' decreasing; and H'
   tide-minimal, which
   the greedy pass does not guarantee and (ii) uses.
P3 (proved, (iv)) Q in H' at every step.
P4 (proved, (iii)) 20 tide-led seats past each final state never lower
   the tide, each raising lambda.
P5 (a guess, 60%) the largest |H'| over the steps is at most 30.

THE PRINT. "L = F AT EVERY STEP OF 4..10^4: <n> steps" when P1-P4 hold
at every step, else "KILL: THE CONSTRUCTION FAILS AT <t2>"; a failure
kills the proof, not a heuristic.

CONTROLS, read first. C1 the hand run at t = 25, Q = 97: 61, 67, 73, 97
from the void, each raising lambda (60, 66, 72, 96 carry 5, 11, 3^2,
2^5), tide 29. C2 the raising test flags 13 after 79 and 53 (12 divides
lcm(78, 52)), and cgreedy.raises agrees. C3 choosy.tide agrees with
cgreedy.m0 (growth's door formulas on the full factor map) at C1's
states and at every final state with tide below 20000. C4 the
minimality test fails on the full witness H at the first step where H'
is smaller. C5 at every step feasible(t2 + 1, the prime before Q) is
None.

FINDINGS (from the printed run; the controls passed first). C1: the
hand run's tides are 3, 17, 17, 17, 29 (61 alone lifts the tide from 3
to 17). C3 compares 28 final states, C4 fails the full witness at step
5..6 (|H| 4, |H'| 2), C5 holds at all 28 steps: F takes 28 values on
4..10^4. P1-P4 hold at every step. THE PRINT: L = F AT EVERY STEP OF
4..10^4: 28 steps. P5 FAILS: |H'| has median 96 and largest 460, at the
top step 8543..10^4 (F = 153757, tide 10007), whose H' holds 1997 and
its anchor 87869 = p(1997); the count cut leaves at most 1142. At step
17..46 (F = 97) H' is 11, 23, 29, 47, 59, 73, 97, tide 47.
So the dam's bar is the least envelope at every t >= 4: L = F, proved
in (i)-(iii), the construction checked at every step to 10^4. The run
attaining it at t depends on t, and holds F(t) when its tide first
passes t; F itself, as a slack, is dammed from the void at 23, so no
single run attains L at every t.
RUN RECORD. 9/10, 37.9 s, 65.4 MB: P5 was a check and failed; it is
now a printed reading, as a guess does not gate: 9/9, 38.2 s, 65.3 MB.
With P2's tide-minimality check, added on audit: 9/9, 39.7 s, 65.3 MB.
Run from code/: 9/9, 38.9 s, 65.3 MB.

    python pointwise.py
"""

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
import dambar  # noqa: E402
import fwide  # noqa: E402
import anchor  # 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 lam_of(held):
    vN = {}
    for p in held:
        for q, e in ev.fac(p - 1).items():
            if e > vN.get(q, 0):
                vN[q] = e
    return vN


def tide_of(held):
    return choosy.tide(set(held), lam_of(held))[0]


def seat_run(order):
    """Seat order from the void: (every move raised lambda, tides before
    each move and after the last, the final held set and vN)."""
    held, vN, ok = set(), {}, True
    tides = [choosy.tide(held, vN)[0]]
    for p in order:
        new = dict(vN)
        for q, e in ev.fac(p - 1).items():
            if e > new.get(q, 0):
                new[q] = e
        if new == vN or p in held:
            ok = False
        held.add(p)
        vN = new
        tides.append(choosy.tide(held, vN)[0])
    return ok, tides, held, vN


def minimal(S, t2):
    return tide_of(S) > t2 and all(tide_of(S - {p}) <= t2 for p in S)


def cut(H, t2):
    """N_s-minimal by counts, then tide-minimal, greedily."""
    comp = {p: {q: e for q, e in ev.fac(p - 1).items() if q <= t2}
            for p in H}
    vmax, cnt = {}, {}
    for p in H:
        for q, e in comp[p].items():
            if e > vmax.get(q, 0):
                vmax[q], cnt[q] = e, 1
            elif e == vmax[q]:
                cnt[q] += 1
    keep = set(H)
    for p in sorted(H, reverse=True):
        top = [q for q, e in comp[p].items() if e == vmax[q]]
        if all(cnt[q] >= 2 for q in top):
            keep.discard(p)
            for q in top:
                cnt[q] -= 1
    mid = len(keep)
    for p in sorted(keep, reverse=True):
        if tide_of(keep - {p}) > t2:
            keep = keep - {p}
    return keep, mid


def continue_ok(held, vN, n=20):
    held, vN = set(held), dict(vN)
    m_prev = choosy.tide(held, vN)[0]
    for _ in range(n):
        m0, r, kind = choosy.tide(held, vN)
        s = anchor.modulus(m0, r, kind, vN)
        P = next(anchor.cls(s))
        new = dict(vN)
        for q, e in choosy.factor(P - 1).items():
            if e > new.get(q, 0):
                new[q] = e
        if P in held or new == vN:
            return False
        held.add(P)
        vN = new
        m1 = choosy.tide(held, vN)[0]
        if m1 < m_prev:
            return False
        m_prev = m1
    return True


def full_m0(held):
    return cgreedy.m0({p: 1 for p in held})


def main():
    t0 = time.time()
    fwide.widen(fwide.PMAX)
    F = dambar.f_table(fwide.tau_wide(fwide.PMAX, T))
    assert all(F[t] is not None for t in range(4, T + 1))
    print(f"F fixed on 4..{T} ({time.time() - t0:.1f} s)")
    steps = []
    for t in range(4, T + 1):
        if steps and F[t] == steps[-1][2]:
            steps[-1][1] = t
        else:
            steps.append([t, t, F[t]])
    PR = cgreedy.PR

    print("CONTROLS")
    ok, tides, held, vN = seat_run([61, 67, 73, 97])
    check("C1 the hand run 61, 67, 73, 97 raises lambda at every move, "
          "tide 29", ok and tides[-1] == 29 and F[25] == 97,
          f"tides {tides}, F(25) {F[25]}")
    c3 = all(choosy.tide(set(h), lam_of(h))[0] == full_m0(h)
             for h in ([], [61], [61, 67], [61, 67, 73], [61, 67, 73, 97]))
    ok2, _, _, _ = seat_run([79, 53, 13])
    ok_pre, _, _, _ = seat_run([79, 53])
    mf = {79: 1, 53: 1}
    flag = not cgreedy.raises(mf, cgreedy.lam(mf), 13)
    check("C2 the raising test flags 13 after 79 and 53; cgreedy agrees",
          ok_pre and not ok2 and flag)
    res = []
    for t1, t2, Q in steps:
        X = cgreedy.feasible(t2 + 1, Q)
        H = set(X) | {p for p in PR if t2 + 1 <= p <= Q}
        Hc, mid = cut(H, t2)
        Qprev = max(p for p in PR if p < Q)
        res.append((t1, t2, Q, H, Hc, mid,
                    cgreedy.feasible(t2 + 1, Qprev) is None))
    finals = []
    for t1, t2, Q, H, Hc, mid, _ in res:
        tm = tide_of(Hc)
        if tm < 20000:
            finals.append((tm, full_m0(Hc)))
    check("C3 choosy.tide = cgreedy.m0 at C1's states and every final "
          "state with tide < 20000", c3 and all(a == b for a, b in finals),
          f"{len(finals)} final states")
    big = next((r for r in res if len(r[4]) < len(r[3])), None)
    check("C4 the minimality test fails on the full witness H",
          big is not None and not minimal(big[3], big[1])
          and minimal(big[4], big[1]),
          f"step {big[0]}..{big[1]}: |H| {len(big[3])}, |H'| {len(big[4])}")
    check("C5 at every step no state on the primes below Q has tide > t2",
          all(r[6] for r in res), f"{len(res)} steps")
    if not all(ok for _, ok in CHECKS):
        print("CONTROL FAILED: nothing below is read.")
        raise SystemExit(1)

    print("THE STEPS")
    fail = {}
    sizes = []
    for t1, t2, Q, H, Hc, mid, _ in res:
        up = sorted(Hc)
        ok1, tides1, held, vN = seat_run(up)
        ok2, tides2, _, _ = seat_run(up[::-1])
        p1 = ok1 and max(up) <= Q and tides1[-1] > t2
        p2 = ok2 and tides2[-1] > t2
        p3 = Q in Hc
        p4 = continue_ok(held, vN)
        p2 = p2 and minimal(Hc, t2)
        for name, v in (("P1", p1), ("P2", p2), ("P3", p3), ("P4", p4)):
            if not v:
                fail.setdefault(name, []).append(t2)
        sizes.append((len(Hc), t2, mid))
    for name in ("P1", "P2", "P3", "P4"):
        bad = fail.get(name, [])
        check(f"{name} at every step", not bad,
              f"{len(bad)} failing, first {bad[:3]}")
    smax = max(sizes)
    print(f"  P5 (guess) the largest |H'| is at most 30: "
          f"{'HOLDS' if smax[0] <= 30 else 'FAILS'}, largest {smax[0]} at "
          f"t2 = {smax[1]}")

    print("READINGS")
    ss = sorted(s for s, _, _ in sizes)
    print(f"  {len(steps)} steps; |H'| median {ss[len(ss) // 2]}, "
          f"largest {smax[0]} at t2 = {smax[1]}; after the count cut "
          f"largest {max(m for _, _, m in sizes)}")
    for t1, t2, Q, H, Hc, mid, _ in res:
        if t1 <= 25 <= t2 or t2 in (T,) or t1 in (4, 5, 7, 11):
            print(f"  step {t1}..{t2}, F = {Q}: H' = {sorted(Hc)}, "
                  f"tide {tide_of(Hc)}")

    print("THE PRINT")
    if not fail:
        print(f"  L = F AT EVERY STEP OF 4..10^4: {len(steps)} steps")
    else:
        first = min(min(v) for v in fail.values())
        print(f"  KILL: THE CONSTRUCTION FAILS AT {first}")
    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()