"""RUN-031 - Round 28: exact root reconstruction and the bulk rational-interval migration of cell 0.

Round 28 rebuilds the root in directed arithmetic - the exact master target 1673/2000, d* by directed
bisection of the monotone a-priori area, t_3, t_5, t_7 as intervals, the D3 root's endpoints - stores
cell 0's 40 base splits and its witness tree's 9277 split axes explicitly (0 overrides; a 2-bit
stream), measures how far the stored binary64 boxes sit from the intended ones, and migrates all 9278
leaves of cell 0 to exact rational inner polygons on the intended boxes, each at a density chosen from
its reference slack (256 ... 16384): 9278/9278 pass, the least margin 3.1948922738e-8. Here the root is
bracketed by this tree's own integer intervals (acos certified by bracketing it with an enclosed
cosine; F increasing), the axes are recomputed, the stored boxes' distances remeasured, and all 9278
leaves are certified again on the intended boxes - at the ledger's density, and at the least density
that passes.

Checks
  A0 anchors      the numbers and formulas below occur in Round 28 as written
  W1 root         sec. 1-4: d*, t_3, t_5, t_7 bracketed here, inside the package's intervals; the
                  binary64 roots against them
  W2 base         sec. 5-7: cell 0's 40 base splits - axes, the intended box, the stored box's distance
  W3 witness      sec. 8-9: the topology, the 2-bit axis stream, the stored boxes' distances
  W4 leaves       sec. 10-18: all 9278 leaves certified on the intended boxes; the densities
  W5 kernel       this tree's exact kernel against a verified envelope and the ledger's reference slacks
  P1 package      the root file, the manifest, the migration, the policy, the ledger, the crystal, the text
  P2 package      VALIDATION against the archive; its checks from the data
  R1 registry     Round 28's judgments reviewed, first-used statuses defined

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

import mpmath
import numpy as np

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
import run030_round27_interval_replay as r30
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 run030_round27_interval_replay import (ONE, P, add, candidates, cos_sin, div_int, down, exact, exact_hull_area, inside, mul,
                                            split_sequence, up)

PKG = "main.zip!/AMRAL_LUC_FC_Round_28_Package_v0.1.zip!/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_28_Exact_Root_Bulk_Migration_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_28_v0.1.md"
ROOTREC = PKG + "AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json"
BULK = PKG + "AMRAL_LUC_FC_Round_28_CELL0_BULK_MIGRATION.json"
CERTMAN = PKG + "AMRAL_LUC_FC_Round_28_ARITHMETIC_CERTIFICATE_MANIFEST.json"
POLICY = PKG + "AMRAL_LUC_FC_Round_28_MIGRATION_POLICY.json"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_28_VALIDATION.json"
REF = PKG + "AMRAL_LUC_FC_Round_28_reference/"
LEAVES = REF + "cell0_leaf_migration_ledger.json"
TOPO = REF + "cell0_topology.bin"
AXES = REF + "witness_axis_stream_2bit.bin"
EDGE24 = r27.EDGE + "manifest.json"
LOG = TREE / "data" / "gate-logs" / "run031-round28-exact-root.json"
CACHE = TREE / "data" / "cache" / "run031-migration.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"

T, TM = 0.835, 0.8365
T_EXACT, TM_EXACT = Fraction(167, 200), Fraction(1673, 2000)
DENSITIES = (256, 512, 1024, 2048, 4096, 8192, 16384)
INWARD = r30.INWARD

# ---------------------------------------------------------------- more integer intervals, and pi to 1e-113

def atan_inv(k):
    """atan(1 / k), k > 1: the alternating series, each term enclosed outward, and the first omitted
    term's bound added both ways"""
    lo = hi = 0
    n = 0
    while True:
        den = (2 * n + 1) * k ** (2 * n + 1)
        t_lo, t_hi = ONE // den, -(-ONE // den)
        if t_hi < 1 << (P - 380):
            return lo - t_hi, hi + t_hi
        if n % 2:
            lo, hi = lo - t_hi, hi - t_lo
        else:
            lo, hi = lo + t_lo, hi + t_hi
        n += 1


def machin_pi():
    """pi = 16 atan(1/5) - 4 atan(1/239) (Machin), enclosed: RUN-030's 60 decimals are too few here, since
    d* inherits pi's width"""
    a, b = atan_inv(5), atan_inv(239)
    return 16 * a[0] - 4 * b[1], 16 * a[1] - 4 * b[0]


PI = machin_pi()


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


def sub(x, y):
    return x[0] - y[1], x[1] - y[0]


def neg(x):
    return -x[1], -x[0]


def sqrt_iv(x):
    """the square root of a nonnegative interval"""
    v = x[1] << P
    hi = math.isqrt(v)
    return math.isqrt(max(x[0], 0) << P), hi + (hi * hi < v)


def recip(x):
    """1 / x over a positive interval"""
    return ONE * ONE // x[1], -(-ONE * ONE // x[0])


def mpf_scaled(x):
    """an mpf times 2^P, floored"""
    man, e = x.man_exp
    return man << (e + P) if e + P >= 0 else man >> -(e + P)


def acos_iv(u):
    """acos over an interval inside (-1, 1): decreasing, so [acos(u_hi), acos(u_lo)]; each end is an
    approximation at 150 digits certified by bracketing it - cos decreases on [0, pi], so cos(b) < v <
    cos(a) puts acos(v) in (a, b); the bracket's 2^-320 must exceed the cosine's own width (2^-340)"""
    def bracket(v):
        with mpmath.workdps(150):
            t = mpf_scaled(mpmath.acos(mpmath.mpf(v) / mpmath.mpf(ONE)))
        a, b = t - (1 << (P - 320)), t + (1 << (P - 320))
        assert cos_sin((b, b))[0][1] < v < cos_sin((a, a))[0][0]
        return a, b
    return bracket(u[1])[0], bracket(u[0])[1]


def apriori(d):
    """sec. 2: F(d) = (pi - acos(1 / 2d)) / 4 + sqrt(d^2 - 1/4) / 2 over an interval d > 1/2, enclosed"""
    a = acos_iv(recip((2 * d[0], 2 * d[1])))
    s = sqrt_iv(sub(mul(d, d), exact(Fraction(1, 4))))
    return add(div_int(sub(PI, a), 4), div_int(s, 2))


def d_star_iv():
    """sec. 2: d* with F(d*) = 1673/2000, bracketed - F increases for d > 1/2 (F' = sqrt(d^2 - 1/4) / 2d) -
    by its two ends, 2^-300 either side of a 150-digit root (F' is 0.35 there and F's own width 1e-97)"""
    with mpmath.workdps(150):
        f = lambda d: (mpmath.pi - mpmath.acos(1 / (2 * d))) / 4 + mpmath.sqrt(d * d - mpmath.mpf(1) / 4) / 2
        t = mpf_scaled(mpmath.findroot(lambda d: f(d) - mpmath.mpf(1673) / 2000, mpmath.mpf(d_star(TM))))
    a, b = t - (1 << (P - 300)), t + (1 << (P - 300))
    tm = exact(TM_EXACT)
    assert apriori((a, a))[1] < tm[0] and apriori((b, b))[0] > tm[1]
    return a, b


def t_iv(n, d):
    """sec. 3: t_n = -R_n c + sqrt(R_n^2 c^2 - R_n^2 + d*^2), c = cos(pi / n), over d* enclosed"""
    R, c = radius(n), cos_sin(div_int(PI, n))[0]
    Rc = mul(R, c)
    return add(neg(Rc), sqrt_iv(add(sub(mul(Rc, Rc), mul(R, R)), mul(d, d))))


def root_scales():
    """the irrational scales of the D3 root and the witness root: x3 in [0, t3], y3 in [0, (sqrt3 / 2) t3],
    phi5 in [0, 2 pi / 5], x5, y5 in [-t5, t5]; phi7 in [0, 2 pi / 7], x7, y7 in [-t7, t7]"""
    d = d_star_iv()
    t3, t5, t7 = (t_iv(n, d) for n in (3, 5, 7))
    two_pi = (2 * PI[0], 2 * PI[1])
    return {"d": d, "t3": t3, "t5": t5, "t7": t7, "y3": mul(div_int(sqrt_iv(exact(3)), 2), t3), "phi5": div_int(two_pi, 5),
            "phi7": div_int(two_pi, 7)}


BASE = (("t3", False), ("y3", False), ("phi5", False), ("t5", True), ("t5", True))
WITNESS = (("phi7", False), ("t7", True), ("t7", True))


def fractions(path, axes, dims):
    """each coordinate's share [lo, hi] of its root range after the splits (bit 1 the upper half)"""
    lo, hi = [Fraction(0)] * dims, [Fraction(1)] * dims
    for bit, a in zip(path, axes):
        mid = (lo[a] + hi[a]) / 2
        if bit == "1":
            lo[a] = mid
        else:
            hi[a] = mid
    return lo, hi


def directed_box(lo, hi, frame, scales):
    """centre and half-width intervals of the intended box: coordinate k spans lo..hi of [0, S] or
    of [-S, S], S its scale"""
    centres, halves = [], []
    for fl, fh, (name, symmetric) in zip(lo, hi, frame):
        S = scales[name]
        c, h = (fl + fh - 1, fh - fl) if symmetric else ((fl + fh) / 2, (fh - fl) / 2)
        centres.append(mul(exact(c), S))
        halves.append(mul(exact(h), S))
    return centres, halves


def distance(v, iv):
    """a binary64 value's distance to an interval"""
    q, lo, hi = Fraction(v), Fraction(iv[0], ONE), Fraction(iv[1], ONE)
    return float(max(lo - q, q - hi, 0))


def core_iv(n, phi, tx, ty, halves_hi):
    """an eroded Reuleaux core over an intended box: corners V_j = t + R_n (cos, sin)(phi + 2 pi j / n)
    enclosed over the centre intervals, rho's lower end 1 - delta_hi from the half-widths' upper ends"""
    R = radius(n)
    hphi, hx, hy = halves_hi
    v = hx * hx + hy * hy
    s = math.isqrt(v)
    delta = s + (s * s < v)
    if hphi:
        delta += mul((2 * R[0], 2 * R[1]), cos_sin(div_int((hphi, hphi), 2))[1])[1]
    discs = []
    for j in range(n):
        cs, sn = cos_sin(add(phi, 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


# ---------------------------------------------------------------- this tree's exact kernel, verified

def verified_hull(pieces, n=1024, tol=1e-14):
    """the exact hull area with the envelope verified. RUN-008's envelope finds hand-overs between grid
    angles, so a piece that wins only inside one grid step, both ends of the step keeping one owner, is
    lost - and the area comes out low. Here every segment is checked in closed form against every other
    piece: h_j - h_k = |dC| cos(t - a) + drho peaks at t = a, so its maximum on the segment (within j's
    range of normals) is at an end or at a. A piece that beats the owner by more than tol takes the
    sub-arc where it does, and the new segments are checked again, until none is beaten."""
    for turn in r19.TURNS:
        try:
            tp = r19.turned(pieces, turn)
            C = np.array([p[0] for p in tp], dtype=float)
            rho = np.array([p[1] for p in tp], dtype=float)
            ranged = [(k, p[2]) for k, p in enumerate(tp) if p[2] is not None]

            def owner(t):
                V = C @ np.stack([np.cos(t), np.sin(t)]) + rho[:, None]
                for k, (mid, half) in ranged:
                    V[k, np.abs(r8.wrap(t - mid)) > half] = -np.inf
                return np.argmax(V, axis=0)

            cuts, owners = r8.envelope(owner, n, len(tp))
            break
        except RuntimeError:
            continue
    else:
        raise RuntimeError("envelope refused at every turn")
    rng = [p[2] for p in tp]

    def windows(j, a, b):
        """the parts of [a, b] inside piece j's range of normals"""
        if rng[j] is None:
            return [(a, b)]
        mid, half = rng[j]
        out = []
        m0 = math.floor((a - mid - half) / (2 * math.pi))
        for m in range(m0, m0 + 3):
            lo, hi = mid - half + 2 * math.pi * m, mid + half + 2 * math.pi * m
            if max(lo, a) < min(hi, b):
                out.append((max(lo, a), min(hi, b)))
        return out

    segs, fixes, changed = list(r8.segments(cuts, owners)), 0, True
    while changed:
        changed, nxt = False, []
        for a, b, k in segs:
            best = None
            for j in range(len(tp)):
                if j == k:
                    continue
                d = C[j] - C[k]
                A, al, B = math.hypot(d[0], d[1]), math.atan2(d[1], d[0]), rho[j] - rho[k]
                for lo, hi in windows(j, a, b):
                    peaks = [al + 2 * math.pi * m for m in range(math.floor((lo - al) / (2 * math.pi)), math.floor((hi - al) / (2 * math.pi)) + 2)]
                    for t in [lo, hi] + [p for p in peaks if lo < p < hi]:
                        v = A * math.cos(t - al) + B
                        if v > tol and (best is None or v > best[0]):
                            best = (v, j, t, lo, hi, A, al, B)
            if best is None:
                nxt.append((a, b, k))
                continue
            v, j, t, lo, hi, A, al, B = best
            if A == 0:
                s, e = lo, hi
            else:
                beta = math.acos(max(-1.0, min(1.0, -B / A)))
                centre = al + 2 * math.pi * round((t - al) / (2 * math.pi))
                s, e = max(lo, centre - beta), min(hi, centre + beta)
            nxt += [x for x in ((a, s, k), (s, e, j), (e, b, k)) if x[1] > x[0]]
            changed, fixes = True, fixes + 1
        segs = nxt
    cn, al = np.hypot(C[:, 0], C[:, 1]), np.arctan2(C[:, 1], C[:, 0])
    F = lambda k, t: cn[k] ** 2 / 2 * math.sin(2 * (t - al[k])) + 2 * rho[k] * cn[k] * math.sin(t - al[k]) + rho[k] ** 2 * t
    return sum(F(k, b) - F(k, a) for a, b, k in segs) / 2, fixes


def _kernel(args):
    """one leaf's exact area three ways: the grid envelope alone (this tree's kernel before RUN-031's
    correction), this file's verified envelope, and the shared kernel as corrected (RUN-027's bound)"""
    c, h, wc, wh = args
    base = r19.cores(np.asarray(c, dtype=float), np.asarray(h, dtype=float))
    rho = 1 - r23.delta_n(7, wh)
    kn = core_pieces(placed_vertices(7, wc[0], wc[1:3]), rho)[0]
    pieces = placed_disc() + base[0] + base[1] + kn
    grid = None
    for turn in r19.TURNS:
        try:
            grid = r9.hull_pieces(r19.turned(pieces, turn), 1024, verify=False)[0]
            break
        except RuntimeError:
            continue
    area, fixes = verified_hull(pieces)
    return [grid, area, fixes, r27._exact(args)]


# ---------------------------------------------------------------- the stored binary64 trees

def base_axes(path):
    """the official split from the binary64 D3 root along a path: its axes and the stored cell"""
    c, h = r20.d3_root()
    axes = []
    for bit in path:
        a = r19.official_axis(h)
        axes.append(a)
        c, h = r20.children(c, h, a)[int(bit)]
    return axes, c.tolist(), h.tolist()


def float_box(path, seq, t7):
    """a witness box as the binary64 lift builds it from the root (pi / 7, 0, 0) +- (pi / 7, t7, t7)"""
    wc, wh = [math.pi / 7, 0.0, 0.0], (math.pi / 7, t7, t7)
    for bit, (a, hh) in zip(path, seq):
        wc[a] = wc[a] + hh[a] if bit == "1" else wc[a] - hh[a]
        wh = hh
    return wc, list(wh)


def float_sequence(t7, depth):
    """the lift's axes and half-widths per depth, from a root radius t7"""
    wh, seq = (math.pi / 7, t7, t7), []
    for _ in range(depth):
        a, wh = r30.split_axis(wh)
        seq.append((a, wh))
    return seq


def decode_topology(data, nodes):
    """preorder, 1 an internal node, lower child first, MSB first: (path, internal) per node. A stream
    that ends inside the tree, or leaves anything but zero padding after it, or does not hold the stated
    node count, is malformed - an error, never a tree"""
    bits = [(data[i // 8] >> (7 - i % 8)) & 1 for i in range(8 * len(data))]
    out, pos = [], 0

    def walk(p):
        nonlocal pos
        if pos >= len(bits):
            raise ValueError("the topology ends inside the tree")
        b = bits[pos]
        pos += 1
        out.append((p, b))
        if b:
            walk(p + "0")
            walk(p + "1")

    walk("")
    if len(out) != nodes or any(bits[pos:]):
        raise ValueError(f"the topology holds {len(out)} nodes, padding {'clean' if not any(bits[pos:]) else 'not zero'}")
    return out


def decode_axes(data, count, msb_pair):
    """2 bits per internal node, MSB first; the pair read high bit first, or low bit first"""
    bits = [(data[i // 8] >> (7 - i % 8)) & 1 for i in range(2 * count)]
    return [(bits[2 * k] << 1 | bits[2 * k + 1]) if msb_pair else (bits[2 * k + 1] << 1 | bits[2 * k]) for k in range(count)]


# ---------------------------------------------------------------- the migration (cached)

def migrate(args):
    """one leaf on its intended box: the ledger's density, and the ladder from 256 up to the least that
    passes; candidates from this tree's binary64 box, each checked inside its own intended body"""
    c, h, wc, wh, box, base, ledger_density = args
    centres, halves = box
    b7 = core_iv(7, centres[0], centres[1], centres[2], [x[1] for x in halves])
    cores = {1: base[0], 2: base[1], 3: b7}

    def certify(n):
        cand = candidates(c, h, wc, wh, n, INWARD)
        verified = []
        for x, y, b in cand:
            ok = Fraction(x) ** 2 + Fraction(y) ** 2 < Fraction(1, 4) if b == 0 else inside((exact(x), exact(y)), *cores[b])
            if ok:
                verified.append((x, y))
        area, vertices = exact_hull_area(verified)
        return {"n": n, "candidates": len(cand), "failures": len(cand) - len(verified), "hull": vertices,
                "margin": float(area - T_EXACT), "pass": area > T_EXACT}

    out = {"ledger": certify(ledger_density)}
    for n in DENSITIES:
        r = out["ledger"] if n == ledger_density else certify(n)
        if r["pass"]:
            out["least"] = r
            break
    else:
        out["least"] = None
    return out


def compute(cell, ledger):
    """the root, the intended base box and its two cores; this tree's CERT leaves of cell 0 (RUN-030's
    lift, with paths) migrated at the ledger's density for the same path, and on the ladder"""
    scales = root_scales()
    axes, _, _ = base_axes(cell["path"])
    lo, hi = fractions(cell["path"], axes, 5)
    bc, bh = directed_box(lo, hi, BASE, scales)
    base = (core_iv(3, exact(0), bc[0], bc[1], [0, bh[0][1], bh[1][1]]), core_iv(5, bc[2], bc[3], bc[4], [bh[2][1], bh[3][1], bh[4][1]]))
    tn = t_text(7, d_star(TM))
    seq = float_sequence(tn, 30)
    waxes = [a for a, _ in seq]
    density = {x["path"]: x["density"] for x in ledger}
    with Pool(14) as pool:
        leaves = r30.leaves_with_paths(pool, cell["center"], cell["half"], 30)
        jobs = []
        for path, _, _, _ in leaves:
            wc, wh = float_box(path, seq, tn)
            wlo, whi = fractions(path, waxes, 3)
            jobs.append((cell["center"], cell["half"], wc, wh, directed_box(wlo, whi, WITNESS, scales), base, density.get(path, DENSITIES[-1])))
        results = pool.map(migrate, jobs, chunksize=16)
        kernel = pool.map(_kernel, [(cell["center"], cell["half"], wc, wh) for _, wc, wh, _ in leaves], chunksize=16)
    return {"scales": {k: [str(v[0]), str(v[1])] for k, v in scales.items()},
            "leaves": [[p, area] for p, _, _, area in leaves], "results": results, "kernel": kernel}


def _key(key_bytes):
    digest = hashlib.sha256()
    for fn in (atan_inv, machin_pi, radius, sub, neg, sqrt_iv, recip, mpf_scaled, acos_iv, apriori, d_star_iv, t_iv, root_scales, fractions,
               directed_box, core_iv, verified_hull, _kernel, base_axes, float_box, float_sequence, migrate, compute):
        digest.update(inspect.getsource(fn).encode())
    for fn in r30.CERT_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(key_bytes)
    return digest.hexdigest()


def computed(cell, ledger, key_bytes):
    key = _key(key_bytes + json.dumps(cell, sort_keys=True).encode())
    if CACHE.exists():
        cached = json.loads(CACHE.read_text(encoding="utf-8"))
        if cached.get("key") == key:
            return cached["results"]
    results = json.loads(json.dumps(compute(cell, ledger)))
    CACHE.parent.mkdir(parents=True, exist_ok=True)
    CACHE.write_text(json.dumps({"key": key, "results": results}) + "\n", encoding="utf-8")
    return results


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = {EDGE24, r30.TIGHT12, r29.LEDGER}
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id.startswith(PKG) or l.id in want) if d is not None}
    return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "rootrec": json.loads(got[ROOTREC]),
            "bulk": json.loads(got[BULK]), "certman": json.loads(got[CERTMAN]), "policy": json.loads(got[POLICY]),
            "validation": json.loads(got[VALIDATION]), "leaves28": json.loads(got[LEAVES]), "topology": got[TOPO], "axes": got[AXES],
            "raw": {name: hashlib.sha256(got[name]).hexdigest() for name in (ROOTREC, BULK, CERTMAN, POLICY, LEAVES, TOPO, AXES)},
            "edge": json.loads(got[EDGE24]), "tight12": json.loads(got[r30.TIGHT12]),
            "code": sorted(k[len(PKG):] for k in got if k.startswith(PKG) and k.endswith(".py")),
            "ledger_bytes": got[r29.LEDGER], "key_bytes": got[LEAVES], "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))}


ANCHORS = {
    "W1": [r"\boxed{T_M=\frac{1673}{2000}.}", r"\boxed{T=\frac{167}{200}.}", r"F(d)=\frac14\left(\pi-\arccos\frac1{2d}\right)+\frac12\sqrt{d^2-\frac14}.",
           r"\boxed{d_\star\in[d_-,d_+].}", r"$$O(10^{-63}).$$", r"R_n=\frac1{2\sin((n-1)\pi/(2n))}.",
           r"t_n=-R_n\cos\frac\pin+\sqrt{R_n^2\cos^2\frac\pin-R_n^2+d_\star^2}.", r"$$10^{-50}.$$", r"$$0\lex_3\let_3,$$",
           r"$$0\ley_3\le\frac{\sqrt3}{2}t_3,$$", r"$$0\le\phi_5\le\frac{2\pi}{5},$$", r"$$|x_5|,|y_5|\let_5.$$", r"$$0\le\phi_7\le\frac{2\pi}{7},$$",
           r"$$|x_7|,|y_7|\let_7.$$"],
    "W2": [r"$$\boxed{40}.$$", r"\boxed{0\text{CPGoverrides}}", r"$$\boxed{0}.$$所以這條path本身恰好完全走officialaxis", r"$$10^{-17}$$級",
           r"$$C=C_0\cupC_1.$$", r"\boxed{[a,b]=[a,m]\cup[m,b].}"],
    "W3": [r"$$18555\text{nodes},$$", r"$$9278\text{leaves}.$$", r"$$\boxed{9277}$$", r"$$2.1\times10^{-16}.$$"],
    "W4": [r"$$256,512,1024,2048,4096,8192,16384.$$", r"##256$$821$$leaves。", r"##512$$3425.$$", r"##1024$$3709.$$", r"##2048$$1115.$$",
           r"##4096$$163.$$", r"##8192$$39.$$", r"$$\boxed{6}.$$", r"\boxed{9278/9278\text{PASS}}", r"\boxed{\text{directmigrationfraction}=1.}",
           r"\boxed{\text{selectiveresplitfraction}=0.}", r"\boxed{\text{failures}=0.}", r"\boxed{3.1948922738\times10^{-8}.}",
           r"1101011010010011111001110", r"\boxed{D_{\max}^2<\rho_{\rmlo}^2,}", r"$$A(P)>\frac{167}{200},$$"],
    "P1": [r"\boxed{\texttt{CELL0-ARITHMETIC-MIGRATED-PROTOTYPE}}", r"a_{\mathrm{Leb}}\ge0.835\text{remainsNOTCERTIFIED}."],
}

CLAIMS = {
    # this tree's brackets (1e-90 wide) inside the package's; the binary64 roots in units in the last place above (+)
    # or below (-) the exact, [this tree's, the shipped state's]: the translations above, both angles short
    "root": {"inside": {"d": True, "t3": True, "t5": True, "t7": True},
             "floats": {"t3": [7.01, 1.01], "y3": [6.18, 0.18], "phi5": [-0.22, -0.22], "t5": [8.77, 4.77], "phi7": [-0.32, -0.32],
                        "t7": [7.39, 3.39]}},
    # the 40 axes and their counts per coordinate (x3, y3, phi5, x5, y5); the shipped cell reproduces the distance table,
    # and sits up to 6 units from this tree's binary64 cell
    "base": {"axes_equal": True, "splits": {0: 7, 1: 7, 2: 9, 3: 9, 4: 8}, "table": True, "stored_ulps_apart": 6},
    # distances [all nodes' centres, halves, the leaves' centres, halves]: the package's pair is the shipped tree's leaves
    "witness": {"nodes": 18555, "internal": 9277, "leaves": 9278, "leaf_paths_equal": True, "axes": {"high-first": True, "low-first": False},
                "shipped_replay": True,
                "distances": {"own": [2.1013778688701305e-16, 2.0523899368121494e-16, 2.1013778688701305e-16, 1.0261949684060747e-16],
                              "shipped": [2.1013778688701305e-16, 9.42166912186993e-17, 2.1013778688701305e-16, 4.710834560934965e-17]}},
    # every leaf passes at the ledger's density with its candidate count; the least density that passes is lower for 8457
    # leaves, and no leaf needs 16384
    "migration": {"leaves": 9278, "missing_in_ledger": 0, "passed": 9278, "failures": 0, "density_used": True,
                  "least": ["1101011010010011111001110", 3.194892273812446e-08], "margin_difference": 1.6783449630075609e-16,
                  "candidates_equal": 9278, "ladder": {"256": 7727, "512": 1285, "1024": 177, "2048": 67, "4096": 18, "8192": 4},
                  "below_ledger": 8457, "ladder_not_above_ledger": True, "bands_disjoint": True},
    # this tree's kernel loses a piece inside one grid step on one leaf, 1.47e-9 low; verified, it is the package's to 1.7e-15
    "kernel": {"changed": [["001110010110000100", 1.474065092210708e-09, 1]], "one_sided": True,
               "old_vs_reference": 1.4740645370991956e-09, "verified_vs_reference": 1.6653345369377348e-15, "shared_is_verified": True},
}


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


def scales_of(w):
    return {k: (int(v[0]), int(v[1])) for k, v in w["computed"]["scales"].items()}


def w1_root(w):
    """sec. 1-4: this tree's brackets of d* and t_n inside the package's intervals, and where the
    binary64 roots - this tree's and the shipped state's - sit against the exact ones"""
    out, rr, sc = [], w["rootrec"], scales_of(w)
    theirs = {"d": rr["d_star_interval"], **{k: rr["tmax_intervals"][k] for k in ("t3", "t5", "t7")}}
    inside_theirs = {k: Fraction(v["lo"]) <= Fraction(sc[k][0], ONE) and Fraction(sc[k][1], ONE) <= Fraction(v["hi"]) for k, v in theirs.items()}
    mid = {k: Fraction(v[0] + v[1], 2 * ONE) for k, v in sc.items()}
    count = collections.Counter(rr["base_axis_trace"])
    bh, tn = w["edge"]["base_halfwidth"], t_text(7, d_star(TM))
    ship7 = {v * 2 ** round(math.log2(tn / v)) for r in w["tight12"] for v in r["wh"][1:]}
    t3 = t_text(3, d_star(TM))
    values = {"t3": [t3, bh[0] * 2 ** (count[0] + 1)], "y3": [2 * (r20.S3 / 4 * t3), bh[1] * 2 ** (count[1] + 1)],
              "phi5": [2 * (math.pi / 5)] * 2, "t5": [t_text(5, d_star(TM)), bh[3] * 2 ** count[3]], "phi7": [2 * (math.pi / 7)] * 2,
              "t7": [tn, min(ship7)]}
    floats = {k: [round(float((Fraction(v) - mid[k]) / Fraction(math.ulp(v))), 2) for v in vals] for k, vals in values.items()}
    widths = {k: float(Fraction(sc[k][1] - sc[k][0], ONE)) for k in theirs}
    got = {"inside": inside_theirs, "floats": floats}
    if not all(inside_theirs.values()) or len(ship7) != 1 or max(widths.values()) > 1e-80 or got != w["root"]:
        out.append(f"the root: {got}, widths {widths}")
    w["w1"] = {**got, "widths": widths, "package_widths": {k: float(Fraction(v["hi"]) - Fraction(v["lo"])) for k, v in theirs.items()},
               "exact": {k: str(mpmath.mpf(v.numerator) / v.denominator) for k, v in mid.items()}}
    return out


def w2_base(w):
    """sec. 5-7: cell 0's 40 base splits from the D3 root - the axes, the intended box, and the stored
    box's distance to it (the shipped cell reproduces the package's table; this tree's cell differs by a
    few units in the last place)"""
    out, rr, cm, edge = [], w["rootrec"], w["certman"], w["edge"]
    path, sc = rr["base_path"], scales_of(w)
    axes, c, h = base_axes(path)
    lo, hi = fractions(path, axes, 5)
    bc, bh = directed_box(lo, hi, BASE, sc)
    shipped = [(distance(edge["base_center"][k], bc[k]), distance(edge["base_halfwidth"][k], bh[k])) for k in range(5)]
    own = [(distance(c[k], bc[k]), distance(h[k], bh[k])) for k in range(5)]
    table = all(near(s[0], r["stored_center_distance_to_directed_interval"], 1e-12 * r["stored_center_distance_to_directed_interval"])
                and near(s[1], r["stored_half_distance_to_directed_interval"], 1e-12 * r["stored_half_distance_to_directed_interval"])
                for s, r in zip(shipped, rr["base_stored_vs_directed"]))
    apart = max(r30.ulps(a, b) for a, b in zip(c + h, edge["base_center"] + edge["base_halfwidth"]))
    got = {"axes_equal": axes == rr["base_axis_trace"] == cm["base_axis_trace"], "splits": dict(sorted(collections.Counter(axes).items())),
           "table": table, "stored_ulps_apart": apart}
    if not got["axes_equal"] or len(axes) != 40 or path != edge["base_path"] or path != w["computed"]["cell"]["path"] or rr["base_override_count"] != 0 \
            or not table or got != w["base"]:
        out.append(f"the base: {got}")
    w["w2"] = {**got, "shipped_distances": shipped, "own_distances": own}
    return out


_WITNESS = {}


def witness_distances(topology, seq_own, seq_ship, t_own, t_ship, sc):
    """every node's stored box against its intended box, for this tree's binary64 tree and the shipped
    one: the largest centre and half-width distances over all nodes and over the leaves"""
    key = hashlib.sha256(topology).hexdigest()
    if key not in _WITNESS:
        nodes = decode_topology(topology, 18555)
        axes = [a for a, _ in seq_own]
        res = {}
        for name, seq, root in (("own", seq_own, t_own), ("shipped", seq_ship, t_ship)):
            worst = [0.0, 0.0, 0.0, 0.0]
            for p, internal in nodes:
                wc, wh = float_box(p, seq, root)
                lo, hi = fractions(p, axes, 3)
                cc, hh = directed_box(lo, hi, WITNESS, sc)
                dc = max(distance(wc[k], cc[k]) for k in range(3))
                dh = max(distance(wh[k], hh[k]) for k in range(3))
                worst[0], worst[1] = max(worst[0], dc), max(worst[1], dh)
                if not internal:
                    worst[2], worst[3] = max(worst[2], dc), max(worst[3], dh)
            res[name] = worst
        _WITNESS[key] = res
    return _WITNESS[key]


def w3_witness(w):
    """sec. 8-9: the topology and the 2-bit axis stream against this tree's lift; the stored boxes'
    distances to the intended ones"""
    out, rr, sc = [], w["rootrec"], scales_of(w)
    try:
        nodes = decode_topology(w["topology"], rr["witness_tree"]["nodes"])
    except ValueError as e:
        w["w3"] = {"topology": str(e)}
        return [f"the witness tree: {e}"]
    internal = [p for p, b in nodes if b]
    leaves = [p for p, b in nodes if not b]
    tn = t_text(7, d_star(TM))
    ship = {v * 2 ** round(math.log2(tn / v)) for r in w["tight12"] for v in r["wh"][1:]}
    t_ship = min(ship)
    seq_own, seq_ship = float_sequence(tn, 30), float_sequence(t_ship, 30)
    axes_same = [a for a, _ in seq_own] == [a for a, _ in seq_ship]
    match = {order: decode_axes(w["axes"], len(internal), order == "high-first") == [seq_own[len(p)][0] for p in internal]
             for order in ("high-first", "low-first")}
    replay = all(float_box(r["path"], seq_ship, t_ship) == (r["wc"], r["wh"]) for r in w["tight12"])
    dist = witness_distances(w["topology"], seq_own, seq_ship, tn, t_ship, sc)
    got = {"nodes": len(nodes), "internal": len(internal), "leaves": len(leaves),
           "leaf_paths_equal": sorted(leaves) == sorted(p for p, _ in w["computed"]["leaves"]), "axes": match, "shipped_replay": replay,
           "distances": dist}
    wt = rr["witness_tree"]
    if (len(nodes), len(internal), len(leaves)) != (wt["nodes"], wt["internal_nodes"], wt["leaves"]) or not got["leaf_paths_equal"] \
            or not any(match.values()) or not axes_same or not replay or wt["axis_stream_bits"] != 2 * len(internal) \
            or not near(dist["shipped"][2], wt["max_stored_center_distance_to_directed_interval"], 1e-12 * dist["shipped"][2]) \
            or not near(dist["shipped"][3], wt["max_stored_half_distance_to_directed_interval"], 1e-12 * dist["shipped"][3]) or got != w["witness"]:
        out.append(f"the witness tree: {got}")
    w["w3"] = got
    return out


def w4_leaves(w):
    """sec. 10-18: every leaf of this tree's lift certified on its intended box at the ledger's density
    for the same path, and the least density that passes; the ledger's bands"""
    out, led, comp = [], w["leaves28"], w["computed"]
    by_path = {x["path"]: x for x in led}
    rows = [(p, area, r, by_path.get(p)) for (p, area), r in zip(comp["leaves"], comp["results"])]
    missing = sum(L is None for _, _, _, L in rows)
    rows = [x for x in rows if x[3] is not None]
    at = [r["ledger"] for _, _, r, _ in rows]
    least = min(rows, key=lambda x: x[2]["ledger"]["margin"])
    ladder = collections.Counter(r["least"]["n"] if r["least"] else None for _, _, r, _ in rows)
    bands = {}
    for L in led:
        b = bands.setdefault(str(L["density"]), [L["reference_slack"], L["reference_slack"]])
        b[0], b[1] = min(b[0], L["reference_slack"]), max(b[1], L["reference_slack"])
    ordered = [bands[str(n)] for n in DENSITIES if str(n) in bands]
    got = {"leaves": len(comp["leaves"]), "missing_in_ledger": missing, "passed": sum(a["pass"] for a in at),
           "failures": sum(a["failures"] for a in at), "density_used": [a["n"] for a in at] == [L["density"] for _, _, _, L in rows],
           "least": [least[0], least[2]["ledger"]["margin"]],
           "margin_difference": max(abs(a["margin"] - L["rational_margin_decimal"]) for a, (_, _, _, L) in zip(at, rows)),
           "candidates_equal": sum(a["candidates"] == L["candidate_vertices"] for a, (_, _, _, L) in zip(at, rows)),
           "ladder": {str(k): v for k, v in sorted(ladder.items(), key=lambda x: x[0] or 0)},
           "below_ledger": sum(r["least"]["n"] < L["density"] for _, _, r, L in rows if r["least"]),
           "ladder_not_above_ledger": all(r["least"] and r["least"]["n"] <= L["density"] for _, _, r, L in rows),
           "bands_disjoint": all(a[1] < b[0] for a, b in zip(ordered[1:], ordered[:-1]))}
    if got["leaves"] != len(led) or missing or got["passed"] != len(led) or got["failures"] or not got["density_used"] \
            or least[0] != w["bulk"]["minimum_exact_rational_margin_path"] or got["margin_difference"] > 1e-15 \
            or not got["ladder_not_above_ledger"] or not got["bands_disjoint"] or got != w["migration"]:
        out.append(f"the migration: {got}")
    w["w4"] = {**got, "bands": bands}
    return out


def w5_kernel(w):
    """this tree's exact kernel - the grid envelope alone, as it was before this round - against the
    verified one on every leaf, and both against the package's reference slacks: the error is one-sided,
    and where it errs the package's kernel is right; the shared kernel, corrected, is the verified one"""
    out, comp = [], w["computed"]
    by = {x["path"]: x for x in w["leaves28"]}
    rows = [(p, k, by.get(p)) for (p, _), k in zip(comp["leaves"], comp["kernel"])]
    changed = [[p, k[1] - k[0], k[2]] for p, k, _ in rows if abs(k[1] - k[0]) > 1e-14]
    got = {"changed": changed, "one_sided": all(k[1] >= k[0] - 1e-15 for _, k, _ in rows),
           "old_vs_reference": max(abs(k[0] - 1e-10 - T - L["reference_slack"]) for _, k, L in rows),
           "verified_vs_reference": max(abs(k[1] - 1e-10 - T - L["reference_slack"]) for _, k, L in rows),
           "shared_is_verified": max(abs(k[3] - k[1]) for _, k, _ in rows) <= 1e-15}
    if any(L is None for _, _, L in rows) or not got["one_sided"] or got["verified_vs_reference"] > 5e-15 or got != w["kernel"]:
        out.append(f"the kernel: {got}")
    w["w5"] = got
    return out


def p1_package(w):
    out, rr, bulk, cm, pol, led, raw = [], w["rootrec"], w["bulk"], w["certman"], w["policy"], w["leaves28"], w["raw"]
    counts = {str(k): v for k, v in sorted(collections.Counter(x["density"] for x in led).items())}
    least = min(led, key=lambda x: x["rational_margin_decimal"])
    if len(led) != 9278 or [x["index"] for x in led] != list(range(len(led))) or counts != bulk["density_counts"] \
            or any(x["status"] != "RATIONAL-INTERVAL-PASS" or x["membership_failures"] or not x["convex_order_verified_exactly"] for x in led) \
            or (least["path"], least["rational_margin_decimal"]) != (bulk["minimum_exact_rational_margin_path"], bulk["minimum_exact_rational_margin_decimal"]) \
            or any(len(x["path"]) != x["depth"] for x in led):
        out.append("the ledger against the migration file")
    lm = cm["leaf_migration"]
    if (lm["leaves_total"], lm["leaves_pass"], lm["leaves_inconclusive"]) != (bulk["leaves_total"], bulk["leaves_pass"], bulk["leaves_inconclusive"]) \
            or (lm["minimum_exact_rational_margin_decimal"], lm["minimum_exact_rational_margin_path"]) != (bulk["minimum_exact_rational_margin_decimal"], bulk["minimum_exact_rational_margin_path"]) \
            or (pol["bulk_result"]["leaves_total"], pol["bulk_result"]["leaves_pass"]) != (bulk["leaves_total"], bulk["leaves_pass"]) \
            or (cm["base_path"], cm["base_axis_trace"], cm["base_override_count"]) != (rr["base_path"], rr["base_axis_trace"], rr["base_override_count"]) \
            or cm["witness_tree"]["nodes"] != rr["witness_tree"]["nodes"] \
            or {pol["root_rule"]["master_target"], cm["master_target_exact"], rr["master_target_exact"]} != {"1673/2000"}:
        out.append("the manifest, the policy and the root file against the migration file")
    digests = {"topology": (hashlib.sha256(w["topology"]).hexdigest(), rr["witness_tree"]["topology_sha256"], cm["witness_tree"]["topology_sha256"],
                            bulk["topology_sha256"]),
               "axes": (hashlib.sha256(w["axes"]).hexdigest(), rr["witness_tree"]["axis_stream_sha256"], cm["witness_tree"]["axis_stream_sha256"],
                        bulk["witness_axis_stream_sha256"]),
               "ledger": (raw[LEAVES], cm["leaf_migration"]["ledger_sha256"], bulk["leaf_ledger_sha256"]),
               "root": (raw[ROOTREC], cm["root_reconstruction_sha256"], bulk["root_reconstruction_sha256"])}
    for name, ds in digests.items():
        if len(set(ds)) != 1:
            out.append(f"the {name} digests")
    widths = {k: float(Fraction(v["hi"]) - Fraction(v["lo"])) for k, v in {"d": rr["d_star_interval"], **rr["tmax_intervals"]}.items()}
    if any(not near(widths[k], v["width_decimal"], 1e-3 * v["width_decimal"]) for k, v in {"d": rr["d_star_interval"], **rr["tmax_intervals"]}.items()):
        out.append("the root file's widths")
    crystal = gate.squash(w["crystal"])
    for frag in ("T=167/200,", "T_M=1673/2000.", "-256:821leaves", "-512:3425", "-1024:3709", "-2048:1115", "-4096:163", "-8192:39",
                 "-16384:6", r"\boxed{9278/9278\text{PASS}.}", r"\boxed{3.1948922738\times10^{-8}.}", "-18,555nodes", "-9,277internalnodes"):
        if frag not in crystal:
            out.append(f"crystal: {frag}")
    if w["code"]:
        out.append(f"scripts shipped: {w['code']}")
    w["p1"] = {"density_counts": counts, "d_width": widths["d"], "text_says_d_width": "O(1e-63)"}
    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 (("round28", 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 (("root_reconstruction_sha256", ROOTREC), ("bulk_migration_sha256", BULK), ("certificate_manifest_sha256", CERTMAN),
                         ("migration_policy_sha256", POLICY), ("leaf_ledger_sha256", LEAVES), ("axis_stream_sha256", AXES)):
        if v[key] != leaves[leaf_id][2]:
            out.append(f"VALIDATION {key} against the archive")
    rr, bulk, cm, led = w["rootrec"], w["bulk"], w["certman"], w["leaves28"]
    kc = {"root_reconstruction_pass": rr["status"] == "DIRECTED-ROOT-PATH-RECONSTRUCTION-PASS",
          "base_path_depth_40": len(rr["base_path"]) == rr["base_path_depth"] == 40, "base_axis_trace_40": len(rr["base_axis_trace"]) == 40,
          "base_override_zero": rr["base_override_count"] == 0, "leaf_count_9278": len(led) == bulk["leaves_total"] == 9278,
          "all_leaves_pass": bulk["leaves_pass"] == bulk["leaves_total"] and all(x["status"] == "RATIONAL-INTERVAL-PASS" for x in led),
          "no_inconclusive": bulk["leaves_inconclusive"] == 0, "no_membership_failures": sum(x["membership_failures"] for x in led) == 0,
          "min_exact_margin_positive": min(x["rational_margin_decimal"] for x in led) > 0, "publication_scope_false": bulk["publication_scope"] is False,
          "global_claim_false": cm["global_lebesgue_claim"] is False}
    if kc != v["checks"] or v["status"] != "PASS":
        out.append(f"VALIDATION checks {kc}")
    w["p2"] = kc
    return out


R28_DEFINITIONS = {
    "PUBLICATION-CANDIDATE": ("in-line", "sec. 25: a certificate that has passed its own arithmetic replay and awaits independent audit - "
                                         "not a theorem"),
    "PUBLICATION-CANDIDATE LIFT SHARD": ("in-line", "sec. 25: the first shard to be so named once cell 0's independent A1 arithmetic replay "
                                                    "passes (Round 29)"),
    "RATIONAL-INTERVAL-PASS": ("in-line", "sec. 13, 15: a leaf whose interval-verified rational inner polygon has exact area above 167/200"),
    "REFERENCE-COMPLETE": ("in-line", "sec. 19: a tree complete under the reference (binary64, padded) arithmetic"),
    "CELL0-ARITHMETIC-MIGRATED-PROTOTYPE": ("in-line", "sec. 0, 19: cell 0 with a directed root, explicit splits and every leaf "
                                                       "RATIONAL-INTERVAL-PASS, under a prototype backend"),
}
R28_REVIEWS = [
    ("PASS", "cell0 base path explicitization", "computation", "PASS", "the 40 axes are the official split's, replayed here (W2)"),
    ("PASS", "witness split-axis stream", "computation", "PASS", "the stream decodes to this tree's axes node for node (W3)"),
    ("PASS", "9278/9278", "computation", "PASS",
     "every leaf passes here too on its intended box, with the ledger's candidate counts and margins to 1.7e-16 (W4)"),
    ("PASS", "9278/9278", "computation", "PASS",
     "every leaf passes here too on its intended box, with the ledger's candidate counts and margins to 1.7e-16 (W4)"),
    ("CLOSED", "Exact rational master target", "reading", "PASS", "1673/2000 and 167/200 throughout"),
    ("OPEN", "publication backend pinning", "reading", "PASS", "true: mpmath.iv is still the backend, and no script is shipped"),
    ("OPEN", "global arithmetic replay", "reading", "PASS", "true: one cell of 77"),
    ("IMPLEMENTED", "Directed $d_\\star$", "computation", "PASS", "this tree's bracket, 1e-90 wide, lies inside the package's (W1)"),
    ("IMPLEMENTED", "Directed $t_3,t_5,t_7$", "computation", "PASS", "this tree's brackets lie inside the package's (W1)"),
    ("IMPLEMENTED", "D3 root reconstruction", "computation", "PASS", "the intended base box reproduces the package's distance table (W2)"),
    ("NOT CERTIFIED", "global $a_{\\mathrm{Leb}}\\ge0.835$", "reading", "PASS", "true"),
    ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"),
    ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"),
    ("RATIONAL-INTERVAL-PASS", "15. Bulk migration result", "computation", "PASS", "every leaf here too, on the intended boxes (W4)"),
    ("REFERENCE-COMPLETE", "", "n/a", "n/a", "a label of sec. 19, defined there; not a judgment"),
    ("CELL0-ARITHMETIC-MIGRATED-PROTOTYPE", "", "computation", "PASS",
     "right, as a prototype: the root, the splits and every leaf check under this tree's own arithmetic (W1-W4)"),
    ("CELL0-ARITHMETIC-MIGRATED-PROTOTYPE", "", "computation", "PASS",
     "right, as a prototype: the root, the splits and every leaf check under this tree's own arithmetic (W1-W4)"),
    ("PUBLICATION-CANDIDATE LIFT SHARD", "", "n/a", "n/a", "a goal of sec. 25 for Round 29; not a judgment"),
]


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


CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_root, "W2": w2_base, "W3": w3_witness, "W4": w4_leaves, "W5": w5_kernel,
          "P1": p1_package, "P2": p2_package, "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "W1": {"computed", "rootrec", "edge", "tight12", "root"},
           "W2": {"computed", "rootrec", "certman", "edge", "base"}, "W3": {"computed", "rootrec", "topology", "axes", "tight12", "witness"},
           "W4": {"computed", "leaves28", "bulk", "migration"}, "W5": {"computed", "leaves28", "kernel"},
           "P1": {"rootrec", "bulk", "certman", "policy", "leaves28", "raw", "topology", "axes", "crystal", "code"},
           "P2": {"validation", "manifest", "text", "crystal", "rootrec", "bulk", "certman", "leaves28"},
           "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()
    atlas = r29.computed(inputs["ledger_bytes"])
    cert = next(a for a in atlas["atlas"] if a["path"] == atlas["certificate"]["path"])
    cell = {k: cert[k] for k in ("path", "center", "half")}
    results_computed = {**computed(cell, inputs["leaves28"], inputs["key_bytes"]), "cell": cell}

    def build():
        return {**{k: v for k, v in inputs.items() if k not in ("ledger_bytes", "key_bytes")}, "computed": results_computed,
                "registry": registry.load(), "definitions": dict(R28_DEFINITIONS), "reviews": list(R28_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
    rr, led, text = inputs["rootrec"], inputs["leaves28"], inputs["text"]

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

    def shift_lo(x):
        lo = Fraction(x["tmax_intervals"]["t7"]["hi"]) - Fraction(1, 10 ** 70)
        x["tmax_intervals"]["t7"]["lo"] = f"{lo.numerator}/{lo.denominator}"

    k = next(i for i, x in enumerate(led) if x["density"] == 512)
    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()),
        ("K2-root-keys-sorted", "control", {"rootrec": json.loads(json.dumps(rr, sort_keys=True))}, set()),
        ("K3-bulk-keys-sorted", "control", {"bulk": json.loads(json.dumps(inputs["bulk"], sort_keys=True))}, set()),
        ("M1-doc-density", "mutation", {"text": text.replace("3425.", "3426.")}, {"A0"}),
        ("M2-t7-interval", "mutation", {"rootrec": edit(rr, shift_lo)}, {"W1", "P1"}),
        ("M3-root-claim", "mutation", {"root": {**CLAIMS["root"], "floats": {}}}, {"W1"}),
        ("M4-base-trace", "mutation", {"rootrec": edit(rr, lambda x: x["base_axis_trace"].__setitem__(slice(0, 2), [3, 2]))}, {"W2", "P1"}),
        ("M5-base-distance", "mutation",
         {"rootrec": edit(rr, lambda x: x["base_stored_vs_directed"][3].update(stored_center_distance_to_directed_interval=6.7e-18))}, {"W2"}),
        ("M6-topology-bit", "mutation", {"topology": inputs["topology"][:5] + bytes([inputs["topology"][5] ^ 0x10]) + inputs["topology"][6:]},
         {"W3", "P1"}),
        ("M7-axis-bit", "mutation", {"axes": inputs["axes"][:40] + bytes([inputs["axes"][40] ^ 0x80]) + inputs["axes"][41:]}, {"W3", "P1"}),
        ("M8-witness-distance", "mutation",
         {"rootrec": edit(rr, lambda x: x["witness_tree"].update(max_stored_center_distance_to_directed_interval=2.2e-16))}, {"W3"}),
        ("M9-leaf-margin", "mutation", {"leaves28": edit(led, lambda x: x[100].update(rational_margin_decimal=x[100]["rational_margin_decimal"] + 1e-9))},
         {"W4"}),
        ("M10-leaf-density", "mutation", {"leaves28": edit(led, lambda x: x[k].update(density=1024))}, {"W4", "P1"}),
        ("M11-migration-claim", "mutation", {"migration": {**CLAIMS["migration"], "ladder": {}}}, {"W4"}),
        ("M17-reference-slack", "mutation", {"leaves28": edit(led, lambda x: x[200].update(reference_slack=x[200]["reference_slack"] + 1e-12))},
         {"W5"}),
        ("M18-kernel-claim", "mutation", {"kernel": {**CLAIMS["kernel"], "changed": []}}, {"W5"}),
        ("M12-bulk-counts", "mutation", {"bulk": {**inputs["bulk"], "density_counts": {**inputs["bulk"]["density_counts"], "16384": 7}}}, {"P1"}),
        ("M13-crystal", "mutation", {"crystal": inputs["crystal"].replace("- 16384: 6", "- 16384: 7")}, {"P1"}),
        ("M14-validation-digest", "mutation", {"validation": {**inputs["validation"], "leaf_ledger_sha256": "0" * 64}}, {"P2"}),
        ("M15-validation-check", "mutation",
         {"validation": {**inputs["validation"], "checks": {**inputs["validation"]["checks"], "base_override_zero": False}}}, {"P2"}),
        ("M16-review-dropped", "mutation", {"reviews": list(R28_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-031", "subject": "Round 28: exact root reconstruction and the bulk rational-interval migration of cell 0",
           "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("R28", "RUN-031", R28_DEFINITIONS, R28_REVIEWS)
        print(f"registry: {len(R28_DEFINITIONS)} definitions, {len(R28_REVIEWS)} reviews recorded for R28")


if __name__ == "__main__":
    main()