"""RUN-047 - UESFCM Cycles 10-11: the 27- and 617-root finite erosion certificates and the two-root frontier.

Cycle 10 closes Cycle 09's 27 closest roots with a binary-subdivision certificate: one bit per node in preorder
(1 split, 0 leaf), a deterministic split, and at each leaf either the box lies wholly inside the F3 ball, or the
hull of a finite witness set - the disc's inscribed 256-gon and 256 points on each eroded Reuleaux core - less a
safe 1e-9 exceeds A3+. Cycle 11 certifies 617 of the other 622 near-ceiling roots the same way, and localizes the
last five by budgeted search to 225 subroots under two parents, 6217 and 3766. Here the trees are decoded (the
split rule read from the package's verifier after two guesses of this tree's failed), and every leaf is bounded
twice: with this tree's own implementation of the witness set, and in exact arithmetic with this tree's exact
eroded cores. The search logs and the frontier are checked against the certificate and each other.

Checks
  A0 anchors      the numbers below occur in the two documents as written
  X1 paper        Mishra's sec. 5.4 floating-point model, the source of the cycles' eta_model
  W1 roots        the 27 and the 617 roots against Cycles 07 and 09's files
  W2 trees        the trees decoded: every bit used, the per-tree and total counts; the float split's tiling
  W3 witness      every leaf's finite-witness bound (rebuilt here): all pass after 1e-9; the least slacks; eta_model
  W4 exact        every area leaf certified in exact arithmetic with the exact eroded cores; the NOT-F3 leaves
  W5 search       Cycle 11's search logs against the certificate and each other; the two-root frontier
  W6 crystals     the two state crystals against the numbers rebuilt here
  W7 code         the two verifiers, read after the rebuild and never run
  P1 package      the VALIDATION records; Cycle 10's dependency copies

Usage: python code/run047_uesfcm_cycles_10_11.py [--refresh] [--drill] [--blind CID]
"""
import argparse
import base64
import copy
import datetime
import hashlib
import inspect
import io
import json
import math
import re
from fractions import Fraction
from multiprocessing import Pool

import mpmath
import numpy as np
from scipy.spatial import ConvexHull

import gate
import run019_round16_global_pilot as r19
import run030_round27_interval_replay as r30
import run044_uesfcm_cycles_01_03 as r44
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run009_round06_witness_exchange import hull_pieces, placed_disc
from run011_round08_conditional_lift import placed_vertices
from run012_round09_adaptive_atlas import base_core_pieces, core_pieces
from run013_round10_reference_dry_run import contact_points

FOLDER = "main.zip!/UESFCM/"
PKG = {i: FOLDER + f"UESFCM_Lebesgue_Cycle_{i:02d}_Package_v0.1.zip!/" for i in (7, 9, 10, 11)}
DOCS = {10: PKG[10] + "UESFCM_Lebesgue_Cycle_10_27Root_Finite_Closure_v0.1.md",
        11: PKG[11] + "UESFCM_Lebesgue_Cycle_11_617Root_Batch_and_TwoRoot_Frontier_v0.1.md"}
CERTS = {10: PKG[10] + "UESFCM_Lebesgue_Cycle_10_27Root_F3_Certificate.json",
         11: PKG[11] + "UESFCM_Lebesgue_Cycle_11_617Root_F3_Certificate.json"}
DATA = {"frontier": PKG[7] + "UESFCM_Lebesgue_Cycle_07_F3_Unresolved_Frontier.npz",
        "taylor": PKG[9] + "UESFCM_Lebesgue_Cycle_09_Taylor_Diagnostic.npz",
        "two": PKG[11] + "UESFCM_Lebesgue_Cycle_11_TwoRoot_Hard_Frontier.npz",
        "summary": PKG[11] + "UESFCM_Lebesgue_Cycle_11_TwoRoot_Frontier_Summary.json"}
AUDITS = {"batch": PKG[11] + "audit/c11_probe_5000.json", "hard5": PKG[11] + "audit/UESFCM_Lebesgue_Cycle_11_Hard5_Probe.json",
          "round2": PKG[11] + "audit/UESFCM_Lebesgue_Cycle_11_HardFrontier_Round2_Probe.json",
          "round3": PKG[11] + "audit/UESFCM_Lebesgue_Cycle_11_HardFrontier_Round3_Probe.json",
          "non6217": PKG[11] + "audit/UESFCM_Lebesgue_Cycle_11_Non6217_Probe.json",
          "r3766": PKG[11] + "audit/UESFCM_Lebesgue_Cycle_11_3766_Probe.json"}
CODE = {10: PKG[10] + "UESFCM_Lebesgue_Cycle_10_Verify_27Root_F3.py", 11: PKG[11] + "UESFCM_Lebesgue_Cycle_11_Verify_617Root_F3.py"}
COPIES = {PKG[10] + "dependencies/UESFCM_Lebesgue_Cycle_07_F3_Unresolved_Frontier.npz": DATA["frontier"],
          PKG[10] + "dependencies/UESFCM_Lebesgue_Cycle_09_Taylor_Diagnostic.npz": DATA["taylor"]}
CRYSTALS = {i: PKG[i] + f"UESFCM_Lebesgue_State_Crystal_Cycle_{i:02d}_v0.1.json" for i in (10, 11)}
VALIDATIONS = {i: PKG[i] + f"UESFCM_Lebesgue_Cycle_{i:02d}_VALIDATION.json" for i in (10, 11)}
LOG = TREE / "data" / "gate-logs" / "run047-uesfcm-cycles-10-11.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CACHE = TREE / "data" / "cache" / "run047-searches.json"     # data/cache is not committed
SNAPSHOT = TREE / "data" / "external" / "uesfcm-c10-c11-mishra.json"

MISHRA = ("2608.30538", 2)
# short phrases of sec. 1 and 5.4 only, matched in the full text of v2 (the page itself is never kept)
MISHRA_FACTS = {
    "no_intervals": r"We do not use interval arithmetic\.",
    "acceptance": r"\| p − V j \( n \) \| ≤ 1 − δ n \+ ϑ .{0,60}with ϑ = 10 − 12",
    "distance": r"relative error at most 4 𝐮 .{0,20}with 𝐮 = 2 − 53",
    "trig": r"a further 8 𝐮 R .{0,20}is allowed for their coordinates, with R = 0\.70 \+ R 3",
    "eps0": r"by at most ε 0 = 1\.0016 × 10 − 12",
    "hull_excess": r"by at most ε 0 P \+ π ε 0 2",
    "perimeter": r"so P ≤ 8\.026",
    "hull_term": r"This contributes at most 8\.04 × 10 − 12",
    "gamma": r"γ N = N 𝐮 / \( 1 − N 𝐮 \)",
    "points": r"at most m \+ 2 K = 3072",
    "sum": r"S ≤ N R 2 = 5012",
    "shoelace": r"The contribution is at most 1\.71 × 10 − 9",
    "eta": r"Writing η = 1\.72 × 10 − 9",
}

A3, S_F3, X30, ETA = r44.A3, 0.00882, -0.01215883209899, 1e-9
A3_EXACT, S_EXACT, X30_EXACT = Fraction(834781191, 10 ** 9), Fraction(882, 10 ** 5), Fraction(-1215883209899, 10 ** 14)
R3, R5 = 1 / math.sqrt(3), 1 / (2 * math.cos(math.pi / 10))
M_DISC = K_CORE = 256
HARD = [3766, 6217, 8001, 8015, 8016]
INWARD, DIRECTIONS, WORKERS = 1e-12, (1024, 4096, 16384), 6
PERIMETER = 8.026                     # Mishra's bound on the hull's perimeter, the area's Lipschitz constant


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = (set(DOCS.values()) | set(CERTS.values()) | set(DATA.values()) | set(AUDITS.values()) | set(CODE.values()) | set(COPIES)
            | set(CRYSTALS.values()) | set(VALIDATIONS.values()))
    listing, got = [], {}
    for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want):
        listing.append(leaf.id)
        if d is not None:
            got[leaf.id] = d
    rows = {row[0]: row for row in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"]}
    npz = lambda k: {name: a for name, a in np.load(io.BytesIO(got[DATA[k]])).items()}
    return {"texts": {i: got[DOCS[i]].decode("utf-8") for i in DOCS}, "code": {i: got[CODE[i]].decode("utf-8") for i in CODE},
            "certs": {i: json.loads(got[CERTS[i]]) for i in CERTS}, "frontier": npz("frontier"),
            "taylor": {k: v.tolist() for k, v in npz("taylor").items()},
            "two": {k: v.tolist() for k, v in npz("two").items()},       # lists: the drill compares plants by ==
            "summary": json.loads(got[DATA["summary"]]), "audits": {k: json.loads(got[v]) for k, v in AUDITS.items()},
            "crystals": {i: json.loads(got[CRYSTALS[i]]) for i in CRYSTALS},
            "validations": {i: json.loads(got[VALIDATIONS[i]]) for i in VALIDATIONS},
            "package11": sorted(x.split(PKG[11])[-1] for x in listing if x.startswith(PKG[11])),
            "files": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want}}


# ---------------------------------------------------------------- the trees

def bits_of(b64, n):
    raw = base64.b64decode(b64)
    return [(raw[i // 8] >> (7 - i % 8)) & 1 for i in range(n)]


def d3_upper(c, h):
    return math.hypot(abs(c[0] - X30) + h[0], abs(c[1]) + h[1])


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


def split(c, h):
    """the widest coordinate by the weights: while the box may still meet the F3 ball, B3's translation first; once
    it is wholly outside, B5's turn and translation first (the package's rule; the first index wins a tie)"""
    if d3_lower(c, h) >= S_F3:
        w = [0.7 * h[0], 0.7 * h[1], 1.5 * R5 * h[2], 1.5 * h[3], 1.5 * h[4]]
    else:
        w = [1.5 * h[0], 1.5 * h[1], R5 * h[2], h[3], h[4]]
    k = max(range(5), key=lambda i: (w[i], -i))
    lo, hi, hh = list(c), list(c), list(h)
    lo[k] -= h[k] / 2.0
    hi[k] += h[k] / 2.0
    hh[k] = h[k] / 2.0
    return (lo, hh), (hi, list(hh)), k


def decode(tree):
    """the tree's leaves (centre, half-widths, depth) in preorder, its node count, and whether exactly its bits are used"""
    bits = bits_of(tree["bits_base64"], tree["bit_count"])
    out, stack, pos = [], [(list(tree["root_center"]), list(tree["root_halfwidth"]), 0)], 0
    while stack:
        if pos >= len(bits):
            return out, pos, False
        c, h, depth = stack.pop()
        b = bits[pos]
        pos += 1
        if b:
            (c1, h1), (c2, h2), _ = split(c, h)
            stack.append((c2, h2, depth + 1))
            stack.append((c1, h1, depth + 1))
        else:
            out.append((c, h, depth))
    return out, pos, pos == len(bits)


def tree_stats(tree):
    leaves, nodes, full = decode(tree)
    area = sum(1 for c, h, _ in leaves if d3_upper(c, h) >= S_F3)
    return {"node_count": nodes, "area_leaf_count": area, "not_f3_leaf_count": len(leaves) - area,
            "max_depth": max((d for _, _, d in leaves), default=0), "full": full}


def tiling(certs):
    """every split, in exact arithmetic: do the two children cover the parent box, and how far do they overlap"""
    out = {}
    for cid, cert in certs.items():
        gap = over = 0.0
        splits = exact = 0
        totals = {"nodes": 0, "area": 0, "notf3": 0, "depth": 0}
        for t in cert["trees"]:
            s = tree_stats(t)
            totals["nodes"] += s["node_count"]
            totals["area"] += s["area_leaf_count"]
            totals["notf3"] += s["not_f3_leaf_count"]
            totals["depth"] = max(totals["depth"], s["max_depth"])
            bits = bits_of(t["bits_base64"], t["bit_count"])
            stack, pos = [(t["root_center"], t["root_halfwidth"])], 0
            while stack:
                c, h = stack.pop()
                b = bits[pos]
                pos += 1
                if not b:
                    continue
                (c1, h1), (c2, h2), k = split(c, h)
                splits += 1
                low = (Fraction(c1[k]) - Fraction(h1[k])) - (Fraction(c[k]) - Fraction(h[k]))
                mid = (Fraction(c2[k]) - Fraction(h2[k])) - (Fraction(c1[k]) + Fraction(h1[k]))
                high = (Fraction(c[k]) + Fraction(h[k])) - (Fraction(c2[k]) + Fraction(h2[k]))
                gap = max(gap, float(low), float(mid), float(high))
                over = max(over, float(-mid))
                exact += low == 0 and mid == 0 and high == 0
                stack.append((c2, h2))
                stack.append((c1, h1))
        out[str(cid)] = {"splits": splits, "exact": exact, "gap": gap, "overlap": over, **totals}
    return out


# ---------------------------------------------------------------- the finite witness bound, rebuilt

RING = 0.5 * np.stack([np.cos(2 * np.pi * np.arange(M_DISC) / M_DISC), np.sin(2 * np.pi * np.arange(M_DISC) / M_DISC)], axis=1)


def witness_core(V, rho):
    """the witness set of the core, the intersection of the discs D(V_j, rho): its corners and, on the arc about
    each corner, round(K span / total) - 1 interior points evenly spaced in angle; None when degenerate"""
    O = V.mean(axis=0)
    if rho <= 1e-12 or rho < float(np.max(np.linalg.norm(V - O, axis=1))) - 1e-15:
        return None
    n = len(V)
    if any(float(np.linalg.norm(V[(k + 1) % n] - V[k])) > 2 * rho for k in range(n)):
        return None
    corners = core_pieces(V, rho)[1]
    spans = []
    for k in range(n):
        a0 = math.atan2(*(corners[k - 1] - V[k])[::-1])
        spans.append((k, a0, (math.atan2(*(corners[k] - V[k])[::-1]) - a0) % (2 * math.pi)))
    total = sum(s for _, _, s in spans)
    pts = [np.array(corners)]
    for k, a0, s in spans:
        m = max(1, int(round(K_CORE * s / total)))
        t = a0 + s * np.arange(1, m) / m
        pts.append(V[k] + rho * np.stack([np.cos(t), np.sin(t)], axis=1))
    W = np.vstack(pts)
    far = np.sqrt(((W[:, None, :] - V[None, :, :]) ** 2).sum(-1)).max(axis=1)
    W = W[far <= rho + 1e-12]
    return W if len(W) >= 3 else None


def lemma18(d):
    return math.pi / 4 if d <= 0.5 else 0.25 * (math.pi - math.acos(0.5 / d)) + 0.5 * math.sqrt(d * d - 0.25)


def erosion(h):
    return math.hypot(h[0], h[1]), math.hypot(h[3], h[4]) + 2 * R5 * math.sin(h[2] / 2)


def witness_points(c, h):
    """Lemma 18's a-priori term at the nearest centres, and the ring with the two witness sets (None if a core is
    degenerate)"""
    near3 = math.hypot(max(abs(c[0]) - h[0], 0.0), max(abs(c[1]) - h[1], 0.0))
    near5 = math.hypot(max(abs(c[3]) - h[3], 0.0), max(abs(c[4]) - h[4], 0.0))
    d3, d5 = erosion(h)
    W3 = witness_core(placed_vertices(3, 0.0, c[0:2]), 1 - d3)
    W5 = witness_core(placed_vertices(5, c[2], c[3:5]), 1 - d5)
    return max(lemma18(near3), lemma18(near5)), None if W3 is None or W5 is None else np.vstack([RING, W3, W5])


def witness_bound(c, h):
    """(bound, whether the a-priori term decided it): the larger of that term and the witness hull"""
    ap, pts = witness_points(c, h)
    if pts is None:
        return ap, True
    hull = float(ConvexHull(pts).volume)
    return max(ap, hull), ap > hull


def witness_scan(certs):
    """every area leaf's witness bound: failures after 1e-9, the least raw slack and its leaf, the leaves the a-priori
    term decides, and each tree's least raw slack; on Cycle 10's leaves also the double-precision hull against the
    exact hull of the same points"""
    out = {}
    for cid, cert in certs.items():
        least, fail, prior, n, per_tree, hull_error = [math.inf, None, None, None], 0, 0, 0, [], 0.0
        for t in cert["trees"]:
            tl = math.inf
            for c, h, _ in decode(t)[0]:
                if d3_upper(c, h) < S_F3:
                    continue
                lb, ap = witness_bound(c, h)
                if str(cid) == "10":
                    pts = witness_points(c, h)[1]
                    exact = r30.exact_hull_area([(float(x), float(y)) for x, y in pts])[0]
                    hull_error = max(hull_error, float(abs(Fraction(float(ConvexHull(pts).volume)) - exact)))
                s = lb - A3
                n += 1
                prior += ap
                fail += s - ETA <= 0
                tl = min(tl, s)
                if s < least[0]:
                    least = [s, t["frontier_index"], c, h]
            per_tree.append(None if tl == math.inf else tl)
        out[str(cid)] = {"leaves": n, "failing": fail, "apriori": prior, "least": least, "per_tree": per_tree, "hull_error": hull_error}
    return out


def precise_witness(c, h, dps=50):
    """the witness bound of one leaf with every point and the shoelace carried at dps digits (the vertex order taken
    from the double-precision hull, which the extra digits cannot change beyond 10^-30)"""
    mp = mpmath.mp
    mp.dps = dps
    two_pi = 2 * mp.pi

    def corners_of(n, phi, t):
        R = 1 / (2 * mpmath.cos(mp.pi / (2 * n)))
        return [(mp.mpf(t[0]) + R * mpmath.cos(phi + two_pi * j / n), mp.mpf(t[1]) + R * mpmath.sin(phi + two_pi * j / n)) for j in range(n)]

    def core(V, rho):
        n = len(V)
        O = (sum(v[0] for v in V) / n, sum(v[1] for v in V) / n)
        P = []
        for k in range(n):
            a, b = V[k], V[(k + 1) % n]
            M = ((a[0] + b[0]) / 2, (a[1] + b[1]) / 2)
            f = mpmath.sqrt(rho ** 2 - ((b[0] - a[0]) ** 2 + (b[1] - a[1]) ** 2) / 4) / mpmath.hypot(O[0] - M[0], O[1] - M[1])
            P.append((M[0] + f * (O[0] - M[0]), M[1] + f * (O[1] - M[1])))
        spans = []
        for k in range(n):
            a0 = mpmath.atan2(P[k - 1][1] - V[k][1], P[k - 1][0] - V[k][0])
            spans.append((k, a0, (mpmath.atan2(P[k][1] - V[k][1], P[k][0] - V[k][0]) - a0) % two_pi))
        total = sum(s for _, _, s in spans)
        pts = list(P)
        for k, a0, s in spans:
            m = max(1, int(mpmath.nint(K_CORE * s / total)))
            pts += [(V[k][0] + rho * mpmath.cos(a0 + s * i / m), V[k][1] + rho * mpmath.sin(a0 + s * i / m)) for i in range(1, m)]
        return pts

    d3 = mpmath.hypot(h[0], h[1])
    d5 = mpmath.hypot(h[3], h[4]) + 2 / (2 * mpmath.cos(mp.pi / 10)) * mpmath.sin(mp.mpf(h[2]) / 2)
    pts = [(mpmath.cos(two_pi * k / M_DISC) / 2, mpmath.sin(two_pi * k / M_DISC) / 2) for k in range(M_DISC)]
    pts += core(corners_of(3, mp.mpf(0), c[0:2]), 1 - d3) + core(corners_of(5, mp.mpf(c[2]), c[3:5]), 1 - d5)
    order = ConvexHull(np.array([[float(x), float(y)] for x, y in pts])).vertices
    twice = mpmath.fsum(pts[order[i - 1]][0] * pts[order[i]][1] - pts[order[i]][0] * pts[order[i - 1]][1] for i in range(len(order)))
    slack = twice / 2 - mp.mpf("0.834781191")
    mp.dps = 15
    return float(slack), mpmath.nstr(slack, 20)


# ---------------------------------------------------------------- the exact certification

def certify(c, h, n_dir):
    """exact lower bound on the hull area over the box, less A3+: the contact points of the disc and of the two exact
    eroded cores at n_dir directions, each moved 1e-12 toward its body's centre and proved inside its body (the disc
    exactly, a core against its corners enclosed in 400-bit intervals), and the exact hull of those that pass"""
    th = 2 * np.pi * np.arange(n_dir) / n_dir
    k3, k5 = r19.cores(np.asarray(c, dtype=float), np.asarray(h, dtype=float))
    if k3 is None or k5 is None:
        return None, 0
    pts, owner = [], []
    for b, (body, ctr) in enumerate(((placed_disc(), (0.0, 0.0)), (k3, c[0:2]), (k5, c[3:5]))):
        p = contact_points(body, th)
        pts.append(p + INWARD * (np.asarray(ctr, dtype=float) - p))
        owner += [b] * len(p)
    pts = np.vstack(pts)
    cores = {1: r30.core(3, 0.0, c[0:2], (0.0, h[0], h[1]), False), 2: r30.core(5, c[2], c[3:5], h[2:5], False)}
    verified, fail = [], 0
    for i in ConvexHull(pts).vertices:
        x, y, b = float(pts[i][0]), float(pts[i][1]), owner[i]
        if b == 0:
            ok = Fraction(x) ** 2 + Fraction(y) ** 2 < Fraction(1, 4)
        else:
            ok = r30.inside((r30.exact(x), r30.exact(y)), *cores[b])
        if ok:
            verified.append((x, y))
        else:
            fail += 1
    return r30.exact_hull_area(verified)[0] - A3_EXACT, fail


def exact_tree(task):
    """one tree: every area leaf certified, the directions raised until it passes; every NOT-F3 leaf's box proved
    inside the ball (its farthest corner from the anchor nearer than 0.00882, in exact arithmetic)"""
    cid, t = task
    out = {"cert": cid, "root": t["frontier_index"], "area": 0, "certified": 0, "failures": 0, "escalated": 0, "least": None,
           "notf3": 0, "notf3_inside": 0, "notf3_least": None}
    for c, h, _ in decode(t)[0]:
        if d3_upper(c, h) < S_F3:
            far2 = (abs(Fraction(c[0]) - X30_EXACT) + Fraction(h[0])) ** 2 + (abs(Fraction(c[1])) + Fraction(h[1])) ** 2
            m = float(S_EXACT ** 2 - far2) / (float(S_EXACT) + math.sqrt(float(far2)))
            out["notf3"] += 1
            out["notf3_inside"] += far2 < S_EXACT ** 2
            out["notf3_least"] = m if out["notf3_least"] is None else min(out["notf3_least"], m)
            continue
        out["area"] += 1
        margin, used = None, None
        for n_dir in DIRECTIONS:
            m, fail = certify(c, h, n_dir)
            out["failures"] += fail
            if m is not None and m > 0:
                margin, used = m, n_dir
                break
        out["escalated"] += used != DIRECTIONS[0]
        if margin is not None:
            out["certified"] += 1
            if out["least"] is None or margin < Fraction(out["least"][0]):
                out["least"] = [f"{margin.numerator}/{margin.denominator}", t["frontier_index"], c, h, used]
    return out


def exact_scan(certs):
    tasks = sorted(((cid, t) for cid, cert in certs.items() for t in cert["trees"]), key=lambda x: -x[1]["node_count"])
    with Pool(WORKERS) as pool:
        rows = pool.map(exact_tree, tasks, chunksize=1)
    out = {}
    for cid in certs:
        mine = [r for r in rows if r["cert"] == cid]
        least = min((r["least"] for r in mine if r["least"]), key=lambda x: Fraction(x[0]))
        nl = [r["notf3_least"] for r in mine if r["notf3_least"] is not None]
        out[str(cid)] = {"area": sum(r["area"] for r in mine), "certified": sum(r["certified"] for r in mine),
                         "failures": sum(r["failures"] for r in mine), "escalated": sum(r["escalated"] for r in mine),
                         "least": [float(Fraction(least[0])), *least[1:]], "least_exact": least[0],
                         "notf3": sum(r["notf3"] for r in mine), "notf3_inside": sum(r["notf3_inside"] for r in mine),
                         "notf3_least": min(nl) if nl else None}
    return out


def exact_core_area(c, h):
    """this tree's exact eroded-core hull (closed form, in floats), robust to the grid"""
    P = base_core_pieces(np.asarray(c, dtype=float), np.asarray(h, dtype=float), lambda d: 1 - d)
    for n in (4096, 4093, 2048, 8191, 16381):
        try:
            return hull_pieces(P, n)[0]
        except RuntimeError:
            continue
    raise RuntimeError("no grid resolved the hand-overs")


# ---------------------------------------------------------------- the two-root frontier

def descend(C, H, root, tc, th):
    """the split path from the root's box to the box (tc, th), or None"""
    c, h, path = C[root].tolist(), H[root].tolist(), ""
    while len(path) <= 80:
        if c == tc and h == th:
            return path
        (c1, h1), (c2, h2), k = split(c, h)
        c, h, path = (c1, h1, path + "0") if tc[k] < c[k] else (c2, h2, path + "1")
    return None


def frontier_scan(two, C, H):
    """the 225 subroots: reached from their parent root by the split, how far they leave it, whether any contains
    another, how far unrelated ones overlap; their centre witness values and exact centre areas"""
    pc, ph, par = two["centers"], two["halfwidths"], [int(p) for p in two["parent_root"]]
    paths = [descend(C, H, par[i], pc[i], ph[i]) for i in range(len(pc))]
    fr = lambda x: Fraction(x)
    excursion = max(float(max(fr(C[par[i]][k]) - fr(H[par[i]][k]) - fr(pc[i][k]) + fr(ph[i][k]),
                              fr(pc[i][k]) + fr(ph[i][k]) - fr(C[par[i]][k]) - fr(H[par[i]][k]))) for i in range(len(pc)) for k in range(5))
    nested = over = 0
    widest = 0.0
    for i in range(len(pc)):
        for j in range(i + 1, len(pc)):
            if par[i] != par[j]:
                continue
            ext = [min(fr(pc[i][k]) + fr(ph[i][k]), fr(pc[j][k]) + fr(ph[j][k])) - max(fr(pc[i][k]) - fr(ph[i][k]), fr(pc[j][k]) - fr(ph[j][k]))
                   for k in range(5)]
            if all(e > 0 for e in ext):
                if paths[i] is not None and paths[j] is not None and (paths[i].startswith(paths[j]) or paths[j].startswith(paths[i])):
                    nested += 1
                else:
                    over += 1
                    widest = max(widest, float(min(ext)))
    cw, ce = {}, {}
    for i in range(len(pc)):
        cw.setdefault(str(par[i]), []).append(witness_bound(pc[i], [0.0] * 5)[0])
        ce.setdefault(str(par[i]), []).append(exact_core_area(pc[i], [0.0] * 5))
    return {"reached": sum(p is not None for p in paths), "depth": [min(len(p) for p in paths if p is not None), max(len(p) for p in paths if p is not None)],
            "stored_depth_is_path": sum(p is not None and len(p) == d for p, d in zip(paths, two["depth"])),
            "excursion": excursion, "nested": nested, "overlapping": over, "overlap": widest,
            "duplicates": len(pc) - len({(par[i], paths[i]) for i in range(len(pc))}),
            "centre_witness": {k: min(v) for k, v in cw.items()}, "centre_exact": {k: min(v) for k, v in ce.items()}}


TREE_HELPERS = (bits_of, d3_upper, d3_lower, split, decode)
WITNESS_HELPERS = TREE_HELPERS + (witness_core, lemma18, erosion, witness_points, witness_bound)
HELPERS = {"tiling": TREE_HELPERS + (tree_stats,), "witness": WITNESS_HELPERS, "precise": (),
           "exact": TREE_HELPERS + (certify, exact_tree, r19.cores, contact_points),
           "frontier": WITNESS_HELPERS + (descend, exact_core_area)}


def _key(name, fn, extra=""):
    """a search's cache key: its own source, its helpers' sources, the kernel files it rests on, and its inputs"""
    import run008_round05_saturation_gate as r8
    import run009_round06_witness_exchange as r9
    digest = hashlib.sha256(inspect.getsource(fn).encode())
    for helper in HELPERS[name]:
        digest.update(inspect.getsource(helper).encode())
    for path in (r8.__file__, r9.__file__, r30.__file__):
        digest.update(open(path, "rb").read())
    digest.update(extra.encode())
    return digest.hexdigest()


def searches(inputs):
    """each search cached under its own key"""
    cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {}
    certs, fronts = inputs["certs"], inputs["frontier"]
    tag = hashlib.sha256(json.dumps(certs, sort_keys=True).encode()).hexdigest()
    out, changed = {}, False

    def get(name, fn, call, extra=""):
        nonlocal changed
        key = _key(name, fn, extra)
        if cached.get(name, {}).get("key") != key:
            cached[name] = {"key": key, "value": call()}
            changed = True
            CACHE.parent.mkdir(parents=True, exist_ok=True)
            CACHE.write_text(json.dumps(cached, indent=1) + "\n", encoding="utf-8")
        out[name] = cached[name]["value"]

    get("tiling", tiling, lambda: tiling(certs), tag)
    get("witness", witness_scan, lambda: witness_scan(certs), tag)
    get("precise", precise_witness, lambda: {cid: precise_witness(*out["witness"][cid]["least"][2:4]) for cid in ("10", "11")}, tag)
    get("exact", exact_scan, lambda: exact_scan(certs), tag)
    get("frontier", frontier_scan, lambda: frontier_scan(inputs["two"], fronts["centers"], fronts["halfwidths"]),
        hashlib.sha256(json.dumps(inputs["two"]).encode()).hexdigest())
    return out


def world(inputs):
    return {**inputs, "search": searches(inputs)}


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

ANCHORS = {
    10: {"W1": [r"27\text{priorityroots}.", r"\mathcalR_{27}", "`PRIORITYROOTS:27`", "`PRIORITYROOTSCLOSED:27/27`"],
         "W2": [r"\boxed{2{,}699}", r"\boxed{1{,}363.}", r"\boxed{13.}", r"\boxed{2{,}153}", "`TOTALCERTIFICATENODES:2699`", "`AREALEAVES:1363`",
                "`MAXDEPTH:13`", "one-bit-per-nodeDFSpreordertree"],
         "W3": [r"m=256,\qquadK=256,", r"|t|\le0.70", r"\boxed{\eta_{\mathrm{model}}\le1.149\times10^{-10}.}", r"\eta_{\mathrm{safe}}=10^{-9}.",
                r"\boxed{3.8179493\times10^{-8}.}", r"1.1488\times10^{-10},", r"\boxed{332\times.}", r"\boxed{3.7179493\times10^{-8}>0.}",
                r"\boxed{\le1.2\times10^{-15}.}", "`MINRAWLEAFSLACK:3.8179493e-8`", "`FLOATERRORMODEL:~1.149e-10`", "`SAFESUBTRACTION:1e-9`",
                "`MINVERIFIEDSLACK:>3.7179e-8`"],
         "W4": [r"\widehat\beta(\mathcalB)\le\inf_{v\in\mathcalB}A(v).", "本輪27roots沒有需要`NOT-F3`leaf才能完成"]},
    11: {"W1": [r"\boxed{622}", "`INPUTNEAR-CEILINGROOTS:622`"],
         "W2": [r"\boxed{109{,}037.}", r"\boxed{54{,}786.}", r"\boxed{41.}", r"\boxed{16.}", "`617-ROOTNODES:109037`", "`617-ROOTAREALEAVES:54786`"],
         "W3": [r"\boxed{1.5376482309648054\times10^{-9}>0.}", "`MINVERIFIEDSLACK:1.537648e-9`"],
         "W5": [r"\boxed{616/622}", r"3766,\quad6217,\quad8001,\quad8015,\quad8016,\quad8018.", r"\boxed{13{,}181}", r"\boxed{51}",
                r"\boxed{40/51}", r"\boxed{91}", r"\boxed{63/91}", r"\boxed{242}", "3766:32,", "6217:200,", "8001:3,", "8016:7.",
                r"\boxed{39/42}", r"\boxed{28/31}", r"\boxed{225}", r"\boxed{6217:200}", r"\boxed{3766:25.}", r"\boxed{0.8349695459154723.}",
                r"\boxed{1.88355\times10^{-4}.}", r"\boxed{0.8352612051955018.}", r"\boxed{4.80014\times10^{-4}.}",
                r"\frac{200}{225}\approx88.9\%.", "`FINALHARDSUBROOTFRONTIER:225`", "`8001/8015/8016:SEARCH-CLOSED/PACKAGING-DEBT`"]},
}

CLAIMS = {
    "paper_claim": {"missing": [], "eps0": 1.0016e-12, "perimeter": 8.0258, "hull_term": 8.04e-12, "shoelace_term": 1.7095e-09, "sum_S": 5012.35,
                    "eta": 1.7176e-09},
    "roots_claim": {"c10": [27, True], "c11": [617, True], "boxes": True, "disjoint": True},
    "tree_claim": {"c10": {"wrong_trees": [], "totals": [2699, 1363, 0, 13], "summary_equal": True, "largest": [8006, 2153],
                           "tiling": [1336, 280, 2.5e-18, 3.3e-18], "gap_area": 2e-17},
                   "c11": {"wrong_trees": [], "totals": [109037, 54786, 41, 16], "summary_equal": True, "largest": [8018, 13181],
                           "tiling": [54210, 15915, 4.7e-18, 3.3e-18], "gap_area": 3.7e-17}},
    "witness_claim": {"c10": {"leaves": 1363, "failing": 0, "apriori": 0, "least": [3.8179494e-08, 8006], "precise": 3.81794932e-08},
                      "c11": {"leaves": 54786, "failing": 0, "apriori": 0, "least": [2.5376479e-09, 21309], "precise": 2.53764884e-09},
                      "differences": {"c10_search": 8.9e-16, "c10_verifier": 8.6e-16, "c11_verifier": -3.6e-16, "c10_precise_vs_theirs": 2.7e-16,
                                      "c10_precise_vs_mine": -5.9e-16, "c11_precise_vs_theirs": 6.1e-16, "c11_precise_vs_mine": 9.7e-16},
                      "c11_per_tree": [0, 7e-16], "eta_model": [True, 1.1488e-10, 3.4e-16, True], "c10_hull_error": 1e-15},
    "exact_claim": {"c10": {"area": 1363, "certified": 1363, "failures": 0, "escalated": 0, "least": [2.352e-05, 8006, 1024], "notf3": [0, 0],
                            "notf3_least": None},
                    "c11": {"area": 54786, "certified": 54786, "failures": 0, "escalated": 0, "least": [2.277e-05, 20561, 1024], "notf3": [41, 41],
                            "notf3_least": 1.31e-05}},
    "search_claim": {"batch": [622, True, 616, [3766, 6217, 8001, 8015, 8016, 8018], True, True], "certificate": [616, True, 13181, True],
                     "without_area_leaves": [7989],
                     "chain": {"hard5": True, "round2": True, "round3": True, "non6217": True, "r3766": True, "final": True},
                     "chain_counts": [51, 91, 242, 31, 25],
                     "frontier": {"by_parent": {"3766": 25, "6217": 200}, "reached": 225, "depth": [4, 28], "stored_depth_is_path": 225,
                                  "excursion": 2.3e-18, "nested": 0, "overlapping": 489, "overlap": 5.9e-18, "duplicates": 0},
                     "centre": {"6217": [0.8349695459155, -2e-16, 0.0, 0.8350052734], "3766": [0.8352612051955, -1e-16, 0.0, 0.8353009037]},
                     "summary": [True, True]},
    "crystal_claim": {"C10": [True, True, True, True, -9e-16, True, True], "C11": [True, True, True, True, 4e-16, True, True]},
    "code_facts": {"lines": {10: 210, 11: 87},
                   "defs": {10: ["reuleaux_corners", "f_apriori", "core_points", "hull_area_hand", "box_lower", "d3_upper", "d3_lower", "split_box",
                                 "unpack_bits", "verify"],
                            11: ["pair_lt", "quicksort_idx", "cross", "hull_area_numba", "unpack"]},
                   "imports": {10: ["base64", "json", "math", "numpy", "sys"], 11: ["argparse", "base64", "importlib", "json", "numba", "numpy", "sys", "time"]},
                   "c10": {"weights": [".7*h[0],.7*h[1],1.5*CIRC5*h[2],1.5*h[3],1.5*h[4]", "1.5*h[0],1.5*h[1],CIRC5*h[2],h[3],h[4]"],
                           "asserts_constants": True, "eta_from_certificate": True, "accept_tolerance": True},
                   "c11": {"loads_c10_by_absolute_path": True, "ships_it": False, "numba": True, "checks_constants": False, "eta_fixed": True}},
    "package_claim": {"C10": True, "C11": True, "statuses": True, "replays": True, "manifest": True, "copies": True, "stub_digest_unmatched": True},
}


def sig(x, n=4):
    return float(f"{x:.{n - 1}e}")


def eta_model(n_points, eps0=None, perimeter=None):
    """Mishra sec. 5.4: eps0 P + pi eps0^2 for points accepted up to eps0 outside their body, and gamma_N S for the
    shoelace, gamma_N = N u / (1 - N u), S <= N R^2, R = 0.70 + R3. Unless given, his constants unrounded: the
    tolerance 1e-12, the distance's 4u and the corners' 8uR, so eps0 = 1e-12 + 4u + 8uR; the hull inside the disc of
    radius R, so P <= 2 pi R"""
    u, R = 2.0 ** -53, 0.70 + R3
    eps0 = 1e-12 + 4 * u + 8 * u * R if eps0 is None else eps0
    perimeter = 2 * math.pi * R if perimeter is None else perimeter
    return eps0 * perimeter + math.pi * eps0 ** 2 + n_points * u / (1 - n_points * u) * (n_points * R * R)


def a0_anchors(w):
    out = []
    for i, groups in ANCHORS.items():
        text = gate.squash(w["texts"][i])
        out += [f"Cycle {i:02d} {cid}: anchor not found: {a[:50]}" for cid, frags in groups.items() for a in frags if a not in text]
    return out


def x1_paper(w):
    """Mishra's sec. 5.4 (the model Cycle 10 cites): the acceptance tolerance and the error terms, and whether his
    own numbers follow from his constants"""
    f = w["snapshot"]["facts"]
    n = 3072
    got = {"missing": sorted(k for k in MISHRA_FACTS if not f.get(k)),
           "eps0": sig(1e-12 + 4 * 2.0 ** -53 + 8 * 2.0 ** -53 * (0.70 + R3), 5), "perimeter": round(2 * math.pi * (0.70 + R3), 4),
           "hull_term": sig(1.0016e-12 * PERIMETER + math.pi * 1.0016e-12 ** 2, 3),
           "shoelace_term": sig(eta_model(n, 0.0, 0.0), 5), "sum_S": round(n * (0.70 + R3) ** 2, 2),
           "eta": sig(eta_model(n, 1.0016e-12, PERIMETER), 5)}
    w["x1"] = got
    return [] if got == w["paper_claim"] else [f"Mishra's sec. 5.4: {got}"]


def w1_roots(w):
    """Cycle 10's roots are Cycle 09's 27 closest, in its order; Cycle 11's are the other 649 - 27 but the five hard
    ones; every root box is Cycle 07's row to the bit"""
    T, C, H = w["taylor"], w["frontier"]["centers"], w["frontier"]["halfwidths"]
    near, close = [int(i) for i in T["frontier_indices"]], [int(i) for i in T["closest_frontier_indices"]]
    r10 = [t["frontier_index"] for t in w["certs"][10]["trees"]]
    r11 = [t["frontier_index"] for t in w["certs"][11]["trees"]]
    got = {"c10": [len(r10), r10 == close], "c11": [len(r11), r11 == sorted(set(near) - set(close) - set(HARD))],
           "boxes": all(t["root_center"] == C[t["frontier_index"]].tolist() and t["root_halfwidth"] == H[t["frontier_index"]].tolist()
                        for i in (10, 11) for t in w["certs"][i]["trees"]),
           "disjoint": not set(r10) & set(r11)}
    w["w1"] = got
    return [] if got == w["roots_claim"] else [f"the roots: {got}"]


def w2_trees(w):
    """the trees decoded with the split: every bit used; each tree's stored counts; the totals and the documents'
    summaries; the float split's tiling, and the area's Lipschitz bound across its widest gap"""
    got, bad = {}, []
    for i in (10, 11):
        cert = w["certs"][i]
        stats = [tree_stats(t) for t in cert["trees"]]
        wrong = [t["frontier_index"] for t, s in zip(cert["trees"], stats)
                 if not s["full"] or any(t[k] != s[k] for k in ("node_count", "area_leaf_count", "not_f3_leaf_count", "max_depth"))]
        tot = [sum(s["node_count"] for s in stats), sum(s["area_leaf_count"] for s in stats), sum(s["not_f3_leaf_count"] for s in stats),
               max(s["max_depth"] for s in stats)]
        sm = cert["summary"]
        stored = [sm["total_nodes"], sm.get("total_area_leaves", sm.get("area_leaf_count")),
                  sm.get("total_not_f3_leaves", sm.get("not_f3_leaf_count")), sm["max_depth"]]
        biggest = max(zip(stats, cert["trees"]), key=lambda x: x[0]["node_count"])
        til = w["search"]["tiling"][str(i)]
        got[f"c{i}"] = {"wrong_trees": wrong, "totals": tot, "summary_equal": tot == stored, "largest": [biggest[1]["frontier_index"], biggest[0]["node_count"]],
                        "tiling": [til["splits"], til["exact"], sig(til["gap"], 2), sig(til["overlap"], 2)],
                        "gap_area": sig(PERIMETER * til["gap"] + math.pi * til["gap"] ** 2, 2)}
        if til["gap"] * PERIMETER >= w["search"]["witness"][str(i)]["least"][0] - ETA:
            bad.append(f"Cycle {i}: the widest gap is not covered by the least slack")
    w["w2"] = got
    return bad + ([] if got == w["tree_claim"] else [f"the trees: {got}"])


def w3_witness(w):
    """every area leaf's witness bound rebuilt here: none fails after 1e-9, none decided by the a-priori term; the
    least raw slacks against the certificates and VALIDATION records, and at 50 digits; Cycle 11's per-tree minima;
    eta_model from Mishra's sec. 5.4 constants with m = K = 256"""
    S, got = w["search"], {}
    for i in (10, 11):
        s = S["witness"][str(i)]
        got[f"c{i}"] = {"leaves": s["leaves"], "failing": s["failing"], "apriori": s["apriori"], "least": [sig(s["least"][0], 8), s["least"][1]],
                        "precise": sig(S["precise"][str(i)][0], 9)}
    c10, c11, v10, v11 = w["certs"][10]["summary"], w["certs"][11]["trees"], w["validations"][10], w["validations"][11]
    mine10, mine11 = S["witness"]["10"]["least"][0], S["witness"]["11"]["least"][0]
    theirs = {"c10_search": c10["minimum_raw_area_leaf_slack"], "c10_verifier": v10["replay_verifier"]["minimum_verified_slack"] + ETA,
              "c11_verifier": v11["independent_replay"]["minimum_verified_slack"] + ETA}
    got["differences"] = {"c10_search": sig(mine10 - theirs["c10_search"], 2), "c10_verifier": sig(mine10 - theirs["c10_verifier"], 2),
                          "c11_verifier": sig(mine11 - theirs["c11_verifier"], 2),
                          "c10_precise_vs_theirs": sig(S["precise"]["10"][0] - theirs["c10_verifier"], 2),
                          "c10_precise_vs_mine": sig(S["precise"]["10"][0] - mine10, 2),
                          "c11_precise_vs_theirs": sig(S["precise"]["11"][0] - theirs["c11_verifier"], 2),
                          "c11_precise_vs_mine": sig(S["precise"]["11"][0] - mine11, 2)}
    per = [(a, t["min_raw_search_slack"]) for a, t in zip(S["witness"]["11"]["per_tree"], c11)]
    got["c11_per_tree"] = [sum((a is None) != (b is None) for a, b in per), sig(max(abs(a - b) for a, b in per if a is not None and b is not None), 1)]
    em = eta_model(M_DISC + 2 * K_CORE)
    got["eta_model"] = [em == w["certs"][10]["constants"]["ETA_MODEL_RECOMPUTED"], sig(em, 5),
                        sig(eta_model(M_DISC + 2 * K_CORE, 1.0016e-12, PERIMETER) - em, 2),
                        c10["minimum_raw_area_leaf_slack"] / em == c10["raw_slack_over_eta_model"]]
    got["c10_hull_error"] = sig(S["witness"]["10"]["hull_error"], 1)
    w["w3"] = got
    return [] if got == w["witness_claim"] else [f"the witness bound: {got}"]


def w4_exact(w):
    """every area leaf certified in exact arithmetic (none uncertified, no candidate failing its membership proof);
    the least certified margins; every NOT-F3 leaf's box inside the F3 ball"""
    got = {}
    for i in (10, 11):
        e = w["search"]["exact"][str(i)]
        got[f"c{i}"] = {"area": e["area"], "certified": e["certified"], "failures": e["failures"], "escalated": e["escalated"],
                        "least": [sig(e["least"][0], 4), e["least"][1], e["least"][4]], "notf3": [e["notf3"], e["notf3_inside"]],
                        "notf3_least": None if e["notf3_least"] is None else sig(e["notf3_least"], 3)}
    w["w4"] = got
    ok = all(v["certified"] == v["area"] and v["failures"] == 0 and v["notf3"][0] == v["notf3"][1] for v in got.values())
    return [] if ok and got == w["exact_claim"] else [f"the exact certification: {got}"]


def w5_search(w):
    """Cycle 11 sec. 2-12: the 5,000-node batch against the certificate; the chain of targeted layers, each fed by the
    last; the two-root frontier's boxes and its centre diagnostic"""
    A, T = w["audits"], w["taylor"]
    near, close = [int(i) for i in T["frontier_indices"]], [int(i) for i in T["closest_frontier_indices"]]
    b = A["batch"]
    res = {r["idx"]: r for r in b["results"]}
    closed = sorted(i for i, r in res.items() if r["closed"])
    tree = {t["frontier_index"]: t for t in w["certs"][11]["trees"]}
    none = lambda x: None if x is None or x == math.inf else x        # a tree without area leaves: None here, Infinity there
    same = sum(1 for i in closed if (tree[i]["node_count"], tree[i]["area_leaf_count"], tree[i]["not_f3_leaf_count"], tree[i]["max_depth"],
                                     none(tree[i]["min_raw_search_slack"])) == (res[i]["nodes"], res[i]["area"], res[i]["notf"], res[i]["maxd"], none(res[i]["minraw"])))
    got_empty = sorted(i for i in closed if tree[i]["area_leaf_count"] == 0)
    got = {"batch": [len(res), sorted(res) == sorted(set(near) - set(close)), len(closed), sorted(set(res) - set(closed)),
                     b["total_nodes"] == sum(r["nodes"] for r in res.values()), b["closed"] == len(closed)],
           "certificate": [same, sorted(tree) == sorted(closed + [8018]), tree[8018]["node_count"],
                           sum(t["node_count"] for t in tree.values()) == sum(res[i]["nodes"] for i in closed) + tree[8018]["node_count"]],
           "without_area_leaves": got_empty}
    two, fs, sm = w["two"], w["search"]["frontier"], w["summary"]["two_root_frontier"]
    par = [int(p) for p in two["parent_root"]]

    def step(r):
        rows = r["results"]
        return [r["input_roots"] == len(rows), r["closed"] == sum(x["closed"] for x in rows), r["hard"] == sum(not x["closed"] for x in rows),
                r["new_frontier_roots"] == sum(x["remaining"] for x in rows if not x["closed"]), r["visited_nodes"] == sum(x["nodes"] for x in rows)]

    def left(r):
        out = {}
        for x in r["results"]:
            if not x["closed"]:
                out[str(x["parent"])] = out.get(str(x["parent"]), 0) + x["remaining"]
        return out

    fed = lambda r: {k: v["input"] for k, v in r["by_parent"].items()}
    h5, r2, r3, n6, r37 = A["hard5"], A["round2"], A["round3"], A["non6217"], A["r3766"]
    first = {str(s["idx"]): s["remaining"] for s in h5["stats"]}
    chain = {"hard5": [[s["idx"] for s in h5["stats"]] == HARD, h5["frontier_roots"] == sum(first.values())],
             "round2": step(r2) + [fed(r2) == first], "round3": step(r3) + [fed(r3) == left(r2)],
             "non6217": step(n6) + [fed(n6) == {k: v for k, v in left(r3).items() if k != "6217"}],
             "r3766": step(r37) + [r37["input_roots"] == left(n6).get("3766")],
             "final": [{str(k): par.count(k) for k in sorted(set(par))} == {"3766": r37["new_frontier_roots"], "6217": left(r3).get("6217")}]}
    got["chain"] = {k: all(v) for k, v in chain.items()}
    got["chain_counts"] = [h5["frontier_roots"]] + [A[k]["new_frontier_roots"] for k in ("round2", "round3", "non6217", "r3766")]
    got["frontier"] = {"by_parent": {str(k): par.count(k) for k in sorted(set(par))}, "reached": fs["reached"], "depth": fs["depth"],
                       "stored_depth_is_path": fs["stored_depth_is_path"], "excursion": sig(fs["excursion"], 2), "nested": fs["nested"],
                       "overlapping": fs["overlapping"], "overlap": sig(fs["overlap"], 2), "duplicates": fs["duplicates"]}
    diag = sm["center_finite_witness_diagnostic"]
    got["centre"] = {k: [sig(fs["centre_witness"][k], 13), sig(fs["centre_witness"][k] - diag[f"{k}_min"], 1),
                         sig(diag[f"{k}_gap_above_ceiling"] - (diag[f"{k}_min"] - A3), 1), sig(fs["centre_exact"][k], 10)] for k in ("6217", "3766")}
    got["summary"] = [sm["total_subroots"] == len(par), sm["by_parent"] == got["frontier"]["by_parent"]]
    w["w5"] = got
    return [] if got == w["search_claim"] else [f"Cycle 11's search: {got}"]


def w6_crystals(w):
    """the two state crystals against the numbers rebuilt here"""
    c10, c11, S = w["crystals"][10]["priority_tier"], w["crystals"][11], w["search"]
    t10, t11, s10, s11 = S["tiling"]["10"], S["tiling"]["11"], S["witness"]["10"], S["witness"]["11"]
    par = [int(p) for p in w["two"]["parent_root"]]
    got = {"C10": [c10["roots"] == c10["closed"] == len(w["certs"][10]["trees"]), c10["certificate_nodes"] == t10["nodes"],
                   c10["area_leaves"] == t10["area"] == s10["leaves"], c10["max_depth"] == t10["depth"],
                   sig(c10["min_raw_slack"] - s10["least"][0], 1), c10["min_verified_slack"] == c10["min_raw_slack"] - c10["eta_safe"],
                   c10["eta_model"] == eta_model(M_DISC + 2 * K_CORE)],
           "C11": [c11["formal_batch"]["input_roots"] == 649 - 27, c11["formal_batch"]["verified_closed_roots"] == len(w["certs"][11]["trees"]),
                   c11["formal_batch"]["nodes"] == t11["nodes"], c11["formal_batch"]["area_leaves"] == t11["area"] == s11["leaves"],
                   sig(c11["formal_batch"]["minimum_verified_slack"] - (s11["least"][0] - ETA), 1),
                   [c11["persistent_research_families"]["6217_subroots"], c11["persistent_research_families"]["3766_subroots"]] == [par.count(6217), par.count(3766)],
                   c11["packaging_debt"] == sorted(set(HARD) - set(par))]}
    w["w6"] = got
    return [] if got == w["crystal_claim"] else [f"the crystals: {got}"]


def w7_code(w):
    """the two verifiers, read after the rebuild and never run"""
    code = w["code"]

    def imports(t):
        mods = set()
        for line in t.splitlines():
            s = line.strip()
            if s.startswith("import "):
                mods |= {p.strip().split(" as ")[0].split(".")[0] for p in s[7:].split(",")}
            elif s.startswith("from "):
                mods.add(s[5:].split()[0].split(".")[0])
        return sorted(mods)

    got = {"lines": {i: t.count("\n") for i, t in code.items()}, "defs": {i: re.findall(r"^def (\w+)", t, re.M) for i, t in code.items()},
           "imports": {i: imports(t) for i, t in code.items()},
           "c10": {"weights": re.findall(r"^\s*w=np\.array\(\[(.*)\]\)\s*$", code[10], re.M),
                   "asserts_constants": 'assert C["K_core"]==K and C["M_disk"]==M' in code[10], "eta_from_certificate": 'eta=float(C["ETA_SAFE"])' in code[10],
                   "accept_tolerance": "d.max(axis=1)<=rho+1e-12" in code[10]},
           "c11": {"loads_c10_by_absolute_path": bool(re.search(r"spec_from_file_location\('v','(/|[A-Za-z]:)", code[11])),
                   "ships_it": any("Verify_27Root" in x for x in w["package11"]), "numba": "from numba import njit" in code[11],
                   "checks_constants": "constants" in code[11], "eta_fixed": "ETA=1e-9" in code[11]}}
    w["w7"] = got
    return [] if got == w["code_facts"] else [f"the verifiers: {got}"]


def p1_package(w):
    """each VALIDATION digest against the bytes hashed here and the archive's manifest; the replay numbers against
    this tree's; Cycle 10's copies of Cycle 07's frontier and Cycle 09's diagnostic byte-identical to theirs"""
    files = w["files"]
    sha = lambda k: hashlib.sha256(files[k]).hexdigest()
    v10, v11 = w["validations"][10], w["validations"][11]
    t10, t11 = w["search"]["tiling"]["10"], w["search"]["tiling"]["11"]
    rp10, rp11 = v10["replay_verifier"], v11["independent_replay"]
    checks = {"C10": [v10["paper_sha256"] == sha(DOCS[10]), v10["certificate_sha256"] == sha(CERTS[10]), v10["state_sha256"] == sha(CRYSTALS[10]),
                      v10["standalone_verifier"]["sha256"] == sha(CODE[10]), v10["standalone_verifier"]["status"] == "PASS"],
              "C11": [v11["paper_sha256"] == sha(DOCS[11]), v11["certificate_sha256"] == sha(CERTS[11]), v11["verifier_sha256"] == sha(CODE[11]),
                      v11["frontier_sha256"] == sha(DATA["two"]), v11["frontier_summary_sha256"] == sha(DATA["summary"]), v11["state_sha256"] == sha(CRYSTALS[11])],
              "statuses": [v10["status"] == "PASS", v11["status"] == "PASS", rp11["status"] == "PASS"],
              "replays": [[rp10["roots"], rp10["nodes"], rp10["area_leaves"], rp10["not_f3_leaves"]] == [27, t10["nodes"], t10["area"], t10["notf3"]],
                          [rp11["roots"], rp11["nodes"], rp11["area_leaves"], rp11["not_f3_leaves"]] == [617, t11["nodes"], t11["area"], t11["notf3"]],
                          f"nodes: {t10['nodes']}" in v10["standalone_verifier"]["stdout"]],
              "manifest": [w["manifest_rows"][k][2] == sha(k) for k in sorted(files)],
              "copies": [files[c] == files[o] for c, o in COPIES.items()]}
    got = {k: all(v) for k, v in checks.items()}
    got["stub_digest_unmatched"] = v10["verifier_stub_sha256"] not in {sha(k) for k in files}
    w["p1"] = got
    return [k for k, v in checks.items() if not all(v)] + ([] if got == w["package_claim"] else [f"the package: {got}"])


CHECKS = {"A0": a0_anchors, "X1": x1_paper, "W1": w1_roots, "W2": w2_trees, "W3": w3_witness, "W4": w4_exact, "W5": w5_search, "W6": w6_crystals,
          "W7": w7_code, "P1": p1_package}
DEPENDS = {"A0": {"texts"}, "X1": {"snapshot", "paper_claim"}, "W1": {"certs", "taylor", "frontier", "roots_claim"},
           "W2": {"certs", "search", "tree_claim"}, "W3": {"search", "certs", "validations", "witness_claim"}, "W4": {"search", "exact_claim"},
           "W5": {"audits", "taylor", "certs", "two", "search", "summary", "search_claim"},
           "W6": {"crystals", "certs", "search", "two", "crystal_claim"}, "W7": {"code", "package11", "code_facts"},
           "P1": {"validations", "files", "manifest_rows", "search", "package_claim"}}


def drill_cases(base):
    def edit(obj, fn):
        x = copy.deepcopy(obj)
        fn(x)
        return x

    texts, s = base["texts"], base["search"]

    def flip_last_bit(x):
        t = x[10]["trees"][1]
        raw = bytearray(base64.b64decode(t["bits_base64"]))
        i = t["bit_count"] - 1
        raw[i // 8] ^= 1 << (7 - i % 8)
        t["bits_base64"] = base64.b64encode(bytes(raw)).decode()

    def swap_roots(x):
        x[10]["trees"][0], x[10]["trees"][1] = x[10]["trees"][1], x[10]["trees"][0]

    closed = next(r["idx"] for r in base["audits"]["batch"]["results"] if r["closed"])
    return [
        ("K0-unmodified", "control", {}, set()),
        ("K1-crlf", "control", {"texts": {i: t.replace("\n", "\r\n") for i, t in texts.items()}, "code": {i: t.replace("\n", "\r\n") for i, t in base["code"].items()}},
         set()),
        ("K2-validation-keys-sorted", "control", {"validations": {i: json.loads(json.dumps(v, sort_keys=True)) for i, v in base["validations"].items()}}, set()),
        ("M1-node-total-text", "mutation", {"texts": {**texts, 10: texts[10].replace("2{,}699", "2{,}698")}}, {"A0"}),
        ("M2-snapshot-eps0", "mutation", {"snapshot": edit(base["snapshot"], lambda x: x["facts"].update(eps0=None))}, {"X1"}),
        ("M3-root-order", "mutation", {"certs": edit(base["certs"], swap_roots)}, {"W1"}),
        ("M4-flipped-bit", "mutation", {"certs": edit(base["certs"], flip_last_bit)}, {"W2"}),
        ("M5-tree-count", "mutation", {"certs": edit(base["certs"], lambda x: x[10]["trees"][2].update(area_leaf_count=x[10]["trees"][2]["area_leaf_count"] + 1))},
         {"W2"}),
        ("M6-tiling-gap", "mutation", {"search": edit(s, lambda x: x["tiling"]["11"].update(gap=1e-9))}, {"W2"}),
        ("M7-witness-least", "mutation", {"search": edit(s, lambda x: x["witness"]["11"]["least"].__setitem__(0, x["witness"]["11"]["least"][0] - 1e-13))},
         {"W3", "W6"}),
        ("M8-eta-model", "mutation", {"certs": edit(base["certs"], lambda x: x[10]["constants"].update(ETA_MODEL_RECOMPUTED=1.1488e-10))}, {"W3"}),
        ("M9-exact-margin", "mutation", {"search": edit(s, lambda x: x["exact"]["11"]["least"].__setitem__(0, -1e-9))}, {"W4"}),
        ("M10-notf3-outside", "mutation", {"search": edit(s, lambda x: x["exact"]["11"].update(notf3_inside=40))}, {"W4"}),
        ("M11-batch-row", "mutation", {"audits": edit(base["audits"], lambda x: next(r for r in x["batch"]["results"] if r["idx"] == closed).update(
            nodes=next(r for r in x["batch"]["results"] if r["idx"] == closed)["nodes"] + 2))}, {"W5"}),
        ("M12-chain", "mutation", {"audits": edit(base["audits"], lambda x: x["round2"].update(new_frontier_roots=90))}, {"W5"}),
        ("M13-frontier-parent", "mutation", {"two": edit(base["two"], lambda x: x["parent_root"].__setitem__(0, 3766))}, {"W5", "W6"}),
        ("M14-centre-diagnostic", "mutation", {"summary": edit(base["summary"], lambda x: x["two_root_frontier"]["center_finite_witness_diagnostic"].update(
            **{"6217_min": 0.8349695459155}))}, {"W5"}),
        ("M15-crystal-debt", "mutation", {"crystals": edit(base["crystals"], lambda x: x[11].update(packaging_debt=[8001, 8015]))}, {"W6"}),
        ("M16-verifier-path", "mutation", {"code": {**base["code"], 11: base["code"][11].replace("spec_from_file_location('v','", "spec_from_file_location('v','./")}},
         {"W7"}),
        ("M17-validation-digest", "mutation", {"validations": edit(base["validations"], lambda x: x[11].update(frontier_sha256="0" * 64))}, {"P1"}),
        ("M18-copy-bytes", "mutation", {"files": {**base["files"], next(iter(COPIES)): base["files"][next(iter(COPIES))] + b" "}}, {"P1"}),
    ]


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--refresh", action="store_true")
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    if args.refresh or not SNAPSHOT.exists():
        snap = {"retrieved": datetime.date.today().isoformat(), **gate.fetch_arxiv_facts(*MISHRA, MISHRA_FACTS, strip_invisible=True)}
        SNAPSHOT.write_text(json.dumps(snap, ensure_ascii=False, indent=1) + "\n", encoding="utf-8")
    base = world({**load_inputs(), "snapshot": json.loads(SNAPSHOT.read_text(encoding="utf-8"))})

    def build():
        return {**copy.deepcopy(base), **copy.deepcopy(CLAIMS)}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {}
    for c, fn in CHECKS.items():
        try:
            results[c] = fn(w)
        except KeyError as e:
            results[c] = [f"claim missing: {e}"]
    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 ("x1", "w1", "w2", "w3", "w4", "w5", "w6", "w7", "p1"):
        print(key, "=", json.dumps(w.get(key), default=str, ensure_ascii=False))
    if not args.drill:
        return
    cases = drill_cases(base)
    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-047", "subject": "UESFCM Cycles 10-11: the 27- and 617-root finite erosion certificates and the two-root frontier",
           "documents": list(DOCS.values()), "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("x1", "w1", "w2", "w3", "w4", "w5", "w6", "w7", "p1")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8")


if __name__ == "__main__":
    main()