"""RUN-009 - Round 06: the finite witness exchange compiler.

Round 06 turns Round 05's existence statement - a non-saturated family can always be
beaten by a bigger finite one - into a compiler: the minimizer set of a finite family
is compact, a non-saturated family has a uniform positive violation margin delta_F on
it, a finite dictionary batch with positive separation margin S_F(B) strictly raises
Lambda, and a refinement with cell, dictionary and certificate errors summing below
delta_F/2 must eventually find such a batch. It anchors the ladder at Mishra's
certified three-witness seed. The theorems are read in the report; here the seed is
rebuilt exactly, the margins are recomputed with Round 03's own certificate LP, the
exchange quantities are measured on the one family where they are exact, and the
level-3 seed is attacked by search.

Checks
  A0 anchors      the formulas below occur in Round 06 as written
  A1 citations    its six external references, with Xie's cited title pinned as a stale one
  X1 external     sec. 1-3, 35: Mishra's abstract and full text, Pal's value, Gibbs' search
  W1 seed ladder  sec. 2: lambda_1, Pal's Lambda(D, P3), and Lambda(D, B3) - equal to it
  W2 margin       sec. 29: delta_{D,B3} by Round 03's certificate LP; the worst target (Jung)
  W3 exchange     sec. 19-20 on the seed: the distance bound is attained, gamma is exact
  W4 gauge        sec. 6: the common rotation gauge, d_m = 3m - 4
  W5 level three  sec. 1, 27: a search that could refute 0.8344; the dominance gap
  W6 dominance    sec. 26-27: each regular polygon lies inside its Reuleaux polygon
  D1 Lipschitz    sec. 9, 13: the margin is 1-Lipschitz in cover and target (grid LP)
  P1 sanity       the package's VALIDATION.json rebuilt
  P2 package      the package's self-description of its documents matches the archive
  R1 registry     Round 06's judgments reviewed, first-used statuses defined

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

import numpy as np
from scipy.optimize import differential_evolution, minimize
from scipy.spatial import ConvexHull

import gate
import registry
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run006_round03_placement_certificate import G, body, chiral_cover, eta, grid_margin, proper_law
from run008_round05_saturation_gate import (ABAR, R0, disc_samples, envelope, hull_disc, phi_text, reuleaux_boundary, segments,
                                            reuleaux_support, reuleaux_vertices, verify_segments, wrap)

PKG = "main.zip!/AMRAL_LUC_FC_Round_06_Package_v0.1.zip!/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_06_Witness_Exchange_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_06_v0.1.md"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_06_VALIDATION.json"
SNAPSHOT = TREE / "data" / "external" / "round06-citations.json"
LOG = TREE / "data" / "gate-logs" / "run009-round06-witness-exchange.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
PAL = math.pi / 8 + math.sqrt(3) / 4
DELTA = 1 / math.sqrt(3) - 0.5

ANCHORS = {
    "W1": [r"\Lambda(D,P_3)=\frac{\pi}{8}+\frac{\sqrt3}{4}.",
           r"\Lambda(D,B_3)\ge\frac{\pi}{8}+\frac{\sqrt3}{4}\approx0.8257117836.",
           r"\lambda_1=\frac{\pi}{4}\approx0.7853981634."],
    "W2": [r"\delta_{D,B_3}=\frac1{\sqrt3}-\frac12\approx0.0773502692.",
           r"\delta_{\mathcalF}:=\min_{U\in\mathfrakM(\mathcalF)}W(U)>0."],
    "W3": [r"d_H\left(V,\mathfrakM(\mathcalF)\right)\ges.",
           r"\Lambda(\mathcalF\cup\mathcalB)\ge\Lambda(\mathcalF)+\gamma_{\mathcalF}(s)."],
    "W4": [r"d_m=3(m-1)-1=3m-4."],
    "W5": [r"\Lambda(\mathcalF_3)\ge0.8344.", r"\Lambda(D,B_3,B_5)\ge\Lambda(D,P_3,P_5)."],
    "W6": [r"\Lambda(\mathcalG\cup\{L\})\ge\Lambda(\mathcalG\cup\{K\})."],
    "D1": [r"|W(U)-W(V)|\led_H(U,V).", r"|M_U(K)-M_U(\widehatK)|\led_H(K,\widehatK).",
           r"M_U(K)\ge\mu_{j,K}-\tau_j.", r"\tau_n+\varepsilon_n+\zeta_n<\frac{\delta_{\mathcalF}}{2}."],
    "X1": [r"1.72\times10^{-9}.", r"486,799,600"],
}
REFS = {1: {"kind": "arxiv", "id": "1502.01251"}, 2: {"kind": "arxiv", "id": "1810.10089"},
        3: {"kind": "arxiv", "id": "2608.30538"}, 4: {"kind": "arxiv", "id": "2609.01284"},
        5: {"kind": "arxiv", "id": "2606.04458"}, 6: {"kind": "crossref", "doi": "10.1017/CBO9781139003858"}}
CITE_OPTS = {n: {} for n in REFS}
# Round 06 cites Xie by the title of the preprint's first two versions; v3 (13 Jun 2026)
# retitled it and v4 (8 Jul 2026) raised its bound - both before Round 06's date
PINNED_CITATIONS = ("ref 5: title differs",)
MISHRA_FACTS = {                     # short phrases only; matched in the full text of v2
    "eta": r"Writing η = 1\.72 × 10 − 9",
    "pal_pair": r"Pál \[ 19 \] takes a disc and an equilateral triangle, evaluates the minimum by hand, and obtains "
                r"π / 8 \+ 3 / 4 \\pi/8\+\\sqrt\{3\}/4",
    "pal_ref": r"J\. Pál \(1920\) Über ein elementares Variationsproblem",
    "gibbs_upper": r"reporting 0\.83699098\. He is careful about what that number is, calling it an upper bo",
    "reflection": r"a reflection where a reflection helps",
    "located_optimum": r"numerically located optimum, 0\.834780947 in the first family",
    "reuleaux_bound": r"M\W*\( D , B 3 , B 5 \) ≤ 0\.834781191",
    "reuleaux_arrangement": r"from the arrangement \( [−0-9., ]+ \)",
    "polygon_bound": r"outer polygon of area at most 0\.833597897",
    "polygon_arrangement": r"Place P 3 P_\{3\} by the translation .{0,300}?leaving D D centred at the origin",
}


def numbers(s):
    """the signed decimals of a fact, each once, in order (the HTML repeats them as TeX)"""
    out = []
    for sign, x in re.findall(r"(−\s*|-)?(\d+\.\d+)", s):
        v = -float(x) if sign else float(x)
        if v not in out:
            out.append(v)
    return out


# ---------------------------------------------------------------- the exact hull of placed bodies

def rot(phi):
    c, s = math.cos(phi), math.sin(phi)
    return np.array([[c, -s], [s, c]])


def placed_disc(r=R0):
    return [(np.zeros(2), r, None)]


def placed_polygon(V0, phi, t):
    return [(v, 0.0, None) for v in V0 @ rot(phi).T + np.asarray(t, dtype=float)]


def placed_reuleaux(n, phi, t):
    """vertices (radius 0), and the arc of radius 1 about each vertex, which carries the
    normals within pi/(2n) of the direction opposite that vertex"""
    V = reuleaux_vertices(n) @ rot(phi).T + np.asarray(t, dtype=float)
    return [(v, 0.0, None) for v in V] + [(V[k], 1.0, (2 * math.pi * k / n + phi + math.pi, math.pi / (2 * n)))
                                          for k in range(n)]


def hull_pieces(pieces, n=2048, verify=True):
    """Area and perimeter of the convex hull of bodies given by support pieces - a centre
    c, a radius rho, and for an arc the range of normals it carries: the hull's support
    is h(u) = max over pieces of c.u + rho. Area = 1/2 int (h^2 - h'^2), Per = int h, in
    closed form between the angles where the maximum changes hands (by bisection, then
    every segment checked in closed form: RUN-031; verify=False keeps the grid alone)."""
    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]

    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(wrap(t - mid)) > half] = -np.inf
        return np.argmax(V, axis=0)

    cuts, owners = envelope(owner, n, len(pieces))
    segs = list(segments(cuts, owners))
    if verify:
        segs = verify_segments(C, rho, [p[2] for p in pieces], segs)
    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
    Pf = lambda k, t: cn[k] * math.sin(t - al[k]) + rho[k] * t
    twice = per = 0.0
    for a, b, k in segs:
        twice += F(k, b) - F(k, a)
        per += Pf(k, b) - Pf(k, a)
    return twice / 2, per


def hull_radius(pieces):
    """the largest distance from the origin to the hull. A disc about c reaches |c| + rho;
    an arc's farthest point is the one along its centre's direction if that direction is
    in its range, and otherwise an endpoint - a vertex, counted among the vertex pieces"""
    best = 0.0
    for c, r, rg in pieces:
        n = float(np.linalg.norm(c))
        if rg is None or (n > 0 and abs(wrap(math.atan2(c[1], c[0]) - rg[0])) <= rg[1]):
            best = max(best, n + r)
    return best


V3, V5 = reuleaux_vertices(3), reuleaux_vertices(5)       # P3: side 1; P5: diagonal 1


def family_area(kind, x, n=2048):
    """(t3, rho5, t5) -> hull area of D, the three-body at t3 (orientation fixed by the
    common rotation gauge) and the five-body turned by rho5 at t5"""
    t3, r5, t5 = x[:2], x[2], x[3:5]
    if kind == "reuleaux":
        pieces = placed_disc() + placed_reuleaux(3, 0.0, t3) + placed_reuleaux(5, r5, t5)
    else:
        pieces = placed_disc() + placed_polygon(V3, 0.0, t3) + placed_polygon(V5, r5, t5)
    return hull_pieces(pieces, n)[0]


_SEARCH = {}
CACHE = TREE / "data" / "cache" / "run009-level3-search.json"     # data/cache is not committed


def _code_key():
    """the search depends on this file and on run008's envelope routine"""
    import hashlib
    import run008_round05_saturation_gate as r8
    digest = hashlib.sha256()
    for path in (__file__, r8.__file__):
        digest.update(open(path, "rb").read())
    return digest.hexdigest()


def level3_search():
    """differential evolution over the gauge-fixed five-parameter box (the five-body's
    turn taken modulo its symmetry 2 pi/5), then Nelder-Mead on a finer angle grid; a
    search gives upper bounds on Lambda of the family, never lower bounds. The result
    is cached under the hash of the code it depends on."""
    if not _SEARCH and CACHE.exists():
        cached = json.loads(CACHE.read_text(encoding="utf-8"))
        if cached.get("code") == _code_key():
            _SEARCH.update(cached["search"])
    if not _SEARCH:
        box = [(-0.08, 0.08), (-0.08, 0.08), (0.0, 2 * math.pi / 5), (-0.08, 0.08), (-0.08, 0.08)]
        for kind in ("reuleaux", "polygon"):
            de = differential_evolution(lambda x: family_area(kind, x, 512), box, seed=20260925, popsize=20,
                                        maxiter=150, tol=1e-12, polish=False)
            res = minimize(lambda x: family_area(kind, x, 2048), de.x, method="Nelder-Mead",
                           options={"xatol": 1e-10, "fatol": 1e-14, "maxfev": 4000})
            x = res.x
            area = family_area(kind, x, 16384)
            # the same placement's hull from dense samples, as an independent check of the value
            if kind == "reuleaux":
                pts = np.vstack([disc_samples(200000), reuleaux_boundary(3, 50000) + x[:2],
                                 reuleaux_boundary(5, 50000) @ rot(x[2]).T + x[3:5]])
            else:
                pts = np.vstack([disc_samples(200000), V3 + x[:2], V5 @ rot(x[2]).T + x[3:5]])
            _SEARCH[kind] = {"area": float(area), "sampled_hull": float(ConvexHull(pts).volume),
                             "placement": [float(v) for v in x]}
        CACHE.parent.mkdir(parents=True, exist_ok=True)
        CACHE.write_text(json.dumps({"code": _code_key(), "search": _SEARCH}, indent=1) + "\n", encoding="utf-8")
    return _SEARCH


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

def a1_citations(w):
    fails = gate.citations_check(CITE_OPTS)(w)
    out = [f for f in fails if f not in w["pinned_citations"]]
    out += [f"pinned finding no longer present: {f}" for f in w["pinned_citations"] if f not in fails]
    cited = gate.parse_refs(w["text"])[5]["title"]
    titles = w["snapshot"]["title_history"]["5"]
    current = max(titles, key=int)
    earlier = [v for v, t in titles.items() if v != current and gate.norm_title(t) == gate.norm_title(cited)]
    if not earlier:
        out.append("ref 5: the cited title is no version's title")
    w["a1"] = {"xie_cited_title_is_version": earlier, "xie_current_version": current,
               "xie_current_title": titles[current]}
    return out


def x1_external(w):
    out, claims = [], w["mishra_claims"]
    ab = w["snapshot"]["abstracts"]["3"]["abstract"]
    sentence = re.search(r"[^.]*test sets[^.]*\.", ab)
    named = sentence.group(0).lower() if sentence else ""
    for body_name in claims["test_sets"]:
        if body_name.lower() not in named:
            out.append(f"Mishra's abstract does not list {body_name!r}")
    for key in ("bound", "nodes", "dimension"):
        if claims[key] not in ab:
            out.append(f"Mishra's abstract does not state {claims[key]!r}")
    facts = w["snapshot"]["mishra_fulltext"]["facts"]
    for name, val in facts.items():
        if val is None:
            out.append(f"Mishra's full text: {name} not found")
    if facts.get("eta") and claims["eta"] not in facts["eta"].replace(" ", "").replace("×10−", "e-"):
        out.append(f"Mishra's error bound is {facts['eta']!r}, Round 06 says {claims['eta']}")
    if facts.get("pal_pair") and not all(p in facts["pal_pair"] for p in w["pal_claim"]):
        out.append("Mishra's account of Pal's pair differs from Round 06's")
    return out


def w1_seed_ladder(w):
    out = []
    disc = hull_pieces(placed_disc())[0]
    tri = hull_pieces(placed_disc() + placed_polygon(V3, 0.0, (0, 0)))[0]
    rt = hull_pieces(placed_disc() + placed_reuleaux(3, 0.0, (0, 0)))[0]
    if abs(disc - math.pi / 4) > 1e-14:
        out.append(f"lambda_1: the disc's hull is {disc!r}")
    for name, v in (("Pal's pair D, P3", tri), ("D, B3", rt)):
        if abs(v - w["pal_value"]) > 1e-12:
            out.append(f"{name} concentric: {v!r}, claimed {w['pal_value']!r}")
    # the lower side (a self-contained proof, RUN-008 W2): a vertex 0.7 out costs more than
    # the value; inside 0.7 the three tips are disjoint and Jensen does the rest
    if not phi_text(R0, 0.7) > PAL or not 2 * math.acos(R0 / 0.7) < math.pi / 2:
        out.append("the lower-bound argument's two numerical facts fail")
    worst = min(hull_pieces(placed_disc() + placed_polygon(V3, a, (d * math.cos(b), d * math.sin(b))))[0] - tri
                for d in (0.002, 0.01, 0.05, 0.1) for b in np.linspace(0, 2 * math.pi, 12, endpoint=False)
                for a in (0.0, 0.3))
    if worst < -1e-12:
        out.append(f"a displaced triangle gives a smaller hull by {-worst:.2e}")
    if not math.pi / 4 < w["pal_value"] < w["mishra_lower"]:
        out.append("the seed ladder is not strictly increasing")
    w["w1"] = {"disc": disc, "disc_triangle": tri, "disc_reuleaux_triangle": rt, "pal": PAL,
               "least_displacement_increase": worst}
    return out


def w2_margin(w):
    """M_D(B3) with Round 03's own machinery: the grid LP over both reflection branches,
    and Theorem 17.1's bracket. With the vertex directions on the grid (M divisible by 3)
    the grid value is exact."""
    out = []
    hK, hU = reuleaux_support(3), (lambda t: np.full(np.shape(t), R0))
    M, P = 3072, 12
    g, sigma, _ = G(hK, hU, M, P, proper_law)
    RK = 1 / math.sqrt(3)
    lo, hi = g - RK * math.pi / P, g + eta(RK + R0, M)
    if abs(g - w["delta"]) > 1e-9 or not lo <= w["delta"] <= hi:
        out.append(f"LP margin {g!r} (bracket [{lo:.6f}, {hi:.6f}]) vs claimed {w['delta']!r}")
    # the disc's worst target: circumradius <= 1/sqrt(3) for every set of diameter 1 (Jung),
    # so no constant-width target beats B3 against the disc
    rng = np.random.default_rng(29)
    worst = 0.0
    for _ in range(40):
        coeffs = {n: tuple(rng.uniform(-1, 1) * a for _ in (0, 1)) for n, a in ((3, 0.16), (5, 0.06), (7, 0.03))}
        worst = max(worst, grid_margin(body(coeffs), hU, +1, 0.0, 1024, proper_law)["primal"])
    if worst > DELTA + 1e-12:
        out.append(f"a random target has margin {worst:.6f} > delta against the disc")
    w["w2"] = {"grid_margin": g, "sigma": sigma, "bracket": [lo, hi], "largest_random_target_margin": worst}
    return out


def w3_exchange(w):
    """F = {D}: its minimizer set is {D}; B = {B3} separates it with S = delta.
    sec. 19: every cover V of B3 holding D is at least delta from D - attained by the hull.
    sec. 20: gamma_D(s) = min{Area(V) - pi/4 : V holds D, d_H(V, D) >= s} = Phi(1/2 + s) - pi/4,
    since d_H(V, D) >= s means a point of V at distance >= 1/2 + s (sec. 22 of Round 05)."""
    out, rng = [], np.random.default_rng(19)
    seed = placed_disc() + placed_reuleaux(3, 0.0, (0, 0))
    attained = hull_radius(seed) - R0
    if abs(attained - DELTA) > 1e-15:
        out.append(f"the seed hull sits {attained!r} from D, not delta")
    least = min(hull_radius(placed_disc() + placed_reuleaux(3, rng.uniform(0, 2 * np.pi), rng.uniform(-0.3, 0.3, 2)))
                for _ in range(300)) - R0
    if least < DELTA - 1e-15:
        out.append(f"a cover of B3 sits only {least:.6f} from D")
    g = w["gamma_D"]
    for s in (0.01, DELTA, 0.2):
        tip = hull_disc(np.array([[R0 + s, 0.0]]))[0]
        if abs(tip - math.pi / 4 - g(s)) > 1e-12:
            out.append(f"s={s:.4f}: one tip costs {tip - math.pi / 4:.9f}, gamma says {g(s):.9f}")
        for _ in range(100):
            k = int(rng.integers(1, 6))
            ang = rng.uniform(0, 2 * np.pi, k)
            r = rng.uniform(R0, R0 + 2 * s, k)
            r[0] = R0 + s + rng.uniform(0, s)
            a = hull_disc(r[:, None] * np.stack([np.cos(ang), np.sin(ang)], axis=1))[0]
            if a - math.pi / 4 < g(s) - 1e-12:
                out.append(f"s={s:.4f}: a cover {s:.4f} away gains only {a - math.pi / 4:.9f} < gamma")
                break
    gain = PAL - math.pi / 4
    if gain < g(DELTA) - 1e-15:
        out.append("the seed exchange gains less than gamma")
    w["w3"] = {"attained_distance": attained, "least_random_distance": least, "gamma_at_delta": g(DELTA),
               "actual_gain": gain}
    return out


def w4_gauge(w):
    out, rng = [], np.random.default_rng(6)
    changed = 0.0
    for _ in range(20):
        p3, p5 = rng.uniform(0, 2 * np.pi, 2)
        t3, t5 = rng.uniform(-0.1, 0.1, 2), rng.uniform(-0.1, 0.1, 2)
        a = rng.uniform(0, 2 * np.pi)
        area = lambda q3, s3, q5, s5: hull_pieces(
            placed_disc() + placed_reuleaux(3, q3, s3) + placed_reuleaux(5, q5, s5))[0]
        base = area(p3, t3, p5, t5)
        turned = area(p3 + a, rot(a) @ t3, p5 + a, rot(a) @ t5)
        if abs(turned - base) > 1e-12:
            out.append(f"a common rotation changes the hull area by {turned - base:.2e}")
        changed = max(changed, abs(area(p3 + 0.3, t3, p5, t5) - base))
    if changed < 1e-6:
        out.append("turning one body alone never changes the area - the gauge would be larger")
    for m in range(2, 8):
        if w["dim"](m) != 3 * (m - 1) - 1:
            out.append(f"m={m}: dimension {w['dim'](m)} is not 3(m-1)-1")
    if w["dim"](3) != 5 or "five-dimensional" not in w["snapshot"]["abstracts"]["3"]["abstract"]:
        out.append("m = 3 does not give Mishra's five-dimensional space")
    w["w4"] = {"largest_single_body_turn_change": changed}
    return out


def w5_level_three(w):
    out, s = [], level3_search()
    facts = w["snapshot"]["mishra_fulltext"]["facts"]
    # Mishra's two published placements, rebuilt exactly: each must sit under the bound he states
    at = {"reuleaux": family_area("reuleaux", numbers(facts["reuleaux_arrangement"]), 16384),
          "polygon": family_area("polygon", numbers(facts["polygon_arrangement"]), 16384)}
    for kind, key in (("reuleaux", "reuleaux_bound"), ("polygon", "polygon_bound")):
        stated = numbers(facts[key])[-1]
        if not at[kind] <= stated:
            out.append(f"{kind}: Mishra's placement gives {at[kind]:.10f} > his stated {stated}")
    for kind, r in s.items():
        if abs(r["area"] - r["sampled_hull"]) > 1e-8:
            out.append(f"{kind}: exact hull {r['area']!r} vs sampled {r['sampled_hull']!r}")
    best = {kind: min(s[kind]["area"], at[kind]) for kind in s}
    # a placement is an upper bound on Lambda of its family: one below a claimed lower bound refutes it
    if best["reuleaux"] < w["mishra_lower"]:
        out.append(f"a placement of D, B3, B5 has hull area {best['reuleaux']:.9f} < {w['mishra_lower']}")
    if best["polygon"] < w["classical_lower"]:
        out.append(f"a placement of D, P3, P5 has hull area {best['polygon']:.9f} < {w['classical_lower']}")
    # dominance is strict at the third rung: the polygons' hull goes below Mishra's bound
    if not best["polygon"] < w["mishra_lower"]:
        out.append("no placement of the polygons goes below 0.8344 - dominance gap not shown")
    w["w5"] = {"mishra_placement_areas": at, "search": s,
               "dominance_gap_at_least": w["mishra_lower"] - best["polygon"],
               "lambda_F3_bracket": [w["mishra_lower"], best["reuleaux"]]}
    return out


def w6_dominance(w):
    out = []
    th = 2 * np.pi * np.arange(20000) / 20000
    for n, (hp, hb) in w["dominance"].items():
        gap = float(np.max(hp(th) - hb(th)))
        if gap > 1e-12:
            out.append(f"n={n}: the polygon pokes out of the Reuleaux polygon by {gap:.2e}")
    return out


def d1_lipschitz(w):
    """the grid LP margin is 1-Lipschitz in sup norm in both the cover's and the target's
    support (min over placements of a max of 1-Lipschitz functions), and so is its limit"""
    out, rng = [], np.random.default_rng(13)
    L = w["lipschitz"]
    for _ in range(8):
        coeffs = {n: tuple(rng.uniform(-1, 1) * a for _ in (0, 1)) for n, a in ((3, 0.2), (5, 0.08))}
        hK = body(coeffs)
        hU = chiral_cover(0.56, 0.015, rng.uniform(0, 6), 0.008, rng.uniform(0, 6))
        # eps <= 0.025 keeps both wobbled bodies legal: r_K >= 0.22 loses at most 8 eps
        eps, b = float(rng.uniform(0.01, 0.025)), float(rng.uniform(0, 6))
        for name, hU2, hK2 in (("cover grown", lambda t: hU(t) + eps, hK),
                               ("cover wobbled", lambda t: hU(t) + eps * np.cos(2 * t + b), hK),
                               ("target wobbled", hU, lambda t: hK(t) + eps * np.cos(3 * t + b))):
            m1 = G(hK, hU, 128, 24, proper_law)[0]
            m2 = G(hK2, hU2, 128, 24, proper_law)[0]
            if abs(m1 - m2) > L * eps + 1e-12:
                out.append(f"{name}: margin moved {abs(m1 - m2):.5f} > {L} x {eps:.5f}")
                break
    return out


def p1_sanity(w):
    out, v = [], w["validation"]["sanity_check"]
    mine = {"lambda1_disk": math.pi / 4, "pal_disk_triangle": PAL, "mishra_three_reuleaux_certified_lower": 0.8344,
            "public_upper": 0.8440935944, "public_gap": 0.8440935944 - 0.8344,
            "disk_to_reuleaux_triangle_margin": DELTA, "m3_dimension": w["dim"](3)}
    for k, val in mine.items():
        if abs(v[k] - val) > 1e-15:
            out.append(f"{k}: recorded {v[k]!r}, rebuilt {val!r}")
    if v["strict_seed_ladder"] != (math.pi / 4 < PAL < 0.8344):
        out.append("strict_seed_ladder differs")
    for row in v["dimension_table"]:
        if row["continuous_dimension_before_individual_symmetry_quotient"] != w["dim"](row["m_total_witnesses"]):
            out.append(f"dimension table m={row['m_total_witnesses']} differs")
    b = v["toy_exchange_budget"]
    if abs(b["delta"] - DELTA) > 1e-15:
        out.append("toy budget delta differs")
    robust = b["delta"] - b["target_error_epsilon"] - b["minimizer_cell_radius_tau"] - b["placement_certificate_error_zeta"]
    if abs(robust - b["robust_margin_after_errors"]) > 1e-15 or b["positive_after_errors"] != (robust > 0):
        out.append("toy budget arithmetic differs")
    w["p1"] = {"toy_errors_over_delta": b["target_error_epsilon"] / b["delta"]}
    return out


def p2_package(w):
    out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]}
    for rec, leaf, text in ((w["validation"]["round06"], 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 06)

LABEL = "a sec. 28 witness-ancestry label, defined there; not a judgment"
R06_DEFINITIONS = {
    "REUSED": ("in-line", "sec. 28 label: the witness is already in the family"),
    "DOMINANCE-UPGRADE": ("in-line", "sec. 27-28: the new witness contains a congruent copy of an old one (K below L), "
                                     "so Lambda cannot fall; a label, and sec. 27's name for Mishra's step"),
    "NEW-SEPARATOR": ("in-line", "sec. 28 label: certified to exclude current minimizer cells, not by dominance"),
    "BATCH-ONLY": ("in-line", "sec. 28 label: excludes the minimizer set only together with the rest of its batch"),
    "REDUNDANT": ("in-line", "sec. 28 label: removable from a batch with S_F(B) still positive"),
    "SEARCH-PRIOR": ("in-line", "sec. 35: a numerical search value, usable to seed and initialise, barred from the "
                                "lower-bound ledger until an exhaustive lower certificate exists"),
    "EXTERNAL RESULT IDENTIFIED": ("contextual", "sec. 40: an outside theorem located and its statement recorded; "
                                                 "neither reproduced nor ingested"),
    "PROVED / MATCHES EXTERNAL CERTIFIED SETUP": ("contextual", "sec. 40: proved here, and equal to the setting of an "
                                                                "external certificate (Mishra's five parameters)"),
}
PBCT = "PASS by cited theorem"
R06_REVIEWS = [
    ("PROVED", "Compact placement domain", "analytic", "PASS", "sec. 5: t_i lies in the hull, the hull in B_R (Round 04)"),
    ("PROVED", "Minimizer-set compactness", "analytic", "PASS", "sec. 7-8: hull and area continuous on a compact domain"),
    ("PROVED", "Uniform positive violation if non-saturated", "analytic", "PASS",
     "sec. 9-11: W continuous (1-Lipschitz, Round 04), positive off universality (Round 03 attainment)"),
    ("PROVED", "Finite target-dictionary separation", "analytic", "PASS", "Thm 14.1: Round 02's net and the target Lipschitz bound"),
    ("PROVED", "Robust separation margin", "analytic", "PASS",
     "sec. 17-20; on the seed family the distance bound is attained and gamma is exact (W3)"),
    ("PROVED", "Strict witness-exchange improvement", "analytic", "PASS", "Thm 18.1"),
    ("PROVED", "Eventual finite exchange discovery if non-saturated", "analytic", "PASS",
     "Thm 24.1; assumes certified minimizer-cell covers with radii tending to 0, which it does not construct"),
    ("PROVED", "Witness dominance", "analytic", "PASS", "Thm 26.1; P_n inside B_n (W6)"),
    ("PROVED / MATCHES EXTERNAL CERTIFIED SETUP", "$m=3$ five-dimensional gauge count", "analytic", "PASS",
     "sec. 6 (W4) and Mishra's abstract"),
    ("PASS", "S1：Continuous dimension", "computation", "PASS", "arithmetic (W4, P1)"),
    ("PASS", "S2：disk-to-Reuleaux-triangle violation", "computation", "PASS",
     "1/sqrt(3) - 1/2, also from Round 03's certificate LP (W2)"),
    ("PASS", "S3：seed ladder", "computation", PBCT,
     "pi/4 and Pal's value rebuilt (W1); the 0.8344 rung is Mishra's certificate"),
    ("CLOSED", "FINITE WITNESS EXCHANGE COMPILER", "reading", "PASS",
     "closed as a proof schema (Thm 18.1, 24.1); nothing is compiled or run"),
    ("COMPUTE-DEFERRED", "NEXT WITNESS NUMERIC IDENTITY", "n/a", "n/a", ""),
    ("COMPUTE-DEFERRED", "", "n/a", "n/a", LABEL),
    ("COMPUTE-DEFERRED", "C06-6：New family lower certificate", "n/a", "n/a", ""),
    ("COMPUTE-DEFERRED", "New witness identity", "n/a", "n/a", ""),
    ("NONE", "New numerical lower bound", "reading", "PASS", "none claimed (sec. 42)"),
    ("SEARCH-ONLY", "", "n/a", "n/a", LABEL),
    ("SEARCH-PRIOR", "35. External search prior from larger Reuleaux families", "outside-corpus", "PASS",
     "Gibbs' 2014 values are upper bounds for the family minimum, as Mishra's full text says (X1)"),
    ("DOMINANCE-UPGRADE", "", "n/a", "n/a", LABEL),
    ("BATCH-ONLY", "", "n/a", "n/a", LABEL),
    ("EXTERNAL RESULT IDENTIFIED", "Mishra seed ingestion", "outside-corpus", "PASS",
     "abstract and full text checked (X1); the certificate itself not re-run"),
    ("FALSE-POSITIVE", "", "n/a", "n/a", LABEL),
    ("NEW-SEPARATOR", "", "n/a", "n/a", LABEL),
    ("REDUNDANT", "", "n/a", "n/a", LABEL),
    ("REUSED", "", "n/a", "n/a", LABEL),
]


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


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

CHECKS = {"A0": gate.anchors_check(ANCHORS), "A1": a1_citations, "X1": x1_external, "W1": w1_seed_ladder,
          "W2": w2_margin, "W3": w3_exchange, "W4": w4_gauge, "W5": w5_level_three, "W6": w6_dominance,
          "D1": d1_lipschitz, "P1": p1_sanity, "P2": p2_package, "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "A1": {"text", "snapshot", "pinned_citations"},
           "X1": {"snapshot", "mishra_claims", "pal_claim"}, "W1": {"pal_value", "mishra_lower"},
           "W2": {"delta"}, "W3": {"gamma_D"}, "W4": {"dim", "snapshot"},
           "W5": {"mishra_lower", "classical_lower", "snapshot"}, "W6": {"dominance"}, "D1": {"lipschitz"},
           "P1": {"validation", "dim"}, "P2": {"validation", "text", "crystal", "manifest"},
           "R1": {"registry", "definitions", "reviews"}}


def polygon_support(n):
    V = reuleaux_vertices(n)
    return lambda t: np.max(V @ np.stack([np.cos(t), np.sin(t)]), axis=0)


CLAIMS = {
    "pal_value": PAL,                                 # sec. 2 displays pi/8 + sqrt(3)/4
    "delta": DELTA,                                   # sec. 29: 1/sqrt(3) - 1/2
    "gamma_D": lambda s: phi_text(R0, R0 + s) - math.pi / 4,
    "dim": lambda m: 3 * m - 4,
    "mishra_lower": 0.8344,
    "classical_lower": 0.833,                          # certified for D, P3, P5 in Xie's v4, as Mishra's abstract records
    "dominance": {n: (polygon_support(n), reuleaux_support(n)) for n in (3, 5, 7, 9)},
    "lipschitz": 1.0,
    "mishra_claims": {"test_sets": ("disc", "Reuleaux triangle", "Reuleaux pentagon"), "bound": "0.8344",
                      "nodes": "486,799,600", "dimension": "five-dimensional", "eta": "1.72e-9"},
    "pal_claim": ("disc", "equilateral triangle"),
    "pinned_citations": PINNED_CITATIONS,
}


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = {DOC, CRYSTAL, VALIDATION}
    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(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"]) if r["kind"] == "arxiv" else gate.fetch_crossref(doi=r["doi"]))
                for n, r in REFS.items()}
        snap = {"retrieved": datetime.date.today().isoformat(), "records": recs,
                "abstracts": {"3": gate.fetch_arxiv_abstract(REFS[3]["id"])},
                "title_history": {"5": gate.fetch_arxiv_titles(REFS[5]["id"])}}
        snap["mishra_fulltext"] = gate.fetch_arxiv_facts(REFS[3]["id"], snap["abstracts"]["3"]["version"], MISHRA_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, manifest = load_inputs()

    def build():
        return {"text": text, "crystal": crystal, "validation": json.loads(json.dumps(validation)),
                "manifest": manifest, "snapshot": json.loads(json.dumps(snapshot)), "registry": registry.load(),
                "definitions": dict(R06_DEFINITIONS), "reviews": list(R06_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 ("a1", "w1", "w2", "w3", "w4", "w5", "p1"):
        print(key, w.get(key))
    if not args.drill:
        return
    val = validation["sanity_check"]
    mc = CLAIMS["mishra_claims"]
    shrunk5 = lambda t: 0.99 * reuleaux_support(5)(t)
    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-gamma-rewritten", "control",
         {"gamma_D": lambda s: R0 * math.sqrt((R0 + s) ** 2 - R0 ** 2) - R0 ** 2 * math.atan(math.sqrt((R0 + s) ** 2 - R0 ** 2) / R0)},
         set()),
        ("K2-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()),
        ("K3-dim-rewritten", "control", {"dim": lambda m: 3 * (m - 1) - 1}, set()),
        ("M1-doc-margin-edited", "mutation", {"text": text.replace("0.0773502692", "0.0773502693")}, {"A0"}),
        ("M2-ref-year", "mutation", {"snapshot": {**snapshot, "records": {
            **snapshot["records"], "2": {**snapshot["records"]["2"], "years": [2019]}}}}, {"A1"}),
        ("M3-xie-pin-dropped", "mutation", {"pinned_citations": ()}, {"A1"}),
        ("M4-mishra-eta", "mutation", {"mishra_claims": {**mc, "eta": "1.27e-9"}}, {"X1"}),
        ("M5-pal-pair-misnamed", "mutation", {"pal_claim": ("disc", "square")}, {"X1"}),
        ("M6-pal-value", "mutation", {"pal_value": math.pi / 8 + math.sqrt(3) / 2}, {"W1"}),
        ("M7-margin", "mutation", {"delta": 1 / math.sqrt(3) - 1 / 3}, {"W2"}),
        ("M8-gamma-too-small", "mutation", {"gamma_D": lambda s: phi_text(R0, R0 + s / 2) - math.pi / 4}, {"W3"}),
        ("M9-gamma-too-large", "mutation", {"gamma_D": lambda s: phi_text(R0, R0 + 2 * s) - math.pi / 4}, {"W3"}),
        ("M10-dimension", "mutation", {"dim": lambda m: 3 * m - 3}, {"W4", "P1"}),
        ("M11-mishra-lower-too-high", "mutation", {"mishra_lower": 0.8350}, {"W5"}),
        ("M12-classical-lower-too-high", "mutation", {"classical_lower": 0.8340}, {"W5"}),
        ("M13-pentagon-shrunk", "mutation", {"dominance": {**CLAIMS["dominance"], 5: (polygon_support(5), shrunk5)}},
         {"W6"}),
        ("M14-lipschitz-half", "mutation", {"lipschitz": 0.5}, {"D1"}),
        ("M15-recorded-budget", "mutation", {"validation": {**validation, "sanity_check": {
            **val, "toy_exchange_budget": {**val["toy_exchange_budget"], "robust_margin_after_errors": 0.05}}}}, {"P1"}),
        ("M16-package-sha", "mutation",
         {"validation": {**validation, "round06": {**validation["round06"], "sha256": "0" * 64}}}, {"P2"}),
        ("M17-review-dropped", "mutation", {"reviews": list(R06_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-009", "subject": "Round 06: the finite witness exchange compiler", "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 ("a1", "w1", "w2", "w3", "w4", "w5", "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("R06", "RUN-009", R06_DEFINITIONS, R06_REVIEWS)
        print(f"registry: {len(R06_DEFINITIONS)} definitions, {len(R06_REVIEWS)} reviews recorded for R06")


if __name__ == "__main__":
    main()