"""RUN-045 - UESFCM Cycles 04-06: Gate A's dual certificate, the symmetry quotient, the symmetric anchor and the far branches.

Cycle 04 closes Gate A - B7 does not fit the seed's hull, by a margin M_U0(B7) > 0.0088366789 - with a finite
dual certificate: at each of 1024 orientations three support directions whose sine-gap weights cancel the
translation, B7 replaced by its corner heptagon and each Reuleaux body by the intersection of its unit discs,
evaluated in interval arithmetic, then an orientation-Lipschitz bridge. It rewrites Gate B (every placement at
most A3+ lies within that margin of the seed's orbit) as a far-set minimum. Cycle 05 quotients the turn of B5 by
the configuration's D3 symmetry to [0, pi/15], fixes the leaf language (ORBIT-COVERED or AREA-PRUNED) and a
one-bit tree format, and reports an orbit-basin depth and a runtime probe. Cycle 06 moves the anchor to the
reflection-symmetric U_sym (d_H < 1.66e-5, new radius 0.00882), splits the far set into F3 and F5, searches both,
and adds a farthest-corner box bound. Here the certificate is re-enclosed witness by witness in this tree's own
integer intervals (RUN-030/031), the quotient and the bounds are tested, the far branches searched with the exact
hull, and the scripts read.

Checks
  A0 anchors      the numbers and formulas below occur in the three documents as written
  W1 gate A       every witness enclosed in 400-bit integer intervals: gaps below pi, positive weights, the least
                  lower and its orientation, the bridge; what the file records and what the verifier checks
  W2 conservatism the certified values against the true margin at sampled orientations
  W3 quotient     Cycle 05: the D3 action on placements, the fundamental interval, the orbit-basin depth, the
                  safe constant
  W4 anchor       Cycle 06: d_H(U0, U_sym), U_sym's area, the orbit copies' distance, the new radius
  W5 far sets     Cycle 04's far boundary and Cycle 06's F3, F5, searched with the exact hull
  W6 box bounds   Cycle 06 sec. 15-17 on random boxes: the distance bounds and the farthest-corner area bound
  W7 crystals     the three state crystals against the numbers rebuilt here
  W8 code         the scripts, read after the rebuild and never run
  P1 package      the VALIDATION records against the archive; the dependency copies

Usage: python code/run045_uesfcm_cycles_04_06.py [--drill] [--blind CID]
"""
import argparse
import copy
import hashlib
import inspect
import json
import math
import re
from decimal import Decimal
from fractions import Fraction

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

import gate
import run044_uesfcm_cycles_01_03 as r44
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run008_round05_saturation_gate import phi_text, reuleaux_support, reuleaux_vertices
from run009_round06_witness_exchange import hull_pieces, placed_disc, placed_reuleaux
from run030_round27_interval_replay import ONE, add, cos_sin, div_int, exact, mul
from run031_round28_exact_root import PI, neg, radius, recip, sub
from run044_uesfcm_cycles_01_03 import A3, base_pieces, continuous_margin, family_area, rn, support, t_bound

FOLDER = "main.zip!/UESFCM/"
PKG = {i: FOLDER + f"UESFCM_Lebesgue_Cycle_{i:02d}_Package_v0.1.zip!/" for i in (4, 5, 6)}
DOCS = {4: PKG[4] + "UESFCM_Lebesgue_Cycle_04_GateA_Closure_and_Far_Set_v0.1.md",
        5: PKG[5] + "UESFCM_Lebesgue_Cycle_05_TwoColour_GateB_Certificate_v0.1.md",
        6: PKG[6] + "UESFCM_Lebesgue_Cycle_06_Symmetric_Anchor_and_Far_Branches_v0.1.md"}
CERT = PKG[4] + "UESFCM_Lebesgue_Cycle_04_GateA_Dual_Certificate.json"
SPEC = PKG[5] + "UESFCM_Lebesgue_Cycle_05_GateB_Certificate_Spec.json"
CODE = {"verify_gateA": PKG[4] + "UESFCM_Lebesgue_Cycle_04_Verify_GateA.py",
        "gateB_scaffold": PKG[4] + "UESFCM_Lebesgue_Cycle_04_GateB_FarSet_Scaffold.py",
        "emitter": PKG[5] + "UESFCM_Lebesgue_Cycle_05_GateB_Emitter.py",
        "verifier_skeleton": PKG[5] + "UESFCM_Lebesgue_Cycle_05_GateB_Verifier_Skeleton.py",
        "branch_scaffold": PKG[6] + "UESFCM_Lebesgue_Cycle_06_Branch_Certificate_Scaffold.py"}
COPIES = {PKG[5] + "dependencies/UESFCM_Lebesgue_Cycle_04_GateA_Dual_Certificate.json": CERT,
          PKG[5] + "dependencies/UESFCM_Lebesgue_Cycle_04_Verify_GateA.py": CODE["verify_gateA"]}
CRYSTALS = {i: PKG[i] + f"UESFCM_Lebesgue_State_Crystal_Cycle_{i:02d}_v0.1.json" for i in (4, 5, 6)}
VALIDATIONS = {i: PKG[i] + f"UESFCM_Lebesgue_Cycle_{i:02d}_VALIDATION.json" for i in (4, 5, 6)}
ROUND07 = TREE / "data" / "external" / "round07-citations.json"
LOG = TREE / "data" / "gate-logs" / "run045-uesfcm-cycles-04-06.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CACHE = TREE / "data" / "cache" / "run045-searches.json"     # data/cache is not committed

PER5 = 2 * math.pi / 5
S_C04 = 0.0088366789091384       # Cycle 04's Gate A lower, its Gate B radius
S_A = 0.0088366                  # Cycle 05's safe constant
S_SYM = 0.00882                  # Cycle 06's radius about the symmetric anchor


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = set(DOCS.values()) | set(CODE.values()) | set(CRYSTALS.values()) | set(VALIDATIONS.values()) | {CERT, SPEC} | set(COPIES)
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None}
    rows = {row[0]: row for row in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"]}
    return {"texts": {i: got[DOCS[i]].decode("utf-8") for i in DOCS}, "code": {k: got[p].decode("utf-8") for k, p in CODE.items()},
            "cert": json.loads(got[CERT]), "spec": json.loads(got[SPEC]),
            "crystals": {i: json.loads(got[CRYSTALS[i]]) for i in CRYSTALS},
            "validations": {i: json.loads(got[VALIDATIONS[i]]) for i in VALIDATIONS},
            "files": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want},
            "v0": json.loads(ROUND07.read_text(encoding="utf-8"))["repository"]["reuleaux"]["placement"]}


# ---------------------------------------------------------------- Gate A, enclosed in this tree's integer intervals

def turn(q):
    """2 pi q for a rational q, enclosed"""
    two_pi = (2 * PI[0], 2 * PI[1])
    return mul(two_pi, exact(q)) if q >= 0 else neg(mul(two_pi, exact(-q)))


def imax(xs):
    return max(x[0] for x in xs), max(x[1] for x in xs)


def imin(xs):
    return min(x[0] for x in xs), min(x[1] for x in xs)


def gate_a(cert):
    """Cycle 04 sec. 3-9: at orientation phi_p = 2 pi p / 7P and directions u_j = u(2 pi j / M), the dual bound
    sum_i lambda_i [h_P7(R_{-phi} u_i) - hbar_U0(u_i)], lambda from the sine gaps; P7 the heptagon of B7's corners,
    hbar the maximum of 1/2 and of each body's least unit-disc support. Every quantity is enclosed from the placement's
    decimals, PI (Machin) and Taylor sums; the gaps must all be below pi for the weights to be positive"""
    M, P = cert["support_grid_M"], cert["orientation_grid_P"]
    pl = {k: exact(Fraction(Decimal(v))) for k, v in cert["placement_U0"].items()}
    one = (ONE, ONE)
    R3, R5, R7 = radius(3), radius(5), radius(7)

    def corners(n, R, rho, tx, ty):
        out = []
        for k in range(n):
            cs = cos_sin(add(rho, turn(Fraction(k, n))) if rho is not None else turn(Fraction(k, n)))
            out.append((add(tx, mul(R, cs[0])), add(ty, mul(R, cs[1]))))
        return out

    c3 = corners(3, R3, None, pl["x3"], pl["y3"])
    c5 = corners(5, R5, pl["rho5"], pl["x5"], pl["y5"])
    dirs, covers = {}, {}

    def u(j):
        if j not in dirs:
            dirs[j] = cos_sin(turn(Fraction(j, M)))
        return dirs[j]

    def hbar(j):
        if j not in covers:
            cs = u(j)
            dot = lambda c: add(add(mul(c[0], cs[0]), mul(c[1], cs[1])), one)
            covers[j] = imax([exact(Fraction(1, 2)), imin([dot(c) for c in c3]), imin([dot(c) for c in c5])])
        return covers[j]

    def h7(j, p):
        return imax([mul(R7, cos_sin(turn(Fraction(j, M) - Fraction(p, 7 * P) - Fraction(k, 7)))[0]) for k in range(7)])

    rows = []
    for w in cert["witnesses"]:
        p, js = w["orientation_index"], sorted(w["support_indices"])
        gaps = (Fraction(js[2] - js[1], M), 1 - Fraction(js[2] - js[0], M), Fraction(js[1] - js[0], M))    # g23, g31, g12
        s = [cos_sin(turn(g))[1] for g in gaps]
        S = add(add(s[0], s[1]), s[2])
        val = (0, 0)
        for si, j in zip(s, js):
            val = add(val, mul(mul(si, recip(S)), sub(h7(j, p), hbar(j))))
        rows.append({"p": p, "positive": max(gaps) < Fraction(1, 2), "lo": Fraction(val[0], ONE), "hi": Fraction(val[1], ONE),
                     "recorded": Fraction(Decimal(w["interval_lower"]))})
    half = div_int(PI, 7 * P)
    return {"rows": rows, "half_gap": (Fraction(half[0], ONE), Fraction(half[1], ONE)), "M": M, "P": P}


# ---------------------------------------------------------------- the symmetry, the anchor, the far sets

def orbit(v):
    """Cycle 05 sec. 3: the D3 images of a placement - the whole configuration turned by 2 pi k / 3, each also
    reflected in the x-axis - with B5's turn taken mod 2 pi / 5"""
    out = []
    for k in range(3):
        c, s = math.cos(2 * math.pi * k / 3), math.sin(2 * math.pi * k / 3)
        w = [c * v[0] - s * v[1], s * v[0] + c * v[1], (v[2] + 2 * math.pi * k / 3) % PER5, c * v[3] - s * v[4], s * v[3] + c * v[4]]
        out += [w, [w[0], -w[1], (-w[2]) % PER5, w[3], -w[4]]]
    return out


def q_metric(v, w):
    d = abs((v[2] - w[2] + PER5 / 2) % PER5 - PER5 / 2)
    return max(math.hypot(v[0] - w[0], v[1] - w[1]), math.hypot(v[3] - w[3], v[4] - w[4]) + 2 * rn(5) * math.sin(d / 2))


def orbit_depth(v0, T3, T5, s):
    """Cycle 05 sec. 18: down the weighted-split branch holding the normalized seed, the first depth at which the
    box is ORBIT-COVERED (q to the orbit at the centre, plus tau, below s)"""
    orb = orbit(v0)
    vn = [v0[0], v0[1], v0[2] % PER5, v0[3], v0[4]]
    c, h = [0.0, 0.0, math.pi / 30, 0.0, 0.0], [T3, T3, math.pi / 30, T5, T5]
    for depth in range(80):
        tau = max(math.hypot(h[0], h[1]), math.hypot(h[3], h[4]) + 2 * rn(5) * math.sin(h[2] / 2))
        if min(q_metric(c, w) for w in orb) + tau < s:
            return depth
        k = int(np.argmax([h[0], h[1], rn(5) * h[2], h[3], h[4]]))
        half = h[k] / 2
        c = c.copy()
        c[k] += half if vn[k] > c[k] else -half
        h = h.copy()
        h[k] = half
    return None


def d3_invariance(v0, trials=40, seed=5):
    rng, worst = np.random.default_rng(seed), 0.0
    for _ in range(trials):
        v = np.asarray(v0) + rng.normal(0, [0.02, 0.02, 0.3, 0.02, 0.02])
        a0 = family_area(v)
        worst = max(worst, max(abs(family_area(w) - a0) for w in orbit(v)[1:]))
    return worst


def hausdorff(pieces_a, pieces_b, n=1 << 18):
    th = 2 * np.pi * np.arange(n) / n
    return float(np.max(np.abs(support(pieces_a)(th) - support(pieces_b)(th))))


def far_search(f, box, seed):
    """differential evolution, then Nelder-Mead from its point and four random ones; the least exact hull"""
    de = differential_evolution(lambda y: f(y, 512), box, seed=seed, popsize=15, maxiter=120, tol=1e-12, polish=False)
    best = None
    rng = np.random.default_rng(seed)
    for start in [de.x] + [np.array([rng.uniform(lo, hi) for lo, hi in box]) for _ in range(4)]:
        res = minimize(lambda y: f(y, 2048), start, method="Nelder-Mead", options={"xatol": 1e-11, "fatol": 1e-15, "maxfev": 4000})
        val = f(res.x, 16384)
        if best is None or val < best[0]:
            best = (float(val), [float(a) for a in res.x])
    return {"area": best[0], "point": best[1]}


def far_sets(v0):
    """Cycle 06 sec. 9-11 and Cycle 04 sec. 15: the far branches searched on their boundaries. About the symmetric
    anchor (x3^0, 0, 0, x5^0, 0) at radius 0.00882: F3 puts t3 on the circle, F5 spends the radius between B5's turn
    and its translation. About the seed itself at Cycle 04's radius: the same two boundaries, the turn measured from
    the seed's normalized angle"""
    X3, X5, r5 = v0[0], v0[3], rn(5)

    def f3(anchor, s):
        def f(y, N):
            a, rho, x5, y5 = y
            return family_area([anchor[0] + s * math.cos(a), anchor[1] + s * math.sin(a), rho, x5, y5], 5, N)
        return f

    def f5(anchor, s):
        def f(y, N):
            r, b, x3, y3 = y
            left = s - 2 * r5 * math.sin(abs(r) / 2)
            return family_area([x3, y3, anchor[2] + r, anchor[3] + left * math.cos(b), anchor[4] + left * math.sin(b)], 5, N)
        return f

    rmax = lambda s: 2 * math.asin(s / (2 * r5))
    sym = [X3, 0.0, 0.0, X5, 0.0]
    seed = [v0[0], v0[1], v0[2] % PER5, v0[3], v0[4]]
    return {"F3": far_search(f3(sym, S_SYM), [(-math.pi, math.pi), (0.0, math.pi / 15), (X5 - 0.03, X5 + 0.03), (-0.03, 0.03)], 45),
            "F5": far_search(f5(sym, S_SYM), [(0.0, rmax(S_SYM)), (-math.pi, math.pi), (X3 - 0.03, X3 + 0.03), (-0.03, 0.03)], 45),
            "C04_F3": far_search(f3(seed, S_C04), [(-math.pi, math.pi), (0.0, math.pi / 15), (X5 - 0.03, X5 + 0.03), (-0.03, 0.03)], 44),
            "C04_F5": far_search(f5(seed, S_C04), [(-rmax(S_C04), rmax(S_C04)), (-math.pi, math.pi), (X3 - 0.03, X3 + 0.03), (-0.03, 0.03)], 44)}


def box_bounds(v0, boxes=400, per_box=30, seed=6):
    """Cycle 06 sec. 15-17 on random boxes about the symmetric anchor: the d3, d5 bounds against sampled points,
    and the farthest-corner area bound against the exact hull at sampled points"""
    X3, X5, r5 = v0[0], v0[3], rn(5)
    rng = np.random.default_rng(seed)
    V3, V5 = reuleaux_vertices(3), reuleaux_vertices(5)
    bad, worst = 0, -math.inf
    for _ in range(boxes):
        cc = np.array([X3, 0, rng.uniform(0, math.pi / 15), X5, 0]) + rng.normal(0, [0.02, 0.02, 0, 0.02, 0.02])
        hh = rng.uniform(0, [0.02, 0.02, 0.05, 0.02, 0.02]) * 10 ** rng.uniform(-2, 0)
        d3p = math.hypot(abs(cc[0] - X3) + hh[0], abs(cc[1]) + hh[1])
        d3m = math.hypot(max(abs(cc[0] - X3) - hh[0], 0), max(abs(cc[1]) - hh[1], 0))
        d5p = math.hypot(abs(cc[3] - X5) + hh[3], abs(cc[4]) + hh[4]) + 2 * r5 * math.sin(min(cc[2] + hh[2], math.pi / 15) / 2)
        for _ in range(per_box):
            v = cc + rng.uniform(-1, 1, 5) * hh
            v[2] = min(max(v[2], 0.0), math.pi / 15)
            d3 = math.hypot(v[0] - X3, v[1])
            d5 = math.hypot(v[3] - X5, v[4]) + 2 * r5 * math.sin(v[2] / 2)
            bad += not (d3m - 1e-15 <= d3 <= d3p + 1e-15 and d5 <= d5p + 1e-15)
        rot = np.array([[math.cos(cc[2]), -math.sin(cc[2])], [math.sin(cc[2]), math.cos(cc[2])]])
        far = max(np.max(np.hypot(*(V3 + cc[:2]).T)) - math.hypot(hh[0], hh[1]),
                  np.max(np.hypot(*(V5 @ rot.T + cc[3:5]).T)) - math.hypot(hh[3], hh[4]) - 2 * r5 * math.sin(hh[2] / 2))
        beta = phi_text(0.5, max(0.5, far))
        for _ in range(3):
            worst = max(worst, beta - family_area(cc + rng.uniform(-1, 1, 5) * hh, 5, 4096))
    return {"violations": bad, "samples": boxes * per_box, "corner_bound_excess": worst}


def true_margins(v0, cert, step=32):
    """the true margin of B7 in U0 at every step-th certified orientation and at the least one, to set beside the
    certificate's values"""
    hU, hK = support(base_pieces(v0)), reuleaux_support(7)
    P = cert["orientation_grid_P"]
    ps = sorted(set(range(0, P, step)) | {cert["minimum_sample_orientation_index"]})
    return {str(p): list(continuous_margin(hU, hK, 2 * math.pi * p / (7 * P))) for p in ps}


HELPERS = (orbit, far_search, r44.support, r44.base_pieces, r44.family_area, r44.lp_margin, r44.golden_max, r44.continuous_margin, r44.rn)


def _key(fn):
    """a search's cache key: its own code, the helpers it calls, and run008/run009's hull kernel"""
    import run008_round05_saturation_gate as r8
    import run009_round06_witness_exchange as r9
    digest = hashlib.sha256(inspect.getsource(fn).encode())
    for helper in HELPERS:
        digest.update(inspect.getsource(helper).encode())
    for path in (r8.__file__, r9.__file__):
        digest.update(open(path, "rb").read())
    return digest.hexdigest()


SEARCHES = {"true_margins": (true_margins, lambda v0, cert: true_margins(v0, cert)), "d3": (d3_invariance, lambda v0, cert: d3_invariance(v0)),
            "far": (far_sets, lambda v0, cert: far_sets(v0)), "boxes": (box_bounds, lambda v0, cert: box_bounds(v0))}


def searches(v0, cert):
    """each search cached under its own key, so a change to one leaves the others"""
    cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {}
    out, changed = {}, False
    for name, (fn, call) in SEARCHES.items():
        key = _key(fn)
        if cached.get(name, {}).get("key") != key:
            cached[name] = {"key": key, "value": call(v0, cert)}
            changed = True
        out[name] = cached[name]["value"]
    if changed:
        CACHE.parent.mkdir(parents=True, exist_ok=True)
        CACHE.write_text(json.dumps(cached, indent=1) + "\n", encoding="utf-8")
    return out


def world(inputs):
    v0, cert = inputs["v0"], inputs["cert"]
    vbar = [v0[0], 0.0, 0.0, v0[3], 0.0]
    return {**inputs, "gate_a": gate_a(cert), "search": searches(v0, cert),
            "orbit_depth": orbit_depth(v0, inputs["spec"]["constants"]["T3"], inputs["spec"]["constants"]["T5"], S_A),
            "anchor": {"area_sym": family_area(vbar), "area_seed": family_area(v0),
                       "hausdorff": hausdorff(base_pieces(v0), base_pieces(vbar))}}


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

ANCHORS = {
    4: {"W1": [r"m_{\mathrm{grid}}^-=0.0092749591342486.", "$$p=767.$$", r"M_{U_0}(B_7)>0.0088366789091384.", r"\lambda_1=\frac{\sing_{23}}{S},",
               r"\overlineh_{U_0}(u)=\max\left\{\frac12,\min_k(c_{3,k}\cdotu+1),\min_k(c_{5,k}\cdotu+1)\right\}.", "`CERTIFIED-FINITE-DUAL`",
               r"|m(\phi)-m(\psi)|\le|\phi-\psi|."],
        "W5": [r"A_{\mathrm{far}}^{\mathrm{search}}\approx0.834804245159.", r"\Delta_{\mathrm{far}}^{\mathrm{search}}\approx2.3054\times10^{-5}.", "1.97\\times10^{-4}."]},
    5: {"W3": [r"s_A=0.0088366.", r"0\le\rho_5\le\frac{\pi}{15}=12^\circ.", r"\frac{2\pi}{3}\equiv\frac{4\pi}{15}\pmod{2\pi/5}.", "`PROVED/SYMMETRY-QUOTIENT`",
               r"M_{U_0}(B_7)>0.008836669.", r">6.9\times10^{-8}", r"\boxed{31}", r"\boxed{985.6\times.}"],
        "W5": [r"A\approx0.8348051"]},
    6: {"W4": [r"d_H(U_0,U_{\mathrm{sym}})<1.66\times10^{-5}.", r"M_{U_{\mathrm{sym}}}(B_7)>0.00882.", r"A(U_{\mathrm{sym}})\approx0.834780945826.",
               r"2R_5\sin\frac{\pi}{30}\approx0.109907730484.", r"\left|\rho_5^0-\frac{2\pi}{5}\right|<2.413\times10^{-5}."],
        "W5": [r"A_3^{\mathrm{search}}\approx0.834968965913228.", r"A_5^{\mathrm{search}}\approx0.834804245410142.", r"\Delta_5^{\mathrm{search}}\approx2.305441014e-05."],
        "W6": [r"d_{3,\mathcalB}^+=\sqrt{(|c_x-x_3^0|+h_x)^2+(|c_y|+h_y)^2}.", r"r_\rho^+=2R_5\sin\frac{\min(c_\rho+h_\rho,\pi/15)}{2}.",
               r"A(v)\ge\Phi_{1/2}\left(\max\left\{\frac12,d_{\mathrm{corner}}^-(\mathcalB)\right\}\right)."]},
}

CLAIMS = {
    "gate_a_claim": {"orientations_complete": True, "all_gaps_below_pi": True, "width": 7e-103, "least": 0.00927495913424859, "at": 767,
                     "half_gap": 0.000438280225110183, "certified": 0.0088366789091384, "file_degenerate": True, "file_above_enclosure": [76, 3e-19],
                     "file_agrees": True, "file_least": [True, True]},
    "conservatism_claim": {"orientations": 33, "below": True, "least_loss": 2.17e-07, "largest_loss": 0.000184, "true_at_least": 0.009458708251},
    "quotient_claim": {"invariance": 1e-15, "step": "4/15", "fundamental": "1/15", "depth": 31, "safe": ["0.008836669", "6.9E-8"],
                       "spec_T_inward_ulps": [22, 12], "spec_rho_max": True, "spec_R5": True, "spec_status": "SCHEMA CLOSED / TREE NOT YET EMITTED"},
    "anchor_claim": {"turn": 2.4129e-05, "heights": [True, True], "bound": [1.658e-05, 1.66e-05], "true_hausdorff": 7.073e-06,
                     "area_sym": 0.834780945826, "sym_below_seed": True, "radius": "0.0088200", "copies": 0.109907730484},
    "far_claim": {"F3": 0.834968955147, "F5": 0.834804244389, "C04_F3": 0.83496965443, "C04_F5": 0.834804245864,
                  "gaps": {"F3": 0.000187764, "F5": 2.30534e-05, "C04_F3": 0.000188463, "C04_F5": 2.30549e-05},
                  "cycle06_minus_mine": [1.1e-08, 1e-09], "cycle04_minus_mine": -7.1e-10, "all_above_A3": True},
    "box_claim": {"violations": 0, "samples": 12000, "corner_bound_below": True},
    "crystal_claim": {"C04": [True, True, True, True, -7e-10], "C05": [True, "rho5 in [0, pi/15]", True, 985.6307081],
                      "C06": [True, True, True, 1e-16, 1.1e-08, 1e-09]},
    "code_facts": {"lines": {"verify_gateA": 101, "gateB_scaffold": 105, "emitter": 128, "verifier_skeleton": 36, "branch_scaffold": 149},
                   "verify_gateA": {"dps": ["60"], "checks_positive_weights": False, "checks_orientations": False, "float_keys": 3, "rounds_the_lower": True,
                                    "tolerance": ["1e-15"]},
                   "gateB_scaffold": {"S_A": ["0.0088366789091384"], "inflation": False, "injected": True},
                   "emitter": {"S_A": ["0.0088366"], "T": ["0.19394974887230254", "0.19711758544561647"], "injected": True},
                   "verifier_skeleton": {"executable_lines": 0}, "branch_scaffold": {"weights": 5, "injected": True}},
}


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


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


def w1_gate_a(w):
    """Cycle 04's certificate, re-enclosed: every orientation present once; every triple's gaps below pi; the
    least lower bound, its orientation, the bridge pi / 7P and the certified margin; the file's own records (the
    'intervals' have no width) against the enclosures"""
    g, cert = w["gate_a"], w["cert"]
    rows = g["rows"]
    least = min(rows, key=lambda r: r["lo"])
    over = [float(r["recorded"] - r["lo"]) for r in rows if r["recorded"] > r["lo"]]
    got = {"orientations_complete": [r["p"] for r in rows] == list(range(g["P"])), "all_gaps_below_pi": all(r["positive"] for r in rows),
           "width": sig(float(max(r["hi"] - r["lo"] for r in rows)), 1), "least": sig(float(least["lo"]), 15), "at": least["p"],
           "half_gap": sig(float(g["half_gap"][1]), 15), "certified": sig(float(least["lo"] - g["half_gap"][1]), 15),
           "file_degenerate": all(x["interval_lower"] == x["interval_upper"] for x in cert["witnesses"]),
           "file_above_enclosure": [len(over), sig(max(over), 1) if over else 0.0],
           "file_agrees": max(abs(float(r["recorded"] - r["lo"])) for r in rows) < 1e-17,
           "file_least": [cert["minimum_sample_orientation_index"] == least["p"],
                          abs(Fraction(Decimal(cert["certified_global_lower"])) - (least["lo"] - g["half_gap"][1])) < Fraction(1, 10 ** 17)]}
    w["w1"] = got
    ok = got["orientations_complete"] and got["all_gaps_below_pi"] and least["lo"] - g["half_gap"][1] > Fraction(S_A)
    return [] if ok and got == w["gate_a_claim"] else [f"Gate A: {got}"]


def w2_conservatism(w):
    """the certificate's lower bound at each sampled orientation against the true margin there (B7 itself, the
    exact supports, the translation optimized): it must lie below, and how far"""
    rows = {r["p"]: r for r in w["gate_a"]["rows"]}
    tm = w["search"]["true_margins"]
    loss = [lo - float(rows[int(p)]["hi"]) for p, (lo, up) in tm.items()]
    got = {"orientations": len(tm), "below": all(x > 0 for x in loss), "least_loss": sig(min(loss), 3), "largest_loss": sig(max(loss), 3),
           "true_at_least": sig(tm[str(w["cert"]["minimum_sample_orientation_index"])][0], 10)}
    w["w2"] = got
    return [] if got["below"] and got == w["conservatism_claim"] else [f"Gate A's conservatism: {got}"]


def w3_quotient(w):
    """Cycle 05: the six D3 images of random placements have the same hull area; the turn of B5 maps by +4 pi/15
    and reflection, so [0, pi/15] is a fundamental interval; the branch holding the seed is first ORBIT-COVERED at
    depth 31; the safe constant's arithmetic"""
    c = w["spec"]["constants"]
    got = {"invariance": sig(w["search"]["d3"], 1), "step": str(Fraction(2, 3) % Fraction(2, 5)), "fundamental": str(Fraction(2, 5) / 6),
           "depth": w["orbit_depth"], "safe": [str(Decimal("0.00927495") - Decimal("0.000438281")), str(Decimal("0.008836669") - Decimal("0.0088366"))],
           "spec_T_inward_ulps": [round((t_bound(3, A3) - c["T3"]) / math.ulp(c["T3"])), round((t_bound(5, A3) - c["T5"]) / math.ulp(c["T5"]))],
           "spec_rho_max": c["rho_max"] == math.pi / 15, "spec_R5": c["R5"] == rn(5), "spec_status": w["spec"]["proof_status"]}
    w["w3"] = got
    return [] if got["invariance"] < 1e-12 and got == w["quotient_claim"] else [f"Cycle 05's quotient: {got}"]


def w4_anchor(w):
    """Cycle 06 sec. 1-6: the seed's residual turn and heights, the bound on d_H(U0, U_sym) against its true value,
    U_sym's area, the new radius, and the orbit copies' distance"""
    v0, a = w["v0"], w["anchor"]
    t6 = gate.squash(w["texts"][6])
    m = re.search(r"d_H\(U_0,U_{\\mathrm{sym}}\)<([0-9.]+)\\times10\^\{(-\d+)\}", t6)
    bound = float(m.group(1)) * 10 ** int(m.group(2))
    turn0 = v0[2] % PER5
    got = {"turn": sig(turn0, 5), "heights": [abs(v0[1]) < 4e-8, abs(v0[4]) < 3.9e-6],
           "bound": [sig(abs(v0[4]) + 2 * rn(5) * math.sin(turn0 / 2), 4), bound], "true_hausdorff": sig(a["hausdorff"], 4),
           "area_sym": sig(a["area_sym"], 12), "sym_below_seed": bool(a["area_sym"] < a["area_seed"]),
           "radius": str(Decimal("0.0088366") - Decimal("0.0000166")), "copies": sig(2 * rn(5) * math.sin(math.pi / 30), 12)}
    w["w4"] = got
    return [] if a["hausdorff"] < bound and got == w["anchor_claim"] else [f"Cycle 06's anchor: {got}"]


def w5_far(w):
    """the far branches, searched with the exact hull: each is an upper bound on its branch minimum. Against the
    cycles' candidates; every one still above A3+"""
    F = w["search"]["far"]
    orb = orbit(w["v0"])
    got = {k: sig(v["area"], 12) for k, v in F.items()}
    got["gaps"] = {k: sig(v["area"] - A3, 6) for k, v in F.items()}
    got["cycle06_minus_mine"] = [sig(0.834968965913228 - F["F3"]["area"], 2), sig(0.834804245410142 - F["F5"]["area"], 2)]
    got["cycle04_minus_mine"] = sig(0.834804245159 - min(F["C04_F3"]["area"], F["C04_F5"]["area"]), 2)
    got["all_above_A3"] = all(v["area"] > A3 for v in F.values())
    w["w5"] = got
    return [] if got["all_above_A3"] and got == w["far_claim"] else [f"the far sets: {got}"]


def w6_boxes(w):
    """Cycle 06 sec. 15-17: no sampled point falls outside its box's distance bounds, and the farthest-corner bound
    never exceeds the exact hull at a sampled point"""
    b = w["search"]["boxes"]
    got = {"violations": b["violations"], "samples": b["samples"], "corner_bound_below": bool(b["corner_bound_excess"] < 0)}
    w["w6"] = got
    return [] if not b["violations"] and got == w["box_claim"] else [f"Cycle 06's box bounds: {got}"]


def w7_crystals(w):
    """the three state crystals against the numbers rebuilt here"""
    c4, c5, c6 = (w["crystals"][i] for i in (4, 5, 6))
    g = w["gate_a"]
    least = min(r["lo"] for r in g["rows"])
    F = w["search"]["far"]
    ga, gb, anc = c4["gate_A"], c4["gate_B"], c6["symmetric_anchor"]
    got = {"C04": [abs(Fraction(ga["sample_lower"]) - least) < Fraction(1, 10 ** 17), ga["orientation_loss"] == float(g["half_gap"][1]),
                   abs(ga["certified_global_lower"] - float(least - g["half_gap"][1])) <= 2 * math.ulp(ga["certified_global_lower"]),
                   (ga["orientation_grid_P"], ga["support_grid_M"]) == (g["P"], g["M"]),
                   sig(gb["search_candidate"] - min(F["C04_F3"]["area"], F["C04_F5"]["area"]), 2)],
           "C05": [c5["gate_A"]["safe_lower"] == S_A, c5["gate_B"]["symmetry_quotient"], c5["representative_branch_probe"]["orbit_covered_depth"] == w["orbit_depth"],
                   sig(c5["domain_reduction"]["combined_naive_coordinate_volume_factor"], 10)],
           "C06": [anc["x3"] == w["v0"][0], anc["x5"] == w["v0"][3], anc["gateA_margin_safe"] == S_SYM, sig(anc["numerical_area_search"] - w["anchor"]["area_sym"], 1),
                   sig(c6["search_evidence"]["F3_min_candidate"] - F["F3"]["area"], 2), sig(c6["search_evidence"]["F5_min_candidate"] - F["F5"]["area"], 2)]}
    w["w7"] = got
    return [] if got == w["crystal_claim"] else [f"the crystals: {got}"]


def w8_code(w):
    """the scripts, read after the rebuild and never run"""
    sq = {k: gate.squash(t) for k, t in w["code"].items()}
    body = lambda t: [l for l in re.sub(r'"""[\s\S]*?"""', "", t).splitlines() if l.strip() and not l.strip().startswith("#")]
    got = {"lines": {k: t.count("\n") for k, t in w["code"].items()},
           "verify_gateA": {"dps": re.findall(r"mp\.iv\.dps=(\d+)", sq["verify_gateA"]), "checks_positive_weights": bool(re.search(r"s[123]\.a>0|s[123]>0", sq["verify_gateA"])),
                            "checks_orientations": "range(P)" in sq["verify_gateA"] or "len(cert[\"witnesses\"])" in sq["verify_gateA"],
                            "float_keys": sq["verify_gateA"].count("key=lambdaz:float(z)"), "rounds_the_lower": "x=float(v.a)" in sq["verify_gateA"],
                            "tolerance": re.findall(r"global_lower\+(1e-\d+)<declared", sq["verify_gateA"])},
           "gateB_scaffold": {"S_A": re.findall(r"S_A=([0-9.]+)", sq["gateB_scaffold"]), "inflation": "EPS" in sq["gateB_scaffold"],
                              "injected": "defcertify(root,beta_lower" in sq["gateB_scaffold"]},
           "emitter": {"S_A": re.findall(r"S_A=([0-9.]+)", sq["emitter"]), "T": re.findall(r"T[35]=([0-9.]+)", sq["emitter"]),
                       "injected": "defemit(area_lower" in sq["emitter"]},
           "verifier_skeleton": {"executable_lines": len(body(w["code"]["verifier_skeleton"]))},
           "branch_scaffold": {"weights": sq["branch_scaffold"].count("1.5*"), "injected": "defcertify_branch(root,branch,area_lower" in sq["branch_scaffold"]}}
    w["w8"] = got
    return [] if got == w["code_facts"] else [f"the scripts: {got}"]


def p1_package(w):
    """each VALIDATION's digests and document record against the bytes hashed here and the archive's manifest;
    the Cycle 05 dependency copies byte-identical to Cycle 04's files"""
    out, files, rows = [], w["files"], w["manifest_rows"]
    by_name = {k.split("!/")[-1]: k for k in files}
    sha = lambda name: hashlib.sha256(files[by_name[name]]).hexdigest()

    def doc_ok(rec):
        b = files[by_name[rec["file"]]]
        t = b.decode("utf-8")
        mine = {"sha256": hashlib.sha256(b).hexdigest(), "bytes": len(b), "lines": len(t.split("\n")),
                "delims": t.count("$$") % 2 == 0 and t.replace("$$", "").count("$") % 2 == 0 and not re.search(r"\\\[|\\\]|\\\(|\\\)", t)}
        return (rec["sha256"], rec["bytes"], rec["lines"], rec["canonical_math_delimiters"]) == (mine["sha256"], mine["bytes"], mine["lines"], mine["delims"]) \
            and rows[by_name[rec["file"]]][2] == mine["sha256"]

    v4, v5, v6 = (w["validations"][i] for i in (4, 5, 6))
    checks = {"C04 paper": doc_ok(v4["paper"]), "C04 certificate": v4["certificate"]["sha256"] == sha(v4["certificate"]["file"])
              and v4["certificate"]["witness_count"] == len(w["cert"]["witnesses"]),
              "C04 verifier": v4["gateA_verifier"]["sha256"] == sha(v4["gateA_verifier"]["file"]),
              "C04 scaffold": v4["gateB_scaffold"]["sha256"] == sha(v4["gateB_scaffold"]["file"]), "C04 state": v4["state"]["sha256"] == sha(v4["state"]["file"]),
              "C05 paper": doc_ok(v5["canonical_source"]), "C05 spec": v5["spec_sha256"] == sha(SPEC.split("!/")[-1]),
              "C05 emitter": v5["emitter_sha256"] == sha(CODE["emitter"].split("!/")[-1]),
              "C05 verifier": v5["verifier_sha256"] == sha(CODE["verifier_skeleton"].split("!/")[-1]),
              "C05 state": v5["state_sha256"] == sha(CRYSTALS[5].split("!/")[-1]),
              "C06 paper": doc_ok(v6["paper"]), "C06 runtime": v6["runtime_sha256"] == sha(CODE["branch_scaffold"].split("!/")[-1]),
              "C06 state": v6["state_sha256"] == sha(CRYSTALS[6].split("!/")[-1]),
              "statuses": all(v["status"] == "PASS" for v in (v4, v5, v6)),
              "copies": all(files[a] == files[b] for a, b in COPIES.items())}
    out += [k for k, ok in checks.items() if not ok]
    w["p1"] = checks
    return out


CHECKS = {"A0": a0_anchors, "W1": w1_gate_a, "W2": w2_conservatism, "W3": w3_quotient, "W4": w4_anchor, "W5": w5_far, "W6": w6_boxes,
          "W7": w7_crystals, "W8": w8_code, "P1": p1_package}
DEPENDS = {"A0": {"texts"}, "W1": {"gate_a", "cert", "gate_a_claim"}, "W2": {"gate_a", "search", "cert", "conservatism_claim"},
           "W3": {"search", "orbit_depth", "spec", "quotient_claim"}, "W4": {"v0", "anchor", "texts", "anchor_claim"},
           "W5": {"search", "v0", "far_claim"}, "W6": {"search", "box_claim"}, "W7": {"crystals", "gate_a", "search", "v0", "orbit_depth", "anchor", "crystal_claim"},
           "W8": {"code", "code_facts"}, "P1": {"validations", "files", "manifest_rows", "cert"}}


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

    texts, s, g = base["texts"], base["search"], base["gate_a"]
    crlf = {i: t.replace("\n", "\r\n") for i, t in texts.items()}
    first_true = next(iter(s["true_margins"]))
    return [
        ("K0-unmodified", "control", {}, set()),
        ("K1-crlf", "control", {"texts": crlf, "code": {k: t.replace("\n", "\r\n") for k, t in base["code"].items()}}, set()),
        ("K2-validation-keys-sorted", "control", {"validations": {i: json.loads(json.dumps(v, sort_keys=True)) for i, v in base["validations"].items()}}, set()),
        ("M1-least-lower-text", "mutation", {"texts": {**texts, 4: texts[4].replace("0.0092749591342486.", "0.0092749591342487.")}}, {"A0"}),
        ("M2-witness-missing", "mutation", {"gate_a": {**g, "rows": [r for r in g["rows"] if r["p"] != 500]}}, {"W1"}),
        ("M3-weight-negative", "mutation", {"gate_a": {**g, "rows": [{**r, "positive": r["p"] != 12} for r in g["rows"]]}}, {"W1"}),
        ("M4-true-below", "mutation", {"search": edit(s, lambda x: x["true_margins"].update({first_true: [0.0, 0.0]}))}, {"W2"}),
        ("M5-d3-broken", "mutation", {"search": edit(s, lambda x: x.update(d3=1e-9))}, {"W3"}),
        ("M6-orbit-depth", "mutation", {"orbit_depth": 32}, {"W3", "W7"}),
        ("M7-sym-area", "mutation", {"anchor": {**base["anchor"], "area_sym": base["anchor"]["area_sym"] + 1e-10}}, {"W4", "W7"}),
        ("M8-hausdorff-text", "mutation", {"texts": {**texts, 6: texts[6].replace("1.66\\times10^{-5}.\n}", "1.26\\times10^{-5}.\n}")}}, {"A0", "W4"}),
        ("M9-far-below", "mutation", {"search": edit(s, lambda x: x["far"]["F5"].update(area=0.8347))}, {"W5", "W7"}),
        ("M10-box-violation", "mutation", {"search": edit(s, lambda x: x["boxes"].update(violations=1))}, {"W6"}),
        ("M11-crystal-radius", "mutation", {"crystals": edit(base["crystals"], lambda x: x[6]["symmetric_anchor"].update(gateA_margin_safe=0.00883))}, {"W7"}),
        ("M12-verifier-dps", "mutation", {"code": {**base["code"], "verify_gateA": base["code"]["verify_gateA"].replace("mp.iv.dps = 60", "mp.iv.dps = 30")}}, {"W8"}),
        ("M13-validation-digest", "mutation", {"validations": edit(base["validations"], lambda x: x[4]["certificate"].update(sha256="0" * 64))}, {"P1"}),
        ("M14-copy-bytes", "mutation", {"files": {**base["files"], next(iter(COPIES)): base["files"][next(iter(COPIES))] + b" "}}, {"P1"}),
    ]


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 {**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", "w7", "w8", "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-045", "subject": "UESFCM Cycles 04-06: Gate A's dual certificate, the symmetry quotient, the symmetric anchor and the far branches",
           "documents": list(DOCS.values()), "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "w6", "w7", "w8", "p1")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8")


if __name__ == "__main__":
    main()