"""RUN-010 - Round 07: the minimizer atlas and threshold-conditioned witness lifting.

Round 07 takes Mishra's certified seed D, B3, B5 and turns Round 06's exchange into a
computation that need not grow with the number of witnesses: a new witness only has
to be placed over the base configurations whose hull is still below the target (the
threshold sublevel atlas), different cells may be closed by different witnesses
(witness switching), and a cell's representative transfers to the whole cell with
an explicit area penalty. It fixes the seed's domain and best placement from Mishra's
repository, ranks four regular Reuleaux witnesses by a search-only probe, and sets
the first exact gate: B7 must lift every base placement below 0.835 to at least 0.835.
The theorems are read in the report; here each number the round computes or quotes is
rebuilt - the domain from its derivation, the seed and the lifts with this tree's
exact hull, the four-body search, the cost extrapolation from the logged counts - and
the external numbers are checked against the paper and the repository's logs.

Checks
  A0 anchors      the formulas and numbers below occur in Round 07 as written
  A1 citations    its arXiv references (Gibbs 2014 new here)
  X1 paper        sec. 1, 21: Mishra's full text - leaf slack, the fourth body, throughput
  X2 repository   sec. 3-4, 20-21: the logs at the commit the paper cites
  W1 domain       sec. 3-4: f = Phi_{1/2}; d*; t_n(T) derived, at both thresholds; exclusion sound
  W2 seed         sec. 20: the exhibited placement's exact hull; its normalized angle; the headroom
  W3 lifts        sec. 22-23: J_{B_n}(H^dagger) for n = 7, 9, 11, 13, exactly; the ranking
  W4 four bodies  sec. 21, 24, 26: an 8-D search that could refute gate R07-G1's premise
  W5 cost         sec. 21: the 5.527e12 boxes and 5635.8 days refitted from the logged counts
  D1 transfer     sec. 17: omega_T = 4 pi T tau + pi tau^2 from Steiner and Per <= 4 pi T
  D2 switching    sec. 11: a two-witness hull is at least the larger single lift
  P1 package      VALIDATION.json and LOCAL_COMPUTE_SPEC.json rebuilt
  P2 package      the package's self-description of its documents matches the archive
  R1 registry     Round 07's judgments reviewed, first-used statuses defined

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

import numpy as np
import sympy as sp
from scipy.optimize import brentq, differential_evolution, minimize
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, phi_text, reuleaux_boundary, reuleaux_vertices
from run009_round06_witness_exchange import hull_pieces, placed_disc, placed_polygon, placed_reuleaux, rot, V3, V5

PKG = "main.zip!/AMRAL_LUC_FC_Round_07_Package_v0.1.zip!/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_07_Minimizer_Atlas_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_07_v0.1.md"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_07_VALIDATION.json"
SPEC = PKG + "AMRAL_LUC_FC_Round_07_LOCAL_COMPUTE_SPEC.json"
SNAPSHOT = TREE / "data" / "external" / "round07-citations.json"
LOG = TREE / "data" / "gate-logs" / "run010-round07-minimizer-atlas.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CACHE = TREE / "data" / "cache" / "run010-searches.json"          # data/cache is not committed
REPO, COMMIT = "Ujjwal238/universal-cover-problem", "da956b117a5f876fc3c530db3e00673e6cb18865"

ANCHORS = {
    "W1": [r"f(d)=\frac14\left(\pi-\arccos\frac{1}{2d}\right)+\frac12\sqrt{d^2-\frac14},",
           r"t_n(T)=-R_n\cos\frac{\pi}{n}+\sqrt{R_n^2\cos^2\frac{\pi}{n}-R_n^2+d_\star(T)^2}.",
           r"d_\star\approx0.693830648713.", r"|t_3|\le0.194856180909,", r"|t_5|\le0.197820670401."],
    "W2": [r"0.834780945912.", r"0.834781190917.", r"2.4128951\times10^{-5}.", r"2.19\times10^{-4}."],
    "W3": [r"J_{B_7}(H^\dagger)\approx0.83713.", r"J_K(H)=\min_{g\inE(2)}\operatorname{Area}"],
    "W4": [r"\Lambda(D,B_3,B_5,B_7)\le0.836494901", r"J_{B_7}(H_{\mathcalF_3}(q))\ge0.8350."],
    "W5": [r"\sim5.527\times10^{12}", r"\sim5635.8"],
    "D1": [r"\omega_T(\tau)=4\piT\tau+\pi\tau^2,", r"\operatorname{Per}(C_q)\le4\piT."],
    "D2": [r"\Lambda(\mathcalF\cup\mathcalB)\ge\min_q\max_{K\in\mathcalB}J_K(H(q))."],
}
REFS = {1: {"kind": "arxiv", "id": "2608.30538"}, 3: {"kind": "arxiv", "id": "1810.10089"},
        4: {"kind": "arxiv", "id": "1401.8217"}, 5: {"kind": "arxiv", "id": "2609.01284"}}
CITE_OPTS = {n: {} for n in REFS}
MISHRA_FACTS = {                      # short phrases only; matched in the full text of v2
    "slack": r"the smallest margin being 1\.2409 × 10 − 5",
    "fourth_body": r"Adding the Reuleaux heptagon raises the attainable value to 0\.836494901",
    "eight": r"raises the parameter count from five to eight",
    "throughput": r"Throughput was 19,648 boxes per second and 11,351 respectively",
    "commit": r"frozen at commit da956b117a",
}


def repository_facts():
    """the numbers Round 07 quotes from the repository, read from its logs at the commit
    the paper cites (the repository is MIT-licensed; only the numbers are kept)"""
    ceil = gate.fetch_github_file(REPO, COMMIT, "logs/ceilings.log")
    scal = gate.fetch_github_file(REPO, COMMIT, "logs/scaling.log")
    dom = gate.fetch_github_file(REPO, COMMIT, "logs/domain.log")
    blocks = ceil.split("-- disk + ")
    num = lambda s: [float(x) for x in re.findall(r"-?\d+\.\d+(?:e[-+]\d+)?", s)]
    out = {}
    for key, block in (("polygon", blocks[1]), ("reuleaux", blocks[2])):
        v = re.search(r"witness placement v = \[(.*?)\]", block, re.S).group(1)
        out[key] = {"placement": num(v),
                    "exact_kernel": float(re.search(r"exact-kernel area at v\s+(\d\.\d+)", block).group(1)),
                    "outer_1e6": float(re.search(r"1,000,000\s+(\d\.\d+)", block).group(1))}
    rows = re.search(r"family \(3, 5, 7\), dimension 8, optimum (\d\.\d+)(.*?)\n\n", scal, re.S)
    out["four_body_optimum"] = float(rows.group(1))
    out["eight_d_rows"] = [[float(m), float(t), int(b.replace(",", ""))] for m, t, b in
                           re.findall(r"(\d\.\d{6})\s+(\d\.\d{6})\s+([\d,]+)\s", rows.group(2))]
    out["eight_d_exponent"] = float(re.search(r"family \(3, 5, 7\) \(d=8\):\s+global fit\s+N ~ m\^(-?\d\.\d+)", scal).group(1))
    out["eight_d_throughput"] = int(re.findall(r"median throughput ([\d,]+) box/s", scal)[1].replace(",", ""))
    ex = re.search(r"8-D target 0\.835: margin (\d\.\d+) -> ~([\d.e+]+) boxes ~ ([\d,.]+) days", scal)
    out["extrapolation_0835"] = {"margin": float(ex.group(1)), "boxes": float(ex.group(2)),
                                 "days": float(ex.group(3).replace(",", ""))}
    out["d_star_08344"] = float(re.search(r"d\* with f\(d\*\) = target\s+:\s+(\d\.\d+)", dom).group(1))
    out["t_bounds_08344"] = [float(x) for x in re.findall(r"->  \|t\| <= (\d\.\d+)", dom)]
    return out


# ---------------------------------------------------------------- the round's formulas, as written

def f_text(d):
    """sec. 3 (domain.py): the area of conv(D, a point at distance d)"""
    sqrt, acos, pi = (sp.sqrt, sp.acos, sp.pi) if isinstance(d, sp.Basic) else (math.sqrt, math.acos, math.pi)
    return (pi - acos(1 / (2 * d))) / 4 + sqrt(d * d - sp.Rational(1, 4) if isinstance(d, sp.Basic) else d * d - 0.25) / 2


def t_text(n, dstar):
    """sec. 3: the translation radius at which B_n's nearest corner leaves B_{d*}"""
    Rn = 1 / (2 * math.sin(math.pi * (n - 1) / (2 * n)))
    c = math.cos(math.pi / n)
    return -Rn * c + math.sqrt(Rn * Rn * c * c - Rn * Rn + dstar * dstar)


def d_star(T, f=f_text):
    return brentq(lambda d: f(d) - T, 0.5 + 1e-12, 2.0, xtol=1e-15)


def omega_text(T, tau):
    pi = sp.pi if isinstance(T, sp.Basic) else math.pi
    return 4 * pi * T * tau + pi * tau ** 2


# ---------------------------------------------------------------- the searches (cached)

_S = {}


def _code_key():
    """the searches depend on their own code, the base placement, and the hull routines of
    run008/run009 - not on the checks, so editing a check does not force a recomputation"""
    import inspect
    import run008_round05_saturation_gate as r8
    import run009_round06_witness_exchange as r9
    digest = hashlib.sha256()
    for src in (inspect.getsource(searches), inspect.getsource(base_pieces)):
        digest.update(src.encode("utf-8"))
    for path in (r8.__file__, r9.__file__):
        digest.update(open(path, "rb").read())
    return digest.hexdigest()


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


def searches(qdag):
    """J_{B_n}(H^dagger) for n = 7, 9, 11, 13 (3-D); the four-body family D, B3, B5, B7 (8-D);
    the two-witness hull H^dagger + B7 + B9 (6-D). Differential evolution, then Nelder-Mead."""
    if not _S and CACHE.exists():
        cached = json.loads(CACHE.read_text(encoding="utf-8"))
        if cached.get("code") == _code_key() and cached.get("qdag") == list(qdag):
            _S.update(cached["results"])
    if _S:
        return _S
    base = base_pieces(qdag)
    lifts = {}
    for n in (7, 9, 11, 13):
        box = [(0.0, 2 * math.pi / n), (-0.06, 0.06), (-0.06, 0.06)]
        fun = lambda x, n=n, m=512: hull_pieces(base + placed_reuleaux(n, x[0], x[1:3]), m)[0]
        de = differential_evolution(fun, box, seed=7 * n, popsize=25, maxiter=150, tol=1e-12, polish=False)
        res = minimize(lambda x: fun(x, n, 2048), de.x, method="Nelder-Mead",
                       options={"xatol": 1e-10, "fatol": 1e-14, "maxfev": 3000})
        lifts[str(n)] = {"J": float(fun(res.x, n, 8192)), "placement": [float(v) for v in res.x]}
    box8 = [(-0.08, 0.08), (-0.08, 0.08), (0.0, 2 * math.pi / 5), (-0.08, 0.08), (-0.08, 0.08),
            (0.0, 2 * math.pi / 7), (-0.08, 0.08), (-0.08, 0.08)]
    four = lambda x, m=512: hull_pieces(base_pieces(x[:5]) + placed_reuleaux(7, x[5], x[6:8]), m)[0]
    de = differential_evolution(four, box8, seed=20260926, popsize=15, maxiter=250, tol=1e-12, polish=False)
    res = minimize(lambda x: four(x, 2048), de.x, method="Nelder-Mead",
                   options={"xatol": 1e-10, "fatol": 1e-14, "maxfev": 6000})
    four_body = {"area": float(four(res.x, 8192)), "placement": [float(v) for v in res.x]}
    box6 = [(0.0, 2 * math.pi / 7), (-0.06, 0.06), (-0.06, 0.06), (0.0, 2 * math.pi / 9), (-0.06, 0.06), (-0.06, 0.06)]
    two = lambda x, m=512: hull_pieces(base + placed_reuleaux(7, x[0], x[1:3]) + placed_reuleaux(9, x[3], x[4:6]), m)[0]
    de = differential_evolution(two, box6, seed=79, popsize=15, maxiter=150, tol=1e-12, polish=False)
    res = minimize(lambda x: two(x, 2048), de.x, method="Nelder-Mead",
                   options={"xatol": 1e-10, "fatol": 1e-14, "maxfev": 4000})
    two_witness = {"area": float(two(res.x, 8192)), "placement": [float(v) for v in res.x]}
    _S.update({"lifts": lifts, "four_body": four_body, "two_witness": two_witness})
    CACHE.parent.mkdir(parents=True, exist_ok=True)
    CACHE.write_text(json.dumps({"code": _code_key(), "qdag": list(qdag), "results": _S}, indent=1) + "\n",
                     encoding="utf-8")
    return _S


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

def x1_paper(w):
    out = []
    for name, val in w["snapshot"]["mishra_fulltext"]["facts"].items():
        if val is None:
            out.append(f"Mishra's full text: {name} not found")
    facts = w["snapshot"]["mishra_fulltext"]["facts"]
    claims = w["paper_claims"]
    if facts.get("slack") and claims["slack"] not in facts["slack"].replace(" ", "").replace("×10−", "e-"):
        out.append(f"leaf slack: Mishra {facts['slack']!r}, Round 07 {claims['slack']}")
    if facts.get("fourth_body") and claims["four_body"] not in facts["fourth_body"]:
        out.append("the fourth body's value differs")
    return out


def x2_repository(w):
    out, rep, cl = [], w["snapshot"]["repository"], w["repo_claims"]
    pairs = [("exhibited placement", rep["reuleaux"]["placement"], cl["qdag"], 1e-12),
             ("exact-kernel area", rep["reuleaux"]["exact_kernel"], cl["exact"], 0.0),
             ("rigorous outer area", rep["reuleaux"]["outer_1e6"], cl["outer"], 0.0),
             ("four-body optimum", rep["four_body_optimum"], cl["four_body"], 0.0),
             ("8-D boxes at 0.835", rep["extrapolation_0835"]["boxes"], cl["boxes"], 0.0),
             ("8-D days at 0.835", rep["extrapolation_0835"]["days"], cl["days"], 0.0),
             ("d* at 0.8344", rep["d_star_08344"], cl["d_star"], 0.0)]
    for name, logged, quoted, tol in pairs:
        a, b = np.atleast_1d(logged), np.atleast_1d(quoted)
        if a.shape != b.shape or np.max(np.abs(a - b) / np.maximum(1.0, np.abs(a))) > tol + 1e-15:
            out.append(f"{name}: repository {logged}, Round 07 {quoted}")
    return out


def w1_domain(w):
    out = []
    d = sp.symbols("d", positive=True)
    for dv in (0.5001, 0.6, 0.6938, 1.3):
        at = {d: sp.Float(dv, 40)}
        if abs(sp.N((w["domain_f"](d) - phi_text(sp.Rational(1, 2), d)).subs(at), 40)) > 1e-30:
            out.append(f"f({dv}) is not Phi_1/2({dv})")
    ds = d_star(0.8344, w["domain_f"])
    if abs(ds - w["d_star"]) > 5e-13:
        out.append(f"d*(0.8344) = {ds!r}, claimed {w['d_star']}")
    # derivation: some corner of B_n lies within pi/n of t's direction, so a corner sits at
    # distance >= sqrt(t^2 + R^2 + 2 t R cos(pi/n)); beyond d* the hull already has area >= T
    Rn = lambda n: 1 / (2 * math.cos(math.pi / (2 * n)))
    derived = lambda n, T: brentq(lambda t: t * t + Rn(n) ** 2 + 2 * t * Rn(n) * math.cos(math.pi / n)
                                  - d_star(T) ** 2, 0.0, 1.0, xtol=1e-15)
    for T, bounds in w["t_claims"].items():
        for n, claimed in bounds.items():
            mine, text = derived(n, float(T)), w["t_n"](n, d_star(float(T)))
            if abs(mine - text) > 1e-13 or abs(mine - claimed) > 5e-13:
                out.append(f"T={T} n={n}: derived {mine!r}, formula {text!r}, claimed {claimed}")
    # the exclusion is sound: a body beyond the bound makes the hull of D and that body alone reach T
    rng = np.random.default_rng(3)
    for n in (3, 5):
        tb = derived(n, 0.8344)
        for _ in range(60):
            r, a, phi = tb + rng.uniform(1e-9, 0.05), rng.uniform(0, 2 * np.pi), rng.uniform(0, 2 * np.pi)
            area = hull_pieces(placed_disc() + placed_reuleaux(n, phi, (r * math.cos(a), r * math.sin(a))))[0]
            if area < 0.8344:
                out.append(f"B{n} at |t| = {r:.6f} > {tb:.6f} gives hull {area:.9f} < 0.8344")
                break
    w["w1"] = {"d_star_08344": ds, "d_star_0835": d_star(0.835),
               "t": {T: {n: derived(n, float(T)) for n in (3, 5)} for T in w["t_claims"]}}
    return out


def w2_seed(w):
    out, rep = [], w["snapshot"]["repository"]
    q = rep["reuleaux"]["placement"]
    area = hull_pieces(base_pieces(q), 16384)[0]
    poly = hull_pieces(placed_disc() + placed_polygon(V3, 0.0, rep["polygon"]["placement"][:2])
                       + placed_polygon(V5, rep["polygon"]["placement"][2], rep["polygon"]["placement"][3:5]), 16384)[0]
    if abs(area - rep["reuleaux"]["exact_kernel"]) > 1e-11 or area > rep["reuleaux"]["outer_1e6"]:
        out.append(f"seed hull {area!r} vs the repository's exact {rep['reuleaux']['exact_kernel']}")
    if abs(poly - rep["polygon"]["exact_kernel"]) > 1e-11:
        out.append(f"classical hull {poly!r} vs the repository's exact {rep['polygon']['exact_kernel']}")
    norm = q[2] % (2 * math.pi / 5)
    if abs(norm - w["phi5_norm"]) > 5e-13:          # the text rounds to 8 digits
        out.append(f"normalized angle {norm!r}, claimed {w['phi5_norm']}")
    head = 0.835 - rep["reuleaux"]["exact_kernel"]
    if abs(head - w["headroom"]) > 5e-7:
        out.append(f"headroom {head:.4e}, claimed {w['headroom']}")
    w["w2"] = {"exact_hull": area, "classical_exact_hull": poly, "normalized_phi5": norm, "headroom": head}
    return out


def sampled_hull(q, extra, per_arc=20000):
    """the same hull from dense boundary samples - an inner polygon, independent of the
    exact envelope; extra = [(n, phi, t)] for further Reuleaux bodies"""
    pts = [disc_samples(200000), reuleaux_boundary(3, per_arc) + np.asarray(q[:2]),
           reuleaux_boundary(5, per_arc) @ rot(q[2]).T + np.asarray(q[3:5])]
    for n, phi, t in extra:
        pts.append(reuleaux_boundary(n, per_arc) @ rot(phi).T + np.asarray(t))
    return float(ConvexHull(np.vstack(pts)).volume)


_POLISH = {}


def polish_lift(qdag, n, start):
    """Nelder-Mead from a given placement of B_n on the fixed base (memoized)"""
    key = (tuple(qdag), n, tuple(start))
    if key not in _POLISH:
        base = base_pieces(qdag)
        fun = lambda x, m=2048: hull_pieces(base + placed_reuleaux(n, x[0], x[1:3]), m)[0]
        res = minimize(fun, np.array(start, dtype=float), method="Nelder-Mead",
                       options={"xatol": 1e-10, "fatol": 1e-14, "maxfev": 3000})
        _POLISH[key] = (float(fun(res.x, 8192)), [float(v) for v in res.x])
    return _POLISH[key]


def w3_lifts(w):
    """J_{B_n}(H^dagger): the minimum of this tree's search and of a polish started at the
    package's recorded placement, each minimum confirmed by a sampled hull"""
    out, rep = [], w["snapshot"]["repository"]
    qdag = rep["reuleaux"]["placement"]
    s = searches(tuple(qdag))["lifts"]
    base = base_pieces(qdag)
    recorded = {r["n"]: r for r in w["validation"]["search_prior"]["candidate_ranking_strongest_first"]}
    rows = {}
    for n in (7, 9, 11, 13):
        rec = recorded[n]
        start = (rec["phi"], rec["tx"], rec["ty"])
        at_theirs = hull_pieces(base + placed_reuleaux(n, *start[:1], start[1:]), 8192)[0]
        pol, pol_x = polish_lift(qdag, n, start)
        cand = [(s[str(n)]["J"], s[str(n)]["placement"], "search"), (pol, pol_x, "polish from the package's placement")]
        J, x, found_by = min(cand, key=lambda c: c[0])
        samp = sampled_hull(qdag, [(n, x[0], x[1:3])])
        rows[n] = {"J": J, "found_by": found_by, "placement": x, "search": s[str(n)]["J"], "polish": pol,
                   "exact_at_package_placement": at_theirs, "package_sampled": rec["sampled_fixed_base_min_area"],
                   "sampled_at_J": samp, "text": w["lift_claims"][n]}
        if abs(J - samp) > 1e-8:
            out.append(f"B{n}: exact {J:.10f} vs sampled {samp:.10f} at the minimizing placement")
        if not rec["sampled_fixed_base_min_area"] < at_theirs:
            out.append(f"B{n}: the package's sampled value is not below the exact hull at its own placement")
        if abs(J - w["lift_claims"][n]) > 1e-4:
            out.append(f"B{n}: J = {J:.6f}, Round 07 says {w['lift_claims'][n]}")
    order = sorted(rows, key=lambda n: -rows[n]["J"])
    if order != list(w["ranking"]):
        out.append(f"ranking by exact J is {order}, claimed {list(w['ranking'])}")
    w["w3"] = {"rows": rows, "order": order}
    return out


def w4_four_bodies(w):
    out, rep = [], w["snapshot"]["repository"]
    s = searches(tuple(rep["reuleaux"]["placement"]))
    four, x = s["four_body"]["area"], s["four_body"]["placement"]
    j7 = min(s["lifts"]["7"]["J"], (w.get("w3") or {}).get("rows", {}).get(7, {}).get("J", 1.0))
    # an optimizer is an adversary to its objective's artefacts: confirm the value independently
    samp = sampled_hull(x[:5], [(7, x[5], x[6:8])])
    if abs(four - samp) > 1e-8:
        out.append(f"four-body exact {four:.10f} vs sampled {samp:.10f}")
    # a placement of D, B3, B5, B7 below 0.835 would make gate R07-G1 false
    if four < w["gate_target"]:
        out.append(f"a four-body placement has hull {four:.9f} < {w['gate_target']}")
    # sec. 24: the base reconfigures - the four-body optimum lies below the fixed-seed lift
    if not four < j7:
        out.append(f"four-body search {four:.9f} does not go below the fixed-seed lift {j7:.9f}")
    w["w4"] = {"four_body_search": four, "sampled_hull": samp, "placement": x, "fixed_seed_J7": j7,
               "repository_optimum": rep["four_body_optimum"], "search_minus_repository": four - rep["four_body_optimum"]}
    return out


def w5_cost(w):
    """The repository's rule (scaling.py at the cited commit): the least-squares exponent
    of the logged counts, anchored at the run with the largest margin - the run farthest
    from the target - with the margin taken from the four-body optimum. Rebuilt from the
    counts; the alternatives show how much the digits depend on that choice."""
    out, rep = [], w["snapshot"]["repository"]
    rows = np.array(sorted(rep["eight_d_rows"]), dtype=float)
    slope, icpt = np.polyfit(np.log(rows[:, 0]), np.log(rows[:, 2]), 1)
    margin = rep["four_body_optimum"] - w["cost_target"]
    anchored = lambda m0, n0: n0 * (m0 / margin) ** (-slope)
    boxes = anchored(rows[-1, 0], rows[-1, 2])
    days = boxes / rep["eight_d_throughput"] / 86400
    if abs(-slope - (-rep["eight_d_exponent"])) > 5e-4:
        out.append(f"refitted exponent {slope:.4f}, logged {rep['eight_d_exponent']}")
    if abs(boxes / w["cost_claims"]["boxes"] - 1) > 1e-3 or abs(days / w["cost_claims"]["days"] - 1) > 1e-3:
        out.append(f"rebuilt {boxes:.4e} boxes / {days:.1f} days vs claimed {w['cost_claims']}")
    alt = {"least-squares centre": math.exp(icpt) * margin ** slope,
           "anchored at the nearest run": anchored(rows[0, 0], rows[0, 2])}
    w["w5"] = {"exponent": -slope, "margin": margin, "boxes": boxes, "days": days,
               "alternatives": {k: {"boxes": v, "days": v / rep["eight_d_throughput"] / 86400} for k, v in alt.items()}}
    return out


def d1_transfer(w):
    T, tau = sp.symbols("T tau", positive=True)
    R = 2 * T                                   # Round 04: a hull of area < T holding D lies in B_{2T}
    derived = tau * (2 * sp.pi * R) + sp.pi * tau ** 2
    return [] if sp.simplify(w["omega"](T, tau) - derived) == 0 else ["omega_T is not tau 2 pi (2T) + pi tau^2"]


def d2_switching(w):
    out, rep = [], w["snapshot"]["repository"]
    qdag = rep["reuleaux"]["placement"]
    s = searches(tuple(qdag))
    joint, x = s["two_witness"]["area"], s["two_witness"]["placement"]
    base = base_pieces(qdag)
    # at the joint minimum, each witness's own hull with the base (the proof's A_K(q, g_K))
    a7 = hull_pieces(base + placed_reuleaux(7, x[0], x[1:3]), 8192)[0]
    a9 = hull_pieces(base + placed_reuleaux(9, x[3], x[4:6]), 8192)[0]
    samp = sampled_hull(qdag, [(7, x[0], x[1:3]), (9, x[3], x[4:6])])
    rows = (w.get("w3") or {}).get("rows", {})
    j7 = rows.get(7, {}).get("J", s["lifts"]["7"]["J"])
    j9 = rows.get(9, {}).get("J", s["lifts"]["9"]["J"])
    if abs(joint - samp) > 1e-8:
        out.append(f"joint exact {joint:.10f} vs sampled {samp:.10f}")
    if joint < max(a7, a9) - 1e-12:
        out.append(f"the two-witness hull {joint:.9f} is below a single-witness hull at the same placement")
    # sec. 11: min over independent placements of the max is the max of the minima
    if joint < w["switch_bound"](j7, j9, hull_pieces(base, 8192)[0]) - 1e-9:
        out.append(f"the two-witness minimum {joint:.9f} is below the claimed bound "
                   f"{w['switch_bound'](j7, j9, hull_pieces(base, 8192)[0]):.9f}")
    w["d2"] = {"joint_min": joint, "sampled": samp, "A7_at_joint": a7, "A9_at_joint": a9, "J7": j7, "J9": j9}
    return out


def p1_package(w):
    out, v, spec = [], w["validation"]["search_prior"], w["spec"]
    rep = w["snapshot"]["repository"]
    if v["official_exact_kernel_base_area"] != rep["reuleaux"]["exact_kernel"]:
        out.append("official exact area differs from the repository")
    if v["official_rigorous_outer_base_area"] != rep["reuleaux"]["outer_1e6"]:
        out.append("official outer area differs from the repository")
    if abs(v["normalized_phi5"] - rep["reuleaux"]["placement"][2] % (2 * math.pi / 5)) > 1e-15:
        out.append("normalized phi5 differs")
    t835 = {n: t_text(n, d_star(0.835)) for n in (3, 5)}
    if abs(v["tmax3_at_0835"] - t835[3]) > 1e-13 or abs(v["tmax5_at_0835"] - t835[5]) > 1e-13:
        out.append("tmax at 0.835 differs")
    if not v["sampled_inner_base_area"] < rep["reuleaux"]["exact_kernel"]:
        out.append("the sampled inner base area is not below the exact one")
    if w["validation"]["expected_search_only_strongest_regular_reuleaux"] != v["candidate_ranking_strongest_first"][0]["n"]:
        out.append("expected strongest differs from the recorded ranking")
    if (spec["threshold"] != 0.835 or spec["primary_witness"] != "Reuleaux7"
            or abs(spec["phi5_domain"][1] - 2 * math.pi / 5) > 1e-15
            or abs(spec["translation_radius_bounds"]["Reuleaux3"] - t835[3]) > 5e-13
            or abs(spec["translation_radius_bounds"]["Reuleaux5"] - t835[5]) > 5e-13):
        out.append("the local compute spec disagrees with the text")
    return out


def p2_package(w):
    out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]}
    for rec, leaf, text in ((w["validation"]["round07"], DOC, w["text"]),
                            (w["validation"]["state_crystal"], CRYSTAL, w["crystal"])):
        _, size, digest = leaves[leaf]
        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")
    return out


# ---------------------------------------------------------------- registry (Round 07)

LABEL = "a sec. 31 atlas-status label, defined there; not a judgment"
R07_DEFINITIONS = {
    "VERIFIED": ("contextual", "sec. 41: an external fact checked against its source (paper, repository)"),
    "LIFT-CLOSED": ("in-line", "sec. 31 label: a witness is certified to lift every base placement of the cell to T"),
    "BASE-PRUNED": ("in-line", "sec. 7, 31 label: the base family's own lower bound on the cell is already >= T"),
    "NEW-SEPARATOR-CERTIFIED": ("in-line", "sec. 25, 37: what B7 becomes if gate R07-G1 is certified"),
    "OPEN / COMPUTE-DEFERRED": ("contextual", "sec. 41: open, and waiting on a computation that is specified"),
    "BOUNDARY-ANOMALY": ("in-line", "sec. 31 label: an erosion, core or interval assumption fails on the cell"),
    "EXTERNAL-NUMERICAL-FAMILY-CEILING": ("in-line", "sec. 25: a family minimum located numerically by an outside "
                                                     "search - an upper bound on Lambda of the family"),
    "MULTI-WITNESS-CLOSED": ("in-line", "sec. 31 label: the cell is closed by a witness-switching batch"),
    "PROVED AS CERTIFICATE LOGIC": ("contextual", "sec. 41: the procedure is shown sound; nothing is computed"),
    "REFINE": ("in-line", "sec. 31 label: no certificate yet; split further"),
    "REUSED / ANCHOR": ("in-line", "sec. 37: the disc, reused and fixed at the origin"),
    "SEARCH-HIT": ("in-line", "sec. 31 label: a numerical witness candidate only"),
    "SEARCH-PRIOR ONLY": ("contextual", "sec. 23: the ranking is a search prior and nothing more"),
}
PBCT = "PASS by cited theorem"
R07_REVIEWS = [
    ("PROVED", "Threshold-conditioned atlas theorem", "analytic", "PASS", "Thm 10.1"),
    ("PROVED", "Witness-switching theorem", "analytic", "PASS", "Thm 11.1; min over independent placements of a max (D2)"),
    ("PROVED", "Robust cell-lift transfer", "analytic", PBCT,
     "Thm 17.1: Steiner and Round 04's radius bound (D1); loose by pi, as Round 05's sec. 9"),
    ("PROVED AS CERTIFICATE LOGIC", "Lazy dimension activation", "analytic", "PASS", "sec. 13: a hull only grows"),
    ("CLOSED", "MINIMIZER-ATLAS SCHEMA", "reading", "PASS", "closed as a schema; nothing is emitted or run"),
    ("CLOSED", "CONDITIONAL WITNESS LIFTING", "analytic", "PASS", "Thm 10.1, 11.1, 17.1"),
    ("VERIFIED", "External seed source", "outside-corpus", "PASS", "Mishra's paper and repository (X1, X2)"),
    ("VERIFIED", "Official five-dimensional parameterization", "outside-corpus", "PASS", "X1; W2"),
    ("VERIFIED", "Sharper translation domain", "analytic", "PASS", "derived here and matched to the log (W1, X2)"),
    ("VERIFIED", "Official exhibited near-minimizer seed", "computation", "PASS",
     "rebuilt with this tree's exact hull to 1e-11 of the logged exact kernel (W2)"),
    ("SEARCH-ONLY", "Regular Reuleaux ranking", "computation", "PASS",
     "rebuilt exactly; the order holds (W3), and a search is all it claims to be"),
    ("SEARCH-PRIOR ONLY", "", "n/a", "n/a", "sec. 23's status line for the ranking"),
    ("SEARCH-PRIOR", "25. $B_7$ 的當前身份", "reading", "PASS", "correctly not upgraded"),
    ("SEARCH-PRIOR", "$B_7$", "reading", "PASS", "sec. 37"),
    ("SEARCH-PRIOR", "$B_9,B_{11},B_{13}$", "reading", "PASS", "sec. 37"),
    ("EXTERNAL-NUMERICAL-FAMILY-CEILING", "25. $B_7$ 的當前身份", "outside-corpus", "PASS",
     "0.836494901, the repository's four-body optimum; this tree's search finds the same (W4)"),
    ("NEW-SEPARATOR-CERTIFIED", "25. $B_7$ 的當前身份", "n/a", "n/a", "conditional on R07-G1"),
    ("NEW-SEPARATOR-CERTIFIED", "$B_7$", "n/a", "n/a", "conditional on R07-G1"),
    ("DOMINANCE-UPGRADE", "$B_3$", "reading", "PASS", "P3 inside B3 (RUN-009 W6)"),
    ("DOMINANCE-UPGRADE", "$B_5$", "reading", "PASS", "P5 inside B5 (RUN-009 W6)"),
    ("REUSED / ANCHOR", "$D$", "reading", "PASS", ""),
    ("OPEN", "$B_7$ as certified next witness", "n/a", "n/a", ""),
    ("OPEN / COMPUTE-DEFERRED", "$0.8350$ lower bound", "n/a", "n/a", "no four-body placement below 0.835 was found (W4)"),
    ("COMPUTE-DEFERRED", "Gate R07-G1", "n/a", "n/a", "equivalent to Lambda(D, B3, B5, B7) >= 0.835; W4 finds no counterexample"),
    ("COMPUTE-DEFERRED", "FIRST ACTUAL 0.8350 CERTIFICATE", "n/a", "n/a",
     "the boxed conclusion G; read from census v3 on (RUN-003)"),
    ("COMPUTE-DEFERRED", "", "n/a", "n/a", LABEL),
    ("BASE-PRUNED", "", "n/a", "n/a", LABEL),
    ("LIFT-CLOSED", "", "n/a", "n/a", LABEL),
    ("MULTI-WITNESS-CLOSED", "", "n/a", "n/a", LABEL),
    ("REFINE", "", "n/a", "n/a", LABEL),
    ("SEARCH-HIT", "", "n/a", "n/a", LABEL),
    ("BOUNDARY-ANOMALY", "", "n/a", "n/a", LABEL),
]


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


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

CHECKS = {"A0": gate.anchors_check(ANCHORS), "A1": gate.citations_check(CITE_OPTS), "X1": x1_paper,
          "X2": x2_repository, "W1": w1_domain, "W2": w2_seed, "W3": w3_lifts, "W4": w4_four_bodies,
          "W5": w5_cost, "D1": d1_transfer, "D2": d2_switching, "P1": p1_package, "P2": p2_package,
          "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "A1": {"text", "snapshot"}, "X1": {"snapshot", "paper_claims"},
           "X2": {"snapshot", "repo_claims"}, "W1": {"domain_f", "t_n", "d_star", "t_claims"},
           "W2": {"snapshot", "phi5_norm", "headroom"}, "W3": {"snapshot", "validation", "lift_claims", "ranking"},
           "W4": {"snapshot", "gate_target"}, "W5": {"snapshot", "cost_claims", "cost_target"}, "D1": {"omega"},
           "D2": {"snapshot", "switch_bound"}, "P1": {"validation", "spec", "snapshot"},
           "P2": {"validation", "text", "crystal", "manifest"}, "R1": {"registry", "definitions", "reviews"}}

CLAIMS = {
    "domain_f": f_text, "t_n": t_text, "d_star": 0.693830648713,
    "t_claims": {"0.8344": {3: 0.192366411526, 5: 0.195890714644}, "0.835": {3: 0.194856180909, 5: 0.197820670401}},
    "phi5_norm": 2.4128951e-5, "headroom": 2.19e-4,
    "lift_claims": {7: 0.83713, 9: 0.83563, 11: 0.83613, 13: 0.83597}, "ranking": (7, 11, 13, 9),
    "gate_target": 0.835, "cost_target": 0.835, "cost_claims": {"boxes": 5.527e12, "days": 5635.8},
    "omega": omega_text, "switch_bound": lambda a, b, base: max(a, b),
    "paper_claims": {"slack": "1.2409e-5", "four_body": "0.836494901"},
    "repo_claims": {"qdag": [-0.01215883209899, -3.7081986e-8, 1.256661190387, 0.02299660691706, -3.8969815e-6],
                    "exact": 0.834780945912, "outer": 0.834781190917, "four_body": 0.836494901,
                    "boxes": 5.527e12, "days": 5635.8, "d_star": 0.693830648713},
}


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 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:
        recs = {str(n): gate.fetch_arxiv(r["id"]) for n, r in REFS.items()}
        snap = {"retrieved": datetime.date.today().isoformat(), "records": recs,
                "mishra_fulltext": gate.fetch_arxiv_facts(REFS[1]["id"], 2, MISHRA_FACTS),
                "repository": {"repo": REPO, "commit": COMMIT, **repository_facts()}}
        SNAPSHOT.write_text(json.dumps(snap, ensure_ascii=False, indent=1) + "\n", encoding="utf-8")
    snapshot = json.loads(SNAPSHOT.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)), "registry": registry.load(),
                "definitions": dict(R07_DEFINITIONS), "reviews": list(R07_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", "d2"):
        print(key, w.get(key))
    if not args.drill:
        return
    cl, pc, lift = CLAIMS["repo_claims"], CLAIMS["paper_claims"], CLAIMS["lift_claims"]
    sprior = validation["search_prior"]

    def f_plus(d):                        # the arccos term added instead of subtracted
        sqrt, acos, pi = (sp.sqrt, sp.acos, sp.pi) if isinstance(d, sp.Basic) else (math.sqrt, math.acos, math.pi)
        quarter = sp.Rational(1, 4) if isinstance(d, sp.Basic) else 0.25
        return (pi + acos(1 / (2 * d))) / 4 + sqrt(d * d - quarter) / 2

    def t_by_cos(n, ds):                  # R_n written as 1/(2 cos(pi/2n)): the same number
        R, c = 1 / (2 * math.cos(math.pi / (2 * n))), math.cos(math.pi / n)
        return -R * c + math.sqrt(R * R * c * c - R * R + ds * ds)

    def t_sign(n, ds):                    # +R cos(pi/n): the corner taken on the far side
        R, c = 1 / (2 * math.sin(math.pi * (n - 1) / (2 * n))), math.cos(math.pi / n)
        return R * c + math.sqrt(R * R * c * c - R * R + ds * ds)

    pi_of = lambda T: sp.pi if isinstance(T, sp.Basic) else math.pi
    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-f-as-phi", "control",
         {"domain_f": lambda d: phi_text(sp.Rational(1, 2) if isinstance(d, sp.Basic) else 0.5, d)}, set()),
        ("K2-t-by-cos", "control", {"t_n": t_by_cos}, set()),
        ("K3-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()),
        ("K4-omega-factored", "control", {"omega": lambda T, tau: pi_of(T) * tau * (4 * T + tau)}, set()),
        ("M1-doc-seed-area", "mutation", {"text": text.replace("0.834780945912", "0.834780945913")}, {"A0"}),
        ("M2-ref-year", "mutation", {"snapshot": {**snapshot, "records": {
            **snapshot["records"], "3": {**snapshot["records"]["3"], "years": [2019]}}}}, {"A1"}),
        ("M3-slack-misquoted", "mutation", {"paper_claims": {**pc, "slack": "1.2490e-5"}}, {"X1"}),
        ("M4-four-body-misquoted", "mutation", {"repo_claims": {**cl, "four_body": 0.836494910}}, {"X2"}),
        ("M5-seed-digit", "mutation", {"repo_claims": {**cl, "qdag": [cl["qdag"][0] + 1e-9] + cl["qdag"][1:]}}, {"X2"}),
        ("M6-f-arccos-sign", "mutation", {"domain_f": f_plus}, {"W1"}),
        ("M7-t-far-corner", "mutation", {"t_n": t_sign}, {"W1"}),
        ("M8-dstar-digit", "mutation", {"d_star": 0.693830648714}, {"W1"}),
        ("M9-phi5-norm", "mutation", {"phi5_norm": 2.4128952e-5}, {"W2"}),
        ("M10-headroom", "mutation", {"headroom": 2.29e-4}, {"W2"}),
        ("M11-B7-lift", "mutation", {"lift_claims": {**lift, 7: 0.83813}}, {"W3"}),
        ("M12-ranking", "mutation", {"ranking": (7, 9, 11, 13)}, {"W3"}),
        ("M13-gate-too-high", "mutation", {"gate_target": 0.8370}, {"W4"}),
        ("M14-cost-boxes", "mutation", {"cost_claims": {"boxes": 5.0e12, "days": 5635.8}}, {"W5"}),
        ("M15-omega-without-pi", "mutation", {"omega": lambda T, tau: 4 * T * tau + pi_of(T) * tau ** 2}, {"D1"}),
        ("M16-switch-additive", "mutation", {"switch_bound": lambda a, b, base: a + b - base}, {"D2"}),
        ("M17-recorded-exact-area", "mutation", {"validation": {**validation, "search_prior": {
            **sprior, "official_exact_kernel_base_area": 0.834780945913}}}, {"P1"}),
        ("M18-spec-threshold", "mutation", {"spec": {**spec, "threshold": 0.8344}}, {"P1"}),
        ("M19-package-sha", "mutation",
         {"validation": {**validation, "round07": {**validation["round07"], "sha256": "0" * 64}}}, {"P2"}),
        ("M20-review-dropped", "mutation", {"reviews": list(R07_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-010", "subject": "Round 07: the minimizer atlas and threshold-conditioned witness lifting",
           "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", "d2")}, "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("R07", "RUN-010", R07_DEFINITIONS, R07_REVIEWS)
        print(f"registry: {len(R07_DEFINITIONS)} definitions, {len(R07_REVIEWS)} reviews recorded for R07")


if __name__ == "__main__":
    main()