"""RUN-058 - LESR Paper 08: positive-rotation certificate reduction.

LESR Paper 08 (2026-09-20) reduces the root-6217 barrier's positive-rotation gate, m(rho) >= m(0) on [0, pi/120],
to two certificates: LOCAL-QUADRATIC, m(rho) >= m(0) + 0.1 rho^2 on [0, 0.003], and AREF-TAIL, m(rho) >= 0.8349865
on [0.003, pi/120]; their composition is arithmetic. It calls rho = 0 a topology wall, claims first-order rotation
criticality "derived from Paper 07's pressure/KKT structure", reads a local quadratic ratio 0.224-0.246 off the
first eight profile samples, and rebuilds the barrier-shape ledger from Cycle 11's 200 subroots of root 6217: five are
pruned by the tight reference, 195 stay active, split at rho = 0.003 into 10 local-only, 141 tail-only and 44
crossing roots. It ships the 195-root ledger, a diagnostic, a certificate schema, a verifier, a state record and
VALIDATION. It is evidence, not a canonical document. Here the arithmetic is recomputed, the diagnostic against the
profile and a re-minimization, the first-order claim against the affine model and the true hull, and the ledger
against the subroots and against the part of root 6217 that Cycle 11 closed.

Checks
  A0 anchors      the statements below occur in the document as written
  W1 arithmetic   sec. 7-8, 11, 20: A_ref - m(0), the crossing radius, the overlap margin, from RUN-057's 65-digit m(0)
  W2 profile      sec. 5-6: the first eight samples' ratios from Cycle 12's profile; samples 1 and 2 re-minimized; the
                  whole profile's ratios (RUN-048)
  W3 criticality  sec. 3: the first-order value with rho-dot = 1 in the finite active-contact (affine) model, and the
                  true hull's one-sided rate along the profile's own compensations
  W4 ledger       sec. 12-16: the 200 subroots, the five prunes, the 10 / 141 / 44 split; the rest of root 6217's box -
                  what is NOT-F3 and what Cycle 11 closed for A3+ only
  W5 records      the ledger file, the diagnostic, the schema and the state against the text
  W6 verifier     the verifier, read after this rebuild and never run
  P1 package      the VALIDATION record against the bytes and the archive

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

import mpmath as mp
import numpy as np
from scipy.optimize import linprog

import gate
import run046_uesfcm_cycles_07_09 as r46
import run048_uesfcm_cycles_12_14 as r48
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run053_lesr_paper03 import first_order_parts, structure, velocities

FOLDER = "main.zip!/LESR_Skew_Field_Variational/"
PKG = FOLDER + "LESR_Paper08_Package_v0.1.zip!/"
DOC = PKG + "LESR_Paper08_Positive_Rotation_Certificate_Reduction_v0.1.md"
LEDGER = PKG + "LESR_Paper08_Barrier_Shape_Ledger_200_to_195_v0.1.json"
DIAG = PKG + "LESR_Paper08_Positive_Rotation_Diagnostic_v0.1.json"
SCHEMA = PKG + "LESR_Paper08_Positive_Rotation_Certificate_Schema_v0.1.json"
VERIFIER = PKG + "LESR_Paper08_Verify_Target_Specific_Ledger.py"
STATE = PKG + "LESR_State_Paper08_v0.1.json"
VALIDATION = PKG + "LESR_Paper08_VALIDATION.json"
PAPER09A = FOLDER + "LESR_Paper09A_v0.2_Package.zip!/LESR_Paper09A_Multiscale_Topology_Wall_and_Blowup_Critical_Cone_v0.2.md"
LOG = TREE / "data" / "gate-logs" / "run058-lesr-paper08.json"
LOG48 = TREE / "data" / "gate-logs" / "run048-uesfcm-cycles-12-14.json"
LOG57 = TREE / "data" / "gate-logs" / "run057-lesr-paper07.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CACHE = TREE / "data" / "cache" / "run058-searches.json"     # data/cache is not committed
M0 = "0.83498611055922409985066235655770059210182728925748306508259408038"      # RUN-057, from the contact equations
AREF = "0.8349865"
X30, S = -0.01215883209899, 0.00882
VB = [X30 - S, 0.0, 0.0, 0.019770946347947549, 0.0]
AREF5 = [28, 36, 68, 144, 155]


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = (DOC, LEDGER, DIAG, SCHEMA, VERIFIER, STATE, VALIDATION)
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want + (PAPER09A,)) if d is not None}
    rows = {row[0]: row for row in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"]}
    c12 = r48.load_inputs()
    return {"text": got[DOC].decode("utf-8"), "ledger": json.loads(got[LEDGER]), "diag": json.loads(got[DIAG]), "schema": json.loads(got[SCHEMA]),
            "verifier": got[VERIFIER].decode("utf-8"), "state": json.loads(got[STATE]), "validation": json.loads(got[VALIDATION]),
            "bytes": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want}, "paper09a": got[PAPER09A].decode("utf-8"),
            "profile": c12["profile"], "root": c12["root"], "subroots": c12["subroots"],
            "log48": json.loads(LOG48.read_text(encoding="utf-8")), "log57": json.loads(LOG57.read_text(encoding="utf-8"))}


# ---------------------------------------------------------------- the arithmetic

def arithmetic():
    """sec. 7-8 with m(0) to 65 digits: A_ref - m(0); the radius where m(0) + 0.1 rho^2 reaches A_ref; the margin
    m(0) + 0.1 (0.003)^2 - A_ref"""
    mp.mp.dps = 70
    m0, aref = mp.mpf(M0), mp.mpf(AREF)
    gap = aref - m0
    s = lambda x: mp.nstr(x, 40, strip_zeros=False)
    return {"gap": s(gap), "rho_cross": s(mp.sqrt(gap / mp.mpf("0.1"))), "margin": s(m0 + mp.mpf("0.1") * mp.mpf("0.003") ** 2 - aref)}


# ---------------------------------------------------------------- the profile, re-minimized

def profile_recheck(profile, root):
    """samples 1 and 2 (the smallest positive rho) re-minimized on the circle d3 = s in the root's box, as RUN-048 did"""
    tasks = [(profile["samples"][k], root) for k in (1, 2)]
    with Pool(2) as pool:
        out = pool.map(r48.profile_one, tasks, chunksize=1)
    return [{"rho": t[0]["rho"], "stored": t[0]["area_min_search"], "circle": o["circle"], "point": o["circle_point"]} for t, o in zip(tasks, out)]


# ---------------------------------------------------------------- first-order criticality

def criticality(recheck):
    """sec. 3. The finite active-contact model at the barrier with rho-dot = 1: B5 turns at unit rate, B3 may move into
    the far branch (x3-velocity <= 0 at the circle's leftmost point) or along it, B5 translates; the least affine
    first-order change (RUN-053's LP). And the true hull's one-sided rate (A(v + t d) - A(v)) / t, t = 1e-6, along the
    compensation the re-minimized samples 1 and 2 use, d = (point - barrier) / rho"""
    st = structure(VB)
    n = len(st["atoms"])
    unit = [first_order_parts(st, VB, e)[0] for e in np.eye(5)]
    cobj = np.concatenate([unit, [m for _, m, _, _, _ in st["atoms"]]])
    rows = []
    for i, (x, m, _, _, act) in enumerate(st["atoms"]):
        for j in act:
            r = np.zeros(5 + n)
            r[:5] = [float(velocities(st["C"], VB, e)[j] @ np.array([math.cos(x), math.sin(x)])) for e in np.eye(5)]
            r[5 + i] = -1.0
            rows.append(r)
    res = linprog(cobj, A_ub=np.array(rows), b_ub=np.zeros(len(rows)), bounds=[(-10, 0), (-10, 10), (1, 1), (-10, 10), (-10, 10)] + [(None, None)] * n,
                  method="highs")
    A0 = r46.area(VB)
    rates = []
    for smp in recheck:
        p, rho = smp["point"], smp["rho"]
        d = [(p[0] - VB[0]) / rho, p[1] / rho, 1.0, (p[3] - VB[3]) / rho, p[4] / rho]
        rates.append([rho, (r46.area([VB[i] + 1e-6 * d[i] for i in range(5)]) - A0) / 1e-6, d])
    return {"affine": float(res.fun), "affine_xi": [float(x) for x in res.x[:5]], "rates": rates, "pure_turn": (r46.area([VB[0], 0.0, 1e-6, VB[3], 0.0]) - A0) / 1e-6}


# ---------------------------------------------------------------- the ledger's domain

def box_shares(root, subroots, n=400000, seed=58):
    """root 6217's box, sampled uniformly: the share inside the 200 subroots; outside them, the share with d3 < s
    (NOT-F3: never in the far branch) and with d3 >= s (in the branch, closed by Cycle 11's search for A3+ only), and
    how the latter splits at rho = 0.003"""
    C0, H0 = np.array(root[0]), np.array(root[1])
    Cs, Hs = np.array(subroots["centers"]), np.array(subroots["halfwidths"])
    rng = np.random.default_rng(seed)
    P = C0 + H0 * (2 * rng.random((n, 5)) - 1)
    inside = np.zeros(n, dtype=bool)
    for c, h in zip(Cs, Hs):
        inside |= np.all(np.abs(P - c) <= h, axis=1)
    f3 = np.hypot(P[:, 0] - X30, P[:, 1]) >= S
    out_f3 = ~inside & f3
    return {"inside": float(inside.mean()), "outside_not_f3": float((~inside & ~f3).mean()), "outside_f3": float(out_f3.mean()),
            "outside_f3_local": float((out_f3 & (P[:, 2] < 0.003)).mean()), "outside_f3_tail": float((out_f3 & (P[:, 2] >= 0.003)).mean())}


# ---------------------------------------------------------------- the cache

def _key(name, fn, extra=""):
    import run008_round05_saturation_gate as r8
    import run009_round06_witness_exchange as r9
    import run052_lesr_paper02 as r52
    import run053_lesr_paper03 as r53
    digest = hashlib.sha256(inspect.getsource(fn).encode())
    for helper in HELPERS[name]:
        digest.update(inspect.getsource(helper).encode())
    for path in (r8.__file__, r9.__file__, r52.__file__, r53.__file__):
        digest.update(open(path, "rb").read())
    digest.update(extra.encode())
    return digest.hexdigest()


HELPERS = {"arithmetic": (), "recheck": (r48.profile_one, r48.area), "criticality": (r46.area, r46.hull), "shares": ()}


def searches(inputs):
    cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {}
    out = {}
    tag = lambda *xs: hashlib.sha256(json.dumps(xs, sort_keys=True).encode()).hexdigest()
    jobs = (("arithmetic", arithmetic, lambda: arithmetic(), lambda: ""),
            ("recheck", profile_recheck, lambda: profile_recheck(inputs["profile"], inputs["root"]), lambda: tag(inputs["profile"], inputs["root"])),
            ("criticality", criticality, lambda: criticality(out["recheck"]), lambda: tag(out["recheck"])),
            ("shares", box_shares, lambda: box_shares(inputs["root"], inputs["subroots"]), lambda: tag(inputs["root"], inputs["subroots"])))
    for name, fn, call, extra in jobs:
        key = _key(name, fn, extra())
        if cached.get(name, {}).get("key") != key:
            cached[name] = {"key": key, "value": json.loads(json.dumps(call()))}
            CACHE.parent.mkdir(parents=True, exist_ok=True)
            CACHE.write_text(json.dumps(cached, indent=1) + "\n", encoding="utf-8")
        out[name] = cached[name]["value"]
    return out


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

ANCHORS = {"A0": [r"A_{\mathrm{ref}}-m(0)=3.8944077590\times10^{-7}.", r"\rho\approx0.00197342538724.", r"m(\rho_c)-A_{\mathrm{ref}}\ge5.1055922410\times10^{-7}.",
                  r"0.22406", r"0.24570.", r"m(\rho)\gem(0)+0.1\rho^2", r"\inf\{\deltaA[d]:d\in\mathcalK_{\mathrm{feas}},\\dot\rho=1\}=0.",
                  "`FIRST-ORDERCRITICALITY—DERIVEDFROMPAPER07PRESSURE/KKTSTRUCTURE`", r"200\to195.", r"10+141+44=195.", "`PROVED—ARITHMETICREDUCTION`"]}
CLAIMS = {
    "arithmetic_claim": {"text": [True, True, True], "diagnostic": [True, True, True], "replay": [True, True, True], "composition": True, "kappa": True},
    "profile_claim": {"first8": [0.22406, 0.24571], "listed": [False, True], "m0_search_excess": 7.3e-11, "recheck": [[0.2254, 1.5e-09], [0.2253, 8.3e-08]],
                      "whole_profile": [0.1738, 0.2254], "all_positive": True},
    "criticality_claim": {"affine": 0.0293, "affine_turn_centre": [0.0, -0.0, 1.0, -0.0221, -0.1625], "pure_turn": 0.0474,
                          "rates": [[0.001007, 5.3e-05], [0.002014, 0.00011]], "proportional": True, "p07_subgradient": True},
    "ledger_claim": {"subroots": 200, "counts": {"LOCAL_ONLY": 10, "TAIL_ONLY": 141, "SPLIT_AT_RHO_CUT": 44}, "file_counts": [195, 10, 141, 44], "listed": 200,
                     "file_classes": True, "file_boxes": True, "pruned": [True, ["SHAPE_PRUNED_BY_AREF"] * 5],
                     "shares": {"inside": 0.559, "outside_not_f3": 0.295, "outside_f3": 0.146, "outside_f3_local": 0.033, "outside_f3_tail": 0.113}},
    "records_claim": {"first_order": ["critical by Paper07 contact-pressure/KKT architecture; interval dual audit still required", "CRITICAL_GIVEN_P07_PRESSURE_KKT"],
                      "gates": {"LOCAL_QUADRATIC": "OPEN", "AREF_TAIL": "OPEN"}, "schema_domains": [True, True],
                      "responsibility": {"tail_only_roots": 141, "split_roots_tail_portions": 44, "already_Aref_pruned_roots": 5},
                      "diag_status": "NUMERICAL_DIAGNOSTIC_NOT_PROOF", "next": [True, False]},
    "verifier_facts": {"lines": 86, "defs": ["rebuild", "arithmetic_gate"], "prunes_constant": True, "only_subroots": True, "cut_tolerance": True},
    "package_claim": {"digests": [True] * 6, "utf8": True, "delimiters": ["PASS", []], "manifest": True},
}


def sig(x, n=2):
    return float(f"{x:.{n - 1}e}")


def w1_arithmetic(w):
    s, d = w["search"]["arithmetic"], w["diag"]
    mp.mp.dps = 50
    near = lambda a, b, tol: bool(abs(mp.mpf(a) - mp.mpf(b)) <= mp.mpf(tol))
    replay = json.loads(w["validation"]["fresh_replay_stdout"].split("arithmetic: ")[1])
    # the diagnostic and the replay are doubles: a difference of two numbers near 0.835 carries ~5e-17 of rounding, a
    # relative 1.3e-10 of the gap, so the crossing radius moves by ~1.3e-13
    got = {"text": [near(s["gap"], "3.8944077590e-7", "5e-18"), near(s["rho_cross"], "0.00197342538724", "5e-15"), near(s["margin"], "5.1055922410e-7", "5e-18")],
           "diagnostic": [near(s["gap"], d["A_ref_minus_m0"], "2e-16"), near(s["rho_cross"], d["rho_where_c_rho2_reaches_Aref"], "5e-13"),
                          near(s["margin"], d["local_lower_margin_over_Aref_at_rho_cut_if_certificate_holds"], "2e-16")],
           "replay": [near(s["gap"], replay["Aref_minus_m0"], "2e-16"), near(s["rho_cross"], replay["rho_cross"], "5e-13"), near(s["margin"], replay["margin_at_cut"], "2e-16")],
           "composition": mp.mpf(AREF) > mp.mpf(M0), "kappa": 0.5 * 0.2 >= 0.1}
    w["w1"] = got
    return [] if got == w["arithmetic_claim"] else [f"the arithmetic: {got}"]


def w2_profile(w):
    """sec. 5: the first eight samples' ratios (m(rho) - m(0)) / rho^2 from Cycle 12's profile, with m(0) exact, as the
    diagnostic lists them; samples 1 and 2 re-minimized - sample 2's stored value is a search artefact; the whole
    profile's re-minimized ratios from RUN-048"""
    prof, d, rc = w["profile"]["samples"], w["diag"], w["search"]["recheck"]
    m0, m0_search = float(M0), prof[0]["area_min_search"]
    first8 = [(s["area_min_search"] - m0) / s["rho"] ** 2 for s in prof[1:9]]
    listed = [e["area_minus_m0_search"] for e in d["first_8_positive_profile_samples"]]
    circle = w["log48"]["w7"]["circle"]
    # the diagnostic's differences: against its own m0 (the exact barrier), or against the profile's rho = 0 search value?
    got = {"first8": [round(min(first8), 5), round(max(first8), 5)],
           "listed": [max(abs(a - (s["area_min_search"] - m)) for a, s in zip(listed, prof[1:9])) < 1e-15 for m in (d["m0_barrier_high_precision"], m0_search)],
           "m0_search_excess": sig(m0_search - m0, 2),
           "recheck": [[round((r["circle"] - m0) / r["rho"] ** 2, 4), sig(r["stored"] - r["circle"], 2)] for r in rc],
           "whole_profile": circle[4], "all_positive": w["log48"]["w7"]["monotone"]}
    w["w2"] = got
    return [] if got == w["profile_claim"] else [f"the profile: {got}"]


def w3_criticality(w):
    """sec. 3 says the first-order value with rho-dot = 1 is 0 in the finite active-contact model, and derives it from
    Paper 07's pressure split. In that model it is positive; Paper 07's split is not a subgradient (RUN-057); on the
    true hull the one-sided rate along the profile's compensations falls in proportion to rho"""
    s = w["search"]["criticality"]
    got = {"affine": sig(s["affine"], 3), "affine_turn_centre": [round(x, 4) for x in s["affine_xi"]], "pure_turn": sig(s["pure_turn"], 3),
           "rates": [[round(r[0], 6), sig(r[1], 2)] for r in s["rates"]], "proportional": all(abs(r[1] / r[0] - s["rates"][0][1] / s["rates"][0][0]) < 0.1 * s["rates"][0][1] / s["rates"][0][0] for r in s["rates"]),
           "p07_subgradient": w["log57"]["w3"]["margin_72"] < 0}
    w["w3"] = got
    return [] if got == w["criticality_claim"] else [f"the criticality: {got}"]


def w4_ledger(w):
    """sec. 12-16: the partition, from the subroots; the ledger file's classes; and the part of root 6217's box that
    Paper 08's own rule (closed for A3+ only -> REOPEN_FOR_SHAPE unless pruned by A_ref or impossible) would reopen"""
    sub, led, sh = w["subroots"], w["ledger"], w["search"]["shares"]
    lo = [c[2] - h[2] for c, h in zip(sub["centers"], sub["halfwidths"])]
    hi = [c[2] + h[2] for c, h in zip(sub["centers"], sub["halfwidths"])]
    cls = {i: ("LOCAL_ONLY" if hi[i] <= 0.003 else "TAIL_ONLY" if lo[i] >= 0.003 else "SPLIT_AT_RHO_CUT") for i in range(len(lo)) if i not in AREF5}
    counts = {k: list(cls.values()).count(k) for k in ("LOCAL_ONLY", "TAIL_ONLY", "SPLIT_AT_RHO_CUT")}
    rows = {r["local_index"]: r for r in led["roots"]}
    got = {"subroots": len(lo), "counts": counts, "file_counts": [led["counts"][k] for k in ("shape_active", "local_only", "tail_only", "split_at_rho_cut")],
           "listed": len(rows), "file_classes": all(i in rows and rows[i]["rho_class"] == c for i, c in cls.items()),
           "file_boxes": all(rows[i]["center"] == sub["centers"][i] and rows[i]["halfwidth"] == sub["halfwidths"][i] for i in cls),
           "pruned": [led["safe_shape_prunes"] == AREF5, sorted(rows[i]["barrier_shape_status"] for i in AREF5 if i in rows)],
           "shares": {k: round(v, 3) for k, v in sh.items()}}
    w["w4"] = got
    return [] if got == w["ledger_claim"] else [f"the ledger: {got}"]


def w5_records(w):
    sc, st, d, text = w["schema"], w["state"], w["diag"], gate.squash(w["text"])
    got = {"first_order": [sc["gate_local"]["first_order_status"], st["first_order_rotation"]], "gates": st["certificate_gates"],
           "schema_domains": [sc["gate_local"]["domain"] == [0.0, 0.003], abs(sc["gate_tail"]["domain"][1] - math.pi / 120) < 1e-15],
           "responsibility": sc["gate_tail"]["responsibility"], "diag_status": d["status"],
           "next": [st["next_cloud_node"] == "Critical-Cone Second Variation at rho=0+", "Critical-ConeSecondVariation" in gate.squash(w["paper09a"][:400])]}
    w["w5"] = got
    return [] if got == w["records_claim"] else [f"the records: {got}"]


def w6_verifier(w):
    """the verifier, read: it rebuilds the ledger from the 200 subroots only (nothing of the rest of root 6217's box),
    takes the five prunes as a constant rather than checking their certificates, and checks the arithmetic"""
    code = w["verifier"]
    got = {"lines": code.count("\n"), "defs": re.findall(r"^def (\w+)", code, re.M),
           "prunes_constant": bool(re.search(r"SAFE_AREF = \{28,36,68,144,155\}", code)),
           "only_subroots": bool(re.search(r'mask = z\["parent_root"\] == 6217', code)) and not re.search(r"not.?f3|d3|outside|root box|halfwidths\[6217\]", code, re.I),
           "cut_tolerance": bool(re.search(r"RHO_CUT \+ 1e-15", code))}
    w["w6"] = got
    return [] if got == w["verifier_facts"] else [f"the verifier: {got}"]


def p1_package(w):
    v, B = w["validation"], w["bytes"]
    sha = lambda b: hashlib.sha256(b).hexdigest()
    body = B[DOC].decode("utf-8")
    got = {"digests": [v["paper_sha256"] == sha(B[DOC]), v["manifest_sha256"] == sha(B[LEDGER]), v["diagnostic_sha256"] == sha(B[DIAG]),
                       v["schema_sha256"] == sha(B[SCHEMA]), v["verifier_sha256"] == sha(B[VERIFIER]), v["state_sha256"] == sha(B[STATE])],
           "utf8": v["utf8"] is True, "delimiters": [v["math_delimiters"], sorted(set(re.findall(r"\\\(|\\\)|\\\[|\\\]", body)))],
           "manifest": all(w["manifest_rows"][k][2] == sha(b) for k, b in B.items())}
    w["p1"] = got
    return [] if got == w["package_claim"] else [f"the package: {got}"]


def a0_anchors(w):
    text = gate.squash(w["text"])
    return [f"anchor not found: {a[:60]}" for a in ANCHORS["A0"] if a not in text]


CHECKS = {"A0": a0_anchors, "W1": w1_arithmetic, "W2": w2_profile, "W3": w3_criticality, "W4": w4_ledger, "W5": w5_records, "W6": w6_verifier, "P1": p1_package}
DEPENDS = {"A0": {"text"}, "W1": {"search", "diag", "validation", "arithmetic_claim"}, "W2": {"profile", "diag", "search", "log48", "profile_claim"},
           "W3": {"search", "log57", "criticality_claim"}, "W4": {"subroots", "ledger", "search", "ledger_claim"},
           "W5": {"schema", "state", "diag", "text", "paper09a", "records_claim"}, "W6": {"verifier", "verifier_facts"},
           "P1": {"validation", "bytes", "manifest_rows", "package_claim"}}


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

    text, s = base["text"], base["search"]
    return [
        ("K0-unmodified", "control", {}, set()),
        ("K1-crlf", "control", {"text": text.replace("\n", "\r\n"), "verifier": base["verifier"].replace("\n", "\r\n")}, set()),
        ("K2-validation-keys-sorted", "control", {"validation": json.loads(json.dumps(base["validation"], sort_keys=True))}, set()),
        ("M1-ledger-text", "mutation", {"text": text.replace("200\\to195.", "200\\to190.")}, {"A0"}),     # both boxed statements
        ("M2-gap", "mutation", {"search": edit(s, lambda x: x["arithmetic"].update(gap="3.9e-7"))}, {"W1"}),
        ("M3-diagnostic-rho", "mutation", {"diag": edit(base["diag"], lambda x: x.update(rho_where_c_rho2_reaches_Aref=0.00197))}, {"W1"}),
        ("M4-profile-sample", "mutation", {"profile": edit(base["profile"], lambda x: x["samples"][2].update(area_min_search=x["samples"][2]["area_min_search"] + 1e-7))}, {"W2"}),
        ("M5-recheck", "mutation", {"search": edit(s, lambda x: x["recheck"][1].update(circle=x["recheck"][1]["stored"]))}, {"W2"}),
        ("M6-affine-zero", "mutation", {"search": edit(s, lambda x: x["criticality"].update(affine=0.0))}, {"W3"}),
        ("M7-p07-holds", "mutation", {"log57": edit(base["log57"], lambda x: x["w3"].update(margin_72=0.001))}, {"W3"}),
        ("M8-subroot-rho", "mutation", {"subroots": edit(base["subroots"], lambda x: x["halfwidths"][0].__setitem__(2, 0.02))}, {"W4"}),
        ("M9-shares", "mutation", {"search": edit(s, lambda x: x["shares"].update(outside_f3=0.0))}, {"W4"}),
        ("M10-state-first-order", "mutation", {"state": edit(base["state"], lambda x: x.update(first_order_rotation="OPEN"))}, {"W5"}),
        ("M11-schema-domain", "mutation", {"schema": edit(base["schema"], lambda x: x["gate_local"].update(domain=[0.0, 0.004]))}, {"W5"}),
        ("M12-verifier-prunes", "mutation", {"verifier": base["verifier"].replace("SAFE_AREF = {28,36,68,144,155}", "SAFE_AREF = load_prunes()", 1)}, {"W6"}),
        ("M13-verifier-box", "mutation", {"verifier": base["verifier"] + "\ndef outside_share(root_box, d3):\n    return 0.0\n"}, {"W6"}),
        ("M14-validation-digest", "mutation", {"validation": {**base["validation"], "diagnostic_sha256": "0" * 64}}, {"P1"}),
        ("M15-ledger-bytes", "mutation", {"bytes": {**base["bytes"], LEDGER: base["bytes"][LEDGER] + b" "}}, {"P1"}),
    ]


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    inputs = load_inputs()
    base = {**inputs, "search": searches(inputs)}

    def build():
        return {**copy.deepcopy(base), **copy.deepcopy(CLAIMS)}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {}
    for c, fn in CHECKS.items():
        try:
            results[c] = fn(w)
        except KeyError as e:
            results[c] = [f"claim missing: {e}"]
    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", "p1"):
        print(key, "=", json.dumps(w.get(key), default=str, ensure_ascii=False))
    if not args.drill:
        return
    cases = drill_cases(base)
    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-058", "subject": "LESR Paper 08: positive-rotation certificate reduction", "document": DOC,
           "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "w6", "p1")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8")


if __name__ == "__main__":
    main()