"""RUN-030 - Round 27: residual continuation and the first rational / interval leaf certificates.

Round 27 continues only the residual B7 tails past the common depth 36 and reports lower bounds -
at least 57 of the 77 cells closed by depth 38 and 63 by depth 40, "not a common-depth curve" -
with the 14 cells still open at their last tested depths; and it certifies the five thinnest leaves
of the certificate cell (cell 0) by rational inner polygons: dense contact points of the disc and the
three common cores, nudged inward by 1e-12, rounded to 17-digit decimals, checked inside their cores
by mpmath.iv intervals around the stored binary64 box, and their exact rational hull above 167/200 on
all five (the thinnest by 3.1949e-8). Here all 26 residual cells are continued, from the boxes RUN-029
left open at depth 36, to a common depth 40 with exact cores under the package's pad (a box closes once
its exact hull less 1e-10 reaches T), the twelve thinnest leaves of cell 0 are found in this tree's own
lift, and all twelve
are certified again by an independent construction: every real in the cores' definitions - pi, R_n,
the vertices, delta and rho - enclosed by integer intervals at 2^-400 with outward rounding (cos and
sin by their Taylor sums and Lagrange remainder), the candidate points kept as exact binary floats,
their hull and its area computed in exact integers.

Checks
  A0 anchors      the numbers and formulas below occur in Round 27 as written
  W1 residual     sec. 0, 3: the residual at a common depth 40; the lower bounds; the 14 cells
                  without a known edge at their last tested depths
  W2 leaves       sec. 14, 17: the twelve thinnest leaves of cell 0 - paths, boxes, bounds
  W3 rational     sec. 10-11, 13, 15-17: the twelve certified by this tree's own inner polygons
  W4 theorem      sec. 7: the inner-polygon theorem, the enclosures, and the verifier refusing what
                  it must refuse
  W5 code         what the package ships, read after the rebuild and never run
  P1 package      the progress file, the audits, the backend spec, the crystal and the text agree
  P2 package      VALIDATION against the archive; its checks from the data
  R1 registry     Round 27's judgments reviewed, first-used statuses defined

Usage: python code/run030_round27_interval_replay.py [--drill] [--blind CID]
"""
import argparse
import collections
import copy
import hashlib
import inspect
import json
import math
from decimal import Decimal
from fractions import Fraction
from multiprocessing import Pool

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

import gate
import registry
import run008_round05_saturation_gate as r8
import run009_round06_witness_exchange as r9
import run011_round08_conditional_lift as r11
import run012_round09_adaptive_atlas as r12
import run013_round10_reference_dry_run as r13
import run019_round16_global_pilot as r19
import run020_round17_d3_cpg as r20
import run022_round19_necessity_lift as r22
import run023_round20_mixed_escalation as r23
import run025_round22_fourier_pareto as r25
import run026_round23_portfolio_closure as r26
import run027_round24_residual_joint as r27
import run028_round25_closure_wave as r28
import run029_round26_full_atlas as r29
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run009_round06_witness_exchange import placed_disc
from run010_round07_minimizer_atlas import d_star, t_text
from run011_round08_conditional_lift import placed_vertices
from run012_round09_adaptive_atlas import core_pieces
from run013_round10_reference_dry_run import contact_points

PKG = "main.zip!/AMRAL_LUC_FC_Round_27_Package_v0.1.zip!/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_27_Residual_Interval_Replay_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_27_v0.1.md"
PROGRESS = PKG + "AMRAL_LUC_FC_Round_27_RESIDUAL_PROGRESS.json"
TIGHT = PKG + "AMRAL_LUC_FC_Round_27_INTERVAL_TIGHT_LEAF_AUDIT.json"
REPLAY = PKG + "AMRAL_LUC_FC_Round_27_INTERVAL_POLYGON_REPLAY.json"
BACKEND = PKG + "AMRAL_LUC_FC_Round_27_INTERVAL_BACKEND_SPEC.json"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_27_VALIDATION.json"
REF = PKG + "AMRAL_LUC_FC_Round_27_reference/"
TIGHT12 = REF + "cell0_tight12_reference.json"
LOG = TREE / "data" / "gate-logs" / "run030-round27-interval-replay.json"
CERT_CACHE = TREE / "data" / "cache" / "run030-certificates.json"
RESIDUAL_CACHE = TREE / "data" / "cache" / "run030-residual.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"

T, TM, T_EXACT = 0.835, 0.8365, Fraction(167, 200)
DEEP, TIGHT_N, CERT_N = 40, 12, 5
DIRECTIONS, INWARD, PKG_PAD = 16384, 1e-12, 1e-10
ROOT7 = r29.ROOT7

# ---------------------------------------------------------------- integer intervals at 2^-P, rounded outward

P = 400
ONE = 1 << P
TAYLOR_EPS = 1 << (P - 340)
# pi cut after its 60th decimal: PI_LO < pi < PI_LO + 10^-60
PI_LO = Fraction(3141592653589793238462643383279502884197169399375105820974944, 10 ** 60)


def down(q):
    q = Fraction(q)
    return (q.numerator << P) // q.denominator


def up(q):
    q = Fraction(q)
    return -((-q.numerator << P) // q.denominator)


def exact(q):
    return down(q), up(q)


PI = (down(PI_LO), up(PI_LO + Fraction(1, 10 ** 60)))


def add(x, y):
    return x[0] + y[0], x[1] + y[1]


def mul(x, y):
    ps = (x[0] * y[0], x[0] * y[1], x[1] * y[0], x[1] * y[1])
    return min(ps) >> P, -(-max(ps) >> P)


def div_int(x, k):
    return x[0] // k, -(-x[1] // k)


def cos_sin(x):
    """enclosures of cos and sin over the interval x: the Taylor sums, every term enclosed
    outward, and the Lagrange remainder |x|^k / k! - once below 2^-340 - added both ways"""
    c, s, term, k = (ONE, ONE), (0, 0), (ONE, ONE), 0
    while True:
        k += 1
        term = div_int(mul(term, x), k)
        m = max(abs(term[0]), abs(term[1]))
        if m < TAYLOR_EPS:
            return (c[0] - m, c[1] + m), (s[0] - m, s[1] + m)
        signed = term if k % 4 in (0, 1) else (-term[1], -term[0])
        if k % 2:
            s = add(s, signed)
        else:
            c = add(c, signed)


def radius(n):
    """R_n = 1 / (2 cos(pi / 2n)), enclosed"""
    c, _ = cos_sin(div_int(PI, 2 * n))
    return ONE * ONE // (2 * c[1]), -(-ONE * ONE // (2 * c[0]))


def stored(v, adjacent):
    """a stored binary64 value, exact, or enclosed by its neighbouring floats (sec. 13)"""
    if not adjacent:
        return exact(v)
    return down(math.nextafter(v, -math.inf)), up(math.nextafter(v, math.inf))


def core(n, phi, centre, halves, adjacent):
    """an eroded Reuleaux core, the discs D(V_j, rho): every corner V_j = t + R_n (cos, sin)(phi +
    2 pi j / n) enclosed, and the lower end of rho = 1 - delta, delta = hypot(h_x, h_y) + 2 R_n sin(h_phi / 2)
    at its upper end (B_3's phi and h_phi are 0 by construction and stay exact)"""
    R = radius(n)
    ph = exact(0) if n == 3 else stored(phi, adjacent)
    tx, ty = (stored(v, adjacent) for v in centre)
    hx, hy = stored(halves[1], adjacent)[1], stored(halves[2], adjacent)[1]
    v = hx * hx + hy * hy
    s = math.isqrt(v)
    delta_hi = s + (s * s < v)
    if n != 3:
        _, sin_half = cos_sin(div_int(stored(halves[0], adjacent), 2))
        delta_hi += mul((2 * R[0], 2 * R[1]), sin_half)[1]
    discs = []
    for j in range(n):
        cs, sn = cos_sin(add(ph, div_int((2 * j * PI[0], 2 * j * PI[1]), n)))
        discs.append((add(tx, mul(R, cs)), add(ty, mul(R, sn))))
    return discs, ONE - delta_hi


def inside(point, discs, rho_lo):
    """|p - V_j|^2 < rho_lo^2 for every j, with every V_j at its worst in its enclosure"""
    if rho_lo <= 0:
        return False
    (x0, x1), (y0, y1) = point
    bound = rho_lo * rho_lo
    for vx, vy in discs:
        dx, dy = (x0 - vx[1], x1 - vx[0]), (y0 - vy[1], y1 - vy[0])
        if max(dx[0] * dx[0], dx[1] * dx[1]) + max(dy[0] * dy[0], dy[1] * dy[1]) >= bound:
            return False
    return True


def exact_hull_area(points):
    """Andrew's monotone chain and the shoelace in exact integers (a binary64 value is an integer
    multiple of 2^-1074)"""
    pts = sorted({(int(Fraction(x) * 2 ** 1074), int(Fraction(y) * 2 ** 1074)) for x, y in points})
    if len(pts) < 3:
        return Fraction(0), len(pts)

    def cross(o, a, b):
        return (a[0] - o[0]) * (b[1] - o[1]) - (a[1] - o[1]) * (b[0] - o[0])

    lower, upper = [], []
    for p in pts:
        while len(lower) >= 2 and cross(lower[-2], lower[-1], p) <= 0:
            lower.pop()
        lower.append(p)
    for p in reversed(pts):
        while len(upper) >= 2 and cross(upper[-2], upper[-1], p) <= 0:
            upper.pop()
        upper.append(p)
    hull = lower[:-1] + upper[:-1]
    twice = sum(hull[i][0] * hull[i - 1][1] - hull[i - 1][0] * hull[i][1] for i in range(len(hull)))
    return Fraction(abs(twice), 2 ** 2149), len(hull)


def decimal(q, digits=20):
    """q in (0, 1) cut after its digits-th decimal"""
    return "0." + str(q.numerator * 10 ** digits // q.denominator).rjust(digits, "0")


# ---------------------------------------------------------------- one leaf's certificate

def candidates(c, h, wc, wh, directions, inward):
    """the contact points of the disc and the three cores at the directions 2 pi k / directions,
    each moved the fraction inward toward its body's centre; the float hull's vertices"""
    th = 2 * np.pi * np.arange(directions) / directions
    k3, k5 = r19.cores(np.asarray(c, dtype=float), np.asarray(h, dtype=float))
    kn = core_pieces(placed_vertices(7, wc[0], wc[1:3]), 1 - r23.delta_n(7, wh))[0]
    pts, owner = [], []
    for b, (body, ctr) in enumerate(zip((placed_disc(), k3, k5, kn), ((0.0, 0.0), c[0:2], c[3:5], wc[1:3]))):
        p = contact_points(body, th)
        pts.append(p + inward * (np.asarray(ctr, dtype=float) - p))
        owner += [b] * len(p)
    pts = np.vstack(pts)
    return [(float(pts[i][0]), float(pts[i][1]), owner[i]) for i in ConvexHull(pts).vertices]


def certify(args):
    """sec. 15-16 rebuilt: every candidate checked inside its own body - the disc exactly, a core
    against its enclosed discs - and the exact hull of those that pass"""
    c, h, wc, wh, directions, inward, adjacent = args
    cand = candidates(c, h, wc, wh, directions, inward)
    cores = {1: core(3, 0.0, c[0:2], (0.0, h[0], h[1]), adjacent), 2: core(5, c[2], c[3:5], h[2:5], adjacent),
             3: core(7, wc[0], wc[1:3], wh, adjacent)}
    verified = []
    for x, y, b in cand:
        if b == 0:
            ok = Fraction(x) ** 2 + Fraction(y) ** 2 < Fraction(1, 4)
        else:
            ok = inside((exact(x), exact(y)), *cores[b])
        if ok:
            verified.append((x, y))
    area, vertices = exact_hull_area(verified)
    return {"candidates": len(cand), "verified": len(verified), "failures": len(cand) - len(verified),
            "hull_vertices": vertices, "area": f"{area.numerator}/{area.denominator}", "area_decimal": decimal(area),
            "margin": float(area - T_EXACT), "pass": area > T_EXACT,
            "rho_lo": [float(Fraction(cores[b][1], ONE)) for b in (1, 2, 3)]}


# ---------------------------------------------------------------- the certificate cell's leaves, with paths

def split_axis(wh):
    """the lift's split: the axis whose halving leaves the least delta, ties to phi, then x"""
    trial = []
    for a in range(3):
        hh = list(wh)
        hh[a] /= 2
        trial.append(r23.delta_n(7, hh))
    a = int(np.argmin(trial))
    hh = list(wh)
    hh[a] /= 2
    return a, tuple(hh)


def leaves_with_paths(pool, c, h, max_depth):
    """RUN-027's exact lift on a cell, keeping each CERT leaf: path (0 the lower child), centre,
    half-widths, exact area"""
    tn = t_text(7, d_star(TM))
    level = [("", (math.pi / 7, 0.0, 0.0), (math.pi / 7, tn, tn))]
    out = []
    for d in range(max_depth + 1):
        areas = pool.map(r27._exact, [(list(c), list(h), wc, wh) for _, wc, wh in level], chunksize=8)
        nxt = []
        for (p, wc, wh), area in zip(level, areas):
            lb = math.pi / 4 if area is None else area - r19.PAD
            if lb >= T:
                out.append([p, list(wc), list(wh), area])
                continue
            if d == max_depth:
                continue
            a, hh = split_axis(wh)
            lo, hi = list(wc), list(wc)
            lo[a] -= hh[a]
            hi[a] += hh[a]
            nxt += [(p + "0", tuple(lo), hh), (p + "1", tuple(hi), hh)]
        level = nxt
        if not level:
            break
    return out


def certificate_compute(cell):
    with Pool(14) as pool:
        leaves = leaves_with_paths(pool, cell["center"], cell["half"], 30)
        tight = sorted(leaves, key=lambda x: x[3])[:TIGHT_N]

        def jobs(directions, inward, adjacent, k):
            return [(cell["center"], cell["half"], x[1], x[2], directions, inward, adjacent) for x in tight[:k]]

        return {"leaves": len(leaves), "tight": tight,
                "adjacent": pool.map(certify, jobs(DIRECTIONS, INWARD, True, TIGHT_N)),
                "stored": pool.map(certify, jobs(DIRECTIONS, INWARD, False, CERT_N)),
                "outward": pool.map(certify, jobs(DIRECTIONS, -INWARD, True, 1)),
                "sparse": pool.map(certify, jobs(4096, INWARD, True, 1))}


# ---------------------------------------------------------------- the residual, lifted on to a common depth 40

def split_sequence(depth):
    """every box at a depth has the same half-widths, so the lift's split axes are one sequence:
    (axis, the children's half-widths) at each depth"""
    tn = t_text(7, d_star(TM))
    wh, seq = (math.pi / 7, tn, tn), []
    for _ in range(depth):
        a, wh = split_axis(wh)
        seq.append((a, wh))
    return seq


def resume(pool, c, h, lift, from_depth, max_depth, pad):
    """a lift continued from its open boxes at from_depth (paths with a leading 1, then 0 for the
    lower child, in hexadecimal): each box rebuilt from the root exactly as the lift builds it, split,
    and lifted on to max_depth under the pad; per depth (nodes, closed, open, least slack closed there),
    and the boxes open at max_depth"""
    seq = split_sequence(max_depth)
    level = []
    for x in lift["frontier"]:
        p = int(x, 16)
        wc = [math.pi / 7, 0.0, 0.0]
        for (a, hh), bit in zip(seq, bin(p)[3:]):
            wc[a] = wc[a] + hh[a] if bit == "1" else wc[a] - hh[a]
        a, hh = seq[from_depth]
        lo, hi = list(wc), list(wc)
        lo[a] -= hh[a]
        hi[a] += hh[a]
        level += [(2 * p, tuple(lo), hh), (2 * p + 1, tuple(hi), hh)]
    per = {k: v for k, v in lift["per"].items() if int(k) <= from_depth}
    nodes, closed, frontier = per[str(from_depth)][0], per[str(from_depth)][1], []
    for d in range(from_depth + 1, max_depth + 1):
        areas = pool.map(r27._exact, [(list(c), list(h), wc, wh) for _, wc, wh in level], chunksize=8)
        nodes += len(level)
        nxt, opened, slack = [], 0, None
        for (p, wc, wh), area in zip(level, areas):
            lb = math.pi / 4 if area is None else area - pad
            if lb >= T:
                closed += 1
                slack = lb - T if slack is None else min(slack, lb - T)
                continue
            opened += 1
            if d == max_depth:
                frontier.append(format(p, "x"))
                continue
            a, hh = seq[d]
            lo, hi = list(wc), list(wc)
            lo[a] -= hh[a]
            hi[a] += hh[a]
            nxt += [(2 * p, tuple(lo), hh), (2 * p + 1, tuple(hi), hh)]
        per[str(d)] = [nodes, closed, opened, slack]
        level = nxt
        if not level:
            break
    return {"per": per, "frontier": frontier}


def residual_compute(cells, lifts):
    with Pool(14) as pool:
        return {cell["path"]: resume(pool, cell["center"], cell["half"], lifts[cell["path"]], 36, DEEP, PKG_PAD) for cell in cells}


# ---------------------------------------------------------------- the two caches

def _key(fns, extra):
    digest = hashlib.sha256()
    for fn in fns:
        digest.update(inspect.getsource(fn).encode())
    for mod in (r8, r9, r11, r12, r13, r19, r20, r22, r23, r25, r26, r27, r28):
        digest.update(open(mod.__file__, "rb").read())
    digest.update(json.dumps(extra, sort_keys=True).encode())
    return digest.hexdigest()


def _cached(path, key, fn):
    if path.exists():
        cached = json.loads(path.read_text(encoding="utf-8"))
        if cached.get("key") == key:
            return cached["results"]
    results = json.loads(json.dumps(fn()))
    path.parent.mkdir(parents=True, exist_ok=True)
    path.write_text(json.dumps({"key": key, "results": results}) + "\n", encoding="utf-8")
    return results


CERT_FNS = (down, up, exact, add, mul, div_int, cos_sin, radius, stored, core, inside, exact_hull_area, decimal,
            candidates, certify, split_axis, leaves_with_paths, certificate_compute)


def certificates(cell):
    extra = {"cell": cell, "consts": [P, str(PI_LO), DIRECTIONS, INWARD, TIGHT_N, CERT_N]}
    return _cached(CERT_CACHE, _key(CERT_FNS, extra), lambda: certificate_compute(cell))


def residual(cells, lifts):
    extra = {"cells": cells, "lifts": hashlib.sha256(json.dumps({c["path"]: lifts[c["path"]] for c in cells}, sort_keys=True).encode()).hexdigest(),
             "depth": DEEP, "pad": PKG_PAD}
    return _cached(RESIDUAL_CACHE, _key((split_axis, split_sequence, resume, residual_compute), extra), lambda: residual_compute(cells, lifts))


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id.startswith(PKG) or l.id == r29.LEDGER)
           if d is not None}
    return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "progress": json.loads(got[PROGRESS]),
            "tight_audit": json.loads(got[TIGHT]), "replay": json.loads(got[REPLAY]), "backend": json.loads(got[BACKEND]),
            "validation": json.loads(got[VALIDATION]), "tight12": json.loads(got[TIGHT12]), "ledger": json.loads(got[r29.LEDGER]),
            "code": {k[len(REF):]: v.decode("utf-8") for k, v in got.items() if k.startswith(REF) and k.endswith(".py")},
            "ledger_bytes": got[r29.LEDGER], "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))}


def computed_all(inputs):
    """RUN-029's atlas and its lifts under the package's pad (its caches), the certificates of its
    certificate cell, and the residual continued from depth 36 to 40 under the package's pad"""
    atlas = r29.computed(inputs["ledger_bytes"])
    lifts = r29.pad_computed(r29.relift_cells(atlas, inputs["ledger"]))
    cert = next(a for a in atlas["atlas"] if a["path"] == atlas["certificate"]["path"])
    cell = {k: cert[k] for k in ("path", "center", "half")}
    open36 = [{k: a[k] for k in ("path", "center", "half")} for a in atlas["atlas"] if a["path"] in lifts and lifts[a["path"]]["frontier"]]
    return {"atlas": atlas, "lifts": lifts, "cell": cell, "certificates": certificates(cell), "residual": residual(open36, lifts)}


ANCHORS = {
    "W1": [r"$$\boxed{51/77}$$", r"\boxed{\ge57/77\text{haveknownclosuredepth}\le38,}", r"\boxed{\ge63/77\text{haveknownclosuredepth}\le40.}",
           r"\boxed{\Gamma_{B_7}(36)=51}", r"\boxed{\Gamma_{B_7}(38)\ge57,\qquad\Gamma_{B_7}(40)\ge63.}", r"不能寫equality。"],
    "W2": [r"1101011010010011111001110", r"$$25.$$", r"$$0.835000042074202.$$", r"\boxed{4.20742\times10^{-8}.}", r"4.2074\times10^{-8}."],
    "W3": [r"$$16384$$個candidatedirections", r"$$10^{-12}.$$floathullcandidatevertices", r"\boxed{3170/3170\text{PASS}.}",
           r"\boxed{0.8350000319489227.}", r"$$\boxed{0.8350000319489227}$$", r"0.835=167/200.", r"\boxed{A_{\rmpoly}-167/200>0.}",
           r"\boxed{3.19489\times10^{-8}.}", r"\boxed{3.1949\times10^{-8}>0.}", r"1.$3.19\times10^{-8}$", r"2.$6.42\times10^{-8}$",
           r"3.$1.16\times10^{-7}$", r"4.$1.57\times10^{-7}$", r"5.$2.03\times10^{-7}$", r"\boxed{5/5\text{PASS}.}", r"\boxed{x^2+y^2<1/4.}",
           r"\boxed{\|p-V_j\|^2<\rho^2\qquad\forallj.}", r"d^2_{\rmhi}<(\rho^2)_{\rmlo}", r"[\operatorname{nextdown}(x),\operatorname{nextup}(x)]"],
    "W4": [r"\boxed{\operatorname{conv}(P)\subseteq\operatorname{conv}\left(\bigcup_iG_i\right).}",
           r"\text{cancreatefalsenegatives,butcannotcreatefalsepositives}"],
    "P1": [r"\boxed{\text{PUBLICATIONTHEOREM:NOTYET}.}", r"\boxed{\text{theorem-readyremainsfalse}.}",
           r"\boxed{a_{\mathrm{Leb}}\ge0.835\text{NOTCERTIFIED}.}"],
}

CLAIMS = {
    # cell 0's CERT leaves; the twelve thinnest: phi exact, x and y within 4 units in the last place of the shipped
    # boxes, whose root radius t_7 is 4 units below this tree's - both above the exact t_7 (7.39 and 3.39 units), while
    # the phi root 2 fl(pi / 7) falls 3.5e-17 short of 2 pi / 7, less than one unit of pi / 7
    "leaves": {"leaves": 9278, "phi_equal": 12, "xy_ulps": 4, "root_ulps": 4, "t7_ulps_above_exact": [7.39, 3.39],
               "phi_root_short": 3.4989908547067234e-17},
    # at a common depth the package's lower bounds are exact: 57 by 38 and 63 by 40; the 14 open at 40 are its 14; the
    # twelve others close at 37 (5), 38 (1) and 39 (6); at 40 the 14 still contract, the slowest cell 23
    "residual": {"common": {"36": 51, "37": 56, "38": 57, "39": 63, "40": 63}, "open_at_40": [1, 2, 6, 7, 13, 23, 24, 25, 26, 27, 31, 32, 33, 34],
                 "depths": {"0": 39, "1": None, "2": None, "4": 37, "6": None, "7": None, "13": None, "14": 37, "16": 39, "18": 39, "23": None,
                            "24": None, "25": None, "26": None, "27": None, "28": 39, "29": 39, "31": None, "32": None, "33": None, "34": None,
                            "35": 37, "36": 37, "37": 38, "44": 39, "51": 37},
                 "ratio_40_max": 0.6076692121924157, "contracting_40": True},
    # [this tree's boxes, the shipped boxes]
    "rational": {"passed": [12, 12], "failures": [0, 0], "counts_match": True, "stored_identical": True},
    # the polygons' loss against the exact hull; the tightest leaf with its points pushed outward, and at 4096 directions
    "theorem": {"enclosures": True, "inside_hull": True, "gap": [9.879097908788533e-09, 1.407692679663419e-08],
                "outward": [3170, 0, False], "sparse": [806, 0, False, -1.8046716792384747e-07]},
    # the three shipped scripts: each loads its inputs from an absolute path; one input of each certificate script, and both
    # of the prefilter's modules, are not in the archive under the names they are loaded by
    "code_facts": {"fast_negative_prefilter.py": {"lines": 46, "absolute_path": True, "uses": ["r26_fastgeom", "r26_wave_scheduler"],
                                                  "not_in_archive": ["r26_fastgeom", "r26_wave_scheduler"], "interval": False, "decimal17": False},
                   "interval_polygon_replay.py": {"lines": 171, "absolute_path": True,
                                                  "uses": ["AMRAL_LUC_FC_Round_24_reference/cell0_B7_complete_edge/manifest.json",
                                                           "AMRAL_LUC_FC_Round_27_INTERVAL_POLYGON_REPLAY.json", "r25_incremental_wave.py",
                                                           "r27_cell0_worst_leaf.json"],
                                                  "not_in_archive": ["r27_cell0_worst_leaf.json"], "interval": True, "decimal17": True},
                   "tight_leaf_interval_batch.py": {"lines": 72, "absolute_path": True,
                                                    "uses": ["AMRAL_LUC_FC_Round_24_reference/cell0_B7_complete_edge/manifest.json",
                                                             "AMRAL_LUC_FC_Round_27_INTERVAL_TIGHT_LEAF_AUDIT.json", "r25_incremental_wave.py",
                                                             "r27_cell0_tight12.json"],
                                                    "not_in_archive": ["r27_cell0_tight12.json"], "interval": True, "decimal17": True}},
}


def near(a, b, tol):
    return abs(a - b) <= tol


def vol(per, d):
    return r28.at(per, d)[2] / 2 ** d * ROOT7


def closing_depths(w):
    """every one of the 77 cells' closing depth under the package's pad, by its ledger index: the
    depth-40 continuation for the residual (None: still open at 40), RUN-029's second lift for a cell
    it lifted again, its atlas tree for any other (RUN-029 W4: none of those holds a box in the window)"""
    comp, index = w["computed"], {c["path"]: c["cell"] for c in w["ledger"]["cells"]}
    res, lifts = comp["residual"], comp["lifts"]
    return {index[a["path"]]: r28.closing_depth(res[a["path"]]["per"] if a["path"] in res else lifts[a["path"]]["per"] if a["path"] in lifts else per)
            for a, per in zip(comp["atlas"]["atlas"], comp["atlas"]["trees"])}


def w1_residual(w):
    """sec. 0, 3: the 26 residual cells continued to a common depth 40 under the package's pad; the
    package's lower bounds and its 14 cells without a known edge, each at its last tested depth"""
    out, comp, prog = [], w["computed"], w["progress"]
    path = {c["cell"]: c["path"] for c in w["ledger"]["cells"]}
    res = comp["residual"]
    # the continuation starts where RUN-029's lift stopped, and splits every box it left open
    same = all(v["per"]["36"] == comp["lifts"][p]["per"]["36"] and v["per"]["37"][0] == v["per"]["36"][0] + 2 * v["per"]["36"][2]
               for p, v in res.items())
    depths = closing_depths(w)
    common = {str(d): sum(x is not None and x <= d for x in depths.values()) for d in range(36, DEEP + 1)}
    open40 = sorted(i for i, x in depths.items() if x is None)
    residual_depths = {str(i): depths[i] for i in sorted(depths) if path[i] in res}
    lb = prog["new_known_strict_closure_lower_bounds"]
    can = prog["canonical_common_budget"]
    if not same or len(res) != 26 or common["36"] != can["complete"] or can["residual"] != 77 - common["36"] \
            or common["38"] < lb["depth_le_38"]["known_complete_at_least"] or common["40"] < lb["depth_le_40"]["known_complete_at_least"]:
        out.append(f"the common curve {common} against the canonical {can['complete']} and the bounds; the continuation joins {same}")
    recs, bad = prog["currently_without_known_complete_edge"]["cells"], []
    for r in recs:
        per, d = res[path[r["cell"]]]["per"], r["last_tested_depth"]
        v = vol(per, d)
        if r28.at(per, d)[2] != r["pending"] or not near(v, r["unresolved_volume"], 1e-12 * v) \
                or not near(v / vol(per, d - 2), r["ratio_vs_previous"], 1e-12):
            bad.append(r["cell"])
    known = {r["cell"] for r in recs}
    edges = [i for i in residual_depths if int(i) not in known]
    if bad or not set(open40) <= known or any(residual_depths[i] is None for i in edges):
        out.append(f"the 14 cells' records differ at {bad}; open at 40 {open40}")
    # beyond the package: the cells still open at 40, from 38 to 40
    ratios = [vol(v["per"], DEEP) / vol(v["per"], DEEP - 2) for v in res.values() if r28.closing_depth(v["per"]) is None]
    got = {"common": common, "open_at_40": open40, "depths": residual_depths, "ratio_40_max": max(ratios),
           "contracting_40": all(r < 1 for r in ratios)}
    if got != w["residual"]:
        out.append(f"residual {got}")
    w["w1"] = {**got, "continuation_joins": same, "frontier_40": sum(len(v["frontier"]) for v in res.values()),
               "records_matched": len(recs) - len(bad)}
    return out


def ulps(a, b):
    return round(abs(a - b) / math.ulp(max(abs(a), abs(b))))


def w2_leaves(w):
    """sec. 14, 17: cell 0's leaves; the twelve thinnest against the shipped reference, box by box -
    the paths and phi exactly, x and y to a few units in the last place, from a root radius t_7 that
    differs by as many"""
    out, cert, ref = [], w["computed"]["certificates"], w["tight12"]
    got = [{"path": p, "depth": len(p), "wc": wc, "wh": wh, "lb": area - PKG_PAD, "slack": area - PKG_PAD - T} for p, wc, wh, area in cert["tight"]]
    bound = max(max(abs(g["lb"] - r["lb"]), abs(g["slack"] - r["slack"])) for g, r in zip(got, ref))
    phi = sum(g["wc"][0] == r["wc"][0] and g["wh"][0] == r["wh"][0] for g, r in zip(got, ref))
    xy = max(ulps(a, b) for g, r in zip(got, ref) for a, b in zip(g["wc"][1:] + g["wh"][1:], r["wc"][1:] + r["wh"][1:]))
    tn = t_text(7, d_star(TM))
    roots = {v * 2 ** round(math.log2(tn / v)) for r in ref for v in r["wh"][1:]}
    same = [g["path"] for g in got] == [r["path"] for r in ref] and all(g["depth"] == r["depth"] for g, r in zip(got, ref))
    # sec. 13's stored state against the exact root: t_7 from d* at 60 digits, and 2 pi / 7
    with mpmath.workdps(60):
        f = lambda d: (mpmath.pi - mpmath.acos(1 / (2 * d))) / 4 + mpmath.sqrt(d * d - mpmath.mpf(1) / 4) / 2
        d = mpmath.findroot(lambda d: f(d) - mpmath.mpf(8365) / 10000, mpmath.mpf(d_star(TM)))
        R, c7 = 1 / (2 * mpmath.sin(6 * mpmath.pi / 14)), mpmath.cos(mpmath.pi / 7)
        t_exact = -R * c7 + mpmath.sqrt(R * R * c7 * c7 - R * R + d * d)
        above = [round(float((mpmath.mpf(v) - t_exact) / math.ulp(tn)), 2) for v in (tn, min(roots))]
        short = float(2 * mpmath.pi / 7 - mpmath.mpf(2 * (math.pi / 7)))
    got_claim = {"leaves": cert["leaves"], "phi_equal": phi, "xy_ulps": xy, "root_ulps": ulps(tn, min(roots)) if len(roots) == 1 else None,
                 "t7_ulps_above_exact": above, "phi_root_short": short}
    if not same or bound > 1e-15 or w["cell"]["path"] != w["computed"]["cell"]["path"] or got_claim != w["leaves"] \
            or min(above) <= 0 or not 0 < short < math.ulp(math.pi / 7):
        out.append(f"the leaves: {got_claim}, paths the same {same}, bounds differ by {bound:.1e}")
    w["w2"] = {**got_claim, "bound_difference": bound, "cell": w["computed"]["cell"]["path"], "root": [tn.hex(), sorted(x.hex() for x in roots)],
               "slacks": [g["slack"] for g in got]}
    return out


def w3_rational(w):
    """sec. 13, 15-17: the twelve thinnest leaves certified by this tree's own inner polygons - on this
    tree's boxes and on the shipped ones, each enclosed by its adjacent floats, and on this tree's
    boxes at the stored values themselves; against the package's five"""
    out, cert, audit, cell = [], w["computed"]["certificates"], w["tight_audit"]["leaves"], w["computed"]["cell"]
    shipped = [certify((cell["center"], cell["half"], r["wc"], r["wh"], DIRECTIONS, INWARD, True)) for r in w["tight12"]]
    own, sto = cert["adjacent"], cert["stored"]

    def against(rows):
        """the package's five: the same counts, the areas to the rounding of its printed binary64, and
        the margins - exact differences rounded once - to what precision"""
        counts = all(a["path"] == t[0] and (r["candidates"], r["verified"], r["hull_vertices"]) ==
                     (a["candidate_vertices"], a["verified_vertices"], a["rational_hull_vertices"])
                     and abs(float(Fraction(r["area"]) - Fraction(Decimal(a["area_decimal"])))) <= 1.2e-16
                     for a, r, t in zip(audit, rows, cert["tight"]))
        return counts, max(abs(r["margin"] - float(a["margin_decimal"])) for a, r in zip(audit, rows))

    counts_own, diff_own = against(own)
    counts_shipped, diff_shipped = against(shipped)
    got = {"passed": [sum(r["pass"] for r in own), sum(r["pass"] for r in shipped)],
           "failures": [sum(r["failures"] for r in own), sum(r["failures"] for r in shipped)],
           "counts_match": counts_own and counts_shipped,
           "stored_identical": all(s["area"] == a["area"] and s["verified"] == a["verified"] for s, a in zip(sto, own))}
    worst = max(diff_own, diff_shipped)
    if got["passed"] != [TIGHT_N, TIGHT_N] or any(got["failures"]) or any(a["membership_failures"] for a in audit) or len(audit) != CERT_N \
            or worst > 1e-16 or not got["counts_match"] or not got["stored_identical"] or got != w["rational"]:
        out.append(f"the certificates: {got}, margins differ from the package's by up to {worst:.1e}")
    w["w3"] = {**got, "margin_difference": [diff_own, diff_shipped], "least_margin": [min(r["margin"] for r in own), min(r["margin"] for r in shipped)],
               "areas": [r["area_decimal"] for r in own], "margins": [r["margin"] for r in own], "shipped_margins": [r["margin"] for r in shipped]}
    return out


def w4_theorem(w):
    """sec. 7: each certified polygon lies inside the cores' hull (its area below the exact hull's);
    the enclosures hold what they enclose; points pushed outward are refused, and a sparse polygon
    stays below the target"""
    out, cert = [], w["computed"]["certificates"]
    mpmath.mp.prec = 600
    one = mpmath.mpf(ONE)
    pi_ok = mpmath.mpf(PI[0]) / one < mpmath.pi < mpmath.mpf(PI[1]) / one
    r_ok = all(mpmath.mpf(R[0]) / one < 1 / (2 * mpmath.cos(mpmath.pi / (2 * n))) < mpmath.mpf(R[1]) / one for n, R in ((n, radius(n)) for n in (3, 5, 7)))
    wc, wh = cert["tight"][0][1], cert["tight"][0][2]
    discs, _ = core(7, wc[0], wc[1:3], wh, False)
    corners = [(wc[1] + mpmath.cos(wc[0] + 2 * mpmath.pi * j / 7) / (2 * mpmath.cos(mpmath.pi / 14)),
                wc[2] + mpmath.sin(wc[0] + 2 * mpmath.pi * j / 7) / (2 * mpmath.cos(mpmath.pi / 14))) for j in range(7)]
    v_ok = all(mpmath.mpf(vx[0]) / one <= x <= mpmath.mpf(vx[1]) / one and mpmath.mpf(vy[0]) / one <= y <= mpmath.mpf(vy[1]) / one
               for (vx, vy), (x, y) in zip(discs, corners))
    width = float(max(max(vx[1] - vx[0], vy[1] - vy[0]) for vx, vy in discs) / one)
    gaps = [float(Fraction(t[3]) - Fraction(r["area"])) for t, r in zip(cert["tight"], cert["adjacent"])]
    o, s = cert["outward"][0], cert["sparse"][0]
    got = {"enclosures": pi_ok and r_ok and v_ok and width < 1e-50, "inside_hull": min(gaps) > 0, "gap": [min(gaps), max(gaps)],
           "outward": [o["candidates"], o["verified"], o["pass"]], "sparse": [s["candidates"], s["failures"], s["pass"], s["margin"]]}
    if not got["enclosures"] or not got["inside_hull"] or o["pass"] or s["pass"] or s["failures"] or got != w["theorem"]:
        out.append(f"the theorem and the refusals: {got}")
    w["w4"] = {**got, "corner_width": width}
    return out


def w5_code(w):
    """what the package ships: three scripts, read after the rebuild and never run - what each loads
    or writes beside it, and which of those files the archive holds"""
    import re
    leaves = [row[0] for row in w["manifest"]["leaves"]]
    facts = {}
    for name, src in sorted(w["code"].items()):
        uses = sorted(set(re.findall(r"ROOT/'([^']+)'", src)) | set(re.findall(r"^import (r\d+_\w+)", src, re.M)))
        facts[name] = {"lines": src.count("\n"), "absolute_path": bool(re.search(r"(?:Path\(|=)\s*['\"]/", src)), "uses": uses,
                       "not_in_archive": [u for u in uses if not any(u.split(".")[0] in leaf for leaf in leaves)],
                       "interval": "mp.iv" in src, "decimal17": "'.17g'" in src}
    w["w5"] = facts
    return [] if facts == w["code_facts"] else [f"the scripts: {facts}"]


def p1_package(w):
    out, prog, audit, rep, spec = [], w["progress"], w["tight_audit"], w["replay"], w["backend"]
    can, recs = prog["canonical_common_budget"], prog["currently_without_known_complete_edge"]
    lb = prog["new_known_strict_closure_lower_bounds"]
    cells = recs["cells"]
    vols = sorted(c["unresolved_volume"] for c in cells)
    dist = collections.Counter(str(c["last_tested_depth"]) for c in cells)
    if (can["depth"], can["complete"], can["total"], can["residual"]) != (36, 51, 77, 26) or can["coverage_fraction"] != 51 / 77 \
            or (lb["depth_le_38"]["known_complete_at_least"], lb["depth_le_40"]["known_complete_at_least"]) != (57, 63) \
            or recs["count"] != len(cells) or dict(dist) != recs["tested_depth_distribution"] \
            or (vols[0], float(np.median(vols)), vols[-1]) != (recs["observed_unresolved_volume_min"], recs["observed_unresolved_volume_median"],
                                                                recs["observed_unresolved_volume_max"]) \
            or any(not near(c["unresolved_volume"], c["pending"] / 2 ** c["last_tested_depth"] * ROOT7, 1e-12 * c["unresolved_volume"]) for c in cells):
        out.append("the progress file's own totals")
    ledger = {c["cell"]: c for c in w["ledger"]["cells"]}
    if any(ledger[c["cell"]]["pending_at_depth36"] == 0 for c in cells) \
            or any((c["pending"], c["unresolved_volume"]) != (ledger[c["cell"]]["pending_at_depth36"], ledger[c["cell"]]["unresolved_volume_at_depth36"])
                   for c in cells if c["last_tested_depth"] == 36):
        out.append("the 14 cells against Round 26's ledger")
    ref, first = w["tight12"], audit["leaves"][0]
    frac = Fraction(rep["exact_area_fraction"])
    if [a["path"] for a in audit["leaves"]] != [r["path"] for r in ref[:CERT_N]] \
            or [a["reference_slack"] for a in audit["leaves"]] != [r["slack"] for r in ref[:CERT_N]] \
            or (rep["reference_leaf_path"], rep["reference_leaf_depth"], rep["reference_lower"]) != (ref[0]["path"], ref[0]["depth"], ref[0]["lb"]) \
            or (rep["float_candidate_hull_vertices"], rep["interval_verified_points"], rep["interval_membership_failures"], rep["exact_rational_hull_vertices"]) \
            != (first["candidate_vertices"], first["verified_vertices"], first["membership_failures"], first["rational_hull_vertices"]) \
            or rep["exact_area_decimal"] != first["area_decimal"] or format(float(frac), ".17g") != first["area_decimal"] \
            or format(float(frac - T_EXACT), ".17g") != first["margin_decimal"] or rep["exact_margin_over_0_835"] != first["margin_decimal"] \
            or (rep["directions_per_body"], rep["inward_fraction"]) != (DIRECTIONS, INWARD) or rep["target_fraction"] != "167/200" \
            or any(abs(float(Decimal(a["area_decimal"]) - Decimal("0.835")) - float(a["margin_decimal"])) > 1.2e-16 for a in audit["leaves"]):
        out.append("the tight-leaf audit, the replay and the reference")
    text = gate.squash(w["text"])
    for k, a in enumerate(audit["leaves"]):
        m = f"{float(a['margin_decimal']):.2e}".split("e")
        if f"{k + 1}.${m[0]}\\times10^{{{int(m[1])}}}$" not in text:
            out.append(f"sec. 17's margin {k + 1}")
    if spec["interval_engine"]["precision_decimal_digits"] != 80 or not spec["leaf_certificate"]["fail_closed"] \
            or set(spec["migration_rule"]) != {"INTERVAL-PASS", "INTERVAL-INCONCLUSIVE", "AUDIT-FAIL"} \
            or "mpmath.iv" not in audit["backend"] or "mpmath.iv" not in rep["backend"]:
        out.append("the backend spec")
    crystal = gate.squash(w["crystal"])
    for frag in (r"\boxed{51/77\text{at}d=36.}", r"\boxed{\Gamma_{B7}(38)\ge57,}", r"\boxed{\Gamma_{B7}(40)\ge63.}", r"4.2074\times10^{-8}.",
                 "16,384directions/body.", "$$3170.$$", r"\boxed{0.8350000319489227.}", r"\boxed{3.1949\times10^{-8}.}", r"\boxed{5/5\text{PASS}.}"):
        if frag not in crystal:
            out.append(f"crystal: {frag}")
    w["p1"] = {"distribution": dict(dist), "volumes": [vols[0], float(np.median(vols)), vols[-1]]}
    return out


def p2_package(w):
    import re
    out, v = [], w["validation"]
    leaves = {row[0]: row for row in w["manifest"]["leaves"]}
    for key, leaf_id, text in (("round27", DOC, w["text"]), ("state_crystal", CRYSTAL, w["crystal"])):
        rec, (_, size, digest) = v[key], leaves[leaf_id]
        n = text.count("$$")
        if rec["sha256"] != digest or rec["bytes"] != size or not rec["utf8"] \
                or rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0) \
                or rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)) \
                or rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)):
            out.append(f"VALIDATION {key} against the archive and the document")
    for key, leaf_id in (("residual_progress_sha256", PROGRESS), ("interval_backend_spec_sha256", BACKEND),
                         ("interval_polygon_replay_sha256", REPLAY), ("tight_leaf_audit_sha256", TIGHT)):
        if v[key] != leaves[leaf_id][2]:
            out.append(f"VALIDATION {key} against the archive")
    prog, rep, audit = w["progress"], w["replay"], w["tight_audit"]
    lb = prog["new_known_strict_closure_lower_bounds"]
    kc = {"canonical_common_d36_51": prog["canonical_common_budget"]["complete"] == 51,
          "known_le38_at_least_57": lb["depth_le_38"]["known_complete_at_least"] >= 57,
          "known_le40_at_least_63": lb["depth_le_40"]["known_complete_at_least"] >= 63,
          "tight5_all_pass": len(audit["leaves"]) == 5 and all(a["pass"] for a in audit["leaves"]),
          "worst_leaf_exact_margin_positive": Fraction(rep["exact_area_fraction"]) > T_EXACT,
          "worst_leaf_membership_failures_zero": rep["interval_membership_failures"] == 0,
          "publication_scope_false": rep["publication_scope"] is False, "no_global_claim": prog["global_lebesgue_claim"] is False}
    if kc != v["checks"] or v["status"] != "PASS":
        out.append(f"VALIDATION checks {kc}")
    w["p2"] = kc
    return out


R27_DEFINITIONS = {
    "NOT YET": ("in-line", "sec. 0, 19: not established so far; the missing layers are listed - an exact / directed root and "
                           "split boxes, every active leaf and marker replayed, a second interval backend"),
}
R27_REVIEWS = [
    ("PASS", "5/5", "computation", "PASS", "the same five leaves clear 167/200 under this tree's own integer-interval polygons (W3)"),
    ("PASS", "3170/3170", "computation", "PASS", "3170 of 3170 here too, the same candidate count, no membership failure (W3)"),
    ("PASS", "5/5", "computation", "PASS", "the five margins agree with this tree's to 4.8e-17 (W3); the next seven pass as well"),
    ("PASS", "first rational/interval lower leaf certificates", "computation", "PASS",
     "right: this tree's integer-interval polygons certify the same five and the next seven, on its own boxes and on the "
     "shipped ones (W3)"),
    ("NOT YET", "PUBLICATION THEOREM", "reading", "PASS",
     "right: the boxes are binary64 states - this tree rebuilds them bit for bit from its own float root (W2), which is not the "
     "exact root sec. 19 asks for"),
    ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"),
]


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


CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_residual, "W2": w2_leaves, "W3": w3_rational, "W4": w4_theorem, "W5": w5_code,
          "P1": p1_package, "P2": p2_package, "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "W1": {"computed", "ledger", "progress", "residual"},
           "W2": {"computed", "tight12", "leaves", "cell"}, "W3": {"computed", "tight_audit", "rational"},
           "W4": {"computed", "theorem"}, "W5": {"code", "code_facts", "manifest"},
           "P1": {"progress", "ledger", "tight_audit", "replay", "backend", "tight12", "text", "crystal"},
           "P2": {"validation", "manifest", "text", "crystal", "progress", "replay", "tight_audit"},
           "R1": {"registry", "definitions", "reviews"}}


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

    def build():
        return {**{k: v for k, v in inputs.items() if k != "ledger_bytes"}, "computed": results_computed, "cell": results_computed["cell"],
                "registry": registry.load(), "definitions": dict(R27_DEFINITIONS), "reviews": list(R27_REVIEWS),
                **copy.deepcopy(CLAIMS)}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {c: fn(w) for c, fn in CHECKS.items()}
    for c, f in results.items():
        print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n     {x}" for x in f[:6]))
    for key in ("w1", "w2", "w3", "w4", "w5", "p1", "p2"):
        print(key, json.dumps(w.get(key), default=float, ensure_ascii=False)[:1500])
    if not args.drill:
        return
    prog, audit, text = inputs["progress"], inputs["tight_audit"], inputs["text"]

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

    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()),
        ("K2-progress-keys-sorted", "control", {"progress": json.loads(json.dumps(prog, sort_keys=True))}, set()),
        ("K3-audit-keys-sorted", "control", {"tight_audit": json.loads(json.dumps(audit, sort_keys=True))}, set()),
        ("M1-doc-margin", "mutation", {"text": text.replace(r"3.19489\times10^{-8}", r"3.19490\times10^{-8}")}, {"A0"}),
        ("M2-cell-pending", "mutation",
         {"progress": edit(prog, lambda x: x["currently_without_known_complete_edge"]["cells"][3].update(
             pending=x["currently_without_known_complete_edge"]["cells"][3]["pending"] + 1))}, {"W1", "P1"}),
        ("M3-lower-bound", "mutation",
         {"progress": edit(prog, lambda x: x["new_known_strict_closure_lower_bounds"]["depth_le_40"].update(known_complete_at_least=77))}, {"W1", "P1"}),
        ("M4-residual-claim", "mutation", {"residual": {**CLAIMS["residual"], "open_at_40": []}}, {"W1"}),
        ("M5-reference-box", "mutation",
         {"tight12": edit(inputs["tight12"], lambda x: x[6]["wc"].__setitem__(0, math.nextafter(x[6]["wc"][0], 1.0)))}, {"W2"}),
        ("M6-cell", "mutation", {"cell": {**results_computed["cell"], "path": "0" * 40}}, {"W2"}),
        ("M7-audit-area", "mutation",
         {"tight_audit": edit(audit, lambda x: x["leaves"][2].update(area_decimal="0.83500011567310917"))}, {"W3", "P1"}),
        ("M8-audit-count", "mutation", {"tight_audit": edit(audit, lambda x: x["leaves"][4].update(candidate_vertices=3537))}, {"W3"}),
        ("M9-theorem-claim", "mutation", {"theorem": {**CLAIMS["theorem"], "inside_hull": False}}, {"W4"}),
        ("M10-code-claim", "mutation", {"code_facts": {}}, {"W5"}),
        ("M11-replay-fraction", "mutation",
         {"replay": {**inputs["replay"], "exact_area_fraction": "8350000319489237383110508557834427977/10000000000000000000000000000000000000"}}, {"P1"}),
        ("M12-backend-precision", "mutation",
         {"backend": {**inputs["backend"], "interval_engine": {**inputs["backend"]["interval_engine"], "precision_decimal_digits": 60}}}, {"P1"}),
        ("M13-crystal", "mutation", {"crystal": inputs["crystal"].replace("0.8350000319489227.", "0.8350000319489228.")}, {"P1"}),
        ("M14-validation-digest", "mutation", {"validation": {**inputs["validation"], "tight_leaf_audit_sha256": "0" * 64}}, {"P2"}),
        ("M15-validation-check", "mutation",
         {"validation": {**inputs["validation"], "checks": {**inputs["validation"]["checks"], "publication_scope_false": False}}}, {"P2"}),
        ("M16-review-dropped", "mutation", {"reviews": list(R27_REVIEWS[1:])}, {"R1"}),
    ]
    if args.blind:
        cases = [c for c in cases if args.blind in c[3]]
    d = gate.run_drill(build, CHECKS, DEPENDS, cases)
    summary = gate.summarize(d, CHECKS)
    print(gate.report_drill(summary))
    for x in d:
        if not x["ok"]:
            print("   DRILL FAIL", x)
    if args.blind:
        n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"])
        print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)")
        return
    log = {"run": "RUN-030", "subject": "Round 27: residual continuation and the first rational / interval leaf certificates",
           "document": DOC, "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "p1", "p2")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=float) + "\n", encoding="utf-8")
    if not results["R1"]:
        registry.record("R27", "RUN-030", R27_DEFINITIONS, R27_REVIEWS)
        print(f"registry: {len(R27_DEFINITIONS)} definitions, {len(R27_REVIEWS)} reviews recorded for R27")


if __name__ == "__main__":
    main()