"""RUN-019 - Round 16: the capacity-aware global master-root pilot.

Round 16 runs the first pilot from the whole five-dimensional base root D + B3 + B5,
sized at the phase master T_M = 0.8365 and profiled toward T = 0.835: two split
schedulers (Mishra's first-order weights, Round 09's exact tau), the master root against
the immediate 0.835 root, a depth-18 frontier with a centre-area profile and a
margin-to-resolution proxy, and B7 shallow lifts on the two lowest cells. No bound is
claimed. Here the root and the schedulers are rebuilt from the text and the trees are
emitted twice: with exact common cores (this tree's reconstruction), and with the
pilot's sampling - "40 finite boundary inner points", which only its code pins down as
contact points in the directions 2 pi k / 40 (read after the reconstruction). The
frontier's minimizer cells, the proxy and the symmetry are then examined.

Checks
  A0 anchors      the formulas and numbers below occur in Round 16 as written
  W1 root         sec. 1-2: t_3, t_5, t_7 at 0.8365; f(d) is the hull of the disc and a point
  W2 modes        sec. 1-2, 7: APR is pi/4 on the whole root and never fires; REP cannot
                  fire at depth 18; no cell would have needed sec. 1's corner rule
  W3 schedulers   sec. 3: both split sequences (Round 09's rules); the top cells' paths
                  decode to their centres and half-widths
  W4 trees        sec. 4, 6, 7: every count rebuilt with the pilot's sampling and ties; with
                  exact cores the HARD sets shrink inside the sampled ones, and with ties
                  broken to the later axis the counts move; both comparisons keep their
                  direction either way
  W5 frontier     sec. 8-14, 21: the depth-18 profile rebuilt; its centres against exact ones
  W6 minimizer    q-dagger's images in the grid; cells holding a configuration below 0.835
                  are HARD in both trees and the proxy still gives them finite cycles; the
                  proxy on a random sample
  W7 lift         sec. 15: the B7 probes, sampled and exact
  W8 symmetry     sec. 19: the base area's mirror and turn; the mirror maps the grid and
                  every closed and HARD set onto itself; the turn does not map the grid
  P1 package      the summary, raw file, long-run spec and crystal against the text
  P2 package      VALIDATION against the archive; the shipped code against the summary
  R1 registry     Round 16's judgments reviewed, first-used statuses defined

Usage: python code/run019_round16_global_pilot.py [--drill] [--blind CID]
"""
import argparse
import copy
import hashlib
import inspect
import itertools
import json
import math
import re
from multiprocessing import Pool

import numpy as np
from scipy.optimize import minimize
from scipy.spatial import ConvexHull

import gate
import registry
import run008_round05_saturation_gate as r8
import run009_round06_witness_exchange as r9
import run011_round08_conditional_lift as r11
import run012_round09_adaptive_atlas as r12
import run013_round10_reference_dry_run as r13
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run009_round06_witness_exchange import hull_pieces, placed_disc, placed_reuleaux, rot
from run010_round07_minimizer_atlas import d_star, f_text, t_text
from run011_round08_conditional_lift import placed_vertices
from run012_round09_adaptive_atlas import AXES, R5, core_pieces, tau_f3
from run013_round10_reference_dry_run import contact_points

PKG = "main.zip!/AMRAL_LUC_FC_Round_16_Package_v0.1.zip!/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_16_Global_Pilot_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_16_v0.1.md"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_16_VALIDATION.json"
SPEC = PKG + "AMRAL_LUC_FC_Round_16_LONG_RUN_SPEC.json"
SUMMARY = PKG + "AMRAL_LUC_FC_Round_16_GLOBAL_PILOT_SUMMARY.json"
RAW = PKG + "AMRAL_LUC_FC_Round_16_depth18_raw.json"
CODE = PKG + "AMRAL_LUC_FC_Round_16_global_pilot.py"
LOG = TREE / "data" / "gate-logs" / "run019-round16-global-pilot.json"
CACHE = TREE / "data" / "cache" / "run019-pilot.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"

T, TM, PAD = 0.835, 0.8365, 1e-9
P5 = 2 * math.pi / 5
R3, R7 = 1 / math.sqrt(3), 1 / (2 * math.cos(math.pi / 14))
TH = 2 * np.pi * np.arange(40) / 40                 # the pilot's directions (its code)
DISC = 0.5 * np.stack([np.cos(TH), np.sin(TH)], axis=1)
TURNS = (0.01 * (math.sqrt(5) - 1), 0.01 * (math.sqrt(3) - 1), 0.01 * (math.sqrt(7) - 2))
QDAG = [-0.01215883209899, -3.708198611978e-08, 1.256661190387, 0.02299660691706, -3.896981517063e-06]
A_QDAG = 0.834780945912                             # Round 07's repository, exact kernel
FLIP = {0, 2, 4, 5, 7, 9, 10, 12, 14, 15, 17}       # phi5, y5, y3 in the official order

ANCHORS = {
    "W1": [r"t_3=0.20102352900741122,", r"t_5=0.20261828623043526,", r"t_7=0.20147344578628750.", r"T_M=0.8365.",
           r"\phi_5\in[0,2\pi/5),", r"f(d)=\frac14\left(\pi-\arccos\frac1{2d}\right)+\frac12\sqrt{d^2-\frac14}.",
           r"4T\tau+\pi\tau^2.", r"N_{\rmsample}=40,", r"e_{\rmpilot}=10^{-9}."],
    "W2": [r"APR/REP=0`不代表它們永遠沒用", r"APRcontained-centerbound仍不夠接近$0.835$；"],
    "W3": [r"\max\left\{h_{x3},h_{y3},R_5h_{\phi5},h_{x5},h_{y5}\right\\}."],
    "W4": [r"|10|official|2,047|370|654|", r"|10|exact-$\tau$|2,047|0|1,024|", r"|12|official|4,919|1,126|1,334|",
           r"|12|exact-$\tau$|6,519|1,936|1,324|", r"|14|official|11,639|3,218|2,602|",
           r"|14|exact-$\tau$|13,319|3,146|3,514|", r"|16|official|23,455|7,616|4,112|",
           r"|16|exact-$\tau$|28,771|9,134|5,252|", r"18.48\%", r"21.71\%", r"N=24691,", r"CORE=8004,",
           r"HARD=4342.", r"N=23455,", r"CORE=7616,", r"HARD=4112.", r"N=45651.", r"APR=0,", r"REP=0,",
           r"CORE=12378,", r"HARD=10448."],
    "W5": [r"\minA^-_{\rmcenter}=0.8356828349502634>0.835.", r"\#\{A^-_{\rmcenter}<0.835\}=0.",
           r"|$\leT+0.00075$|2|", r"|$\leT+0.001$|2|", r"|$\leT+0.002$|8|", r"|$\leT+0.005$|70|",
           r"|$\leT+0.01$|196|", r"|$\leT+0.02$|714|", r"Q_{0}=0.835682835,", r"Q_{0.01}=0.841831848,",
           r"Q_{0.10}=0.858184427,", r"Q_{0.50}=0.884118492,", r"Q_{0.99}=0.914281848.",
           r"Q_{0.50}\approx0.822136323,", r"Q_{0.90}\approx0.832177159,", r"Q_{0.99}\approx0.834731887,",
           r"0.834989575.", r"\tau_\star(m,T)=\frac{\sqrt{4T^2+\pim}-2T}{\pi},", r"m=A^-_{\rmcenter}-T.",
           r"\tau=0.03855318146790454", r"Q_{0.10}=1,", r"Q_{0.50}=2,", r"Q_{0.90}=3,", r"Q_{0.99}=5,",
           r"\max=8.", r"\ge3\text{cycles}:2186,", r"\ge4:432,", r"\ge5:142,", r"\ge6:48,", r"\ge7:8,",
           r"\ge8:2.", r"A^-_{\rmcenter}\approx0.83568283495.", r"\approx0.79907297849.", r"3.66\times10^{-2}.",
           r"\boxed{142}.", r"2186-142=\boxed{2044}.", r"10448-2186=\boxed{8262}."],
    "W6": [r"的保守proxy。", r"cell內可能包含比center更低的配置。"],
    "W7": [r"x_7,y_7\in[-t_7(0.8365),t_7(0.8365)].", r"2403\text{nodes}", r"568\text{closedleaves},",
           r"634\text{unresolvedleaves}."],
}

# ---------------------------------------------------------------- the root and the schedulers

def root(target):
    t3, t5 = t_text(3, d_star(target)), t_text(5, d_star(target))
    return np.array([0.0, 0.0, math.pi / 5, 0.0, 0.0]), np.array([t3, t3, math.pi / 5, t5, t5])


def official_axis(h):
    """sec. 3 A: the widest half-width, the angle weighted by R_5; ties to the earlier axis"""
    return int(np.argmax([h[0], h[1], R5 * h[2], h[3], h[4]]))


def exact_axis(h):
    """sec. 3 B: the axis whose bisection leaves the least tau; ties to the earlier axis"""
    taus = []
    for i in range(5):
        c = list(h)
        c[i] /= 2
        taus.append(tau_f3(c))
    return min(range(5), key=lambda i: (taus[i], i))


RULES = {"official": official_axis, "exact_tau": exact_axis}
# the text states neither rule's ties; the pilot's code breaks them to the earlier axis
LATE_TIES = {"official": lambda h: max(range(5), key=lambda i: ([h[0], h[1], R5 * h[2], h[3], h[4]][i], i)),
             "exact_tau": lambda h: min(range(5), key=lambda i: (tau_f3([x / 2 if j == i else x for j, x in enumerate(h)]), -i))}


def split_sequence(h0, rule, depth):
    """both rules read only the half-widths, which are the same across a level"""
    seq, h = [], list(h0)
    for _ in range(depth):
        a = rule(h)
        seq.append(a)
        h[a] /= 2
    return seq


def decode(path, seq, c0, h0):
    c, h = np.array(c0, dtype=float), np.array(h0, dtype=float)
    for bit, a in zip(path, seq):
        h[a] /= 2
        c[a] += h[a] if bit == "1" else -h[a]
    return c, h


# ---------------------------------------------------------------- the three routes

def f_apr(d):
    """sec. 2: the hull of the disc and a point at distance d; the disc itself within it"""
    return math.pi / 4 if d <= 0.5 else f_text(d)


def box_distance(c, h):
    return math.hypot(max(abs(c[0]) - h[0], 0.0), max(abs(c[1]) - h[1], 0.0))


def turned(pieces, a):
    """the same bodies turned by a: the area is unchanged, and piece ranges that dyadic
    cells put on the envelope's power-of-two grid move off it"""
    R = rot(a)
    return [(R @ np.asarray(c, dtype=float), r, None if g is None else (g[0] + a, g[1])) for c, r, g in pieces]


def exact_area(pieces):
    """the exact hull area; the envelope refuses rather than guesses, so a refusal is
    retried at another turn and never becomes a number"""
    for a in TURNS:
        try:
            return hull_pieces(turned(pieces, a), 1024)[0]
        except RuntimeError:
            continue
    raise RuntimeError("envelope refused at every turn")


def cores(c, h):
    """the common erosion cores of a cell; a core is empty once 1 - delta falls to R_n"""
    d3 = math.hypot(h[0], h[1])
    d5 = math.hypot(h[3], h[4]) + 2 * R5 * math.sin(h[2] / 2)
    k3 = core_pieces(placed_vertices(3, 0.0, c[:2]), 1 - d3)[0] if 1 - d3 > R3 else None
    k5 = core_pieces(placed_vertices(5, c[2], c[3:5]), 1 - d5)[0] if 1 - d5 > R5 else None
    return k3, k5


def sampled_hull(pieces_list):
    return float(ConvexHull(np.vstack([DISC] + [contact_points(p, TH) for p in pieces_list])).volume) - PAD


def modes(c, h, exact):
    """sec. 2 in its order: APR, REP, CORE; returns (mode or None, best value, centre, core)"""
    c, h = np.asarray(c, dtype=float), np.asarray(h, dtype=float)
    apr = max(f_apr(box_distance(c[0:2], h[0:2])), f_apr(box_distance(c[3:5], h[3:5])))
    if apr >= T:
        return "APR", apr, None, None
    tau = tau_f3(h)
    bodies = [placed_reuleaux(3, 0.0, c[:2]), placed_reuleaux(5, c[2], c[3:5])]
    ac = exact_area(placed_disc() + bodies[0] + bodies[1]) - PAD if exact else sampled_hull(bodies)
    rep = ac - (4 * T * tau + math.pi * tau * tau)
    if rep >= T:
        return "REP", rep, ac, None
    k3, k5 = cores(c, h)
    core = -1.0
    if k3 is not None and k5 is not None:
        core = exact_area(placed_disc() + k3 + k5) - PAD if exact else sampled_hull([k3, k5])
    if core >= T:
        return "CORE", core, ac, core
    return None, max(apr, rep, core), ac, core


def _modes(args):
    return modes(*args)


def emit(target, rule, depth, exact, pool, keep_closed, rules=RULES):
    """the tree, level by level: per depth the counts of sec. 4; the depth-d HARD cells
    and, if asked, every closed cell"""
    c0, h0 = root(target)
    seq = split_sequence(h0, rules[rule], depth)
    level, stats, closed, hard, total = [("", c0, h0)], {}, {}, {}, {"nodes": 0, "APR": 0, "REP": 0, "CORE": 0}
    for d in range(depth + 1):
        vals = pool.map(_modes, [(c.tolist(), h.tolist(), exact) for _, c, h in level], chunksize=32)
        nxt, open_here = [], 0
        for (p, c, h), (mode, lb, ac, core) in zip(level, vals):
            total["nodes"] += 1
            if mode:
                total[mode] += 1
                if keep_closed:
                    closed[p] = mode
                continue
            open_here += 1
            if d == depth:
                hard[p] = [lb, ac, core]
                continue
            a = seq[d]
            hh = h.copy()
            hh[a] /= 2
            lo, hi = c.copy(), c.copy()
            lo[a] -= hh[a]
            hi[a] += hh[a]
            nxt += [(p + "0", lo, hh), (p + "1", hi, hh)]
        stats[d] = {**total, "HARD": open_here}
        level = nxt
    return {"axes": [AXES[a] for a in seq], "stats": stats, "hard": hard, "closed": closed}


# ---------------------------------------------------------------- the B7 probe (sec. 15)

def delta7(h):
    return math.hypot(h[1], h[2]) + 2 * R7 * math.sin(h[0] / 2)


def _lift_value(args):
    wc, wh, base, exact = args
    rho = 1 - delta7(wh)
    if rho <= R7 or base[0] is None or base[1] is None:
        return math.pi / 4
    k7 = core_pieces(placed_vertices(7, wc[0], wc[1:3]), rho)[0]
    return exact_area(placed_disc() + base[0] + base[1] + k7) - PAD if exact else sampled_hull([base[0], base[1], k7])


def b7_probe(c, h, exact, pool, max_depth=12):
    """the phase-master B7 root over a base cell's cores, split by the least child delta_7
    (ties to phi, then x); a leaf closes at the target or stays open at depth 12"""
    base = cores(np.asarray(c), np.asarray(h))
    t7 = t_text(7, d_star(TM))
    level = [((math.pi / 7, 0.0, 0.0), (math.pi / 7, t7, t7))]
    out = {"nodes": 0, "closed": 0, "unresolved": 0, "worst": None}
    for d in range(max_depth + 1):
        vals = pool.map(_lift_value, [(wc, wh, base, exact) for wc, wh in level], chunksize=16)
        nxt = []
        for (wc, wh), lb in zip(level, vals):
            out["nodes"] += 1
            if lb >= T:
                out["closed"] += 1
                out["worst"] = lb - T if out["worst"] is None else min(out["worst"], lb - T)
            elif d == max_depth:
                out["unresolved"] += 1
            else:
                trial = []
                for a in range(3):
                    hh = list(wh)
                    hh[a] /= 2
                    trial.append(delta7(hh))
                a = int(np.argmin(trial))
                hh = list(wh)
                hh[a] /= 2
                lo, hi = list(wc), list(wc)
                lo[a] -= hh[a]
                hi[a] += hh[a]
                nxt += [(tuple(lo), tuple(hh)), (tuple(hi), tuple(hh))]
        level = nxt
    return out


# ---------------------------------------------------------------- the minimizer's cells

def base_area(q):
    q = np.asarray(q, dtype=float)
    return exact_area(placed_disc() + placed_reuleaux(3, 0.0, q[:2]) + placed_reuleaux(5, q[2], q[3:5]))


def mirror(q):
    return np.array([q[0], -q[1], (-q[2]) % P5, q[3], -q[4]])


def turn(q, k=1):
    R = rot(2 * math.pi * k / 3)
    v3, v5 = R @ np.asarray(q[:2]), R @ np.asarray(q[3:5])
    return np.array([v3[0], v3[1], (q[2] + 2 * math.pi * k / 3) % P5, v5[0], v5[1]])


def images():
    q = np.array([*QDAG[:2], QDAG[2] % P5, *QDAG[3:]])
    out = {"q": q, "Mq": mirror(q)}
    for k, name in ((1, "R"), (2, "R2")):
        out[name + "q"] = turn(q, k)
        out["M" + name + "q"] = mirror(turn(q, k))
    return out


GRID_N = np.array([8, 8, 16, 16, 16])               # the official depth-18 grid


def grid():
    c0, h0 = root(TM)
    return c0 - h0, 2 * h0 / GRID_N


def cell_path(idx):
    seq = split_sequence(root(TM)[1], official_axis, 18)
    bits, used, depth_of = [], [0] * 5, [3, 3, 4, 4, 4]
    for a in seq:
        bits.append(str((int(idx[a]) >> (depth_of[a] - 1 - used[a])) & 1))
        used[a] += 1
    return "".join(bits)


def _near_image(lo, hi, W):
    best, bd = None, math.inf
    for img in images().values():
        for shift in (-P5, 0.0, P5):
            p = img.copy()
            p[2] += shift
            x = np.clip(p, lo, hi)
            dist = float(np.linalg.norm((x - p) / W))
            if dist < bd:
                best, bd = x, dist
    return best


def _search_area(q):
    """for the local search only: a refused envelope counts as no improvement; a witness
    is re-evaluated by base_area before it is kept"""
    try:
        return base_area(q)
    except RuntimeError:
        return 1.0


def _subtarget_probe(idx):
    LO, W = grid()
    lo = LO + np.array(idx) * W
    hi = lo + W
    x = _near_image(lo, hi, W)
    a, how = _search_area(x), "clipped image"
    if T <= a < T + 4e-3:
        res = minimize(_search_area, x, method="L-BFGS-B", bounds=list(zip(lo, hi)), options={"maxiter": 60, "eps": 1e-8})
        if res.fun < a:
            x, a, how = np.asarray(res.x), float(res.fun), "local search"
    return list(idx), x.tolist(), a, how


def subtarget_cells(pool):
    """depth-18 cells within one step of a cell holding an image of q-dagger, each with a
    point below the target: the nearest image clipped into the cell, else a bounded local
    search from there"""
    LO, W = grid()
    seeds = {tuple(int(v) for v in np.floor((q - LO) / W)) for q in images().values()}
    cand = set()
    for s in seeds:
        for d in itertools.product((-1, 0, 1), repeat=5):
            c = [s[i] + d[i] for i in range(5)]
            c[2] %= 16
            if all(0 <= c[i] < GRID_N[i] for i in range(5)):
                cand.add(tuple(c))
    out = {}
    for idx, x, a, how in pool.map(_subtarget_probe, sorted(cand), chunksize=4):
        if a < T and base_area(x) < T:
            out[cell_path(idx)] = {"cell": idx, "witness": x, "area": base_area(x), "how": how}
    return {"candidates": len(cand), "cells": out}


# ---------------------------------------------------------------- the proxy on a sample

def tau_star(m):
    """sec. 12: Round 09's radius for a representative margin m at r = 1/2"""
    return (math.sqrt(4 * T * T + math.pi * m) - 2 * T) / math.pi


def proxy_cycles(tau, centre):
    m = centre - T
    if m <= 0:
        return None
    ts = tau_star(m)
    return 0 if tau <= ts else int(math.ceil(math.log(tau / ts, 2)))


def _open_after(args):
    c, h, levels = args
    stack, left = [(np.array(c), np.array(h), 0)], 0
    while stack:
        c, h, d = stack.pop()
        if d > 0 and modes(c, h, False)[0] is not None:
            continue
        if d == levels:
            left += 1
            continue
        a = official_axis(h)
        hh = h.copy()
        hh[a] /= 2
        lo, hi = c.copy(), c.copy()
        lo[a] -= hh[a]
        hi[a] += hh[a]
        stack += [(hi, hh, d + 1), (lo, hh, d + 1)]
    return left


def proxy_sample(hard, pool, per_class=40):
    """HARD cells the proxy gives k = 1, 2 cycles, 40 of each at random: how many close
    within k full cycles (5k further official levels) of the pilot's own tree"""
    c0, h0 = root(TM)
    seq = split_sequence(h0, official_axis, 18)
    tau = tau_f3(decode("0" * 18, seq, c0, h0)[1])
    by_k = {}
    for p in sorted(hard):
        by_k.setdefault(proxy_cycles(tau, hard[p][1]), []).append(p)
    rng = np.random.default_rng(16)
    out = {}
    for k in (1, 2):
        pick = [by_k[k][i] for i in rng.choice(len(by_k[k]), size=per_class, replace=False)]
        args = [(*[v.tolist() for v in decode(p, seq, c0, h0)], 5 * k) for p in pick]
        out[str(k)] = dict(zip(pick, pool.map(_open_after, args, chunksize=1)))
    return out


# ---------------------------------------------------------------- the computation, cached

def _centre(path):
    c0, h0 = root(TM)
    c, _ = decode(path, split_sequence(h0, official_axis, 18), c0, h0)
    return base_area(c) - PAD


def compute():
    with Pool(14) as pool:
        out = {"sampled": {}, "exact": {}}
        for exact, key in ((False, "sampled"), (True, "exact")):
            out[key]["official"] = emit(TM, "official", 18, exact, pool, keep_closed=True)
            out[key]["exact_tau"] = emit(TM, "exact_tau", 16, exact, pool, keep_closed=False)
            out[key]["immediate"] = emit(T, "official", 16, exact, pool, keep_closed=False)
        out["late_ties"] = {"official": emit(TM, "official", 18, False, pool, False, LATE_TIES),
                            "exact_tau": emit(TM, "exact_tau", 16, False, pool, False, LATE_TIES),
                            "immediate": emit(T, "official", 16, False, pool, False, LATE_TIES)}
        hard = out["sampled"]["official"]["hard"]
        paths = sorted(hard)
        out["exact_centres"] = dict(zip(paths, pool.map(_centre, paths, chunksize=64)))
        low = sorted(paths, key=lambda p: hard[p][1])[:2]
        c0, h0 = root(TM)
        seq = split_sequence(h0, official_axis, 18)
        out["b7"] = {key: {p: b7_probe(*[v.tolist() for v in decode(p, seq, c0, h0)], exact, pool) for p in low}
                     for key, exact in (("sampled", False), ("exact", True))}
        out["subtarget"] = subtarget_cells(pool)
        out["proxy"] = proxy_sample(hard, pool)
    return out


def _code_key():
    digest = hashlib.sha256()
    for fn in LATE_TIES.values():
        digest.update(inspect.getsource(fn).encode())
    for fn in (root, official_axis, exact_axis, split_sequence, decode, f_apr, box_distance, turned, exact_area,
               cores, sampled_hull, modes, emit, delta7, _lift_value, b7_probe, base_area, mirror, turn, images,
               grid, cell_path, _near_image, _search_area, _subtarget_probe, subtarget_cells, tau_star, proxy_cycles,
               _open_after,
               proxy_sample, _centre, compute):
        digest.update(inspect.getsource(fn).encode())
    for mod in (r8, r9, r11, r12, r13):
        digest.update(open(mod.__file__, "rb").read())
    return digest.hexdigest()


_COMPUTED = {}


def computed():
    key = _code_key()
    if key not in _COMPUTED:
        if CACHE.exists():
            cached = json.loads(CACHE.read_text(encoding="utf-8"))
            if cached.get("key") == key:
                _COMPUTED[key] = cached["results"]
        if key not in _COMPUTED:
            _COMPUTED[key] = json.loads(json.dumps(compute()))      # the cache's own form
            CACHE.parent.mkdir(parents=True, exist_ok=True)
            CACHE.write_text(json.dumps({"key": key, "results": _COMPUTED[key]}) + "\n", encoding="utf-8")
    return _COMPUTED[key]


# ---------------------------------------------------------------- checks

def depth18_tau():
    c0, h0 = root(TM)
    return tau_f3(decode("0" * 18, split_sequence(h0, official_axis, 18), c0, h0)[1])


def w1_root(w):
    out, got = [], {}
    for n in (3, 5, 7):
        got[f"t{n}"] = t_text(n, d_star(TM))
        if abs(got[f"t{n}"] - w["t_text"][f"t{n}"]) > 1e-15:
            out.append(f"t_{n}(0.8365) = {got[f't{n}']!r}, text {w['t_text'][f't{n}']!r}")
    for d in (0.55, 0.7, 1.0, 1.5):
        hull = hull_pieces(placed_disc() + [(np.array([d, 0.0]), 0.0, None)], 1024)[0]
        if abs(hull - f_text(d)) > 1e-12:
            out.append(f"f({d}) = {f_text(d):.15f} is not the hull of the disc and a point, {hull:.15f}")
    w["w1"] = got
    return out


def w2_modes(w):
    out, comp = [], w["computed"]
    _, h0 = root(TM)
    reach = {n: math.hypot(h0[i], h0[i]) for n, i in ((3, 0), (5, 3))}
    reach[7] = math.hypot(t_text(7, d_star(TM)), t_text(7, d_star(TM)))
    fires = any(f_apr(d) >= T for d in reach.values())
    if (not fires) != w["apr_never_fires"]:
        out.append(f"APR {'can' if fires else 'cannot'} fire on the root (farthest centres {reach}), "
                   f"recorded never-fires {w['apr_never_fires']}")
    tau = depth18_tau()
    if abs(tau - w["tau18"]) > 1e-15:
        out.append(f"tau at depth 18 = {tau!r}, text {w['tau18']!r}")
    need = T + 4 * T * tau + math.pi * tau * tau
    top = max(v[1] for v in comp["sampled"]["official"]["hard"].values())
    if (top < need) != w["rep_blocked_at_18"]:
        out.append(f"REP needs a centre of {need:.6f} at depth 18; the highest HARD centre is {top:.6f}")
    fired = {f"{sch} {k}": [s["APR"], s["REP"]] for sch in ("sampled", "exact") for k, t in comp[sch].items()
             for s in [t["stats"][max(t["stats"], key=int)]]}
    if any(a or r for a, r in fired.values()):
        out.append(f"APR/REP closed cells: {fired}")
    # sec. 1's corner rule: a box wholly outside |t| <= t_n(0.835) in some body is excluded outright
    t3, t5 = t_text(3, d_star(T)), t_text(5, d_star(T))
    beyond = {}
    for name, target, rule, kinds in (("official", TM, "official", ("closed", "hard")),
                                      ("exact_tau", TM, "exact_tau", ("hard",)), ("immediate", T, "official", ("hard",))):
        c0, h0 = root(target)
        seq = split_sequence(h0, RULES[rule], 18)
        tree = comp["sampled"][name]
        for kind in kinds:
            n = 0
            for p in tree[kind]:
                c, h = decode(p, seq, c0, h0)
                n += box_distance(c[0:2], h[0:2]) > t3 or box_distance(c[3:5], h[3:5]) > t5
            beyond[f"{name} {kind}"] = n
    if (not any(beyond.values())) != w["corner_rule_idle"]:
        out.append(f"cells wholly beyond t_n(0.835): {beyond}")
    w["w2"] = {"farthest_centre": reach, "apr_value_everywhere": math.pi / 4, "rep_needs_centre": need,
               "highest_hard_centre": top, "cells_beyond_t_n": beyond}
    return out


def w3_schedulers(w):
    out = []
    c0, h0 = root(TM)
    off = split_sequence(h0, w["rules"]["official"], 18)
    ex = split_sequence(h0, w["rules"]["exact_tau"], 16)
    if off != [AXES.index(a) for a, _ in r12.greedy(h0, "mishra", 18)]:
        out.append("the official sequence is not Round 09's first-order rule")
    if ex != [AXES.index(a) for a, _ in r12.greedy(h0, "radius", 16)]:
        out.append("the exact-tau sequence is not Round 09's radius rule")
    for row in w["raw"]["depth18"]["top8"]:
        c, h = decode(row["path"], off, c0, h0)
        if np.max(np.abs(c - row["center"])) > 1e-15 or np.max(np.abs(h - row["half"])) > 1e-15:
            out.append(f"{row['path']} does not decode to its centre and half-widths")
    w["w3"] = {"official": [AXES[a] for a in off], "exact_tau": [AXES[a] for a in ex]}
    return out


def table_rows(summary):
    rows = {}
    for r in summary["scheduler_table"]:
        for k in ("official", "exact_tau"):
            rows[f"{k}@{r['depth']}"] = [r[k][m] for m in ("nodes", "APR", "REP", "CORE", "HARD")]
    m = summary["master_root_comparison"]
    rows["immediate@16"] = [m["immediate_root_0.835_depth16_official"][x] for x in ("nodes", "APR", "REP", "CORE", "HARD")]
    rows["master@16"] = [m["master_root_0.8365_depth16_official"][x] for x in ("nodes", "APR", "REP", "CORE", "HARD")]
    d = summary["depth18_official"]
    rows["official@18"] = [d["nodes"]] + [d["counts"][x] for x in ("APR", "REP", "CORE", "HARD")]
    return rows


def tree_rows(trees):
    got = {}
    for name, tree in trees.items():
        for d, s in tree["stats"].items():
            if int(d) >= 10 and int(d) % 2 == 0:
                got[f"{name}@{d}"] = [s[m] for m in ("nodes", "APR", "REP", "CORE", "HARD")]
    got["master@16"] = got["official@16"]
    return got


def w4_trees(w):
    out, comp = [], w["computed"]
    claimed = table_rows(w["summary"])
    sampled, exact = tree_rows(comp["sampled"]), tree_rows(comp["exact"])
    for key, row in claimed.items():
        if sampled.get(key) != row:
            out.append(f"{key}: sampled tree {sampled.get(key)}, package {row}")
    s = w["summary"]["depth16_scheduler_result"]
    red = lambda rows, i: (rows["exact_tau@16"][i] - rows["official@16"][i]) / rows["exact_tau@16"][i]
    if abs(red(sampled, 0) - s["official_node_reduction_vs_exact_fraction"]) > 1e-15 \
            or abs(red(sampled, 4) - s["official_hard_reduction_vs_exact_fraction"]) > 1e-15:
        out.append("the depth-16 reductions differ from the package's")
    for name in ("official", "exact_tau", "immediate"):
        extra = set(comp["exact"][name]["hard"]) - set(comp["sampled"][name]["hard"])
        if extra:
            out.append(f"{name}: {len(extra)} cells HARD under exact cores but not under the sampled bound")
    late = tree_rows(comp["late_ties"])
    changed = sorted(k for k in claimed if late.get(k) != sampled.get(k))
    if bool(changed) != w["ties_change_counts"]:
        out.append(f"with ties to the later axis the rows {'that change: ' + str(changed) if changed else 'do not change'}")
    keeps = {}
    for name, rows in (("exact", exact), ("late_ties", late)):
        keeps[name] = (rows["official@16"][0] < rows["exact_tau@16"][0] and rows["official@16"][4] < rows["exact_tau@16"][4]
                       and rows["master@16"][0] < rows["immediate@16"][0])
    if keeps != w["directions_hold"]:
        out.append(f"the scheduler and root comparisons keep their direction: {keeps}, recorded {w['directions_hold']}")
    w["w4"] = {"sampled": sampled, "exact": exact, "late_ties": late, "late_ties_changed_rows": changed,
               "reduction_depth16": {"sampled": [red(sampled, 0), red(sampled, 4)], "exact": [red(exact, 0), red(exact, 4)],
                                     "late_ties": [red(late, 0), red(late, 4)]}}
    return out


QS = (0, .01, .1, .25, .5, .75, .9, .99, 1)
NEAR = (0.00075, 0.001, 0.002, 0.005, 0.01, 0.02)


def profile(centres, tau):
    centres = np.asarray(centres)
    cyc = np.array([proxy_cycles(tau, a) for a in centres], dtype=float)
    return {"centre": {str(q): float(np.quantile(centres, q)) for q in QS},
            "cycles": {str(q): float(np.quantile(cyc, q)) for q in QS},
            "near": {str(m): int(np.sum(centres <= T + m)) for m in NEAR},
            "tail": {str(k): int(np.sum(cyc >= k)) for k in range(1, 9)},
            "below": int(np.sum(centres < T))}


def w5_frontier(w):
    out, comp, raw = [], w["computed"], w["raw"]["depth18"]
    hard = comp["sampled"]["official"]["hard"]
    tau = depth18_tau()
    got = profile([v[1] for v in hard.values()], tau)
    lbq = {str(q): float(np.quantile([v[0] for v in hard.values()], q)) for q in QS}
    for key, mine, theirs in (("centre", got["centre"], raw["center_area_quantiles"]),
                              ("lower bound", lbq, raw["lower_bound_quantiles"]),
                              ("cycles", got["cycles"], raw["cycles_quantiles"])):
        worst = max(abs(mine[q] - theirs[q]) for q in theirs)
        if worst > 1e-12:
            out.append(f"{key} quantiles differ by {worst:.2e}")
    if got["near"] != raw["near_counts"] or got["tail"] != raw["cycle_tail_ge"] or got["below"] != raw["center_below_target"]:
        out.append(f"near {got['near']}, tails {got['tail']}, below {got['below']} differ from the package")
    if len(hard) != raw["hard_count"] or any(abs(t - tau) > 1e-15 for t in raw["tau_quantiles"].values()):
        out.append("HARD count or tau differs")
    top = sorted(hard, key=lambda p: hard[p][1])[:8]
    if set(top) != {r["path"] for r in raw["top8"]}:
        out.append("the eight lowest centres are other cells")
    for r in raw["top8"]:
        v = hard.get(r["path"])
        if v is None or abs(v[1] - r["center_area"]) > 1e-12 or abs(v[0] - r["lower_bound"]) > 1e-12 \
                or proxy_cycles(tau, v[1]) != r["cycles"]:
            out.append(f"{r['path']}: centre, bound or cycles differ")
    t = got["tail"]
    tiers = {"tail_ge_7_cycles": t["7"], "tail_ge_5_cycles": t["5"], "middle_3_to_4_cycles": t["3"] - t["5"],
             "bulk_1_to_2_cycles": len(hard) - t["3"]}
    if tiers != w["summary"]["priority_tiers"]:
        out.append(f"tiers {tiers} differ from the package's")
    exact_c = comp["exact_centres"]
    loss = [exact_c[p] - hard[p][1] for p in hard]
    if min(loss) < 0:
        out.append(f"a sampled centre exceeds the exact one by {-min(loss):.2e}")
    ex = profile([exact_c[p] for p in hard], tau)
    mine = {"within_0002": ex["near"]["0.002"], "ge7": ex["tail"]["7"], "min_centre": round(min(exact_c.values()), 9)}
    if mine != w["exact_profile"]:
        out.append(f"exact-centre profile {mine}, recorded {w['exact_profile']}")
    w["w5"] = {"sampled": {k: got[k] for k in ("near", "tail")}, "exact_centres": {k: ex[k] for k in ("near", "tail")},
               "centre_loss": {"min": min(loss), "median": float(np.median(loss)), "max": max(loss)},
               "exact_min_centre": min(exact_c.values()), "tiers": tiers,
               "share_at_most_3_cycles": 1 - t["4"] / len(hard)}
    return out


def w6_minimizer(w):
    out, comp = [], w["computed"]
    a = base_area(QDAG)
    if abs(a - A_QDAG) > 1e-11 or a >= T:
        out.append(f"A(q-dagger) = {a!r}")
    LO, W = grid()
    cells = {name: cell_path(np.floor((q - LO) / W).astype(int)) for name, q in images().items()}
    if cells != w["image_cells"]:
        out.append(f"images of q-dagger lie in {cells}")
    hard = comp["sampled"]["official"]["hard"]
    lowest = set(sorted(hard, key=lambda p: hard[p][1])[:2])
    if lowest != {cells["Rq"], cells["R2q"]}:
        out.append(f"the two lowest cells {sorted(lowest)} are not those of the 2pi/3 turns")
    c0, h0 = root(TM)
    seq = split_sequence(h0, official_axis, 18)
    tau, finite, tiers = depth18_tau(), 0, {"Tail-A": 0, "Tail-B": 0, "Bulk": 0}
    sub = comp["subtarget"]["cells"]
    for p, v in sub.items():
        c, h = decode(p, seq, c0, h0)
        x = np.asarray(v["witness"])
        if np.any(x < c - h - 1e-12) or np.any(x > c + h + 1e-12) or base_area(x) >= T:
            out.append(f"{p}: the witness is not a configuration below the target in the cell")
        if p not in hard or p not in comp["exact"]["official"]["hard"]:
            out.append(f"{p}: holds a configuration below the target yet is closed")
            continue
        k = proxy_cycles(tau, hard[p][1])
        if k is not None:
            finite += 1
            tiers["Tail-A" if k >= 5 else "Tail-B" if k >= 3 else "Bulk"] += 1
    if len(sub) < w["subtarget_min_cells"]:
        out.append(f"{len(sub)} cells shown to hold a configuration below the target, recorded at least {w['subtarget_min_cells']}")
    if (finite == 0) != w["proxy_conservative"]:
        out.append(f"the proxy gives finite cycles to {finite} cells no base refinement closes")
    if tiers != w["subtarget_tiers"]:
        out.append(f"those cells fall in {tiers}, recorded {w['subtarget_tiers']}")
    closed = {k: sum(1 for left in v.values() if left == 0) for k, v in comp["proxy"].items()}
    if closed != w["proxy_sample_closed"]:
        out.append(f"of the sampled cells {closed} close within their predicted cycles")
    q = images()["q"]
    w["w6"] = {"A_qdag": a, "image_cells": cells, "qdag_to_faces": {"y3": abs(q[1]), "phi5": q[2], "y5": abs(q[4])},
               "subtarget_cells": len(sub), "subtarget_candidates": comp["subtarget"]["candidates"],
               "subtarget_tiers": tiers, "witness_areas": [min(v["area"] for v in sub.values()),
                                                           max(v["area"] for v in sub.values())],
               "witness_found_by": {h: sum(1 for v in sub.values() if v["how"] == h)
                                    for h in ("clipped image", "local search")},
               "subtarget_paths": sorted(sub), "proxy_sample_closed": closed}
    return out


def w7_lift(w):
    out, comp, raw = [], w["computed"], w["raw"]["depth18"]
    for r in raw["b7_probes"]:
        mine = comp["b7"]["sampled"].get(r["path"])
        if mine is None or [mine["nodes"], mine["closed"], mine["unresolved"]] != [r["nodes"], r["leaves"], r["unresolved"]] \
                or abs(mine["worst"] - r["worst"]) > 1e-12 or (mine["unresolved"] == 0) != r["closed"]:
            out.append(f"{r['path']}: probe {mine}, package {r}")
    for p, v in comp["b7"]["exact"].items():
        if [v["nodes"], v["closed"], v["unresolved"]] != w["b7_exact"]:
            out.append(f"{p}: exact probe {v}, recorded {w['b7_exact']}")
    if abs(t_text(7, d_star(TM)) - w["t_text"]["t7"]) > 1e-15:
        out.append("the lift root is not t_7(0.8365)")
    w["w7"] = comp["b7"]
    return out


def mirror_path(p):
    return "".join(str(1 - int(b)) if i in FLIP else b for i, b in enumerate(p))


def w8_symmetry(w):
    out, comp = [], w["computed"]
    rng, worst = np.random.default_rng(19), 0.0
    for _ in range(6):
        q = np.array([*rng.uniform(-0.15, 0.15, 2), rng.uniform(0, P5), *rng.uniform(-0.15, 0.15, 2)])
        a = base_area(q)
        worst = max(worst, abs(base_area(mirror(q)) - a), abs(base_area(turn(q)) - a), abs(base_area(turn(q, 2)) - a))
    if worst > 1e-13:
        out.append(f"the base area moves by {worst:.1e} under the mirror or the turn")
    unmatched = {}
    for sch in ("sampled", "exact"):
        tree = comp[sch]["official"]
        for kind in ("hard", "closed"):
            s = set(tree[kind])
            unmatched[f"{sch} {kind}"] = sum(1 for p in s if w["mirror_path"](p) not in s)
    if any(unmatched.values()):
        out.append(f"cells without a mirrored twin: {unmatched}")
    shift = (2 * math.pi / 3 % P5) / (math.pi / 40)
    if abs(shift - round(shift)) < 1e-9:
        out.append("the turn maps the depth-18 grid onto itself")
    hard = comp["sampled"]["official"]["hard"]
    a, b = sorted(hard, key=lambda p: hard[p][1])[:2]
    if w["mirror_path"](a) != b:
        out.append("the two lowest cells are not mirror twins")
    w["w8"] = {"invariance_worst": worst, "unmatched": unmatched, "turn_in_phi_cells": shift}
    return out


def p1_package(w):
    out, sq, cr = [], gate.squash(w["text"]), gate.squash(w["crystal"])
    s, raw, spec = w["summary"], w["raw"], w["spec"]
    if raw["depth18"] != s["depth18_official"]:
        out.append("the raw file is not the summary's depth-18 block")
    rows = table_rows(s)
    for d in (10, 12, 14, 16):
        for k, label in (("official", "official"), ("exact_tau", "exact-$\\tau$")):
            n, _, _, core, hard = rows[f"{k}@{d}"]
            if f"|{d}|{label}|{n:,}|{core:,}|{hard:,}|" not in sq:
                out.append(f"the text's table lacks the package's {k} row at depth {d}")
    for key, tail in (("immediate@16", "HARD={}."), ("master@16", "HARD={}.")):
        n, _, _, core, hard = rows[key]
        for frag in (f"N={n},", f"CORE={core},", tail.format(hard)):
            if frag not in sq:
                out.append(f"{key}: the text lacks {frag}")
    n, apr, rep, core, hard = rows["official@18"]
    for frag in (f"N={n}.", f"APR={apr},", f"REP={rep},", f"CORE={core},", f"HARD={hard}."):
        if frag not in sq:
            out.append(f"depth 18: the text lacks {frag}")
    r = s["depth16_scheduler_result"]
    for frac in (r["official_node_reduction_vs_exact_fraction"], r["official_hard_reduction_vs_exact_fraction"]):
        if f"{100 * frac:.2f}\\%" not in sq:
            out.append(f"the text does not round {frac} as the package has it")
    for key, val in s["root"].items():
        if key.startswith("t"):
            m = re.search(rf"t_{key[1]}=(0\.\d+)", sq)
            if m is None or float(m.group(1)) != val:
                out.append(f"{key}: package {val!r}, text {m and m.group(1)}")
    d = raw["depth18"]
    frags = [f"\\minA^-_{{\\rmcenter}}={d['center_area_quantiles']['0']!r}>0.835."]
    frags += [f"|$\\leT+{m}$|{c}|" for m, c in d["near_counts"].items()]
    frags += [f"Q_{{{q}}}={d['center_area_quantiles'][k]:.9f}," for q, k in (("0", "0"), ("0.01", "0.01"), ("0.10", "0.1"),
                                                                            ("0.50", "0.5"))]
    frags += [f"Q_{{{q}}}\\approx{d['lower_bound_quantiles'][k]:.9f}," for q, k in (("0.50", "0.5"), ("0.90", "0.9"),
                                                                                  ("0.99", "0.99"))]
    frags += [f"{d['lower_bound_quantiles']['1']:.9f}.", f"Q_{{0.99}}={d['center_area_quantiles']['0.99']:.9f}."]
    frags += [f"Q_{{{q}}}={int(d['cycles_quantiles'][k])}," for q, k in (("0.10", "0.1"), ("0.50", "0.5"), ("0.90", "0.9"),
                                                                        ("0.99", "0.99"))]
    frags += [f"\\max={int(d['cycles_quantiles']['1'])}.", f"\\ge3\\text{{cycles}}:{d['cycle_tail_ge']['3']},"]
    frags += [f"\\ge{k}:{d['cycle_tail_ge'][k]}," for k in ("4", "5", "6", "7")] + [f"\\ge8:{d['cycle_tail_ge']['8']}."]
    frags += [f"{d['top8'][0]['lower_bound']:.11f}."]
    p = d["b7_probes"]
    frags += [f"{p[0]['nodes']}\\text{{nodes}}", f"{p[0]['leaves']}\\text{{closedleaves}},",
              f"{p[0]['unresolved']}\\text{{unresolvedleaves}}."]
    tiers = s["priority_tiers"]
    frags += [f"\\boxed{{{tiers['tail_ge_5_cycles']}}}.", f"=\\boxed{{{tiers['middle_3_to_4_cycles']}}}.",
              f"=\\boxed{{{tiers['bulk_1_to_2_cycles']}}}."]
    out += [f"the text lacks {f}" for f in frags if f not in sq]
    if len({(x["nodes"], x["leaves"], x["unresolved"]) for x in p}) != 1:
        out.append("the two probes differ, though the text says each gives the same result")
    rec = spec["production_recommendation"]
    if rec["priority_tiers"] != {"tail_ge_7_cycles": d["cycle_tail_ge"]["7"], **{k: tiers[k] for k in
                                 ("tail_ge_5_cycles", "middle_3_to_4_cycles", "bulk_1_to_2_cycles")}} \
            or tiers["tail_ge_7_cycles"] != d["cycle_tail_ge"]["7"]:
        out.append("the long-run spec's tiers differ from the summary's")
    if spec["target"] != s["target"] or spec["phase_master_target"] != s["phase_master_target"] \
            or rec["master_root"] != s["phase_master_target"]:
        out.append("the long-run spec's targets differ from the summary's")
    crystal = [f"{rows['official@16'][0]:,}", f"{rows['exact_tau@16'][0]:,}", f"{rows['official@16'][4]:,}",
               f"{rows['exact_tau@16'][4]:,}", f"N={n},", f"CORE={core},", f"HARD={hard}.",
               f"{d['center_area_quantiles']['0']!r}.", f"within+0.002:{d['near_counts']['0.002']}",
               f"within+0.005:{d['near_counts']['0.005']}", f">=5cycles:{d['cycle_tail_ge']['5']}",
               f">=8cycles:{d['cycle_tail_ge']['8']}", f"{p[0]['nodes']:,}nodes", f"{p[0]['leaves']}closedleaves",
               f"{p[0]['unresolved']}unresolvedleaves", f"Tail-A:>=5cycles={tiers['tail_ge_5_cycles']}seeds.",
               f"Tail-B:3–4cycles={tiers['middle_3_to_4_cycles']:,}seeds.",
               f"Bulk:1–2cycles={tiers['bulk_1_to_2_cycles']:,}seeds."]
    out += [f"the crystal lacks {f}" for f in crystal if f not in cr]
    return out


def p2_package(w):
    out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]}
    v = w["validation"]
    for rec, leaf_id, text in ((v["round16"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"])):
        _, size, digest = leaves[leaf_id]
        if rec["sha256"] != digest or rec["bytes"] != size:
            out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive")
        n = text.count("$$")
        if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0):
            out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}")
        if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)):
            out.append(f"{rec['file']}: unicode-escape flag differs")
        if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)):
            out.append(f"{rec['file']}: bracket-delimiter flag differs")
    for key, leaf_id in (("pilot_summary_sha256", SUMMARY), ("depth18_raw_sha256", RAW), ("pilot_code_sha256", CODE)):
        if v[key] != leaves[leaf_id][2]:
            out.append(f"{key}: recorded digest differs from the archive")
    code = w["code"]
    runs = {int(x) for x in re.findall(r"run_base_pilot\(\s*\w+\s*,\s*(\d+)\s*,", code)}
    unrun = sorted({r["depth"] for r in w["summary"]["scheduler_table"]} - runs)
    keys = ("scheduler_table", "cycle_tail_ge", "b7_probes", "cap", "top8", "near_counts", "priority_tiers")
    unwritten = [k for k in keys if f"'{k}'" not in code and f'"{k}"' not in code]
    produced = not unrun and not unwritten
    if produced != w["code_produced_summary"]:
        out.append(f"the shipped code {'writes' if produced else 'does not write'} the shipped summary "
                   f"(depths it never runs: {unrun}; keys it never writes: {unwritten})")
    w["p2"] = {"code_runs_depths": sorted(runs), "summary_depths_not_run": unrun, "summary_keys_not_written": unwritten}
    return out


# ---------------------------------------------------------------- registry (Round 16)

TOKEN = "a proof-mode tag of sec. 2, defined there; not a judgment"
R16_DEFINITIONS = {
    "APR": ("in-line", "sec. 2: a cell closed by f(d), the hull of the disc and a body's centre at the cell's least "
                       "distance d"),
    "CORE": ("in-line", "sec. 2: a cell closed by the hull of finitely many boundary points of the disc and the "
                        "common erosion cores C_3, C_5"),
    "EMPIRICAL-COMPUTE-POLICY": ("in-line", "sec. 16, 24: a compute-scheduling recommendation drawn from pilot data, "
                                            "not a theorem assumption"),
    "HARD": ("in-line", "sec. 2: a cell no route closes by the pilot depth"),
    "MASTER-ROOT-PERFORMANCE-NOT-A-THEOREM": ("in-line", "sec. 20: the pilot's node counts for the 0.8365 root are "
                                                         "empirical"),
    "NUMERICAL-SYMMETRY-SIGNAL": ("in-line", "sec. 19: sign- and orientation-paired patterns among the lowest seeds; "
                                             "not a formal quotient theorem"),
    "R09-STRENGTHENING-EMPIRICAL-001": ("in-line", "sec. 5: an empirical addition to Round 09 (one-step tau "
                                                   "optimality is not tree-cost optimality), not a correction"),
    "VERIFIED-COMPUTATIONAL / PILOT": ("in-line", "sec. 2, 24: computed at finite pilot depth under the pilot's "
                                                  "floating policy (N_sample = 40, e_pilot = 1e-9); not a certificate"),
}
R16_REVIEWS = [
    ("NONE", "New rigorous lower bound", "reading", "PASS", "none is claimed and none follows"),
    ("YES", "Full global five-dimensional root used", "computation", "PASS",
     "t_3, t_5 at 0.8365 to 2e-16 and phi_5 over its whole period (W1); every tree here starts from it (W4)"),
    ("OPEN / COMPUTE-DEFERRED", "$a_{\\rm Leb}\\ge0.8350$", "n/a", "n/a", ""),
    ("REP", "", "n/a", "n/a", TOKEN + "; at depth 18 it needs a centre of 0.9685, above every HARD centre (W2)"),
    ("VERIFIED-COMPUTATIONAL / PILOT", "Finite-depth global pilot", "computation", "PASS",
     "every count, quantile, tail and top cell rebuilds exactly (W4, W5), but only under two choices the code makes and "
     "the text does not: the sampling (stated as 40 boundary points; fixed by the code as contact points in 40 "
     "directions) and both split rules' ties; with exact cores the depth-18 tree has 41899 nodes and 9234 HARD cells, "
     "all inside the pilot's 10448 (W4)"),
    ("VERIFIED-COMPUTATIONAL / PILOT", "Official vs exact-$\\tau$ scheduler comparison", "computation", "PASS",
     "the table rebuilds exactly (W4), with the code's ties to the earlier axis, which the text leaves open: broken the "
     "other way, exact-tau has 29571 nodes and 5688 HARD leaves at depth 16; with exact cores official still uses "
     "17.27% fewer nodes and 21.68% fewer HARD leaves; the direction holds every way"),
    ("APR", "", "n/a", "n/a", TOKEN + "; as defined it is pi/4 on the whole root, every centre lying within 0.287 of the "
                                      "origin, so it can never fire - not merely 'not yet' as sec. 7 says (W2)"),
    ("CORE", "", "n/a", "n/a", TOKEN),
    ("EMPIRICAL-COMPUTE-POLICY", "B7 base-first activation recommendation", "computation", "PASS",
     "the probes rebuild (2403 nodes, 568 closed, 634 open); with exact cores 2251/549/577, the same conclusion (W7)"),
    ("HARD", "", "n/a", "n/a", TOKEN),
    ("MASTER-ROOT-PERFORMANCE-NOT-A-THEOREM", "20. Master-root decision", "computation", "PASS",
     "23455 against 24691 nodes at depth 16 rebuilds; with exact cores 21971 against 22759 (W4)"),
    ("NUMERICAL-EVIDENCE", "Near-frontier compression signal", "computation", "PARTIAL",
     "the counts rebuild, but they measure the sampling: the 40-direction hull puts every HARD centre 1.6e-3 to 5.6e-3 "
     "low, and with exact centres no cell is within +0.002 (8 claimed) and none needs 7 cycles (8 claimed) (W5); the "
     "proxy, called conservative, gives 3 to 8 cycles to 19 cells that hold configurations below 0.835 and that no base "
     "refinement closes (W6)"),
    ("NUMERICAL-SYMMETRY-SIGNAL", "", "computation", "PASS",
     "stronger than numerical: the base area is invariant under the mirror and the 2pi/3 turn, the mirror maps the "
     "pilot grid onto itself and every closed and HARD cell to a twin, and the two lowest cells hold the turns of "
     "q-dagger (W6, W8); the turn does not map the grid"),
    ("R09-STRENGTHENING-EMPIRICAL-001", "", "reading", "PASS",
     "Round 09 claims one-step optimality only (RUN-012 W4); a tree-cost comparison cannot contradict it"),
]


def r1_registry(w):
    return registry.completeness(w["registry"], "R16", w["definitions"], w["reviews"])


# ---------------------------------------------------------------- world, checks, drill

CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_root, "W2": w2_modes, "W3": w3_schedulers, "W4": w4_trees,
          "W5": w5_frontier, "W6": w6_minimizer, "W7": w7_lift, "W8": w8_symmetry, "P1": p1_package,
          "P2": p2_package, "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "W1": {"t_text"},
           "W2": {"computed", "apr_never_fires", "tau18", "rep_blocked_at_18", "corner_rule_idle"},
           "W3": {"rules", "raw"}, "W4": {"computed", "summary", "ties_change_counts", "directions_hold"},
           "W5": {"computed", "raw", "summary", "exact_profile"},
           "W6": {"computed", "image_cells", "subtarget_min_cells", "proxy_conservative", "subtarget_tiers",
                  "proxy_sample_closed"},
           "W7": {"computed", "raw", "b7_exact", "t_text"}, "W8": {"computed", "mirror_path"},
           "P1": {"text", "crystal", "summary", "raw", "spec"},
           "P2": {"validation", "text", "crystal", "manifest", "code", "summary", "code_produced_summary"},
           "R1": {"registry", "definitions", "reviews"}}

CLAIMS = {
    "t_text": {"t3": 0.20102352900741122, "t5": 0.20261828623043526, "t7": 0.20147344578628750},
    "tau18": 0.03855318146790454,
    "apr_never_fires": True, "rep_blocked_at_18": True, "corner_rule_idle": True,
    "ties_change_counts": True, "directions_hold": {"exact": True, "late_ties": True},
    "exact_profile": {"within_0002": 0, "ge7": 0, "min_centre": 0.838555222},
    "image_cells": {"q": "010000011100111001", "Mq": "111011001010010100", "Rq": "101100100111001010",
                    "MRq": "000111110001100111", "R2q": "000111110001100111", "MR2q": "101100100111001010"},
    "subtarget_min_cells": 19, "proxy_conservative": False, "subtarget_tiers": {"Tail-A": 14, "Tail-B": 5, "Bulk": 0},
    "proxy_sample_closed": {"1": 40, "2": 40},
    "b7_exact": [2251, 549, 577],
    "code_produced_summary": False,
}
FNS = {"rules": RULES, "mirror_path": mirror_path}


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = {DOC, CRYSTAL, VALIDATION, SPEC, SUMMARY, RAW, CODE}
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None}
    return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"),
            "validation": json.loads(got[VALIDATION]), "spec": json.loads(got[SPEC]),
            "summary": json.loads(got[SUMMARY]), "raw": json.loads(got[RAW]), "code": got[CODE].decode("utf-8"),
            "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))}


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    inputs = load_inputs()
    results_computed = computed()

    def build():
        return {**copy.deepcopy(inputs), "computed": results_computed, "registry": registry.load(),
                "definitions": dict(R16_DEFINITIONS), "reviews": list(R16_REVIEWS), **copy.deepcopy(CLAIMS),
                "rules": dict(FNS["rules"]), "mirror_path": FNS["mirror_path"]}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {c: fn(w) for c, fn in CHECKS.items()}
    for c, f in results.items():
        print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n     {x}" for x in f[:6]))
    for key in ("w1", "w2", "w3", "w4", "w5", "w6", "w8", "p2"):
        print(key, json.dumps(w.get(key), default=float)[:700])
    if not args.drill:
        return
    s = inputs["summary"]
    raw = inputs["raw"]
    table = copy.deepcopy(s)
    table["scheduler_table"][2]["official"]["nodes"] = 11638
    near = copy.deepcopy(raw)
    near["depth18"]["near_counts"]["0.002"] = 9
    probe = copy.deepcopy(raw)
    probe["depth18"]["b7_probes"][0]["unresolved"] = 633
    spec = copy.deepcopy(inputs["spec"])
    spec["production_recommendation"]["priority_tiers"]["tail_ge_5_cycles"] = 143
    later = lambda h: 4 - int(np.argmax([h[4], h[3], R5 * h[2], h[1], h[0]]))     # ties to the later axis
    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()),
        ("K2-mirror-by-index-complement", "control",
         {"mirror_path": lambda p: "".join(b if i not in FLIP else "10"[int(b)] for i, b in enumerate(p))}, set()),
        ("K3-exact-tau-by-round09-greedy", "control",
         {"rules": {**RULES, "exact_tau": lambda h: AXES.index(r12.greedy(h, "radius", 1)[0][0])}}, set()),
        ("M1-doc-depth18-nodes", "mutation", {"text": inputs["text"].replace("N=45651.", "N=45661.")}, {"A0", "P1"}),
        ("M2-root-t3-digit", "mutation", {"t_text": {**CLAIMS["t_text"], "t3": 0.20102352900742122}}, {"W1"}),
        ("M3-apr-assumed-live", "mutation", {"apr_never_fires": False}, {"W2"}),
        ("M20-corner-rule-needed", "mutation", {"corner_rule_idle": False}, {"W2"}),
        ("M4-official-ties-late", "mutation", {"rules": {**RULES, "official": later}}, {"W3"}),
        ("M5-table-count", "mutation", {"summary": table}, {"W4", "P1"}),
        ("M6-near-count", "mutation", {"raw": near}, {"W5", "P1"}),
        ("M7-exact-profile-as-sampled", "mutation", {"exact_profile": {**CLAIMS["exact_profile"], "within_0002": 8}},
         {"W5"}),
        ("M8-turn-image-cell", "mutation", {"image_cells": {**CLAIMS["image_cells"], "Rq": "010000011100111001"}},
         {"W6"}),
        ("M9-proxy-conservative", "mutation", {"proxy_conservative": True}, {"W6"}),
        ("M10-subtarget-in-bulk", "mutation", {"subtarget_tiers": {"Tail-A": 13, "Tail-B": 5, "Bulk": 1}}, {"W6"}),
        ("M11-probe-count", "mutation", {"raw": probe}, {"W7", "P1"}),
        ("M12-exact-probe-closes", "mutation", {"b7_exact": [2251, 549, 0]}, {"W7"}),
        ("M13-mirror-flips-x3", "mutation",
         {"mirror_path": lambda p: "".join(str(1 - int(b)) if i in {3, 8, 13} else b for i, b in enumerate(p))}, {"W8"}),
        ("M14-directions-lost", "mutation", {"directions_hold": {"exact": False, "late_ties": True}}, {"W4"}),
        ("M19-ties-immaterial", "mutation", {"ties_change_counts": False}, {"W4"}),
        ("M15-spec-tier", "mutation", {"spec": spec}, {"P1"}),
        ("M16-code-digest", "mutation", {"validation": {**inputs["validation"], "pilot_code_sha256": "0" * 64}}, {"P2"}),
        ("M17-code-wrote-summary", "mutation", {"code_produced_summary": True}, {"P2"}),
        ("M18-review-dropped", "mutation", {"reviews": list(R16_REVIEWS[1:])}, {"R1"}),
    ]
    if args.blind:
        cases = [c for c in cases if args.blind in c[3]]
    d = gate.run_drill(build, CHECKS, DEPENDS, cases)
    summary = gate.summarize(d, CHECKS)
    print(gate.report_drill(summary))
    for x in d:
        if not x["ok"]:
            print("   DRILL FAIL", x)
    if args.blind:
        n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"])
        print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)")
        return
    log = {"run": "RUN-019", "subject": "Round 16: the capacity-aware global master-root pilot", "document": DOC,
           "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "w6", "w7", "w8", "p2")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=float) + "\n", encoding="utf-8")
    if not results["R1"]:
        registry.record("R16", "RUN-019", R16_DEFINITIONS, R16_REVIEWS)
        print(f"registry: {len(R16_DEFINITIONS)} definitions, {len(R16_REVIEWS)} reviews recorded for R16")


if __name__ == "__main__":
    main()