"""RUN-048 - UESFCM Cycles 12-14: root 6217 - the 124-root certificate, the symmetric contact, the rho5 = 0 reduction
and its 2-D certificate, the rotation profile and the eight-root rotation-tail certificate.

Cycle 12 takes Cycle 11's 200 subroots of root 6217, closes 124 with the erosion certificate, calls the other 76's
persistence resolution debt, and finds by search that the root's constrained minimum sits at a symmetric triple
contact on the F3 boundary (y3 = rho5 = y5 = 0, x3 = x3^0 - s), which it derives in closed form. With Fary-Redei /
Rogers-Shephard convexity it reduces rho5 = 0 to a convex problem in (x3, x5). Cycle 13 closes that slice with a
2-D certificate on the rectangle x3 <= x3^0 - s. Cycle 14 closes eight more boxes in the rotation tail, and states
boundary locking (d3 = s) as a gate. Here the certificates are replayed as in RUN-047 - decoded, every leaf bounded
with the rebuilt witness set and certified in exact arithmetic - the contact is recomputed at 80 digits, the
rotation profile re-evaluated and searched, and the rho5 = 0 reduction is read against the F3 constraint.

Checks
  A0 anchors      the numbers below occur in the three documents as written
  W1 roots        root 6217; its 200 subroots; the 124 / 76 / 8 / 68 split; the 2-D rectangle; root 93's 30 subroots
  W2 structure    Cycle 12 sec. 2, 5: the 200 centres' body skeletons; the resolution ratios
  W3 certificates the three trees decoded (Cycle 13 with its own 2-D split); every leaf's witness bound; the tiling
  W4 exact        every area leaf certified in exact arithmetic with the exact eroded cores; the NOT-F3 leaves
  W5 contact      Cycle 12 sec. 6-11, 16-17: x3*, theta*, x5*, the triple contact, the switch, the branch gradients
  W6 reduction    Cycle 12 sec. 13-15, Cycle 13 sec. 2-3: the vertical symmetrization against the F3 constraint; the
                  arc d3 = s it leaves out, the least area on it, and which boxes cover it
  W7 profile      Cycle 12 sec. 18-19, Cycle 14 sec. 6-14: the 27 samples, boundary locking, the unconstrained
                  diagnostic, the profile skeletons; convexity along lines
  W8 crystals     the three state crystals
  W9 code         the three verifiers, read after the rebuild and never run
  P1 package      the VALIDATION records; the dependency copies

Usage: python code/run048_uesfcm_cycles_12_14.py [--drill] [--blind CID]
"""
import argparse
import base64
import collections
import copy
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.optimize import minimize

import gate
import run030_round27_interval_replay as r30
from run008_round05_saturation_gate import wrap
import run044_uesfcm_cycles_01_03 as r44
import run046_uesfcm_cycles_07_09 as r46
import run047_uesfcm_cycles_10_11 as r47
from corpus import SOURCES, TREE, source_bytes, walk_sources

FOLDER = "main.zip!/UESFCM/"
PKG = {i: FOLDER + f"UESFCM_Lebesgue_Cycle_{i:02d}_Package_v0.1.zip!/" for i in (7, 10, 11, 12, 13, 14)}
DOCS = {12: PKG[12] + "UESFCM_Lebesgue_Cycle_12_Root6217_Symmetric_Contact_Reduction_v0.1.md",
        13: PKG[13] + "UESFCM_Lebesgue_Cycle_13_Root6217_Rho0_Closure_v0.1.md",
        14: PKG[14] + "UESFCM_Lebesgue_Cycle_14_Rotation_Tail_and_Boundary_Locking_v0.1.md"}
CERTS = {12: PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_124Root_F3_Certificate.json",
         13: PKG[13] + "UESFCM_Lebesgue_Cycle_13_6217_Rho0_2D_Certificate.json",
         14: PKG[14] + "UESFCM_Lebesgue_Cycle_14_RotationTail8_F3_Certificate.json"}
DATA = {"frontier": PKG[7] + "UESFCM_Lebesgue_Cycle_07_F3_Unresolved_Frontier.npz",
        "two": PKG[11] + "UESFCM_Lebesgue_Cycle_11_TwoRoot_Hard_Frontier.npz",
        "remaining": PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_Remaining_76_Roots.npz",
        "profile": PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_Rotation_Profile.json",
        "contact": PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_Symmetric_Contact_Data.json",
        "resolution": PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_Resolution_and_Structure.json",
        "closure": PKG[14] + "UESFCM_Lebesgue_Cycle_14_Formal_Closure_Summary.json",
        "structure": PKG[14] + "UESFCM_Lebesgue_Cycle_14_Rotation_Profile_Structure.json",
        "root93": PKG[14] + "UESFCM_Lebesgue_Cycle_14_Root93_Search_Frontier_Summary.json",
        "root93_npz": PKG[14] + "UESFCM_Lebesgue_Cycle_14_Root93_Remaining_R4.npz",
        "raw": PKG[14] + "dependencies/UESFCM_Lebesgue_Cycle_12_6217_Rotation_Profile_raw.npz"}
CODE = {12: PKG[12] + "UESFCM_Lebesgue_Cycle_12_Verify_6217_124Root_F3.py", 13: PKG[13] + "UESFCM_Lebesgue_Cycle_13_Verify_6217_Rho0_2D.py",
        14: PKG[14] + "UESFCM_Lebesgue_Cycle_14_Verify_RotationTail8_F3.py"}
COPIES = {PKG[13] + "dependencies/UESFCM_Lebesgue_Cycle_10_Verify_27Root_F3.py": PKG[10] + "UESFCM_Lebesgue_Cycle_10_Verify_27Root_F3.py",
          PKG[13] + "dependencies/UESFCM_Lebesgue_Cycle_12_6217_Symmetric_Contact_Data.json": DATA["contact"],
          PKG[13] + "dependencies/UESFCM_Lebesgue_Cycle_12_6217_Rotation_Profile.json": DATA["profile"]}
C11_VERIFIER = PKG[11] + "UESFCM_Lebesgue_Cycle_11_Verify_617Root_F3.py"
CRYSTALS = {i: PKG[i] + f"UESFCM_Lebesgue_State_Crystal_Cycle_{i:02d}_v0.1.json" for i in (12, 13, 14)}
VALIDATIONS = {i: PKG[i] + f"UESFCM_Lebesgue_Cycle_{i:02d}_VALIDATION.json" for i in (12, 13, 14)}
LOG = TREE / "data" / "gate-logs" / "run048-uesfcm-cycles-12-14.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CACHE = TREE / "data" / "cache" / "run048-searches.json"     # data/cache is not committed

A3, S_F3, X30, ETA = r47.A3, r47.S_F3, r47.X30, r47.ETA
ROOT = 6217
R3, R5 = r47.R3, r47.R5
WORKERS = 6


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = (set(DOCS.values()) | set(CERTS.values()) | set(DATA.values()) | set(CODE.values()) | set(COPIES) | set(COPIES.values())
            | set(CRYSTALS.values()) | set(VALIDATIONS.values()) | {C11_VERIFIER})
    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.tolist() for name, a in np.load(io.BytesIO(got[DATA[k]])).items()}     # lists: the drill compares by ==
    front = {name: a for name, a in np.load(io.BytesIO(got[DATA["frontier"]])).items()}
    two = npz("two")
    sub = [i for i, p in enumerate(two["parent_root"]) if p == ROOT]
    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},
            "c11_verifier": got[C11_VERIFIER].decode("utf-8"), "certs": {i: json.loads(got[CERTS[i]]) for i in CERTS},
            "root": [front["centers"][ROOT].tolist(), front["halfwidths"][ROOT].tolist()],
            "subroots": {"centers": [two["centers"][i] for i in sub], "halfwidths": [two["halfwidths"][i] for i in sub],
                         "depth": [two["depth"][i] for i in sub]},
            "remaining": npz("remaining"), "root93_npz": npz("root93_npz"), "raw": npz("raw"),
            **{k: json.loads(got[DATA[k]]) for k in ("profile", "contact", "resolution", "closure", "structure", "root93")},
            "crystals": {i: json.loads(got[CRYSTALS[i]]) for i in CRYSTALS},
            "validations": {i: json.loads(got[VALIDATIONS[i]]) for i in VALIDATIONS},
            "packages": {i: sorted(x.split(PKG[i])[-1] for x in listing if x.startswith(PKG[i])) for i in (12, 13, 14)},
            "files": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want}}


# ---------------------------------------------------------------- the trees: Cycle 10's split, and Cycle 13's own

def split2(c, h):
    """Cycle 13's 2-D rule: the wider of x3 and x5, x3 on a tie"""
    k = 0 if h[0] >= h[3] else 3
    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


RULES = {"c10": r47.split, "c13": split2}


def decode(tree, rule):
    """leaves (centre, half-widths, depth) in preorder, the node count, and whether exactly the bits are used"""
    bits = r47.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), _ = RULES[rule](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 area_leaves(tree, rule):
    """(area leaves, NOT-F3 leaves): Cycle 13's verifier tests no leaf against the ball"""
    leaves = decode(tree, rule)[0]
    if rule == "c13":
        return leaves, []
    return [x for x in leaves if r47.d3_upper(x[0], x[1]) >= S_F3], [x for x in leaves if r47.d3_upper(x[0], x[1]) < S_F3]


def trees(certs):
    """(certificate, rule, tree, its index) for every tree"""
    out = []
    for i, cert in certs.items():
        for t in cert["trees"] if "trees" in cert else [cert["tree"]]:
            out.append((i, "c13" if i == 13 else "c10", t, t.get("local_6217_index", t.get("frontier_index", 0))))
    return out


def tree_stats(t, rule):
    leaves, nodes, full = decode(t, rule)
    area, notf3 = area_leaves(t, rule)
    return {"node_count": nodes, "area_leaf_count": len(area), "not_f3_leaf_count": len(notf3), "max_depth": max(d for _, _, d in leaves),
            "leaf_count": len(leaves), "full": full}


def tiling(certs):
    out = {}
    for i, rule, t, _ in trees(certs):
        o = out.setdefault(str(i), {"splits": 0, "exact": 0, "gap": 0.0, "overlap": 0.0})
        bits = r47.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 = RULES[rule](c, h)
            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]))
            o["splits"] += 1
            o["gap"] = max(o["gap"], float(low), float(mid), float(high))
            o["overlap"] = max(o["overlap"], float(-mid))
            o["exact"] += low == 0 and mid == 0 and high == 0
            stack.append((c2, h2))
            stack.append((c1, h1))
    return out


def witness_scan(certs):
    """every area leaf's witness bound (RUN-047's rebuild): failures after 1e-9, the a-priori decisions, the least raw
    slack and its leaf, each tree's least"""
    out = {}
    for i, rule, t, idx in trees(certs):
        o = out.setdefault(str(i), {"leaves": 0, "failing": 0, "apriori": 0, "least": [math.inf, None, None, None], "per_tree": []})
        tl = math.inf
        for c, h, _ in area_leaves(t, rule)[0]:
            lb, ap = r47.witness_bound(c, h)
            s = lb - A3
            o["leaves"] += 1
            o["apriori"] += ap
            o["failing"] += s - ETA <= 0
            tl = min(tl, s)
            if s < o["least"][0]:
                o["least"] = [s, idx, c, h]
        o["per_tree"].append([idx, None if tl == math.inf else tl])
    return out


def exact_tree(task):
    """one tree: every area leaf certified in exact arithmetic (RUN-047's certify), the directions raised until it
    passes; every NOT-F3 box proved inside the ball"""
    i, rule, t, idx = task
    out = {"cert": i, "root": idx, "area": 0, "certified": 0, "failures": 0, "escalated": 0, "least": None, "notf3": 0, "notf3_inside": 0,
           "notf3_least": None}
    area, notf3 = area_leaves(t, rule)
    for c, h, _ in notf3:
        far2 = (abs(Fraction(c[0]) - r47.X30_EXACT) + Fraction(h[0])) ** 2 + (abs(Fraction(c[1])) + Fraction(h[1])) ** 2
        m = float(r47.S_EXACT ** 2 - far2) / (float(r47.S_EXACT) + math.sqrt(float(far2)))
        out["notf3"] += 1
        out["notf3_inside"] += far2 < r47.S_EXACT ** 2
        out["notf3_least"] = m if out["notf3_least"] is None else min(out["notf3_least"], m)
    for c, h, _ in area:
        out["area"] += 1
        margin, used = None, None
        for n_dir in r47.DIRECTIONS:
            m, fail = r47.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 != r47.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}", idx, c, h, used]
    return out


def exact_scan(certs):
    tasks = sorted(trees(certs), key=lambda x: -x[2]["bit_count"])
    with Pool(WORKERS) as pool:
        rows = pool.map(exact_tree, tasks, chunksize=1)
    out = {}
    for i in certs:
        mine = [r for r in rows if r["cert"] == i]
        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(i)] = {"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


# ---------------------------------------------------------------- the hull at a point, robust to the grid

def area(v, N=2048):
    """this tree's exact hull (RUN-009 with RUN-031's segments); another grid where a noise-level tie breaks one"""
    for n in (N, N - 3, N // 2 + 1, 2 * N - 1, 4 * N - 3):
        try:
            return r44.family_area(list(v), 5, n)
        except RuntimeError:
            continue
    raise RuntimeError(f"no grid for {list(v)}")


def skeleton(v):
    """the body-level cyclic sequence of the hull, and its reflection class"""
    body = r46.runs([r46.LABEL[k] for k in r46.owners(list(v))[0]])
    return list(r46.canon(body)), list(r46.unoriented(body))


def pieces_at(v):
    """the piece-level cyclic sequence of the hull"""
    return list(r46.canon(r46.runs([r46.PIECE[k] for k in r46.owners(list(v))[0]])))


# ---------------------------------------------------------------- the searches

def skeleton_scan(sub):
    return [skeleton(c) for c in sub["centers"]]


def contact_scan():
    """Cycle 12 sec. 6-11, 16-17: theta* and x5* at 80 digits; the hull at the contact; this tree's own minimum over
    x5 on the slice; the three supports at the four directions; the hull's pieces either side of x5*; the one-sided
    gradients"""
    mp = mpmath.mp
    mp.dps = 90
    x3s = mp.mpf("-0.01215883209899") - mp.mpf("0.00882")
    c3 = 1 / mp.sqrt(3) + x3s
    th = mpmath.acos(1 / (2 * c3))
    R5m = 1 / (2 * mpmath.sin(2 * mp.pi / 5))
    c5x, c5y = R5m * mpmath.cos(6 * mp.pi / 5), R5m * mpmath.sin(6 * mp.pi / 5)
    x5s = (-mp.mpf(1) / 2 - c5x * mpmath.cos(th) - c5y * mpmath.sin(th)) / mpmath.cos(th)
    theta_s, x5_s = mpmath.nstr(th, 80), mpmath.nstr(x5s, 80)
    mp.dps = 15
    x3f, x5f, thf = float(x3s), float(x5s), float(th)
    at = lambda x5: r46.area([x3f, 0.0, 0.0, x5, 0.0])
    # golden section for the slice's minimum over x5
    a, b, g = x5f - 2e-4, x5f + 2e-4, (math.sqrt(5) - 1) / 2
    c1, c2 = b - g * (b - a), a + g * (b - a)
    f1, f2 = at(c1), at(c2)
    for _ in range(70):
        if f1 < f2:
            b, c2, f2 = c2, c1, f1
            c1 = b - g * (b - a)
            f1 = at(c1)
        else:
            a, c1, f1 = c1, c2, f2
            c2 = a + g * (b - a)
            f2 = at(c2)
    x5_opt = (a + b) / 2
    P = r44.base_pieces([x3f, 0.0, 0.0, x5f, 0.0])

    def sup(t):
        """the support of D, B3 and B5 at t: the largest over each body's pieces, an arc only on its range"""
        u = [math.cos(t), math.sin(t)]
        return [max(float(np.dot(p[0], u)) + p[1] for p in P[k0:k1] if p[2] is None or abs(wrap(t - p[2][0])) <= p[2][1])
                for k0, k1 in ((0, 1), (1, 7), (7, 17))]
    four = [sup(t) for t in (thf, -thf, math.pi - thf, math.pi + thf)]
    grad = {}
    for side, x5 in (("left", x5f - 2e-5), ("right", x5f + 2e-5)):
        e = 1e-6
        grad[side] = [(r46.area([x3f + e, 0.0, 0.0, x5, 0.0]) - r46.area([x3f - e, 0.0, 0.0, x5, 0.0])) / (2 * e),
                      (r46.area([x3f, 0.0, 0.0, x5 + e, 0.0]) - r46.area([x3f, 0.0, 0.0, x5 - e, 0.0])) / (2 * e)]
    return {"theta": theta_s, "x5": x5_s, "area_at_contact": r46.area([x3f, 0.0, 0.0, x5f, 0.0]), "x5_opt": x5_opt, "area_at_opt": at(x5_opt),
            "supports": four, "pieces_below": pieces_at([x3f, 0.0, 0.0, x5f - 1e-4, 0.0]), "pieces_at": pieces_at([x3f, 0.0, 0.0, x5f, 0.0]),
            "pieces_above": pieces_at([x3f, 0.0, 0.0, x5f + 1e-4, 0.0]), "gradients": grad}


def arc_scan(root):
    """rho5 = 0 on the arc d3 = s inside the root's box: at each angle a, the least area over B5's translation (in the
    box); the angles run from pi, the symmetric point, to where the arc leaves the box"""
    C, H = root
    lo = [c - h for c, h in zip(C, H)]
    hi = [c + h for c, h in zip(C, H)]
    a_edge = math.acos((hi[0] - X30) / S_F3)
    clip = lambda z: [min(max(z[0], lo[3]), hi[3]), min(max(z[1], lo[4]), hi[4])]
    rows, prev = [], None
    for a in np.linspace(math.pi, a_edge, 25):
        x3, y3 = X30 + S_F3 * math.cos(a), S_F3 * math.sin(a)
        f = lambda z: area([x3, y3, 0.0, *clip(z)], 1024)
        best = None
        for s in ([prev] if prev else []) + [[0.01977, 0.0], [0.016, -0.006]]:
            r = minimize(f, s, method="Nelder-Mead", options={"xatol": 1e-10, "fatol": 1e-14, "maxfev": 500})
            z = clip(r.x)
            val = area([x3, y3, 0.0, *z], 8192)
            if best is None or val < best[0]:
                best = (val, z)
        prev = best[1]
        rows.append([float(a), float(x3), float(y3), float(best[0]), best[1]])
    return {"edge": a_edge, "rows": rows}


def coverage_scan(root, sub, remaining, closed14, certified12, samples=20000, seed=48):
    """random rho5 = 0 placements in the root's box with d3 >= s: on the arc side (x3 > x3^0 - s) or the rectangle
    side, and in which subroot - certified in Cycle 12 or 14, open, or in none of the 200 (Cycle 11's search only)"""
    C, H = root
    rng = np.random.default_rng(seed)
    lo = np.array(C) - np.array(H)
    hi = np.array(C) + np.array(H)
    status = {}
    for k in range(len(sub["centers"])):
        status[k] = "c12" if k in certified12 else ("c14" if k in closed14 else ("open" if k in remaining else "?"))
    counts = collections.Counter()
    pc, ph = np.array(sub["centers"]), np.array(sub["halfwidths"])
    n = 0
    while n < samples:
        p = lo + (hi - lo) * rng.random(5)
        p[2] = 0.0
        if math.hypot(p[0] - X30, p[1]) < S_F3:
            continue
        n += 1
        side = "arc" if p[0] > X30 - S_F3 else "rectangle"
        inside = np.nonzero(np.all(np.abs(p - pc) <= ph, axis=1))[0]
        counts[(side, status[int(inside[0])] if len(inside) else "none")] += 1
    return {f"{a}|{b}": v for (a, b), v in sorted(counts.items())}


def body_runs(v):
    """the hull's body-level runs in angular order, each with its angular length, from the verified segments"""
    P = r44.base_pieces(list(v))
    Cc = np.array([p[0] for p in P], dtype=float)
    rho = np.array([p[1] for p in P], dtype=float)
    ranged = [(k, p[2]) for k, p in enumerate(P) if p[2] is not None]

    def owner(t):
        V = Cc @ np.stack([np.cos(t), np.sin(t)]) + rho[:, None]
        for k, (mid, half) in ranged:
            V[k, np.abs(wrap(t - mid)) > half] = -np.inf
        return np.argmax(V, axis=0)
    for n in (4096, 4093, 8191, 16381):
        try:
            cuts, own = r46.envelope(owner, n, len(P))
            segs = sorted(r46.verify_segments(Cc, rho, [p[2] for p in P], list(r46.segments(cuts, own))))
            break
        except RuntimeError:
            continue
    out = []
    for a, b, k in segs:
        if out and out[-1][0] == r46.LABEL[k]:
            out[-1][1] += b - a
        else:
            out.append([r46.LABEL[k], b - a])
    if len(out) > 1 and out[0][0] == out[-1][0]:
        out[0][1] += out.pop()[1]
    return out


def dropped(runs, drop):
    """the cyclic body sequence once runs shorter than drop are removed (neighbours of one body merged)"""
    out = [list(r) for r in runs]
    while len(out) > 2:
        short = [i for i, (_, ln) in enumerate(out) if ln < drop]
        if not short:
            break
        i = short[0]
        out.pop(i)
        j = i % len(out)
        if len(out) > 1 and out[j - 1][0] == out[j][0]:
            out[j - 1][1] += out[j][1]
            out.pop(j)
    return list(r46.canon([lab for lab, _ in out]))


def profile_one(task):
    """one sample: the stored minimizer re-evaluated, with its hull's body runs; this tree's own minimum on the circle
    d3 = s inside the root's box (angle and B5's translation, two starts); its unconstrained minimum over the four
    translations, in the plane and in the box"""
    s, (C, H) = task
    lo = [c - h for c, h in zip(C, H)]
    hi = [c + h for c, h in zip(C, H)]
    a_edge = math.acos((hi[0] - X30) / S_F3)
    clipc = lambda z: [min(max(z[0], a_edge), math.pi), min(max(z[1], lo[3]), hi[3]), min(max(z[2], lo[4]), hi[4])]
    clipb = lambda z: [min(max(z[0], lo[0]), hi[0]), min(max(z[1], lo[1]), hi[1]), min(max(z[2], lo[3]), hi[3]), min(max(z[3], lo[4]), hi[4])]
    inbox = lambda p: all(lo[i] <= p[i] <= hi[i] for i in range(5))
    opts = lambda n: {"xatol": 1e-11, "fatol": 1e-15, "maxfev": n}
    rho = s["rho"]
    v = [s["x3"], s["y3"], rho, s["x5"], s["y5"]]
    on = lambda z: [X30 + S_F3 * math.cos(z[0]), S_F3 * math.sin(z[0]), rho, z[1], z[2]]
    four = lambda z: [z[0], z[1], rho, z[2], z[3]]
    best = None
    for st in ([math.atan2(s["y3"], s["x3"] - X30), s["x5"], s["y5"]], [math.pi, s["x5"] + 0.001, s["y5"]]):
        p = on(clipc(minimize(lambda z: area(on(clipc(z)), 1024), st, method="Nelder-Mead", options=opts(1200)).x))
        val = area(p, 16384)
        if best is None or val < best[0]:
            best = (val, p)
    pf = four(minimize(lambda z: area(four(z), 1024), [X30, 0.0, s["x5"], s["y5"]], method="Nelder-Mead", options=opts(2500)).x)
    pb = four(clipb(minimize(lambda z: area(four(clipb(z)), 1024), [X30, 0.0, s["x5"], s["y5"]], method="Nelder-Mead", options=opts(2500)).x))
    runs = body_runs(v)
    return {"area": area(v, 16384), "d3": math.hypot(s["x3"] - X30, s["y3"]), "runs": runs, "shortest": min(ln for _, ln in runs),
            "body": {str(d): dropped(runs, d) for d in (0.0, 1e-9, 1e-6)},
            "circle": best[0], "circle_point": best[1], "circle_in_box": inbox(best[1]),
            "free": area(pf, 16384), "free_point": pf, "free_d3": math.hypot(pf[0] - X30, pf[1]), "free_in_box": inbox(pf),
            "box": area(pb, 16384), "box_point": pb, "box_d3": math.hypot(pb[0] - X30, pb[1])}


def profile_scan(profile, root):
    with Pool(WORKERS) as pool:
        return pool.map(profile_one, [(s, root) for s in profile["samples"]], chunksize=1)


def convexity_scan(root, lines=200, seed=14):
    """Fary-Redei along lines: second differences of the hull area along random vertical lines (both bodies moving in
    y), horizontal lines, and lines moving B3 in x and B5 in y (not a common direction)"""
    C, H = root
    rng = np.random.default_rng(seed)
    out = {}
    for kind, d in (("vertical", (0, 1, 0, 0, 1)), ("horizontal", (1, 0, 0, 1, 0)), ("mixed", (1, 0, 0, 0, 1))):
        worst = math.inf
        for _ in range(lines):
            p = np.array(C) + np.array(H) * (2 * rng.random(5) - 1)
            p[2] = rng.random() * 2 * H[2]
            u = np.array(d, dtype=float) * (2 * rng.random(5) - 1)
            t = 2e-3
            f = [area(p + k * t * u, 16384) for k in (-1, 0, 1)]
            worst = min(worst, (f[0] - 2 * f[1] + f[2]) / (t * t * float(np.dot(u, u))))
        out[kind] = worst
    return out


def _key(name, fn, extra=""):
    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()


TREE_HELPERS = (split2, decode, area_leaves, trees, r47.split, r47.bits_of, r47.d3_upper, r47.d3_lower)
HELPERS = {"skeletons": (skeleton, r46.owners, r46.runs, r46.canon, r46.unoriented), "tiling": TREE_HELPERS,
           "witness": TREE_HELPERS + (r47.witness_bound, r47.witness_points, r47.witness_core, r47.lemma18, r47.erosion),
           "precise": (r47.precise_witness,), "exact": TREE_HELPERS + (exact_tree, r47.certify),
           "contact": (area, pieces_at, r46.area, r46.hull, r46.owners), "arc": (area,), "coverage": (), "profile": (area, body_runs, dropped, profile_one),
           "convexity": (area,)}


def searches(inputs):
    cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {}
    certs = inputs["certs"]
    tag = hashlib.sha256(json.dumps(certs, sort_keys=True).encode()).hexdigest()
    out = {}

    def get(name, fn, call, extra=""):
        key = _key(name, fn, extra)
        if cached.get(name, {}).get("key") != key:
            cached[name] = {"key": key, "value": call()}
            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"]

    sub, rem = inputs["subroots"], inputs["remaining"]
    closed12 = {t["local_6217_index"] for t in certs[12]["trees"]}
    closed14 = {t["frontier_index"] for t in certs[14]["trees"]}
    get("skeletons", skeleton_scan, lambda: skeleton_scan(sub), hashlib.sha256(json.dumps(sub).encode()).hexdigest())
    get("tiling", tiling, lambda: tiling(certs), tag)
    get("witness", witness_scan, lambda: witness_scan(certs), tag)
    get("precise", r47.precise_witness, lambda: {k: r47.precise_witness(*out["witness"][k]["least"][2:4]) for k in ("12", "13", "14")}, tag)
    get("exact", exact_scan, lambda: exact_scan(certs), tag)
    get("contact", contact_scan, contact_scan)
    get("arc", arc_scan, lambda: arc_scan(inputs["root"]), json.dumps(inputs["root"]))
    get("coverage", coverage_scan, lambda: coverage_scan(inputs["root"], sub, set(rem["local_index"]), closed14, closed12),
        hashlib.sha256(json.dumps([inputs["root"], sub, rem["local_index"], sorted(closed12), sorted(closed14)]).encode()).hexdigest())
    get("profile", profile_scan, lambda: profile_scan(inputs["profile"], inputs["root"]),
        hashlib.sha256(json.dumps([inputs["profile"], inputs["root"]]).encode()).hexdigest())
    get("convexity", convexity_scan, lambda: convexity_scan(inputs["root"]), json.dumps(inputs["root"]))
    return out


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


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

ANCHORS = {
    12: {"W1": [r"\rho_5\in\left[0,\frac{\pi}{120}\right].", "-0.018182788956778363", "0.0060609296522594544", "0.013089969389957471",
                "0.018479773635526546", "-0.0061599245451755148", r"\boxed{200}"],
         "W2": [r"\boxed{3}", r"\boxed{166,\quad25,\quad9.}", r"\boxed{83\%.}", r"\boxed{h_{x_3}:2\times}", r"\boxed{h_{y_3}:4\times}",
                r"\boxed{h_{\rho_5}:4\times}", r"\boxed{h_{x_5}:4\times}", r"\boxed{h_{y_5}:6\times.}", "`CENTERCLASSIFICATION`",
                r"\boxed{\text{6217persistenceisstronglyresolution-driven.}}"],
         "W3": [r"\boxed{124/200}", r"\boxed{76.}", r"\boxed{32568.}", r"\boxed{16151.}", r"\boxed{195.}", r"\boxed{15.}",
                r"\boxed{3.684540239579093\times10^{-8}>0.}", r"\boxed{200\to76.}", "`124-ROOTCERTIFICATENODES:32568`", "`MINVERIFIEDSLACK:3.68454e-8`"],
         "W5": [r"\boxed{y_3=0,\qquad\rho_5=0,\qquady_5=0.}", r"\boxed{d_3=s.}", r"\boxed{x_3^\star=x_3^0-s=-0.02097883209899.}",
                r"\boxed{\theta_\star=\arccos\frac1{2c_3}.}", r"\boxed{\theta_\star\approx0.4540452162931832966751150439895469148442.}",
                r"R_5=\frac1{2\sin(2\pi/5)}.", r"\boxed{x_5^\star\approx0.0197709463479475491438550793632155310301.}",
                r"x_5^{\mathrm{opt}}\approx0.01977094619658554.", r"x_5^\star\approx0.01977094634794755.", r"\boxed{1.52\times10^{-10}}",
                r"g_L\approx(-0.03307,-0.03542),", r"g_R\approx(-0.21251,+0.40323),", r"\lambda\approx0.919254,", r"\approx(-0.04756,0).",
                r"\boxed{A^\star_{\mathrm{contact}}\approx0.834986110559224.}", r"\boxed{2.049195592240e-04.}", "`FOUR-DIRECTIONTRIPLECONTACT:PROVED`"],
         "W6": [r"\boxed{\rho_5=0\Longrightarrow\text{translationminimizer可取}y_3=y_5=0.}", r"\boxed{x_3\lex_3^\star=x_3^0-s.}",
                r"\boxed{\text{two-variableconvexoptimization}.}", "`PROVEDUSINGKNOWNLINEAR-PARAMETERCONVEXITY`"],
         "W7": [r"\boxed{m_{\mathrm{search}}(0)\approx0.83498611056.}", r"\left(\frac{\pi}{120}\right)\approx0.835105226364017.",
                r"\boxed{\text{全部non-decreasing}.}", r"\boxed{0.173793\text{to}0.245696.}", r"\boxed{0\le\rho\le\frac{\pi}{120}.}"]},
    13: {"W3": [r"\boxed{299}", r"\boxed{150.}", r"\boxed{10.}", r"\boxed{3.181940335994504e-06.}", r"\boxed{3.180940335994504e-06>0.}",
                "minimumverifiedslack:3.1809403360227861e-06", "`2DCERTIFICATENODES:299`"],
         "W6": [r"\boxed{\rho_5=0\Longrightarrow\text{theminimumoververticaltranslationsisattainedat}y_3=y_5=0.}",
                r"x_3\in[-0.024243718609038,-0.012121859304519].", "Therootdoesnotintersecttheright$F_3$branch.",
                r"\boxed{x_3\in[-0.024243718609038,-0.020978832098990].}", r"\boxed{x_5\in[0.012319849090351,0.024639698180702].}",
                "ThusGate6217-Aisreducedexactlytoatwo-dimensionalcompactrectangle.", r"\boxed{m_{6217}(0)>0.834781191.}", "`GATE6217-A:CLOSED`"]},
    14: {"W1": [r"\boxed{4,\5,\48,\50,\84,\96,\112,\113.}", r"\boxed{93.}", r"\boxed{30}", r"\boxed{76\to68.}", r"\boxed{68}"],
         "W3": [r"\boxed{102{,}062.}", '"nodes":102062', '"area_leaves":50626', '"not_f3_leaves":409', '"minimum_verified_slack":5.3395948773626856e-09',
                r"\boxed{5.339594877\times10^{-9}>0.}"],
         "W6": [r"Cycle13closedtheentire$\rho=0$slice"],
         "W7": [r"\boxed{2.365e-08.}", r"\boxed{4.27\times10^{-6}\lesssimd_3^{\mathrm{uncon}}\lesssim6.97\times10^{-4}.}", r"\boxed{7.9\%}",
                r"\boxed{4}", r"\boxed{2}", r"0.0010069\le\rho\le0.0080554,", r"0.0090623\le\rho\le0.0130900,", r"0.0151038\le\rho\le\frac{\pi}{120},",
                r"\rho\approx0.01409689,", r"\theta=\frac{3\pi}{2}.", "`FULL4DTRANSLATIONJOINTCONVEXITY:NOTCLAIMED`"]},
}

CLAIMS = {
    "roots_claim": {"printed": True, "rho_range": [0.0, 0.0], "subroots": 200, "split": [124, 76, True, True], "c14": [[4, 5, 48, 50, 84, 96, 112, 113], True, True, 68],
                    "boxes": [True, True, True], "rectangle": [0.0, 0.0, 9e-19, -9e-19], "rectangle_stated": True, "root93": [30, 30, 30, True]},
    "structure_claim": {"oriented": [103, 63, 25, 5, 4], "classes": [166, 25, 9], "ratios": [2.0, 4.0, 4.0, 4.0, 6.0],
                        "stated": [[166, 25, 9], [2.0, 4.0, 4.0, 4.0, 6.0], 200, 124, 76]},
    "cert_claim": {"c12": {"wrong_trees": [], "totals": [32568, 16151, 195, 15], "leaves": 16151, "failing": 0, "apriori": 0, "least": [3.7845403e-08, 181],
                           "precise": 3.7845403e-08, "per_tree": 7e-16, "tiling": [16222, 943, 3e-18, 3.3e-18]},
                   "c13": {"wrong_trees": [], "totals": [299, 150, 0, 10], "leaves": 150, "failing": 0, "apriori": 0, "least": [3.1819403e-06, 0],
                           "precise": 3.18194034e-06, "per_tree": 2e-16, "tiling": [149, 4, 3.5e-18, 1.8e-18]},
                   "c14": {"wrong_trees": [], "totals": [102062, 50626, 409, 19], "leaves": 50626, "failing": 0, "apriori": 0, "least": [6.3395956e-09, 112],
                           "precise": 6.33959533e-09, "per_tree": 4e-16, "tiling": [51027, 4460, 3e-18, 2.3e-18]},
                   "stated": {"c12": 9e-16, "c13": -2e-16, "c14": 7e-16}},
    "exact_claim": {"c12": {"area": 16151, "certified": 16151, "failures": 0, "escalated": 0, "least": [2.597e-05, 181, 1024], "notf3": [195, 195], "notf3_least": 1.31e-05},
                    "c13": {"area": 150, "certified": 150, "failures": 0, "escalated": 0, "least": [3.456e-05, 0, 1024], "notf3": [0, 0], "notf3_least": None},
                    "c14": {"area": 50626, "certified": 50626, "failures": 0, "escalated": 0, "least": [2.61e-05, 96, 1024], "notf3": [409, 409], "notf3_least": 1.93e-06}},
    "contact_claim": {"x3_star": True, "theta": [True, "0.4540452162931832966751150439895469148442"], "x5": [True, "0.0197709463479475491438550793632155310301"],
                      "area": [0.8349861105592, -2e-16], "gap": 0.0, "x5_opt": [-3e-14, 9e-16, -1.51e-10], "supports": [6e-17], "pieces": [False, True, 17, 17, 17],
                      "gradients": {"left": [-0.033, -0.0357], "right": [-0.2126, 0.4037]}, "mix": [-0.04756, -7e-18]},
    "reduction_claim": {"arc_in_root": [True, 0.00886, 1.5666], "symmetric_point": [0.834986110559, -2e-16], "arc_least": [0.8349861106, 3.142, 0.0002049],
                        "monotone_from_pi": False, "arc_end": [0.835483446, -0.012122, 0.0088199],
                        "coverage_arc": {"c12": 145, "none": 3899, "open": 6812}, "coverage_rectangle": {"c12": 68, "none": 5969, "open": 3107}},
    "profile_claim": {"reevaluated": 1e-15, "locking": [2.4e-08, 2.365e-08], "monotone": True, "ratios": [0.173793, 0.245696], "stated_ratios": [True, True],
                      "circle": [27, 8.3e-08, True, True, [0.1738, 0.2254], 0.8351052259], "free": [4.3e-06, 0.0022, 20], "box": [4.3e-06, 0.00091, 0.1],
                      "stated_free": [4.27e-06, 0.000696, 0.0789], "skeletons": [2, 3, 4, 2e-13, [1, 8, 17, 1]], "raw": [True, True, True],
                      "convexity": {"vertical": 2.8, "horizontal": 3.0, "mixed": 3.1}},
    "crystal_claim": {"C12": [True, True, -9e-16, True, True, True, True], "C13": ["CLOSED", True, True, 2e-16], "C14": [True, True, -7e-16, [4, 2], True, "CLOSED"]},
    "code_facts": {"lines": {12: 87, 13: 54, 14: 87},
                   "defs": {12: ["pair_lt", "quicksort_idx", "cross", "hull_area_numba", "unpack"], 13: ["unpack_bits", "split2", "main"],
                            14: ["pair_lt", "quicksort_idx", "cross", "hull_area_numba", "unpack"]},
                   "absolute": {12: True, 13: False, 14: True}, "ships_c10": {12: False, 13: True, 14: False}, "lines_differing_from_c11": {12: 1, 14: 0},
                   "c13_split": True, "c13_tests_reduction": False},
    "package_claim": {"C12": True, "C13": True, "C14": True, "statuses": True, "replays": True, "manifest": True, "copies": True, "c14_verifier_is_c11": True},
}


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


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 w1_roots(w):
    """root 6217 as Cycle 12 prints it; the 200 subroots split 124 / 76, the 76 into 8 and 68; the 2-D rectangle is the
    root's x3 range left of the F3 circle and its x5 range; root 93's 30 subroots"""
    (C, H), sub, rem = w["root"], w["subroots"], w["remaining"]
    printed = [-0.018182788956778363, 0.0060609296522594544, 0.013089969389957471, 0.018479773635526546, -0.0061599245451755148]
    c12 = sorted(t["local_6217_index"] for t in w["certs"][12]["trees"])
    c14 = sorted(t["frontier_index"] for t in w["certs"][14]["trees"])
    left = sorted(rem["local_index"])
    boxes12 = all(t["root_center"] == sub["centers"][t["local_6217_index"]] and t["root_halfwidth"] == sub["halfwidths"][t["local_6217_index"]]
                  for t in w["certs"][12]["trees"])
    boxes14 = all(t["root_center"] == sub["centers"][t["frontier_index"]] and t["root_halfwidth"] == sub["halfwidths"][t["frontier_index"]]
                  for t in w["certs"][14]["trees"])
    rows76 = all(rem["centers"][k] == sub["centers"][i] and rem["halfwidths"][k] == sub["halfwidths"][i] for k, i in enumerate(rem["local_index"]))
    red = w["certs"][13]["reduction"]
    tree = w["certs"][13]["tree"]
    rect = [Fraction(tree["root_center"][0]) - Fraction(tree["root_halfwidth"][0]), Fraction(tree["root_center"][0]) + Fraction(tree["root_halfwidth"][0]),
            Fraction(tree["root_center"][3]) - Fraction(tree["root_halfwidth"][3]), Fraction(tree["root_center"][3]) + Fraction(tree["root_halfwidth"][3])]
    want = [Fraction(C[0]) - Fraction(H[0]), Fraction(X30) - Fraction(S_F3), Fraction(C[3]) - Fraction(H[3]), Fraction(C[3]) + Fraction(H[3])]
    r93 = w["root93_npz"]
    p93 = descend(C, H, sub["centers"][93], sub["halfwidths"][93])
    paths = [descend(C, H, r93["centers"][k], r93["halfwidths"][k]) for k in range(len(r93["centers"]))]
    got = {"printed": printed == C, "rho_range": [C[2] - H[2], sig(C[2] + H[2] - math.pi / 120, 1)], "subroots": len(sub["centers"]),
           "split": [len(c12), len(left), sorted(set(c12) | set(left)) == list(range(200)), not set(c12) & set(left)],
           "c14": [c14, set(c14) <= set(left), 93 in left, len(set(left) - set(c14))], "boxes": [boxes12, boxes14, rows76],
           "rectangle": [sig(float(a - b), 1) for a, b in zip(rect, want)], "rectangle_stated": [red["x3_interval"], red["x5_interval"]] == [
               [float(want[0]), float(want[1])], [float(want[2]), float(want[3])]],
           "root93": [len(r93["centers"]), sum(p is not None and p.startswith(p93) for p in paths),
                      sum(p is not None and len(p) == d for p, d in zip(paths, r93["depth"])), len(p93) == sub["depth"][93]]}
    w["w1"] = got
    return [] if got == w["roots_claim"] else [f"the roots: {got}"]


def descend(c0, h0, tc, th):
    c, h, path = list(c0), list(h0), ""
    while len(path) <= 80:
        if c == list(tc) and h == list(th):
            return path
        (c1, h1), (c2, h2), k = r47.split(c, h)
        c, h, path = (c1, h1, path + "0") if tc[k] < c[k] else (c2, h2, path + "1")
    return None


def w2_structure(w):
    """Cycle 12 sec. 2 and 5: the 200 centres' body skeletons (oriented and up to reflection); the median half-width
    of the 76 over the 124, coordinate by coordinate"""
    sk = w["search"]["skeletons"]
    oriented = collections.Counter(tuple(b) for b, _ in sk)
    classes = collections.Counter(tuple(c) for _, c in sk)
    sub, rem = w["subroots"], w["remaining"]
    left = set(rem["local_index"])
    H = np.array(sub["halfwidths"])
    ratio = [float(np.median(H[sorted(left), k]) / np.median(H[sorted(set(range(200)) - left), k])) for k in range(5)]
    res = w["resolution"]
    got = {"oriented": sorted(oriented.values(), reverse=True), "classes": sorted(classes.values(), reverse=True),
           "ratios": [round(r, 3) for r in ratio],
           "stated": [res["observed_center_body_skeletons"]["counts"], [res["median_halfwidth_ratio_hard_over_closed"][k] for k in ("hx3", "hy3", "hrho5", "hx5", "hy5")],
                      res["current_subroots"], res["formal_closed"], res["formal_remaining"]]}
    w["w2"] = got
    return [] if got == w["structure_claim"] else [f"the structure: {got}"]


def w3_certificates(w):
    """the three trees decoded - Cycles 12 and 14 with Cycle 10's split, Cycle 13 with its own; every bit used; the
    stored counts; the witness bound on every leaf, the least slacks against the documents, each tree's least; the
    tiling"""
    S, got = w["search"], {}
    for i in (12, 13, 14):
        cert = w["certs"][i]
        rows = [(t, tree_stats(t, rule)) for j, rule, t, _ in trees({i: cert}) if j == i]
        wrong = [t.get("local_6217_index", t.get("frontier_index")) for t, s in rows
                 if not s["full"] or any(t[k] != s[k] for k in ("node_count", "area_leaf_count", "not_f3_leaf_count", "max_depth", "leaf_count") if k in t)]
        tot = [sum(s["node_count"] for _, s in rows), sum(s["area_leaf_count"] for _, s in rows), sum(s["not_f3_leaf_count"] for _, s in rows),
               max(s["max_depth"] for _, s in rows)]
        wi, til = S["witness"][str(i)], S["tiling"][str(i)]
        per = [(a, t.get("min_raw_search_slack", t.get("minimum_raw_leaf_slack"))) for (_, a), (t, _) in zip(wi["per_tree"], rows)]
        got[f"c{i}"] = {"wrong_trees": wrong, "totals": tot, "leaves": wi["leaves"], "failing": wi["failing"], "apriori": wi["apriori"],
                        "least": [sig(wi["least"][0], 8), wi["least"][1]], "precise": sig(S["precise"][str(i)][0], 9),
                        "per_tree": sig(max(abs(a - b) for a, b in per if a is not None and b is not None), 1),
                        "tiling": [til["splits"], til["exact"], sig(til["gap"], 2), sig(til["overlap"], 2)]}
    v12, v14 = w["validations"][12], w["validations"][14]
    got["stated"] = {"c12": sig(S["witness"]["12"]["least"][0] - ETA - w["resolution"]["certificate"]["minimum_verified_slack"], 1),
                     "c13": sig(S["witness"]["13"]["least"][0] - w["certs"][13]["tree"]["minimum_raw_leaf_slack"], 1),
                     "c14": sig(S["witness"]["14"]["least"][0] - ETA - 5.3395948773626856e-09, 1)}
    w["w3"] = got
    return [] if got == w["cert_claim"] else [f"the certificates: {got}"]


def w4_exact(w):
    """every area leaf of the three certificates certified in exact arithmetic; the NOT-F3 boxes inside the ball"""
    got = {}
    for i in (12, 13, 14):
        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_contact(w):
    """Cycle 12 sec. 6-11, 16-17 against this tree's 80-digit contact, its hull and its own slice minimum"""
    c, d = w["search"]["contact"], w["contact"]
    th, x5 = c["theta"], c["x5"]
    grad = c["gradients"]
    lam = d["subgradient_mix_lambda_approx"]
    gl, gr = d["left_branch_gradient_approx_dx3_dx5"], d["right_branch_gradient_approx_dx3_dx5"]
    got = {"x3_star": d["x3_star"] == X30 - S_F3, "theta": [d["theta_star_high_precision"][:78] == th[:78], th[:42]],
           "x5": [d["x5_star_high_precision"][:78] == x5[:78], x5[:42]],
           "area": [sig(c["area_at_contact"], 13), sig(c["area_at_contact"] - d["A_contact_search"], 1)],
           "gap": sig(d["A_contact_gap_above_family_ceiling"] - (d["A_contact_search"] - A3), 1),
           "x5_opt": [sig(c["x5_opt"] - float(x5), 1), sig(c["area_at_opt"] - c["area_at_contact"], 1), sig(d["x5_scalar_optimizer"] - float(x5), 3)],
           "supports": [sig(max(abs(v - 0.5) for s in c["supports"] for v in s), 1)],
           "pieces": [c["pieces_below"] == c["pieces_at"], c["pieces_above"] == c["pieces_at"], len(c["pieces_below"]), len(c["pieces_at"]), len(c["pieces_above"])],
           "gradients": {k: [round(v, 4) for v in grad[k]] for k in grad},
           "mix": [sig(lam * gl[0] + (1 - lam) * gr[0], 4), sig(lam * gl[1] + (1 - lam) * gr[1], 1)]}
    w["w5"] = got
    return [] if got == w["contact_claim"] else [f"the contact: {got}"]


def w6_reduction(w):
    """the vertical symmetrization moves (y3, y5) to 0; the F3 constraint d3 >= s is not kept where |x3 - x3^0| < s.
    Root 6217's box holds such points (the arc side); the least area over them lies on the arc d3 = s, which the
    rectangle leaves out. Its profile, and which boxes cover that side at rho5 = 0"""
    (C, H), arc, cov = w["root"], w["search"]["arc"], w["search"]["coverage"]
    x3_hi = C[0] + H[0]
    rows = arc["rows"]
    best = min(rows, key=lambda r: r[3])
    arc_side = {k.split("|")[1]: v for k, v in cov.items() if k.startswith("arc|")}
    rect_side = {k.split("|")[1]: v for k, v in cov.items() if k.startswith("rectangle|")}
    got = {"arc_in_root": [x3_hi > X30 - S_F3, sig(x3_hi - (X30 - S_F3), 3), sig(arc["edge"], 5)],
           "symmetric_point": [sig(rows[0][3], 12), sig(rows[0][3] - w["contact"]["A_contact_search"], 1)],
           "arc_least": [sig(best[3], 10), sig(best[0], 4), sig(best[3] - A3, 4)],
           "monotone_from_pi": all(rows[k + 1][3] >= rows[k][3] - 1e-12 for k in range(len(rows) - 1)),
           "arc_end": [sig(rows[-1][3], 10), sig(rows[-1][1], 5), sig(rows[-1][2], 5)],
           "coverage_arc": arc_side, "coverage_rectangle": rect_side}
    w["w6"] = got
    return [] if got == w["reduction_claim"] else [f"the reduction: {got}"]


def w7_profile(w):
    """Cycle 12 sec. 18-19 and Cycle 14 sec. 7-14: the 27 samples re-evaluated; boundary locking; the monotone profile
    and its quadratic ratios; this tree's circle and unconstrained searches; the skeletons; the raw copy; convexity"""
    prof, st, mine, raw = w["profile"], w["structure"], w["search"]["profile"], w["raw"]
    samples = prof["samples"]
    m = [s["area_min_search"] for s in samples]
    rho = [s["rho"] for s in samples]
    ratios = [(m[k] - m[0]) / rho[k] ** 2 for k in range(1, len(m))]
    circ = [x["circle"] for x in mine]
    cratios = [(circ[k] - circ[0]) / rho[k] ** 2 for k in range(1, len(circ))]
    ob = st["observed_body_level_profile"]
    theirs = [len(ob[k]["sample_indices"]) for k in ("zero_rotation_degenerate", "generic_A", "generic_B", "transition_degenerate")]
    distinct = {d: len({tuple(x["body"][d]) for x in mine}) for d in ("0.0", "1e-09", "1e-06")}
    un = st["unconstrained_translation_diagnostic"]
    got = {"reevaluated": sig(max(abs(x["area"] - s["area_min_search"]) for x, s in zip(mine, samples)), 1),
           "locking": [sig(max(abs(x["d3"] - S_F3) for x in mine), 2), sig(st["all_constrained_candidates_on_F3_boundary_within"]["max_abs_d3_minus_s"], 4)],
           "monotone": all(m[k + 1] >= m[k] for k in range(len(m) - 1)), "ratios": [sig(min(ratios), 6), sig(max(ratios), 6)],
           "stated_ratios": [prof["quadratic_ratio_min_excluding_zero"] == min(ratios), prof["quadratic_ratio_max_excluding_zero"] == max(ratios)],
           "circle": [int(sum(c < s["area_min_search"] - 1e-12 for c, s in zip(circ, samples))), sig(max(s["area_min_search"] - c for c, s in zip(circ, samples)), 2),
                      bool(all(x["circle_in_box"] for x in mine)), bool(all(circ[k + 1] >= circ[k] for k in range(len(circ) - 1))),
                      [sig(min(cratios), 4), sig(max(cratios), 4)], sig(circ[-1], 10)],
           "free": [sig(min(x["free_d3"] for x in mine), 2), sig(max(x["free_d3"] for x in mine), 2), int(sum(not x["free_in_box"] for x in mine))],
           "box": [sig(min(x["box_d3"] for x in mine), 2), sig(max(x["box_d3"] for x in mine), 2), sig(max(x["box_d3"] for x in mine) / S_F3, 2)],
           "stated_free": [sig(un["d3_min"], 3), sig(un["d3_max"], 3), sig(un["max_ratio_to_s"], 3)],
           "skeletons": [distinct["0.0"], distinct["1e-09"], distinct["1e-06"], sig(min(x["shortest"] for x in mine), 1), theirs],
           "raw": [raw["rho"] == rho, raw["m"] == m, raw["z"] == [[s["x3"], s["y3"], s["x5"], s["y5"]] for s in samples]],
           "convexity": {k: sig(v, 2) for k, v in w["search"]["convexity"].items()}}
    w["w7"] = got
    return [] if got == w["profile_claim"] else [f"the profile: {got}"]


def w8_crystals(w):
    """the three state crystals against the numbers rebuilt here"""
    c12, c13, c14 = (w["crystals"][i] for i in (12, 13, 14))
    S, d = w["search"], w["contact"]
    fp, sr = c12["formal_progress"], c12["structural_reduction"]
    tot = lambda i: sum(tree_stats(t, rule)["node_count"] for j, rule, t, _ in trees({i: w["certs"][i]}))
    sk = collections.Counter(tuple(c) for _, c in S["skeletons"])        # reflection classes, as Cycle 12 counts them
    ga = c13["root_6217"]["gate_A_rho0"]
    r14 = c14["root_6217"]
    prof = [tuple(x["body"]["0.0"]) for x in S["profile"]]
    got = {"C12": [[fp["input_subroots"], fp["closed_subroots"], fp["remaining_subroots"]] == [200, len(w["certs"][12]["trees"]), len(w["remaining"]["local_index"])],
                   fp["certificate_nodes"] == tot(12), sig(fp["minimum_verified_slack"] - (S["witness"]["12"]["least"][0] - ETA), 1),
                   [sr["observed_center_body_skeletons"], sr["dominant_center_skeleton_fraction"]] == [len(sk), round(max(sk.values()) / 200, 2)],
                   sr["symmetric_contact"]["theta_star"] == d["theta_star_high_precision"], sr["symmetric_contact"]["x5_star"] == d["x5_star_high_precision"],
                   sr["symmetric_contact"]["candidate_area"] == d["A_contact_search"]],
           "C13": [ga["status"], ga["nodes"] == tot(13), ga["leaves"] == S["witness"]["13"]["leaves"],
                   sig(ga["minimum_verified_slack"] - (S["witness"]["13"]["least"][0] - ETA), 1)],
           "C14": [[r14["formal_boxes_before"], r14["formally_closed_this_cycle"], r14["formal_boxes_remaining"]] == [76, len(w["certs"][14]["trees"]), 68],
                   r14["rotation_tail_certificate"]["nodes"] == tot(14),
                   sig(r14["rotation_tail_certificate"]["minimum_verified_slack"] - (S["witness"]["14"]["least"][0] - ETA), 1),
                   [r14["observed_profile"]["body_level_skeletons"], len(set(prof))], r14["observed_profile"]["d3_boundary_samples"] == len(prof),
                   r14["gate_A_rho0"]]}
    w["w8"] = got
    return [] if got == w["crystal_claim"] else [f"the crystals: {got}"]


def w9_code(w):
    """the three verifiers, read after the rebuild and never run"""
    code, c11 = w["code"], w["c11_verifier"].replace("\r\n", "\n")
    lines = lambda t: t.replace("\r\n", "\n").split("\n")
    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()},
           "absolute": {i: bool(re.search(r"spec_from_file_location\('v','(/|[A-Za-z]:)", t)) for i, t in code.items()},
           "ships_c10": {i: any("Verify_27Root" in x for x in w["packages"][i]) for i in (12, 13, 14)},
           "lines_differing_from_c11": {i: sum(a != b for a, b in zip(lines(code[i]), lines(c11))) + abs(len(lines(code[i])) - len(lines(c11))) for i in (12, 14)},
           "c13_split": re.findall(r"^\s*k=0 if h\[0\]>=h\[3\] else 3\s*$", code[13], re.M) != [],
           "c13_tests_reduction": any(k in code[13] for k in ('"reduction"', "x3_interval", "d3_upper"))}
    w["w9"] = got
    return [] if got == w["code_facts"] else [f"the verifiers: {got}"]


VALIDATED = {12: {"paper_sha256": DOCS[12], "certificate_sha256": CERTS[12], "verifier_sha256": CODE[12], "remaining_frontier_sha256": DATA["remaining"],
                  "rotation_profile_sha256": DATA["profile"], "contact_data_sha256": DATA["contact"], "summary_sha256": DATA["resolution"],
                  "state_sha256": CRYSTALS[12]},
             13: {"paper_sha256": DOCS[13], "certificate_sha256": CERTS[13], "verifier_sha256": CODE[13], "state_sha256": CRYSTALS[13]},
             14: {"paper_sha256": DOCS[14], "certificate_sha256": CERTS[14], "verifier_sha256": CODE[14], "formal_summary_sha256": DATA["closure"],
                  "profile_structure_sha256": DATA["structure"], "state_sha256": CRYSTALS[14], "root93_summary_sha256": DATA["root93"],
                  "root93_frontier_sha256": DATA["root93_npz"]}}


def p1_package(w):
    """each VALIDATION digest against the bytes hashed here and the archive's manifest; the replays' counts against this
    tree's; Cycle 13's dependency copies against their originals"""
    files, S = w["files"], w["search"]
    sha = lambda k: hashlib.sha256(files[k]).hexdigest()
    v12, v13, v14 = (w["validations"][i] for i in (12, 13, 14))
    rep12, rep14 = json.loads(v12["fresh_standalone_replay_stdout"]), json.loads(v14["fresh_replay_stdout"])
    counts = lambda i: [S["tiling"][str(i)]["splits"] * 2 + len(w["certs"][i]["trees"]), S["witness"][str(i)]["leaves"], S["exact"][str(i)]["notf3"]]
    checks = {**{f"C{i}": [w["validations"][i][k] == sha(f) for k, f in VALIDATED[i].items()] for i in (12, 13, 14)},
              "statuses": [v["status"] == "PASS" for v in (v12, v13, v14)] + [rep12["status"] == "PASS", rep14["status"] == "PASS"],
              "replays": [[rep12["nodes"], rep12["area_leaves"], rep12["not_f3_leaves"]] == counts(12), [rep14["nodes"], rep14["area_leaves"], rep14["not_f3_leaves"]] == counts(14),
                          f"nodes: {S['tiling']['13']['splits'] * 2 + 1}" in v13["fresh_replay_stdout"], f"leaves: {S['witness']['13']['leaves']}" in v13["fresh_replay_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["c14_verifier_is_c11"] = files[CODE[14]] == files[C11_VERIFIER]
    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, "W1": w1_roots, "W2": w2_structure, "W3": w3_certificates, "W4": w4_exact, "W5": w5_contact, "W6": w6_reduction,
          "W7": w7_profile, "W8": w8_crystals, "W9": w9_code, "P1": p1_package}
DEPENDS = {"A0": {"texts"}, "W1": {"root", "subroots", "remaining", "certs", "root93_npz", "roots_claim"},
           "W2": {"search", "subroots", "remaining", "resolution", "structure_claim"},
           "W3": {"certs", "search", "validations", "resolution", "cert_claim"}, "W4": {"search", "exact_claim"},
           "W5": {"search", "contact", "contact_claim"}, "W6": {"root", "search", "contact", "reduction_claim"},
           "W7": {"profile", "structure", "search", "raw", "profile_claim"},
           "W8": {"crystals", "search", "contact", "certs", "remaining", "crystal_claim"}, "W9": {"code", "c11_verifier", "packages", "code_facts"},
           "P1": {"validations", "files", "manifest_rows", "search", "certs", "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 swap_local(x):
        a, b = x[12]["trees"][0], x[12]["trees"][1]
        a["local_6217_index"], b["local_6217_index"] = b["local_6217_index"], a["local_6217_index"]

    def flip_last_bit(x):
        t = x[13]["tree"]
        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 new_skeleton(x):
        x["skeletons"][0] = [["B3", "D", "B5"], ["B3", "D", "B5"]]

    def theta_digit(x):
        t = x["theta_star_high_precision"]
        x["theta_star_high_precision"] = t[:30] + ("1" if t[30] != "1" else "2") + t[31:]

    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()},
                                "c11_verifier": base["c11_verifier"].replace("\n", "\r\n")}, 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-certificate-nodes-text", "mutation", {"texts": {**texts, 12: texts[12].replace("32568.", "32569.")}}, {"A0"}),
        ("M2-local-index-swap", "mutation", {"certs": edit(base["certs"], swap_local)}, {"W1"}),
        ("M3-remaining-index", "mutation", {"remaining": {**base["remaining"], "local_index": [199] + base["remaining"]["local_index"][1:]}}, {"W1", "W2"}),
        ("M4-root93-depth", "mutation", {"root93_npz": {**base["root93_npz"], "depth": [base["root93_npz"]["depth"][0] + 1] + base["root93_npz"]["depth"][1:]}},
         {"W1"}),
        ("M5-centre-skeleton", "mutation", {"search": edit(s, lambda x: new_skeleton(x))}, {"W2", "W8"}),
        ("M6-resolution-ratio", "mutation", {"resolution": edit(base["resolution"], lambda x: x["median_halfwidth_ratio_hard_over_closed"].update(hy5=5.0))},
         {"W2"}),
        ("M7-flipped-bit", "mutation", {"certs": edit(base["certs"], flip_last_bit)}, {"W3"}),
        ("M8-tree-count", "mutation", {"certs": edit(base["certs"], lambda x: x[14]["trees"][0].update(area_leaf_count=x[14]["trees"][0]["area_leaf_count"] + 1))},
         {"W3"}),
        ("M9-witness-least", "mutation", {"search": edit(s, lambda x: x["witness"]["14"]["least"].__setitem__(0, x["witness"]["14"]["least"][0] - 1e-13))},
         {"W3", "W8"}),
        ("M10-exact-margin", "mutation", {"search": edit(s, lambda x: x["exact"]["12"]["least"].__setitem__(0, -1e-9))}, {"W4"}),
        ("M11-theta-digit", "mutation", {"contact": edit(base["contact"], theta_digit)}, {"W5", "W8"}),
        ("M12-branch-gradient", "mutation", {"contact": edit(base["contact"], lambda x: x.update(left_branch_gradient_approx_dx3_dx5=[-0.034, -0.03541881121726931]))},
         {"W5"}),
        ("M13-support", "mutation", {"search": edit(s, lambda x: x["contact"]["supports"][0].__setitem__(1, 0.5001))}, {"W5"}),
        ("M14-arc-dip", "mutation", {"search": edit(s, lambda x: x["arc"]["rows"][3].__setitem__(3, 0.8349))}, {"W6"}),
        ("M15-coverage", "mutation", {"search": edit(s, lambda x: x["coverage"].update({"arc|open": x["coverage"].get("arc|open", 0) + 1}))}, {"W6"}),
        ("M16-profile-sample", "mutation", {"profile": edit(base["profile"], lambda x: x["samples"][5].update(area_min_search=x["samples"][5]["area_min_search"] - 1e-6))},
         {"W7"}),
        ("M17-locking", "mutation", {"structure": edit(base["structure"], lambda x: x["all_constrained_candidates_on_F3_boundary_within"].update(max_abs_d3_minus_s=2.4e-08))},
         {"W7"}),
        ("M18-convexity", "mutation", {"search": edit(s, lambda x: x["convexity"].update(vertical=-1.0))}, {"W7"}),
        ("M19-crystal-remaining", "mutation", {"crystals": edit(base["crystals"], lambda x: x[14]["root_6217"].update(formal_boxes_remaining=67))}, {"W8"}),
        ("M20-c13-split", "mutation", {"code": {**base["code"], 13: base["code"][13].replace("k=0 if h[0]>=h[3] else 3", "k=0 if h[0]>h[3] else 3")}}, {"W9"}),
        ("M21-validation-digest", "mutation", {"validations": edit(base["validations"], lambda x: x[12].update(contact_data_sha256="0" * 64))}, {"P1"}),
        ("M22-copy-bytes", "mutation", {"files": {**base["files"], next(iter(COPIES)): base["files"][next(iter(COPIES))] + b" "}}, {"P1"}),
    ]


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

    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 ("w1", "w2", "w3", "w4", "w5", "w6", "w7", "w8", "w9", "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-048", "subject": "UESFCM Cycles 12-14: root 6217 - the 124-root certificate, the symmetric contact, the rho5 = 0 reduction and "
                                        "its 2-D certificate, the rotation profile and the eight-root rotation-tail certificate",
           "documents": list(DOCS.values()), "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", "w9", "p1")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8")


if __name__ == "__main__":
    main()