"""RUN-012 - Round 09: adaptive atlas refinement and certificate-cost minimization.

Round 09 adds no proof domain; it prices Round 08's certificate. A cell's hulls stay
within a Hausdorff radius tau(C) = max_i delta_i of its centre's hull (Thm 1.1,
sec. 2-4); a hull holding B_{1/2} has Per <= 4 Area (sec. 5), so the representative
transfer costs 4T tau + pi tau^2 instead of Round 07's 4 pi T tau + pi tau^2 (Thm 6.1);
a representative margin m closes a cell of radius tau_star(m, T) (sec. 8); the split
that most reduces tau is chosen exactly (sec. 10-14); a representative prune goes
before the common core (sec. 15-17); lift trees are reused across cells whose base
cores are nested (sec. 18-21); a witness containing another lifts at least as high
(sec. 22-23); a uniform margin bounds the depth (sec. 25). Here each is tested on cells
of the 0.835 root and on RUN-011's two leaves, the numbers are rebuilt, and the
repository facts Round 09 leans on are read at the commit Mishra's paper pins.

Checks
  A0 anchors      the formulas and numbers below occur in Round 09 as written
  X1 repository   Mishra's split rule (the angle axis weighted by the circumradius) and
                  his support pieces c.u + r, at commit da956b1
  W1 radius       sec. 1-4: d_H(H(q), H(q_C)) <= tau(C) on random cells, base and joint
  W2 transfer     sec. 5-7: Per <= 4 Area for hulls holding the disc; the Steiner transfer
  W3 resolution   sec. 8-9, 29: tau_star in closed form, and its numbers
  W4 scheduler    sec. 10-14: tau at the root and after each single split; the first cut;
                  the Taylor term; Mishra's weight rule beside it
  W5 prunes       sec. 15-16: the representative prune at RUN-011's two leaves against the
                  exact common core, and the widest cell each closes
  W6 dominance    sec. 18-21: exact core pieces; containment from merged breakpoints
                  against dense sampling; Thm 19.1 on containing pairs
  W7 witnesses    sec. 22-23: a witness containing another lifts at least as high; the
                  regular witnesses of Round 08's pool have constant width 1
  W8 depth        sec. 25: tau_r <= 2^-r S_0 under full cycles; the depth at the root
  P1 package      VALIDATION and LOCAL_COMPUTE_SPEC against the text
  P2 package      the package's self-description of its files matches the archive
  R1 registry     Round 09's judgments reviewed, first-used statuses defined

Usage: python code/run012_round09_adaptive_atlas.py [--refresh] [--drill] [--blind CID]
"""
import argparse
import datetime
import json
import math
import re

import numpy as np
import sympy as sp
from scipy.spatial import ConvexHull

import gate
import registry
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run008_round05_saturation_gate import R0, disc_samples, envelope, reuleaux_support, reuleaux_vertices, segments, verify_segments, wrap
from run009_round06_witness_exchange import hull_pieces, placed_disc, placed_polygon, placed_reuleaux
from run010_round07_minimizer_atlas import COMMIT, REPO, d_star, t_text
from run011_round08_conditional_lift import motion_delta, placed_vertices, reuleaux_core_points

PKG = "main.zip!/AMRAL_LUC_FC_Round_09_Package_v0.1.zip!/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_09_Adaptive_Atlas_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_09_v0.1.md"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_09_VALIDATION.json"
SPEC = PKG + "AMRAL_LUC_FC_Round_09_LOCAL_COMPUTE_SPEC.json"
SNAPSHOT = TREE / "data" / "external" / "round09-repository.json"
ROUND07 = TREE / "data" / "external" / "round07-citations.json"
RUN010 = TREE / "data" / "gate-logs" / "run010-round07-minimizer-atlas.json"
RUN011 = TREE / "data" / "gate-logs" / "run011-round08-conditional-lift.json"
LOG = TREE / "data" / "gate-logs" / "run012-round09-adaptive-atlas.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"

T1 = 0.835
M_SEARCH = 0.001494901                  # the four-body search headroom Round 09 uses for scale
R3, R5, R7 = (1 / (2 * math.cos(math.pi / (2 * n))) for n in (3, 5, 7))
AXES = ("x3", "y3", "phi5", "x5", "y5")

ANCHORS = {
    "W2": [r"\operatorname{Area}(U)\ge\fracr2\operatorname{Per}(U).", r"\operatorname{Per}(U)\le4\operatorname{Area}(U).",
           r"\Omega_T(\tau)=4T\tau+\pi\tau^2.", r"4\piT\tau+\pi\tau^2."],
    "W3": [r"\frac{\sqrt{T^2/r^2+\pim}-T/r}{\pi}.", r"\tau_\star(m,T)=\frac{\sqrt{4T^2+\pim}-2T}{\pi}.",
           r"\tau_\star\approx4.47387\times10^{-4}.", r"1.42462\times10^{-4}.", r"\tau_\star\approx0.0004473869.",
           r"0.0001424615.", r"\approx3.14.", r"m=0.001494901"],
    "W4": [r"h_{x3}=h_{y3}=0.194856180909", r"h_{x5}=h_{y5}=0.197820670401", r"R_5=0.525731112119.",
           r"d_3\approx0.2755682538", r"d_5\approx0.6046803712", r"\tau_{\rmroot}\approx0.6046803712",
           r"\tau_{x3}=\tau_{y3}\approx0.6046803712", r"\tau_{\phi5}\approx0.4442456056",
           r"\tau_{x5}=\tau_{y5}\approx0.5460899294", r"Rh_\phi-\frac{Rh_\phi^3}{24}",
           r"\delta_\phi=\sqrt{h_x^2+h_y^2}+2R\sin\frac{h_\phi}{4}."],
    "W5": [r"s:=\max\{\tau(C),\delta_K\}.", r"\underlineA(H_0)-4Ts-\pis^2\geT,"],
    "W6": [r"h_{G(C_b)}(\theta)\leh_{G(C_a)}(\theta)"],
    "W7": [r"J_L(H)\geJ_K(H)."],
    "W8": [r"S_0=\max_i\left[\sqrt{h_{xi}^2+h_{yi}^2}+R_ih_{\phii}\right].", r"\tau_r\le2^{-r}S_0.",
           r"r\ge\left\lceil\log_2\frac{S_0}{\tau_\star(m,T)}\right\rceil."],
}
REPO_FACTS = {                          # short phrases only, from the files at the pinned commit
    "src/geom.py": {"support_pieces": r"support function\s+h\(theta\) = <c_j, u\(theta\)> \+ r_j",
                    "sinusoid": r"Every piece has support\s+h\(t\) = cx cos t \+ cy sin t \+ r"},
    "src/verifyB.py": {"split_weights": r"w = \(b\[1\], b\[3\], CIRC5\*b\[5\], b\[7\], b\[9\]\)",
                       "circumradius": r"CIRC5 = float\(np\.max\(np\.hypot\(V5\[:, 0\], V5\[:, 1\]\)\)\)",
                       "widest": r"k = int\(np\.argmax\(w\)\)",
                       "children": r"n\[2\*k\+1\] = half\*\(1\.0\+inflate\)"},
    "src/certemitB.py": {"inflate": r"INFLATE = 1e-11"},
}


# ---------------------------------------------------------------- geometry

RS = {n: reuleaux_support(n) for n in (3, 5, 7, 9, 11, 13)}


def root_box(T=T1):
    """the base root at T: centre and half-widths of (x3, y3, phi5, x5, y5)"""
    t3, t5 = t_text(3, d_star(T)), t_text(5, d_star(T))
    return np.array([0.0, 0.0, math.pi / 5, 0.0, 0.0]), np.array([t3, t3, math.pi / 5, t5, t5])


def tau_f3(h):
    """sec. 3: the family radius of a base cell, B3's orientation being the gauge"""
    return max(math.hypot(h[0], h[1]), math.hypot(h[3], h[4]) + 2 * R5 * math.sin(h[2] / 2))


def placed_support(n, phi, t, th):
    return RS[n](th - phi) + t[0] * np.cos(th) + t[1] * np.sin(th)


def hull_support(q, th, x=None):
    h = np.maximum(R0, placed_support(3, 0.0, q[:2], th))
    h = np.maximum(h, placed_support(5, q[2], q[3:5], th))
    if x is not None:
        h = np.maximum(h, placed_support(7, x[0], x[1:3], th))
    return h


def base_pieces(q):
    return placed_disc() + placed_reuleaux(3, 0.0, q[:2]) + placed_reuleaux(5, q[2], q[3:5])


def core_pieces(V, rho):
    """exact support pieces of the core, the intersection of the discs of radius rho about
    the corners V of a regular Reuleaux polygon (R_n < rho <= 1): about each corner an arc
    of radius rho, carrying the normals up to where it meets the arcs about the adjacent
    corners, and those meeting points as vertex pieces"""
    n, O = len(V), V.mean(axis=0)
    corners = []
    for k in range(n):
        a, b = V[k], V[(k + 1) % n]
        M, s = (a + b) / 2, float(np.linalg.norm(b - a))
        inward = (O - M) / np.linalg.norm(O - M)
        corners.append(M + math.sqrt(rho * rho - s * s / 4) * inward)
    pieces = [(c, 0.0, None) for c in corners]
    for k in range(n):
        mid = math.atan2(O[1] - V[k][1], O[0] - V[k][0])
        e = corners[k] - V[k]
        pieces.append((V[k], rho, (mid, abs(wrap(math.atan2(e[1], e[0]) - mid)))))
    return pieces, corners


def base_core_pieces(q, h, core_radius):
    d3 = math.hypot(h[0], h[1])
    d5 = math.hypot(h[3], h[4]) + 2 * R5 * math.sin(h[2] / 2)
    return (placed_disc() + core_pieces(placed_vertices(3, 0.0, q[:2]), core_radius(d3))[0]
            + core_pieces(placed_vertices(5, q[2], q[3:5]), core_radius(d5))[0])


def piece_arrays(pieces):
    C = np.array([p[0] for p in pieces], dtype=float)
    rho = np.array([p[1] for p in pieces], dtype=float)
    ranged = [(k, p[2]) for k, p in enumerate(pieces) if p[2] is not None]
    return C, rho, ranged


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


def pieces_support(pieces, t):
    C, rho, ranged = piece_arrays(pieces)
    return np.max(support_matrix(C, rho, ranged, np.atleast_1d(np.asarray(t, dtype=float))), axis=0)


def interval_min(d, D, s, e):
    """sec. 20: the least of d.u(theta) + D on [s, e] - at an end, or where u points against d"""
    cands = [s, e]
    if np.hypot(*d) > 0:
        c = math.atan2(-d[1], -d[0])
        c += 2 * math.pi * math.ceil((s - c) / (2 * math.pi))
        if c <= e:
            cands.append(c)
    vals = [d[0] * math.cos(t) + d[1] * math.sin(t) + D for t in cands]
    k = int(np.argmin(vals))
    return vals[k], cands[k]


def containment_min(pa, pb, imin, n=2048):
    """min over directions of h_a - h_b from the merged breakpoints of both envelopes: on
    each interval both owners are fixed, so the difference is one sinusoid plus a constant
    (each envelope's segments checked in closed form: RUN-031)"""
    arrays = [piece_arrays(p) for p in (pa, pb)]
    cuts = []
    for C, rho, ranged in arrays:
        own = lambda t, C=C, rho=rho, ranged=ranged: np.argmax(support_matrix(C, rho, ranged, t), axis=0)
        c, o = envelope(own, n, len(C))
        rng = dict(ranged)
        segs = verify_segments(C, rho, [rng.get(k) for k in range(len(C))], segments(c, o))
        cuts += [a % (2 * math.pi) for a, _, _ in segs]
    cuts = sorted(set(cuts)) or [0.0]
    ends = cuts[1:] + [cuts[0] + 2 * math.pi]
    best, where = math.inf, None
    for s, e in zip(cuts, ends):
        if e - s <= 0:
            continue
        m = np.array([(s + e) / 2])
        (Ca, ra, ga), (Cb, rb, gb) = arrays
        i = int(np.argmax(support_matrix(Ca, ra, ga, m), axis=0)[0])
        j = int(np.argmax(support_matrix(Cb, rb, gb, m), axis=0)[0])
        v, t = imin(Ca[i] - Cb[j], ra[i] - rb[j], s, e)
        if v < best:
            best, where = v, t
    return best, where


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

def x1_repository(w):
    out, facts = [], w["snapshot"]["facts"]
    for path, names in REPO_FACTS.items():
        for name in names:
            if not facts.get(path, {}).get(name):
                out.append(f"{path}: {name} not found at the pinned commit")
    split = facts.get("src/verifyB.py", {}).get("split_weights") or ""
    if w["angle_weight"] not in split:
        out.append(f"the angle axis is not weighted by {w['angle_weight']} in Mishra's split rule")
    form = facts.get("src/geom.py", {}).get("sinusoid") or ""
    if w["piece_form"] not in form:
        out.append(f"Mishra's pieces are not {w['piece_form']}")
    return out


def small_cell(rng, c0, h0, frac):
    """a cell of half-widths up to frac of the root's, centred anywhere in the root"""
    return c0 + rng.uniform(-0.9, 0.9, 5) * h0, h0 * frac * rng.uniform(0.3, 1.0, 5)


def random_cell(rng, c0, h0):
    h = h0 * 2.0 ** -float(rng.integers(0, 9)) * rng.uniform(0.3, 1.0, 5)
    return c0 + rng.uniform(-1, 1, 5) * (h0 - h), h


def b7_root():
    t7 = t_text(7, d_star(T1))
    return np.array([math.pi / 7, 0.0, 0.0]), np.array([math.pi / 7, t7, t7])


def w1_radius(w):
    """d_H of two convex bodies is the sup of their support difference: sampled in 4096
    directions, which can only understate it"""
    out, rng, worst = [], np.random.default_rng(91), 0.0
    th = 2 * np.pi * np.arange(4096) / 4096
    c0, h0 = root_box()
    g0c, g0 = b7_root()
    for k in range(80):
        qc, h = random_cell(rng, c0, h0)
        joint = k % 2 == 1
        if joint:
            g = g0 * 2.0 ** -float(rng.integers(0, 9)) * rng.uniform(0.3, 1.0, 3)
            xc = g0c + rng.uniform(-1, 1, 3) * (g0 - g)
            radius = max(w["tau"](h), motion_delta(g[1], g[2], g[0], R7))
        else:
            xc, radius = None, w["tau"](h)
        hc = hull_support(qc, th, xc)
        for _ in range(6):
            q = qc + rng.uniform(-1, 1, 5) * h
            x = xc + rng.uniform(-1, 1, 3) * g if joint else None
            d = float(np.max(np.abs(hull_support(q, th, x) - hc)))
            worst = max(worst, d / radius)
            if d > radius + 1e-12:
                out.append(f"{'joint' if joint else 'base'} cell {k}: d_H {d:.6e} > radius {radius:.6e}")
                break
        if len(out) >= 3:
            break
    w["w1"] = {"largest_dH_over_radius": worst}
    return out


def w2_transfer(w):
    out, rng = [], np.random.default_rng(93)
    f, ratios, slack = w["per_factor"], [], math.inf
    c0, h0 = root_box()
    g0c, g0 = b7_root()
    for k in range(40):
        q = c0 + rng.uniform(-1, 1, 5) * h0
        pieces = base_pieces(q)
        if k % 2:
            x = g0c + rng.uniform(-1, 1, 3) * g0
            pieces = pieces + placed_reuleaux(7, x[0], x[1:3])
        area, per = hull_pieces(pieces, 2048)
        ratios.append(4 * area / per)
        if per > f * area * (1 + 1e-12):
            out.append(f"hull {k}: Per {per:.9f} > {f} x Area {area:.9f}")
    for k in range(30):
        qc, h = random_cell(rng, c0, h0)
        tau = tau_f3(h)
        ac = hull_pieces(base_pieces(qc), 2048)[0]
        for _ in range(4):
            q = qc + rng.uniform(-1, 1, 5) * h
            a = hull_pieces(base_pieces(q), 2048)[0]
            bound = (ac - math.pi * tau * tau) / (1 + f * tau)      # Steiner, and Per(A) <= f Area(A)
            slack = min(slack, (a - bound) / tau)
            if a < bound - 1e-12:
                out.append(f"cell {k}: Area {a:.9f} below the transfer bound {bound:.9f}")
    w["w2"] = {"least_4area_over_per": min(ratios), "least_transfer_slack_over_tau": slack}
    return out


def tau_star(m, T, r=R0):
    """sec. 8's root, written without the cancellation of sqrt(...) - T/r"""
    return m / (math.sqrt(T * T / (r * r) + math.pi * m) + T / r)


def tau_star_old(m, T):
    """Round 07's cost 4 pi T tau + pi tau^2 = m, likewise"""
    return (m / math.pi) / (math.sqrt(4 * T * T + m / math.pi) + 2 * T)


def w3_resolution(w):
    out = []
    tau, T, r, m = sp.symbols("tau T r m", positive=True)
    F = (sp.sqrt(T ** 2 / r ** 2 + sp.pi * m) - T / r) / sp.pi
    if sp.simplify(2 * T / r * F + sp.pi * F ** 2 - m) != 0:
        out.append("tau_star does not solve (2T/r) tau + pi tau^2 = m")
    if sp.simplify(F.subs(r, sp.Rational(1, 2)) - (sp.sqrt(4 * T ** 2 + sp.pi * m) - 2 * T) / sp.pi) != 0:
        out.append("tau_star at r = 1/2 is not the text's closed form")
    new, old = tau_star(M_SEARCH, T1), tau_star_old(M_SEARCH, T1)
    c = w["resolution"]
    if abs(new - c["tau_star"]) > 5e-11 or abs(new - c["tau_star_short"]) > 5e-10:
        out.append(f"tau_star {new!r}, claimed {c['tau_star']} / {c['tau_star_short']}")
    if abs(old - c["tau_star_old"]) > 5e-11 or abs(old - c["tau_star_old_short"]) > 5e-10:
        out.append(f"Round 07's tau {old!r}, claimed {c['tau_star_old']} / {c['tau_star_old_short']}")
    if abs(new / old - c["ratio"]) > 5e-3:
        out.append(f"ratio {new / old:.6f}, claimed {c['ratio']}")
    w["w3"] = {"tau_star": new, "tau_star_old": old, "ratio": new / old}
    return out


def split_taus(h):
    out = {}
    for i, a in enumerate(AXES):
        c = list(h)
        c[i] /= 2
        out[a] = tau_f3(c)
    return out


def greedy(h, rule, steps=16):
    seq, h = [], list(h)
    for _ in range(steps):
        if rule == "radius":
            taus = split_taus(h)
            a = min(AXES, key=lambda k: (taus[k], AXES.index(k)))
        else:                                   # Mishra: halve the widest, the angle weighted by R_5
            wts = [h[0], h[1], R5 * h[2], h[3], h[4]]
            a = AXES[int(np.argmax(wts))]
        h[AXES.index(a)] /= 2
        seq.append((a, tau_f3(h)))
    return seq


def w4_scheduler(w):
    out, c = [], w["scheduler"]
    _, h0 = root_box()
    for key, val in (("t3", h0[0]), ("t5", h0[3]), ("R5", R5)):
        if abs(val - c[key]) > 5e-13:
            out.append(f"{key} = {val!r}, claimed {c[key]}")
    d3 = math.hypot(h0[0], h0[1])
    got = {"root": tau_f3(h0), "d3": d3, **split_taus(h0)}
    for key, val in got.items():
        if abs(val - c["taus"][key]) > 5e-11:
            out.append(f"tau {key} = {val!r}, claimed {c['taus'][key]}")
    first = min(AXES, key=lambda k: (got[k], AXES.index(k)))
    if first != c["first_cut"]:
        out.append(f"the first cut is {first}, claimed {c['first_cut']}")
    R, hh = sp.symbols("R h", positive=True)
    if sp.simplify(sp.series(2 * R * sp.sin(hh / 2), hh, 0, 5).removeO() - (R * hh - R * hh ** 3 / 24)) != 0:
        out.append("2R sin(h/2) is not R h - R h^3/24 + O(h^5)")
    radius, mishra = greedy(h0, "radius"), greedy(h0, "mishra")
    split_at = next((i for i, (a, b) in enumerate(zip(radius, mishra)) if a[0] != b[0]), None)
    w["w4"] = {"taus": got, "first_cut": first, "radius_rule": radius, "mishra_rule": mishra,
               "rules_first_differ_at_step": split_at}
    return out


def leaf_centres(w):
    r7 = w["run010"]
    four = r7["w4"]["placement"]
    return {"seed + best B7": (w["round07"]["repository"]["reuleaux"]["placement"], r7["w3"]["rows"]["7"]["placement"]),
            "four-body optimum": (four[:5], four[5:8])}


def leaf_radii(h):
    return (motion_delta(h, h, 0.0, R3), motion_delta(h, h, h, R5), motion_delta(h, h, h, R7))


def leaf_cores(q, x, h):
    d3, d5, d7 = leaf_radii(h)
    return ((placed_vertices(3, 0.0, q[:2]), 1 - d3), (placed_vertices(5, q[2], q[3:5]), 1 - d5),
            (placed_vertices(7, x[0], x[1:3]), 1 - d7))


def core_bound(q, x, h):
    pieces = placed_disc()
    for V, rho in leaf_cores(q, x, h):
        pieces = pieces + core_pieces(V, rho)[0]
    return hull_pieces(pieces, 2048)[0]


def points_and_corners(q, x, h):
    """RUN-011's inner points with the cores' corners added"""
    pts = [disc_samples(20000)]
    for V, rho in leaf_cores(q, x, h):
        pts += [reuleaux_core_points(V, rho), np.array(core_pieces(V, rho)[1])]
    return float(ConvexHull(np.vstack(pts)).volume)


def widest_closing(bound, lo=1e-6, hi=3e-3):
    """the largest half-width at which bound(h) >= T1, by bisection in log h"""
    if bound(lo) < T1 or bound(hi) >= T1:
        return None
    for _ in range(40):
        mid = math.sqrt(lo * hi)
        lo, hi = (mid, hi) if bound(mid) >= T1 else (lo, mid)
    return lo


_W5 = {}


def w5_prunes(w):
    out, rows, widest = [], {}, {}
    run011 = w["run011"]["w4"]["rows"]
    for name, (q, x) in leaf_centres(w).items():
        q, x = np.asarray(q, dtype=float), np.asarray(x, dtype=float)
        ac = hull_pieces(base_pieces(q) + placed_reuleaux(7, x[0], x[1:3]), 2048)[0]
        rep = lambda h: ac - w["rep_cost"](T1, max(leaf_radii(h)))
        if name not in _W5:
            _W5[name] = {"core": {h: core_bound(q, x, h) for h in (1e-4, 1e-3)},
                         "with_corners": {h: points_and_corners(q, x, h) for h in (1e-4, 1e-3)},
                         "core_widest": widest_closing(lambda h: core_bound(q, x, h))}
        for h in (1e-4, 1e-3):
            r11 = run011[f"{name} @ {h:g}"]
            core = _W5[name]["core"][h]
            corners = _W5[name]["with_corners"][h]
            rows[f"{name} @ {h:g}"] = {"center_area": ac, "rep": rep(h), "core_exact": core,
                                        "core_inner_run011": r11["inner_lower"],
                                        "exact_minus_run011_inner": core - r11["inner_lower"],
                                        "exact_minus_points_and_corners": core - corners}
            if core < corners - 1e-12 or core - corners > 1e-6:
                out.append(f"{name} @ {h:g}: exact core {core:.10f} vs points and corners {corners:.10f}")
            if max(rep(h), core) > r11["least_sampled_actual"] + 1e-12:
                out.append(f"{name} @ {h:g}: a prune bound exceeds a sampled actual hull")
            if core < r11["inner_lower"] - 1e-12:     # the inner points lie in the cores
                out.append(f"{name} @ {h:g}: exact core {core:.10f} below RUN-011's inner points {r11['inner_lower']:.10f}")
        widest[name] = {"rep": widest_closing(rep), "core": _W5[name]["core_widest"]}
    closes = {k: v["rep"] >= T1 for k, v in rows.items()}
    if closes != w["rep_closures"]:
        out.append(f"representative closures {closes} differ from the recorded {w['rep_closures']}")
    for name, v in widest.items():
        if v["rep"] is None or v["core"] is None:
            out.append(f"{name}: no closing width found")
        elif (v["core"] > v["rep"]) != w["core_closes_wider"]:
            out.append(f"{name}: widest closing cell core {v['core']:.3e}, representative {v['rep']:.3e}")
    w["w5"] = {"rows": rows, "rep_closes": closes, "widest_closing_half_width": widest}
    return out


def w6_dominance(w):
    out, rng = [], np.random.default_rng(95)
    # the pieces at rho = 1 are the Reuleaux polygon's own
    for n in (3, 5, 7):
        V = placed_vertices(n, 0.3, (0.05, -0.02))
        pieces, corners = core_pieces(V, 1.0)
        opp = [V[(k + (n + 1) // 2) % n] for k in range(n)]
        if max(np.linalg.norm(a - b) for a, b in zip(corners, opp)) > 1e-12 \
                or max(abs(p[2][1] - math.pi / (2 * n)) for p in pieces if p[2]) > 1e-12:
            out.append(f"B{n}: the core pieces at rho = 1 are not the polygon's")
    c0, h0 = root_box()
    worst_gap, worst_without = 0.0, 0.0
    for _ in range(6):          # exact core hull against the hull of points in the cores
        qc, h = small_cell(rng, c0, h0, 1 / 64)
        exact = hull_pieces(base_core_pieces(qc, h, w["core_radius"]), 2048)[0]
        d3, d5 = math.hypot(h[0], h[1]), math.hypot(h[3], h[4]) + 2 * R5 * math.sin(h[2] / 2)
        pts, corners = [disc_samples(20000)], []
        for V, rho in ((placed_vertices(3, 0.0, qc[:2]), 1 - d3), (placed_vertices(5, qc[2], qc[3:5]), 1 - d5)):
            pts.append(reuleaux_core_points(V, rho))
            corners += core_pieces(V, rho)[1]
            if max(np.linalg.norm(c - v) for c in core_pieces(V, rho)[1] for v in V) > rho + 1e-12:
                out.append("a core corner lies outside the core")
        without = float(ConvexHull(np.vstack(pts)).volume)
        inner = float(ConvexHull(np.vstack(pts + [np.array(corners)])).volume)
        worst_gap, worst_without = max(worst_gap, exact - inner), max(worst_without, exact - without)
        if exact < inner - 1e-12 or exact - inner > 1e-6:
            out.append(f"exact core hull {exact:.10f} vs points and corners {inner:.10f}")
    th = 2 * np.pi * np.arange(8192) / 8192
    counts = {"nested": [0, 0], "shifted": [0, 0], "parent-in-child": [0, 0]}
    theorem_pairs, least_margin = 0, math.inf
    for k in range(36):
        qa, ha = small_cell(rng, c0, h0, 1 / 16)
        kind = ("nested", "shifted", "parent-in-child")[k % 3]
        if kind == "nested":
            qb, hb = qa, ha * rng.uniform(1.2, 3.0)
            ga, gb = base_core_pieces(qa, ha, w["core_radius"]), base_core_pieces(qb, hb, w["core_radius"])
        elif kind == "shifted":
            qb, hb = qa + rng.uniform(-1, 1, 5) * ha * 0.3, ha * rng.uniform(1.0, 3.0)
            ga, gb = base_core_pieces(qa, ha, w["core_radius"]), base_core_pieces(qb, hb, w["core_radius"])
        else:                                   # a = a child, b = its parent
            i = int(rng.integers(0, 5))
            hb, qb = ha, qa
            ha = ha.copy()
            ha[i] /= 2
            qa = qa.copy()
            qa[i] += ha[i] * (1 if rng.uniform() < 0.5 else -1)
            ga, gb = base_core_pieces(qa, ha, w["core_radius"]), base_core_pieces(qb, hb, w["core_radius"])
        exact, where = containment_min(ga, gb, w["interval_min"])
        sampled = float(np.min(pieces_support(ga, th) - pieces_support(gb, th)))
        attained = float(pieces_support(ga, where)[0] - pieces_support(gb, where)[0])
        if sampled < exact - 1e-12 or abs(attained - exact) > 1e-12:
            out.append(f"{kind} pair {k}: merged-breakpoint min {exact:.3e}, sampled {sampled:.3e}, "
                       f"attained {attained:.3e}")
            continue
        inside = exact >= -1e-12                # both hulls touch the disc, so the least gap is often 0
        counts[kind][0] += 1
        counts[kind][1] += inside
        if kind == "nested" and not inside:
            out.append(f"nested pair {k}: the coarser core is not inside the finer one ({exact:.3e})")
        if inside:                              # G_b inside G_a: Thm 19.1 with a B7 core
            for _ in range(2):
                x = np.array([rng.uniform(0, 2 * math.pi / 7), *rng.uniform(-0.19, 0.19, 2)])
                wc = core_pieces(placed_vertices(7, x[0], x[1:3]), 1 - rng.uniform(1e-4, 5e-3))[0]
                aa, ab = hull_pieces(ga + wc, 2048)[0], hull_pieces(gb + wc, 2048)[0]
                theorem_pairs += 1
                least_margin = min(least_margin, aa - ab)
                if aa < ab - 1e-12:
                    out.append(f"pair {k}: Thm 19.1 fails, {aa:.10f} < {ab:.10f}")
    w["w6"] = {"exact_minus_points_and_corners_worst": worst_gap, "exact_minus_points_alone_worst": worst_without,
               "pairs_checked_and_containing": {k: {"checked": v[0], "containing": int(v[1])} for k, v in counts.items()},
               "theorem_19_1_trials": theorem_pairs, "least_area_gain": least_margin}
    return out


def witness_pieces(name, phi, t):
    n = int(name[1:])
    if name[0] == "B":
        return placed_reuleaux(n, phi, t)
    return placed_polygon(reuleaux_vertices(n), phi, t)


def w7_witnesses(w):
    out, rng, gaps = [], np.random.default_rng(97), []
    c0, h0 = root_box()
    for big, small in w["dominance_pairs"]:
        for _ in range(24):
            q = c0 + rng.uniform(-1, 1, 5) * h0
            phi, t = rng.uniform(0, 2 * math.pi), rng.uniform(-0.2, 0.2, 2)
            H = base_pieces(q)
            a_big = hull_pieces(H + witness_pieces(big, phi, t), 2048)[0]
            a_small = hull_pieces(H + witness_pieces(small, phi, t), 2048)[0]
            gaps.append(a_big - a_small)
            if a_big < a_small - 1e-12:
                out.append(f"{big} over {small}: {a_big:.10f} < {a_small:.10f}")
                break
    th = 2 * np.pi * np.arange(4096) / 4096
    width = {n: float(np.max(np.abs(RS[n](th) + RS[n](th + np.pi) - 1))) for n in (7, 9, 11, 13)}
    for n, dev in width.items():
        if dev > 1e-12:
            out.append(f"B{n}: width deviates from 1 by {dev:.2e}")
    w["w7"] = {"least_area_gain": min(gaps), "largest_area_gain": max(gaps), "constant_width_deviation": width}
    return out


def w8_depth(w):
    out, rng = [], np.random.default_rng(99)
    c0, h0 = root_box()
    cells = [h0] + [random_cell(rng, c0, h0)[1] for _ in range(40)]
    for h in cells:
        S0 = w["S0"](h)
        for r in range(25):
            if tau_f3(h / 2 ** r) > S0 / 2 ** r + 1e-15:
                out.append(f"tau after {r} cycles {tau_f3(h / 2 ** r):.6e} > 2^-r S0 = {S0 / 2 ** r:.6e}")
                break
        if len(out) >= 3:
            break
    S0 = w["S0"](h0)
    ts = tau_star(M_SEARCH, T1)
    r = math.ceil(math.log2(S0 / ts))
    if tau_f3(h0 / 2 ** r) > ts:
        out.append(f"after {r} cycles the root's tau {tau_f3(h0 / 2 ** r):.3e} still exceeds tau_star {ts:.3e}")
    exact_r = next(k for k in range(64) if tau_f3(h0 / 2 ** k) <= ts)
    w["w8"] = {"S0_root": S0, "tau_star": ts, "cycles_bound": r, "cycles_actually_needed": exact_r,
               "splits_on_one_path": 5 * r}
    return out


SEC17 = ["APR", "REP", "CORE", "SUPPORT-CORE", "OTHER-VERIFIED"]


def p1_package(w):
    out, v, spec = [], w["validation"]["sanity"], w["spec"]
    _, h0 = root_box()
    d3, d5 = math.hypot(h0[0], h0[1]), math.hypot(h0[3], h0[4]) + 2 * R5 * math.sin(h0[2] / 2)
    rec = {("root", "delta3"): d3, ("root", "delta5"): d5, ("root", "tau"): max(d3, d5),
           **{("child_tau", a): t for a, t in split_taus(h0).items()},
           ("best_child_tau",): min(split_taus(h0).values()),
           ("tau_star_new",): tau_star(v["search_only_margin_for_scale_demo"], T1),
           ("tau_star_old",): tau_star_old(v["search_only_margin_for_scale_demo"], T1),
           ("omega_new_at_1e-4",): 4 * T1 * 1e-4 + math.pi * 1e-8,
           ("omega_old_at_1e-4",): 4 * math.pi * T1 * 1e-4 + math.pi * 1e-8}
    rec[("resolution_relaxation_ratio",)] = rec[("tau_star_new",)] / rec[("tau_star_old",)]
    worst = 0.0
    for path, val in rec.items():             # relative: the package's tau_star values carry the
        got = v                               # cancellation of sqrt(...) - 2T, about 4e-13
        for p in path:
            got = got[p]
        worst = max(worst, abs(got - val) / abs(val))
        if abs(got - val) > 1e-12 * abs(val):
            out.append(f"VALIDATION {'.'.join(path)} = {got!r}, rebuilt {val!r}")
    if v["search_only_margin_for_scale_demo"] != M_SEARCH or v["best_axis"] != "phi5":
        out.append("the recorded margin or best axis differs from the text")
    if spec["target"] != T1:
        out.append("the compute spec's target is not 0.835")
    missing = sorted(set(SEC17) - set(spec["proof_modes"]))
    if missing != sorted(w["spec_modes_missing"]):
        out.append(f"the spec leaves out proof modes {missing}, recorded {w['spec_modes_missing']}")
    unmetered = sorted(m for m in spec["proof_modes"] if f"{m}_leaves" not in spec["metrics"])
    if unmetered != sorted(w["spec_modes_unmetered"]):
        out.append(f"proof modes without a leaf count {unmetered}, recorded {w['spec_modes_unmetered']}")
    w["p1"] = {"largest_relative_difference": worst, "spec_modes_missing": missing, "spec_modes_unmetered": unmetered}
    return out


def p2_package(w):
    out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]}
    v = w["validation"]
    for rec, leaf_id, text in ((v["round09"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"])):
        _, size, digest = leaves[leaf_id]
        if rec["sha256"] != digest or rec["bytes"] != size:
            out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive")
        n = text.count("$$")
        if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0):
            out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}")
        if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)):
            out.append(f"{rec['file']}: unicode-escape flag differs")
        if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)):
            out.append(f"{rec['file']}: bracket-delimiter flag differs")
    if v["compute_spec_sha256"] != leaves[SPEC][2]:
        out.append("compute_spec_sha256: recorded digest differs from the archive")
    return out


# ---------------------------------------------------------------- registry (Round 09)

TOKEN = "a proof-mode tag of sec. 17, defined there; not a judgment"
R09_DEFINITIONS = {
    "REP": ("in-line", "sec. 17 proof-mode tag: a leaf closed by the representative-area transfer (C09-2)"),
    "STILL COMPUTE-DEFERRED": ("in-line", "conclusion J: the heavy 0.835 certificate still waits on the computation "
                                          "specified"),
    "PROVED FOR THE CERTIFIED RADIUS BOUND": ("contextual", "sec. 32: the split is one-step optimal for the bound "
                                                            "tau, not for any cost of the certificate"),
    "R07-STRENGTHENING-001": ("in-line", "結論 B: Round 07's transfer made tighter; a strengthening, not a correction"),
}
R09_REVIEWS = [
    ("PROVED", "Family-cell Hausdorff radius", "analytic", "PASS", "Thm 1.1 and sec. 2-4; W1"),
    ("PROVED", "Sharpened area transfer", "analytic", "PASS",
     "Thm 6.1: Steiner, and Area >= (r/2) Per for a body holding B_r; W2. RUN-008 and RUN-010 recorded the old "
     "bounds as loose by pi for this reason"),
    ("PROVED", "Margin-to-resolution formula", "analytic", "PASS", "W3"),
    ("PROVED", "Representative-area prune", "analytic", "PASS", "Thm 6.1 on the joint box; W5"),
    ("PROVED", "Common-core dominance reuse", "analytic", "PASS",
     "Thm 19.1; sec. 20's closed-form containment rebuilt and checked against sampling (W6)"),
    ("PROVED", "Single-lift witness dominance", "analytic", "PASS",
     "Thm 22.1; W7. Every witness Round 08 names has constant width 1, and such a body lies in no other set of "
     "diameter 1, so among them dominance only matches congruent copies"),
    ("PROVED", "Margin-to-depth finite bound", "analytic", "PASS",
     "sec. 25, reading m as a lower bound on every representative's margin in the region, as sec. 26 does; W8"),
    ("CLOSED", "ADAPTIVE CERTIFICATE-COST LAYER", "reading", "PASS",
     "sound by construction: every rule prunes only by a proved bound; its gain is deferred (C09-5)"),
    ("CLOSED", "SOUNDNESS-PRESERVING REUSE RULES", "analytic", "PASS", "Thm 19.1 and 22.1"),
    ("COMPUTE-DEFERRED", "Scheduler performance gain", "n/a", "n/a", ""),
    ("STILL COMPUTE-DEFERRED", "HEAVY 0.8350 CERTIFICATE", "n/a", "n/a",
     "the boxed conclusion J; read from census v3 on (RUN-003)"),
    ("NOT YET CERTIFIED", "$0.8350$ theorem", "n/a", "n/a", ""),
    ("REP", "C09-2 — Add representative prune mode", "n/a", "n/a", TOKEN),
    ("PROVED FOR THE CERTIFIED RADIUS BOUND", "Exact one-step split scheduler", "analytic", "PASS",
     "W4; the scheduler minimises tau, which the representative prune uses; the core prune depends on each "
     "body's radius separately"),
    ("R07-STRENGTHENING-001", "結論 B：Round 07 的 area-transfer error 可收緊", "n/a", "n/a",
     "the label of 結論 B, reviewed under Sharpened area transfer"),
]


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


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

CHECKS = {"A0": gate.anchors_check(ANCHORS), "X1": x1_repository, "W1": w1_radius, "W2": w2_transfer,
          "W3": w3_resolution, "W4": w4_scheduler, "W5": w5_prunes, "W6": w6_dominance, "W7": w7_witnesses,
          "W8": w8_depth, "P1": p1_package, "P2": p2_package, "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "X1": {"snapshot", "angle_weight", "piece_form"}, "W1": {"tau"}, "W2": {"per_factor"},
           "W3": {"resolution"}, "W4": {"scheduler"},
           "W5": {"run010", "run011", "round07", "rep_cost", "rep_closures", "core_closes_wider"},
           "W6": {"core_radius", "interval_min"}, "W7": {"dominance_pairs"}, "W8": {"S0"},
           "P1": {"validation", "spec", "spec_modes_missing", "spec_modes_unmetered"},
           "P2": {"validation", "text", "crystal", "manifest"}, "R1": {"registry", "definitions", "reviews"}}

CLAIMS = {
    "angle_weight": "CIRC5*b[5]", "piece_form": "cx cos t + cy sin t + r",
    "tau": tau_f3, "per_factor": 4.0,
    "resolution": {"tau_star": 0.0004473869, "tau_star_short": 4.47387e-4, "tau_star_old": 0.0001424615,
                   "tau_star_old_short": 1.42462e-4, "ratio": 3.14},
    "scheduler": {"t3": 0.194856180909, "t5": 0.197820670401, "R5": 0.525731112119, "first_cut": "phi5",
                  "taus": {"root": 0.6046803712, "d3": 0.2755682538, "x3": 0.6046803712, "y3": 0.6046803712,
                           "phi5": 0.4442456056, "x5": 0.5460899294, "y5": 0.5460899294}},
    "rep_cost": lambda T, s: 4 * T * s + math.pi * s * s,
    "rep_closures": {"seed + best B7 @ 0.0001": True, "seed + best B7 @ 0.001": False,
                     "four-body optimum @ 0.0001": True, "four-body optimum @ 0.001": False},
    "core_closes_wider": True,
    "core_radius": lambda delta: 1 - delta, "interval_min": interval_min,
    "dominance_pairs": [("B3", "P3"), ("B5", "P5")],
    "S0": lambda h: max(math.hypot(h[0], h[1]), math.hypot(h[3], h[4]) + R5 * h[2]),
    "spec_modes_missing": ["OTHER-VERIFIED"], "spec_modes_unmetered": ["SUPPORT-CORE"],
}


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


def fetch_repository_facts():
    facts = {}
    for path, pats in REPO_FACTS.items():
        src = gate.fetch_github_file(REPO, COMMIT, path)
        found = {name: re.search(p, src) for name, p in pats.items()}
        facts[path] = {name: (re.sub(r"\s+", " ", m.group(0)) if m else None) for name, m in found.items()}
    return {"retrieved": datetime.date.today().isoformat(), "repo": REPO, "commit": COMMIT, "facts": facts}


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--refresh", action="store_true")
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    if args.refresh or not SNAPSHOT.exists():
        SNAPSHOT.write_text(json.dumps(fetch_repository_facts(), ensure_ascii=False, indent=1) + "\n", encoding="utf-8")
    snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8"))
    round07 = json.loads(ROUND07.read_text(encoding="utf-8"))
    run010 = json.loads(RUN010.read_text(encoding="utf-8"))
    run011 = json.loads(RUN011.read_text(encoding="utf-8"))
    text, crystal, validation, spec, manifest = load_inputs()

    def build():
        return {"text": text, "crystal": crystal, "validation": json.loads(json.dumps(validation)),
                "spec": json.loads(json.dumps(spec)), "manifest": manifest, "snapshot": json.loads(json.dumps(snapshot)),
                "round07": round07, "run010": run010, "run011": run011,
                "registry": registry.load(), "definitions": dict(R09_DEFINITIONS), "reviews": list(R09_REVIEWS),
                **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", "w6", "w7", "w8", "p1"):
        print(key, w.get(key))
    if not args.drill:
        return
    sched, res, val = CLAIMS["scheduler"], CLAIMS["resolution"], validation["sanity"]
    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-radius-by-double-angle", "control",
         {"tau": lambda h: max(math.hypot(h[0], h[1]),
                               math.hypot(h[3], h[4]) + 4 * R5 * math.sin(h[2] / 4) * math.cos(h[2] / 4))}, set()),
        ("K2-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()),
        ("K3-rep-cost-factored", "control", {"rep_cost": lambda T, s: s * (4 * T + math.pi * s)}, set()),
        ("M1-doc-root-radius-digit", "mutation", {"text": text.replace("0.6046803712", "0.6046803713")}, {"A0"}),
        ("M2-split-weight-misread", "mutation", {"angle_weight": "R5**2*b[5]"}, {"X1"}),
        ("M3-radius-without-rotation", "mutation",
         {"tau": lambda h: max(math.hypot(h[0], h[1]), math.hypot(h[3], h[4]))}, {"W1"}),
        ("M4-perimeter-factor-2", "mutation", {"per_factor": 2.0}, {"W2"}),
        ("M5-tau-star-digit", "mutation", {"resolution": {**res, "tau_star": 0.0004473879}}, {"W3"}),
        ("M6-ratio-as-pi-squared", "mutation", {"resolution": {**res, "ratio": 3.14 ** 2}}, {"W3"}),
        ("M7-x5-radius-digit", "mutation",
         {"scheduler": {**sched, "taus": {**sched["taus"], "x5": 0.5460899394}}}, {"W4"}),
        ("M8-first-cut-x5", "mutation", {"scheduler": {**sched, "first_cut": "x5"}}, {"W4"}),
        ("M9-rep-cost-without-4", "mutation", {"rep_cost": lambda T, s: T * s + math.pi * s * s}, {"W5"}),
        ("M10-rep-claimed-wider", "mutation", {"core_closes_wider": False}, {"W5"}),
        ("M11-containment-ends-only", "mutation",
         {"interval_min": lambda d, D, s, e: min((d[0] * math.cos(t) + d[1] * math.sin(t) + D, t) for t in (s, e))},
         {"W6"}),
        ("M12-dominance-reversed", "mutation", {"dominance_pairs": [("P3", "B3"), ("P5", "B5")]}, {"W7"}),
        ("M13-S0-without-rotation", "mutation",
         {"S0": lambda h: max(math.hypot(h[0], h[1]), math.hypot(h[3], h[4]))}, {"W8"}),
        ("M14-validation-child-tau", "mutation", {"validation": {**validation, "sanity": {
            **val, "child_tau": {**val["child_tau"], "phi5": 0.4442456065568814}}}}, {"P1"}),
        ("M15-spec-mode-assumed", "mutation", {"spec_modes_missing": []}, {"P1"}),
        ("M16-crystal-digest", "mutation", {"validation": {**validation, "state_crystal": {
            **validation["state_crystal"], "sha256": "0" * 64}}}, {"P2"}),
        ("M17-review-dropped", "mutation", {"reviews": list(R09_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-012", "subject": "Round 09: adaptive atlas refinement and certificate-cost minimization",
           "document": DOC, "snapshot_retrieved": snapshot["retrieved"],
           "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "w6", "w7", "w8", "p1")}, "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("R09", "RUN-012", R09_DEFINITIONS, R09_REVIEWS)
        print(f"registry: {len(R09_DEFINITIONS)} definitions, {len(R09_REVIEWS)} reviews recorded for R09")


if __name__ == "__main__":
    main()