"""RUN-041 - DLMVC: the deep-lag verification methodology, and its case studies of Rounds 01 and 04.

DLMVC v0.1 (dated 2026-09-19) formalizes a second verification line that deliberately lags the frontier:
lag measured in rounds, time and structure; a blindness provenance for every target; a ladder of deep passes;
closure within one resolution kept apart from saturation across resolutions. It claims 'initial successful
mathematical case studies', and its folder holds them: a lagged verification of Round 01 (a missing
joint-attainment lemma, the one-active branch removed, a Fejer compiler with an explicit error E_M), one of
Round 04 (a sharp anchored radius R_sharp; the sanity example 'independently reproduced'), and Round 00's state
crystal. Here the case studies' mathematics is recomputed and set against this tree's own reading of Rounds 01
and 04 (RUN-004, RUN-007), which was made without them; and the frontier's rounds are searched for what it took
back.

Checks
  A0 anchors      the numbers and formulas below occur in DLMVC and its case studies as written
  W1 fejer        VR01 J: the Fejer compiler's legality and E_M, exactly; its error on three families in the
                  domain; the coefficient bound 1/2 against the attainable 1/pi
  W2 corrections  VR01 D.7, D.12: JPA-01's coercivity on random placements; the one-active branch in Round 01
                  and its correction in Round 03; what the frontier took back
  W3 radius       VR04 J: the hull area Phi_r from the support function, its derivative, R_sharp, the constants
  W4 sanity       VR04 I.2: the 'independently reproduced' sanity numbers against Round 04's definition (RUN-007)
  W5 status       DLMVC sec. 26 against the case studies; the state crystal
  W6 code         the case study's script, read after the rebuild and never run
  P1 package      VR04's VALIDATION against the archive and the constants recomputed here
  R1 registry     DLMVC's judgments reviewed, first-used statuses defined

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

import mpmath as mp
import numpy as np

import gate
import registry
import run007_round04_cover_compiler as r7
from corpus import SOURCES, TREE, source_bytes, walk_sources

FOLDER = "main.zip!/DLMVC_Deep_Lag_Multi_Pass_Verification_Closure_Methodology/"
DOC = FOLDER + "DLMVC_Deep_Lag_Multi_Pass_Verification_Closure_Methodology_v0.1.md"
CRYSTAL = FOLDER + "AMRAL_LUC_FC_State_Crystal_Round_00_v0.1.md"
VR01 = FOLDER + "AMRAL_LUC_FC_Verification_Round_01_by_LaggedAI_v0.1.md"
VR04PKG = FOLDER + "AMRAL_LUC_FC_Verification_Round_04_Package_v0.1.zip!/"
VR04 = VR04PKG + "AMRAL_LUC_FC_Verification_Round_04_by_LaggedAI_v0.1.md"
VR04_PY = VR04PKG + "AMRAL_LUC_FC_Verification_Round_04_sharp_radius.py"
VR04_VAL = VR04PKG + "AMRAL_LUC_FC_Verification_Round_04_VALIDATION.json"
ROUND00 = "main.zip!/AMRAL_Lebesgue_Finite_Closure_Round_00_Methodology_v0.2.md"
LOG = TREE / "data" / "gate-logs" / "run041-dlmvc.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CORPUS = TREE / "data" / "gate-logs" / "run001-corpus-identity.json"

ABAR = "0.8440935944"
FEJER_M = (3, 5, 9, 17, 33, 65, 129)
GRID, NMAX = 4096, 6001
TAKEN_BACK = {"R01-CORRECTION-001": r"R01-CORRECTION-001", "JPA-01": r"JPA", "FLC-01": r"FLC", "AR-04": r"AR-04|R_\\sharp|0\.7212"}


# ---------------------------------------------------------------- VR01: the Fejer compiler

def e_m(M):
    """VR01 J.3's closed form"""
    K = (M - 1) // 2
    H = lambda k: sum((Fraction(1, j) for j in range(1, k + 1)), Fraction(0))
    return (H(K) + H(K + 1) - 1) / (4 * (M + 1)) + Fraction(1, 4 * (K + 1))


def e_m_summed(M, T=1000):
    """the same bound summed mode pair by mode pair (|r_n| <= 1/2): every odd n <= M at its attenuation
    n / (M + 1), the tail telescoped past T terms"""
    K = (M - 1) // 2
    low = sum((Fraction(n, (M + 1) * (n * n - 1)) for n in range(3, M + 1, 2)), Fraction(0))
    tail = sum((Fraction(1, (2 * k + 1) ** 2 - 1) for k in range(K + 1, K + T + 1)), Fraction(0)) + Fraction(1, 4 * (K + T + 1))
    return low + tail


FAMILIES = {
    # the Reuleaux triangle: r = 1 and 0 on alternate arcs of pi/3
    "reuleaux": lambda n: -3j / (math.pi * n) if n % 6 == 3 else 0,
    # VR01 K.2's r_N = (1 + sgn sin N theta) / 2 at N = 9
    "sign_9": lambda n: -1j / (math.pi * (n // 9)) if n % 9 == 0 and (n // 9) % 2 == 1 else 0,
    # the indicator of cos 3 theta > 0: in the domain, and |r_3| = 1/pi
    "extremal_3": lambda n: (-1) ** ((n // 3 - 1) // 2) / (math.pi * (n // 3)) if n % 3 == 0 and (n // 3) % 2 == 1 else 0,
}


def fejer_compute():
    """each family's Fourier coefficients (positive odd modes up to NMAX), the Fejer image P_M r on a grid (a
    finite sum, exactly), and the support error |h_r - h_{P_M r}| (the series past NMAX bounded)"""
    theta = 2 * np.pi * np.arange(GRID) / GRID
    out = {}
    for name, coef in FAMILIES.items():
        modes = np.array([n for n in range(3, NMAX + 1, 2) if coef(n) != 0])
        c = np.array([complex(coef(int(n))) for n in modes])
        B = 2 * (np.cos(np.outer(theta, modes)) * c.real - np.sin(np.outer(theta, modes)) * c.imag)
        # past 20 NMAX every family has n |c_n| <= 9 / pi, so what is left is at most (9 / pi) / (20 NMAX)^2
        tail = float(sum(2 * abs(coef(n)) / (n * n - 1) for n in range(NMAX + 2, 20 * NMAX, 2))) + 9 / (math.pi * (20 * NMAX) ** 2)
        rows = {}
        for M in FEJER_M:
            lam = np.where(modes <= M, 1 - modes / (M + 1), 0.0)
            image = 0.5 + B @ lam
            dev = B @ ((1 - lam) / (1 - modes.astype(float) ** 2))
            rows[str(M)] = {"min": float(image.min()), "max": float(image.max()), "error": float(np.abs(dev).max()), "tail": tail}
        out[name] = rows
    return out


def extremal_coefficient():
    """the third Fourier coefficient of the indicator of cos 3 theta > 0, by quadrature"""
    mp.mp.dps = 30
    re_ = mp.quad(lambda t: mp.cos(3 * t), [-mp.pi / 6, mp.pi / 6]) * 3 / (2 * mp.pi)
    return float(re_)


# ---------------------------------------------------------------- VR01: joint placement attainment

def hull(pts):
    pts = sorted(set(map(tuple, pts)))
    cross = lambda o, a, b: (a[0] - o[0]) * (b[1] - o[1]) - (a[1] - o[1]) * (b[0] - o[0])
    lo, hi = [], []
    for p in pts:
        while len(lo) >= 2 and cross(lo[-2], lo[-1], p) <= 0:
            lo.pop()
        lo.append(p)
    for p in reversed(pts):
        while len(hi) >= 2 and cross(hi[-2], hi[-1], p) <= 0:
            hi.pop()
        hi.append(p)
    return np.array(lo[:-1] + hi[:-1])


def distance(p, poly):
    """a point's distance to a convex polygon (counter-clockwise), 0 inside"""
    a, b = poly, np.roll(poly, -1, axis=0)
    e, v = b - a, p - a
    if np.all(e[:, 0] * v[:, 1] - e[:, 1] * v[:, 0] >= 0):
        return 0.0
    t = np.clip(np.sum(v * e, axis=1) / np.sum(e * e, axis=1), 0, 1)
    return float(np.min(np.hypot(*(v - t[:, None] * e).T)))


def jpa_compute(n=4000, seed=41):
    """VR01 D.7: J(Q, t) = d_+(QK + t, U) >= max(0, |t| - R_K - R_U), on random convex K, U, orthogonal Q
    (rotations and reflections) and translations out to 6"""
    rng = np.random.default_rng(seed)
    worst, far, bad = math.inf, 0, 0
    for _ in range(n):
        K = hull(rng.uniform(-1, 1, (9, 2)))
        U = hull(rng.uniform(-1.3, 1.3, (12, 2)))
        a = rng.uniform(0, 2 * math.pi)
        Q = np.array([[math.cos(a), -math.sin(a)], [math.sin(a), math.cos(a)]]) @ (np.diag([1, -1]) if rng.random() < 0.5 else np.eye(2))
        t = rng.normal(size=2)
        t *= rng.uniform(0, 6) / np.linalg.norm(t)
        J = max(distance(v, U) for v in K @ Q.T + t)
        low = np.linalg.norm(t) - np.max(np.hypot(*K.T)) - np.max(np.hypot(*U.T))
        bad += J < max(0.0, low) - 1e-12
        if low > 0:
            far += 1
            worst = min(worst, J - low)
    return {"samples": n, "violations": int(bad), "beyond_the_radii": far, "least_slack": float(worst)}


# ---------------------------------------------------------------- VR04: the sharp anchored radius

def radius_compute():
    """Phi_r in closed form against the hull's area from its support function max(r, d cos t) and from a polygon
    of 2^20 sides; its derivative; R_sharp; the compiler constants at M = 128, q = 5e-4 for both radii"""
    mp.mp.dps = 40
    A, r = mp.mpf(ABAR), mp.mpf(1) / 2
    phi = lambda d: mp.pi * r ** 2 + r * mp.sqrt(d * d - r * r) - r * r * mp.acos(r / d)
    rs = mp.findroot(lambda d: phi(d) - A, mp.mpf("0.72"))
    t0 = mp.acos(r / rs)
    by_support = (mp.quad(lambda t: (rs * mp.cos(t)) ** 2 - (rs * mp.sin(t)) ** 2, [-t0, t0]) + r * r * (2 * mp.pi - 2 * t0)) / 2
    n = 1 << 20
    ang = np.linspace(float(t0), 2 * math.pi - float(t0), n)
    poly = np.vstack([[float(rs), 0.0], 0.5 * np.column_stack([np.cos(ang), np.sin(ang)])])
    by_polygon = 0.5 * abs(np.dot(poly[:, 0], np.roll(poly[:, 1], -1)) - np.dot(poly[:, 1], np.roll(poly[:, 0], -1)))
    slope = [float(mp.diff(phi, d) - r * mp.sqrt(d * d - r * r) / d) for d in (mp.mpf("0.6"), rs, mp.mpf("1.2"))]
    M, q = 128, mp.mpf("0.0005")
    D = mp.pi / M
    consts = {}
    for name, R in (("original", 2 * A), ("sharp", rs)):
        RP = (R + q) / mp.cos(D)
        eps = q + (R + RP) * 2 * mp.sin(D / 2)
        beta = 2 * mp.pi * R * eps + mp.pi * eps ** 2
        K = int(mp.ceil((R - r) / q)) + 1
        consts[name] = {"R": float(R), "R_P": float(RP), "epsilon": float(eps), "beta": float(beta), "K_q": K, "levels": K + 1}
    return {"R_sharp": mp.nstr(rs, 20), "phi_at_R_sharp": mp.nstr(phi(rs), 20), "by_support": mp.nstr(by_support, 20),
            "by_polygon": float(by_polygon), "slope_residuals": slope, "constants": consts,
            "log10_ratio": float(M * mp.log10(mp.mpf(consts["sharp"]["levels"]) / consts["original"]["levels"]))}


# ---------------------------------------------------------------- VR04: the sanity example

QUOTED = {"area_U": r"\operatorname{Area}(U)\approx", "area_P": r"\operatorname{Area}(P)\approx", "excess": r"d_H^{\mathrm{numeric}}\approx"}


def quoted(text):
    """VR04 I.2's numbers as the text gives them"""
    sq, out = gate.squash(text), {}
    for key, prefix in QUOTED.items():
        i = sq.find(prefix)
        m = re.match(r"([0-9.]*[0-9])(?:\\times10\^\{(-?[0-9]+)\})?", sq[i + len(prefix):]) if i >= 0 else None
        out[key] = None if not m else float(m.group(1)) * (10.0 ** int(m.group(2)) if m.group(2) else 1.0)
    return out


def sanity_compute():
    """RUN-007's reading of Round 04 sec. 33: the outer polygon of h = 0.515 + 0.01 cos 2t at M = 128, q = 5e-4,
    built from the definition"""
    h, area_u = r7.test_covers()["sec33"]
    P, _, _ = r7.outer_polygon(h, 128, 5e-4, r7.up)
    return {"area_U": area_u, "area_P": r7.shoelace(P), "excess": r7.excess(P, h)}


# ---------------------------------------------------------------- inputs

def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    rounds = [r["archived"][0] for r in json.loads(CORPUS.read_text(encoding="utf-8"))["correspondence"][:38]]
    want = {DOC, CRYSTAL, VR01, VR04, VR04_PY, VR04_VAL, ROUND00, r7.VALIDATION} | set(rounds)
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want or l.id.startswith(FOLDER)) if d is not None}
    manifest = json.loads(MANIFEST.read_text(encoding="utf-8"))
    return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "vr01": got[VR01].decode("utf-8"), "vr04": got[VR04].decode("utf-8"),
            "code": {"sharp_radius.py": got[VR04_PY].decode("utf-8")}, "vr04_validation": json.loads(got[VR04_VAL]),
            "r04_sanity": json.loads(got[r7.VALIDATION])["sanity_check"], "rounds": {f"R{i:02d}": got[k].decode("utf-8") for i, k in enumerate(rounds)},
            "folder": sorted(k[len(FOLDER):] for k in got if k.startswith(FOLDER)),
            "crystal_copies": sorted(row[0] for row in manifest["leaves"] if row[0].endswith("State_Crystal_Round_00_v0.1.md")),
            "round00_present": ROUND00 in got, "manifest": manifest}


def world(inputs):
    return {**inputs, "fejer": fejer_compute(), "extremal": extremal_coefficient(), "jpa": jpa_compute(), "radius": radius_compute(),
            "sanity": sanity_compute()}


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

ANCHORS = {
    "text": {"W5": [r"L_r=5\sim6,", r"L_t=12\sim24\text{hours},", r"L_s\ge2.", r"D_{\mathrm{round}}=N-T.", r"D_{\mathrm{round}}=2",
                    "**Empiricalvalidation：PARTIAL****Universalvalidityclaim：NO**",
                    r"\text{DLMVCisanewlyformalizedresearchmethodologywithinitialsuccessfulmathematicalcasestudies.}",
                    r"\boxed{\text{contamination}\Rightarrow\text{independencelabeldowngrade}.}"]},
    "crystal": {"W5": [r"a_{\mathrm{Leb}}\ge0.8344,", r"a_{\mathrm{Leb}}\le0.8440935944.", "Round00：CLOSED。",
                       "**Canonicalparent：**`AMRAL_Lebesgue_Finite_Closure_Round_00_Methodology_v0.2.md`"]},
    "vr01": {"W1": [r"E_M=\frac{H_{K_M}+H_{K_M+1}-1}{4(M+1)}+\frac{1}{4(K_M+1)}", r"K_M=\left\lfloor\frac{M-1}{2}\right\rfloor.", r"|\widehatr_n|\le\frac12.",
                    r"\lambda_{M,n}=\begin{cases}1-\dfrac{|n|}{M+1},&|n|\leM,\\0,&|n|>M.\end{cases}",
                    r"r_N(\theta)=\frac12\left[1+\operatorname{sgn}(\sinN\theta)\right],", r"\widehatr_0=\frac12,"],
             "W2": [r"J(Q,t)\ge\max\left\{0,\|t\|-R_K-", r"\boxed{\text{one-activeoptimalwitnessisimpossible}.}",
                    r"\boxed{\text{2-activeantipodal}\quad\text{or}\quad\text{3-activeorigin-enclosing}.}", "`FUTURE-STATE-EXPOSURE:YES``STRICT-BLINDNESS:COMPROMISED`",
                    "**本輪總Verdict：**`PASS-WITH-GAPS`"]},
    "vr04": {"W3": [r"\Phi_r(d)=\operatorname{Area}\left(\operatorname{conv}(B_r(0)\cup\{x\})\right)=\pir^2+r\sqrt{d^2-r^2}-r^2\arccos\fracrd.",
                    r"\boxed{\Phi_r'(d)=\frac{r\sqrt{d^2-r^2}}d>0.}", r"\boxed{R_\sharp\approx0.721238556039143.}", r"R_P\approx1.689195943036490,",
                    r"\varepsilon_{128,q}\approx0.083391372815752,", r"\beta_{128,q}\approx0.906395396659166.", r"R_P^\sharp\approx0.721955995687207,",
                    r"\varepsilon_{128,q}^\sharp\approx0.035920434390505,", r"\beta_{128,q}^\sharp\approx0.166833279065523.", r"K_q+1=2379.", r"K_q^\sharp+1=445.",
                    r"\left(\frac{445}{2379}\right)^{128}\approx10^{-93.19}.", r"d\le\frac0.84409359440.5.", r"\Delta=\frac{\pi}128."],
             "W4": [r"\operatorname{Area}(U)\approx0.8327576726503144,", r"\operatorname{Area}(P)\approx0.8337053574119659,",
                    r"\DeltaA_{\mathrm{numeric}}\approx9.4768476165\times10^{-4},", r"d_H^{\mathrm{numeric}}\approx6.4598497001\times10^{-4},",
                    "`SANITY:INDEPENDENTLYREPRODUCED`", "`STRICT-BLINDNESSFORROUND04:PASS`"]},
}

_ERRORS = {"3": 0.057, "5": 0.038, "9": 0.022, "17": 0.012, "33": 0.0065, "65": 0.0033, "129": 0.0017}
CLAIMS = {
    "fejer_claim": {"closed_form": True, "legal": True, "below_sharpened": True, "coefficient": [0.3183098862, 0.3183098862],
                    "table": {"3": [0.2188, 0.1393], "5": [0.1806, 0.1149], "9": [0.1342, 0.08541], "17": [0.09093, 0.05789], "33": [0.0575, 0.03661],
                              "65": [0.03465, 0.02206], "129": [0.0202, 0.01286]},
                    "measured": {"reuleaux": _ERRORS, "extremal_3": _ERRORS,
                                 "sign_9": {"3": 0.0077, "5": 0.0077, "9": 0.0069, "17": 0.0037, "33": 0.0019, "65": 0.00099, "129": 0.00051}}},
    "corrections_claim": {"jpa": {"samples": 4000, "violations": 0, "beyond_the_radii": 2236, "least_slack": 1.2713482851820066}, "one_active_in_R01": True,
                          "corrected_in": ["R03"], "taken_back": {"R01-CORRECTION-001": ["R03"], "JPA-01": [], "FLC-01": [], "AR-04": []}},
    "radius_claim": {"area": ["0.8440935944", "0.8440935944", 1e-11], "slope": True, "R_sharp": "0.721238556039142255",
                     "text_digits": {"R_sharp": True, "R_P": True, "R_P_sharp": True, "eps": True, "eps_sharp": True, "beta": True, "beta_sharp": True},
                     "levels": [2379, 445], "log10_ratio": -93.1884},
    "sanity_claim": {"quoted_is_recorded": {"area_U": True, "area_P": True, "excess": True}, "quoted_is_definition": {"area_U": True, "area_P": False, "excess": False},
                     "definition": {"area_U": 0.83275767265, "area_P": 0.833639164382, "excess": 0.000622493675876}},
    "status_claim": {"case_studies": ["AMRAL_LUC_FC_Verification_Round_01_by_LaggedAI_v0.1.md", "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_02_v0.1.md",
                                      "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_03_v0.1.md", "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_04_v0.1.md",
                                      "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_05_v0.1.md", "AMRAL_LUC_FC_Verification_Round_04_by_LaggedAI_v0.1.md"],
                     "blindness": [True, True], "lagged_role": ["R00", "R11", "R12", "R13", "R17"], "crystal": [True, True]},
    "code_facts": {"lines": {"sharp_radius.py": 75}, "hull_area": True, "bisection": ["200"], "constants_as_round04": True,
                   "prints_what_validation_records": [False, False]},
}


def a0_anchors(w):
    out = []
    for doc, groups in ANCHORS.items():
        text = gate.squash(w[doc])
        out += [f"{doc} {cid}: anchor not found: {a[:50]}" for cid, frags in groups.items() for a in frags if a not in text]
    return out


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


def w1_fejer(w):
    """VR01 J: E_M's closed form equals the bound summed mode by mode, for every M of K.1's table; the Fejer image
    of each family stays in [0, 1]; the measured support error sits below E_M; the largest coefficient in the
    domain is 1/pi, attained, so the bound 1/2 behind E_M is not - E_M times 2/pi is a bound too"""
    out, f = [], w["fejer"]
    table = {str(M): [sig(float(e_m(M))), sig(float(e_m(M)) * 2 / math.pi)] for M in FEJER_M}
    got = {"closed_form": all(e_m(M) == e_m_summed(M) for M in FEJER_M), "table": table,
           "legal": all(-1e-12 <= row["min"] and row["max"] <= 1 + 1e-12 for rows in f.values() for row in rows.values()),
           "measured": {name: {M: sig(row["error"], 2) for M, row in rows.items()} for name, rows in f.items()},
           "below_sharpened": all(row["error"] + row["tail"] <= float(e_m(int(M))) * 2 / math.pi for rows in f.values() for M, row in rows.items()),
           "coefficient": [sig(w["extremal"], 10), sig(1 / math.pi, 10)]}
    if not got["closed_form"] or not got["legal"] or not got["below_sharpened"] or abs(w["extremal"] - 1 / math.pi) > 1e-12 or got != w["fejer_claim"]:
        out.append(f"VR01's Fejer compiler: {got}")
    w["w1"] = got
    return out


def w2_corrections(w):
    """VR01 D.7 and D.12: JPA-01's coercivity holds on every random placement; Round 01 lists the one-active
    branch and Round 03 corrects it; which of the case study's results any round takes back by name"""
    out, rounds = [], w["rounds"]
    taken = {k: sorted(r for r, t in rounds.items() if re.search(p, t)) for k, p in TAKEN_BACK.items()}
    got = {"jpa": w["jpa"], "one_active_in_R01": "one-activedegeneracy" in gate.squash(rounds["R01"]),
           "corrected_in": sorted(r for r, t in rounds.items() if r"\text{one-active branch impossible}" in t), "taken_back": taken}
    if w["jpa"]["violations"] or not got["one_active_in_R01"] or got != w["corrections_claim"]:
        out.append(f"VR01's corrections: {got}")
    w["w2"] = got
    return out


def w3_radius(w):
    """VR04 J: the hull's area from its support function and from a fine polygon is Phi_r's; Phi_r' is the
    closed form; R_sharp and the constants at M = 128, q = 5e-4, against the text"""
    out, r = [], w["radius"]
    sq = gate.squash(w["vr04"])
    num = lambda pat: float(re.search(pat, sq).group(1)) if re.search(pat, sq) else None
    text = {"R_sharp": num(r"R_\\sharp\\approx([0-9.]+[0-9])"), "R_P": num(r"R_P\\approx([0-9.]+[0-9])"), "R_P_sharp": num(r"R_P\^\\sharp\\approx([0-9.]+[0-9])"),
            "eps": num(r"varepsilon_\{128,q\}\\approx([0-9.]+[0-9])"), "eps_sharp": num(r"varepsilon_\{128,q\}\^\\sharp\\approx([0-9.]+[0-9])"),
            "beta": num(r"beta_\{128,q\}\\approx([0-9.]+[0-9])"), "beta_sharp": num(r"beta_\{128,q\}\^\\sharp\\approx([0-9.]+[0-9])")}
    c = r["constants"]
    mine = {"R_sharp": float(r["R_sharp"]), "R_P": c["original"]["R_P"], "R_P_sharp": c["sharp"]["R_P"], "eps": c["original"]["epsilon"],
            "eps_sharp": c["sharp"]["epsilon"], "beta": c["original"]["beta"], "beta_sharp": c["sharp"]["beta"]}
    got = {"area": [r["phi_at_R_sharp"][:16], r["by_support"][:16], sig(abs(r["by_polygon"] - float(ABAR)), 1)],
           "slope": max(abs(x) for x in r["slope_residuals"]) < 1e-25, "R_sharp": mp.nstr(mp.mpf(r["R_sharp"]), 18),
           "text_digits": {k: (v is not None and abs(v - mine[k]) < 1e-15) for k, v in text.items()},
           "levels": [c["original"]["levels"], c["sharp"]["levels"]], "log10_ratio": round(r["log10_ratio"], 4)}
    if not all(got["text_digits"].values()) or not got["slope"] or got["levels"] != [2379, 445] or got != w["radius_claim"]:
        out.append(f"VR04's sharp radius: {got}")
    w["w3"] = got
    return out


def w4_sanity(w):
    """VR04 I.2: the numbers the case study calls independently reproduced are Round 04's recorded ones - the
    script's polygon, six edges out one level (RUN-007) - not the polygon Round 04 defines"""
    out, v, d = [], w["r04_sanity"], w["sanity"]
    q = quoted(w["vr04"])
    rec = {"area_U": v["true_area"], "area_P": v["polygon_area"], "excess": v["hausdorff_outer_excess_numeric"]}
    got = {"quoted_is_recorded": {k: bool(q[k] is not None and abs(q[k] - rec[k]) < 1e-12) for k in rec},
           "quoted_is_definition": {k: bool(q[k] is not None and abs(q[k] - d[k]) < 1e-12) for k in rec},
           "definition": {k: sig(d[k], 12) for k in rec}}
    if not all(got["quoted_is_recorded"].values()) or got != w["sanity_claim"]:
        out.append(f"VR04's sanity example: {got}")
    w["w4"] = got
    return out


def w5_status(w):
    """DLMVC sec. 26 against its folder: the case studies it can mean, their blindness records, and the
    frontier's rounds that give the lagged line a role; Round 00's crystal, its parent and its copies"""
    out, rounds = [], w["rounds"]
    s1, s4 = gate.squash(w["vr01"]), gate.squash(w["vr04"])
    got = {"case_studies": [n.split("!/")[-1] for n in w["folder"] if n.endswith(".md") and n.split("!/")[-1].startswith("AMRAL_LUC_FC_Verification_Round")],
           "blindness": ["STRICT-BLINDNESS:COMPROMISED" in s1, "STRICT-BLINDNESSFORROUND04:PASS" in s4],
           "lagged_role": sorted(r for r, t in rounds.items() if re.search(r"[Ll]agged", t)),
           "crystal": [w["crystal_copies"] == [CRYSTAL], w["round00_present"]]}
    if not all(got["crystal"]) or got != w["status_claim"]:
        out.append(f"DLMVC's status: {got}")
    w["w5"] = got
    return out


def w6_code(w):
    """what the case study ships, read after the rebuild and never run"""
    facts = {"lines": {k: v.count("\n") for k, v in sorted(w["code"].items())}}
    facts.update(code_probes(w["code"], w["vr04_validation"]))
    w["w6"] = facts
    return [] if facts == w["code_facts"] else [f"the script: {facts}"]


def code_probes(code, validation):
    """read, never run: the script's hull area is Phi_r's closed form, its root a float bisection, its constants
    Round 04's formulas - and the keys it prints are not the ones VALIDATION records"""
    sq = gate.squash(code["sharp_radius.py"])
    printed = re.findall(r'"([A-Za-z0-9_]+)":', sq.split("out={")[1].split("}")[0])
    per_radius = re.findall(r'"([A-Za-z0-9_]+)":', sq.split("return{")[1].split("}")[0])
    v = validation["sharp_radius_extension"]
    return {"hull_area": "return(math.pi*r*r+r*math.sqrt(d*d-r*r)-r*r*math.acos(r/d))" in sq, "bisection": re.findall(r"iterations=(\d+)", sq),
            "constants_as_round04": "eps=q+(R+RP)*dM" in sq and "beta=2*math.pi*R*eps+math.pi*eps*eps" in sq and "Kq=math.ceil((R-r)/q)+1" in sq,
            "prints_what_validation_records": [sorted(printed) == sorted(v), sorted(per_radius) == sorted(v["sharp"])]}


def p1_package(w):
    out, v = [], w["vr04_validation"]
    leaves = {row[0]: row for row in w["manifest"]["leaves"]}
    rec, (_, size, digest) = v["round04_verification"], leaves[VR04]
    n = w["vr04"].count("$$")
    if (rec["sha256"], rec["bytes"], rec["file"], rec["double_dollar_count"], rec["double_dollar_even"]) != (digest, size, VR04.split("/")[-1], n, n % 2 == 0) \
            or not rec["utf8"] or rec["control_characters"] != [ch for ch in w["vr04"] if ord(ch) < 32 and ch not in "\t\n\r"] \
            or rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", w["vr04"])) \
            or rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", w["vr04"])):
        out.append("VALIDATION's record of the document")
    s, c = v["sharp_radius_extension"], w["radius"]["constants"]
    mine = {"R_sharp": float(w["radius"]["R_sharp"]), "R_triangle": c["original"]["R"]}
    if abs(s["R_sharp"] - mine["R_sharp"]) > 1e-15 or abs(s["R_triangle"] - mine["R_triangle"]) > 1e-15 or abs(s["hull_area_at_R_sharp"] - float(ABAR)) > 1e-15 \
            or (s["Abar"], s["anchor_radius"], s["M"], s["q"]) != (float(ABAR), 0.5, 128, 0.0005) \
            or any(abs(s[k]["R_P"] - c[k]["R_P"]) > 1e-15 or abs(s[k]["epsilon"] - c[k]["epsilon"]) > 1e-15 or abs(s[k]["beta"] - c[k]["beta"]) > 1e-14
                   or (s[k]["K_q"], s[k]["levels"]) != (c[k]["K_q"], c[k]["levels"]) for k in ("original", "sharp")) \
            or abs(s["log10_crude_dictionary_cardinality_ratio"] - w["radius"]["log10_ratio"]) > 1e-12 or v["status"] != "PASS":
        out.append("VALIDATION's constants against this tree's")
    w["p1"] = {"validation_passes_broken_formulas": v["status"] == "PASS" and r"\frac0.8440935944" in w["vr04"]}
    return out


_LABEL = "an output label of the deep-pass ladder (sec. 7); no judgment"
R41_DEFINITIONS = {
    "DEFINED": ("contextual", "sec. 26: a part of the method written down and fixed, as against validated (Empirical validation: PARTIAL)"),
    "BLIND-CLEAN": ("in-line", "sec. 5: no text or state crystal of any round after the target read before its verification"),
    "PARTIAL-EXPOSURE": ("in-line", "sec. 5: only the existence, file names or metadata of later rounds seen, no text"),
    "CONTENT-EXPOSED": ("in-line", "sec. 5: some later state, theorem or correction read - strict blindness may no longer be claimed"),
    "POST-HOC": ("in-line", "sec. 5: hindsight allowed from the start, for comparison"),
    "CORRECTION": ("in-line", "sec. 7, Pass B: an adversarial audit found the target wrong somewhere and says how"),
    "COUNTEREXAMPLE": ("in-line", "sec. 7, Pass B: a replayable instance against a claim"),
    "HIDDEN-BRANCH": ("in-line", "sec. 7, Pass B: a case the target's analysis left out"),
    "MISSING-LEMMA": ("in-line", "sec. 7, Pass C: the conclusion holds but an edge of the proof graph was never written"),
    "HANDOFF-REPAIR": ("in-line", "sec. 7, Pass C: a step between representations supplied"),
    "EXTENSION": ("in-line", "sec. 7, Pass D: a stronger constant, a weaker hypothesis, a more exact representation or a smaller error"),
    "DOMAIN-COMPRESSION": ("in-line", "sec. 7, Pass E: apparent freedom in a finite representation shown not to be free"),
    "EXACT-COMPILER": ("in-line", "sec. 7, Pass F: cells, branches or codewords turned into exactly replayable geometry"),
    "CRITICAL-SET": ("in-line", "sec. 7, Pass G: the states that still cannot be decided finitely, located"),
    "GEOMETRIC-SANDWICH": ("in-line", "sec. 7, Pass H: inner and outer bodies bracketing the object, for a monotone functional"),
    "CONTACT-SKELETON": ("in-line", "sec. 7, Pass I: unresolved critical states forced onto an active-constraint skeleton"),
    "FORMALIZATION-DEFERRED": ("in-line", "sec. 15: a formal proof not yet written, with its inputs, domain, algorithm and dependencies kept"),
}
R41_REVIEWS = [
    ("CLOSED", "Methodology skeleton", "reading", "PASS", "true as a text: roles, lag, provenance, ladder, stop and return rules are all written down; nothing in it is computed"),
    ("COMPUTE-DEFERRED", "15. 計算與形式化位置", "n/a", "n/a", "a label defined in sec. 15; no judgment"),
    ("DEFINED", "Operational target-selection rule", "reading", "PASS", "sec. 3-4"),
    ("DEFINED", "Blindness provenance", "reading", "PASS", "sec. 5"),
    ("DEFINED", "Deep-pass ladder", "reading", "PASS", "sec. 6-9"),
    ("DEFINED", "Intra-resolution / cross-resolution distinction", "reading", "PASS", "sec. 10"),
    ("DEFINED", "RCHM relation", "reading", "PASS", "sec. 18"),
    ("DEFINED", "AMRAL integration", "reading", "PASS", "sec. 19"),
    ("NO", "Universal validity claim", "reading", "PASS", "true: none is made"),
    ("PARTIAL", "Empirical validation", "computation", "PASS",
     "right: the case studies' mathematics recomputes (W1-W3), but one of them calls a re-run of the author's script an independent reproduction "
     "and reproduces the script's polygon, not the round's (W4) - the failure sec. 1 describes"),
    ("BLIND-CLEAN", "", "n/a", "n/a", "a blindness state defined in sec. 5; no judgment"),
    ("CONTENT-EXPOSED", "", "n/a", "n/a", "a blindness state defined in sec. 5; no judgment"),
    ("PARTIAL-EXPOSURE", "", "n/a", "n/a", "a blindness state defined in sec. 5; no judgment"),
    ("POST-HOC", "", "n/a", "n/a", "a blindness state defined in sec. 5; no judgment"),
    ("INDEPENDENT-REPRODUCTION", "Pass A — Independent Reconstruction", "n/a", "n/a", _LABEL),
    ("CORRECTION", "Pass B — Adversarial Audit", "n/a", "n/a", _LABEL),
    ("COUNTEREXAMPLE", "Pass B — Adversarial Audit", "n/a", "n/a", _LABEL),
    ("HIDDEN-BRANCH", "Pass B — Adversarial Audit", "n/a", "n/a", _LABEL),
    ("MISSING-LEMMA", "Pass C — Proof-Graph Repair", "n/a", "n/a", _LABEL),
    ("HANDOFF-REPAIR", "Pass C — Proof-Graph Repair", "n/a", "n/a", _LABEL),
    ("EXTENSION", "Pass D — Theorem Strengthening", "n/a", "n/a", _LABEL),
    ("DOMAIN-COMPRESSION", "Pass E — False-Freedom Compression", "n/a", "n/a", _LABEL),
    ("EXACT-COMPILER", "Pass F — Exact Finite Geometry", "n/a", "n/a", _LABEL),
    ("CRITICAL-SET", "Pass G — Critical-Set Localization", "n/a", "n/a", _LABEL),
    ("GEOMETRIC-SANDWICH", "Pass H — Inner/Outer Sandwich", "n/a", "n/a", _LABEL),
    ("CONTACT-SKELETON", "Pass I — Contact Skeleton", "n/a", "n/a", _LABEL),
    ("DERIVED-CANDIDATE", "Pass J — Continuum Lift", "n/a", "n/a", _LABEL),
    ("FORMALIZATION-DEFERRED", "15. 計算與形式化位置", "n/a", "n/a", "a label defined in sec. 15; no judgment"),
]


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


CHECKS = {"A0": a0_anchors, "W1": w1_fejer, "W2": w2_corrections, "W3": w3_radius, "W4": w4_sanity, "W5": w5_status, "W6": w6_code,
          "P1": p1_package, "R1": r1_registry}
DEPENDS = {"A0": {"text", "crystal", "vr01", "vr04"}, "W1": {"fejer", "extremal", "fejer_claim"}, "W2": {"jpa", "rounds", "corrections_claim"},
           "W3": {"radius", "vr04", "radius_claim"}, "W4": {"r04_sanity", "sanity", "vr04", "sanity_claim"},
           "W5": {"vr01", "vr04", "folder", "rounds", "crystal_copies", "round00_present", "status_claim"}, "W6": {"code", "vr04_validation", "code_facts"},
           "P1": {"vr04_validation", "manifest", "vr04", "radius"}, "R1": {"registry", "definitions", "reviews"}}


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

    v = base["vr04_validation"]
    return [
        ("K0-unmodified", "control", {}, set()),
        ("K1-vr04-crlf", "control", {"vr04": base["vr04"].replace("\n", "\r\n")}, set()),
        ("K2-validation-keys-sorted", "control", {"vr04_validation": json.loads(json.dumps(v, sort_keys=True))}, set()),
        ("M1-doc-lag", "mutation", {"text": base["text"].replace(r"L_r=5\sim6,", r"L_r=4\sim6,")}, {"A0"}),
        ("M2-fejer-image", "mutation", {"fejer": edit(base["fejer"], lambda x: x["reuleaux"]["9"].update(max=1.0001))}, {"W1"}),
        ("M3-fejer-error", "mutation", {"fejer": edit(base["fejer"], lambda x: x["sign_9"]["3"].update(error=0.2))}, {"W1"}),
        ("M4-jpa-violation", "mutation", {"jpa": {**base["jpa"], "violations": 1}}, {"W2"}),
        ("M5-round01-taxonomy", "mutation", {"rounds": {**base["rounds"], "R01": base["rounds"]["R01"].replace("one-active degeneracy", "two-active degeneracy")}},
         {"W2"}),
        ("M6-vr04-radius", "mutation", {"vr04": base["vr04"].replace("0.721238556039143", "0.721238556039144")}, {"A0", "W3"}),
        ("M7-radius-levels", "mutation", {"radius": edit(base["radius"], lambda x: x["constants"]["sharp"].update(levels=444))}, {"W3", "P1"}),
        ("M8-recorded-polygon", "mutation", {"r04_sanity": {**base["r04_sanity"], "polygon_area": 0.8336391643823979}}, {"W4"}),
        ("M9-crystal-copy", "mutation", {"crystal_copies": base["crystal_copies"] + ["main.zip!/elsewhere/AMRAL_LUC_FC_State_Crystal_Round_00_v0.1.md"]}, {"W5"}),
        ("M10-code-claim", "mutation", {"code_facts": {}}, {"W6"}),
        ("M11-validation-digest", "mutation", {"vr04_validation": edit(v, lambda x: x["round04_verification"].update(sha256="0" * 64))}, {"P1"}),
        ("M12-validation-constant", "mutation", {"vr04_validation": edit(v, lambda x: x["sharp_radius_extension"]["sharp"].update(epsilon=0.0359204344))},
         {"P1"}),
        ("M13-review-dropped", "mutation", {"reviews": list(R41_REVIEWS[1:])}, {"R1"}),
        ("M14-definition-dropped", "mutation", {"definitions": {k: d for k, d in R41_DEFINITIONS.items() if k != "POST-HOC"}}, {"R1"}),
    ]


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    base = world(load_inputs())

    def build():
        return {**base, "registry": registry.load(), "definitions": dict(R41_DEFINITIONS), "reviews": list(R41_REVIEWS), **copy.deepcopy(CLAIMS)}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {c: fn(w) for c, fn in CHECKS.items()}
    for c, f in results.items():
        print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n     {x}" for x in f[:6]))
    for key in ("w1", "w2", "w3", "w4", "w5", "w6", "p1"):
        print(key, "=", json.dumps(w.get(key), default=float, 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-041", "subject": "DLMVC: the deep-lag verification methodology, and its case studies of Rounds 01 and 04",
           "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=float) + "\n", encoding="utf-8")
    if not results["R1"]:
        registry.record("DLMVC", "RUN-041", R41_DEFINITIONS, R41_REVIEWS)
        print(f"registry: {len(R41_DEFINITIONS)} definitions, {len(R41_REVIEWS)} reviews recorded for DLMVC")


if __name__ == "__main__":
    main()