"""RUN-006 - Round 03: the fixed-cover placement certificate. For a fixed candidate cover U, Round 03 turns the placement quantifiers min over Q in O(2), min over t, max over theta into finite data: two reflection branches x P orientations x M-direction linear programs, with explicit errors rho_P (orientation, lower side only) and eta_M (support direction, upper side only), and merges them with Round 02's shape dictionary. Its theorems are read in the report. Here the linear programs are solved independently (HiGHS via scipy), the error constants recomputed, the bracket put under attack on random instances, and the sanity example of sec. 30 reproduced. Checks A0 anchors the formulas below occur in Round 03 as written A1 citations its one new reference (Rockafellar) exists B1 reflection Q_{sigma,phi} = R_phi S^{(1-sigma)/2} covers O(2); for sigma = -1, h_K(Q^T u_theta) = h_K(phi - theta), symbolically B2 duality on random instances, the grid LP's primal and dual values agree, an optimal dual vertex has 2 or 3 nonzero weights, and 2 means an antipodal pair weighted 1/2 each (sec. 6-7, 10-11) B3 translation the grid minimiser obeys ||t*_M|| <= 2L / cos(pi/M) (sec. 12) B4 bracket Theorem 17.1 under attack: for a coarse and a fine grid on the same instance, the two brackets [G - rho_P, G + eta_M] must intersect B5 constants eta_M, rho_P and the sec. 30 bracket recomputed from their formulas B6 sanity sec. 30 and the package's VALIDATION.json, from this tree's own LPs B7 width the sec. 30 margin is exactly -0.02: a lower bound from U's width for every placement, an upper bound by a placement found here B8 package the package's self-description of the document matches the archive R1 registry Round 03's judgments reviewed, first-used statuses defined Usage: python code/run006_round03_placement_certificate.py [--refresh] [--drill] [--blind CID] """ import argparse import datetime import json import math import re import numpy as np import sympy as sp from scipy.optimize import linprog import gate import registry from corpus import SOURCES, TREE, source_bytes, walk_sources PKG = "main.zip!/AMRAL_LUC_FC_Round_03_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_03_Placement_Certificate_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_03_v0.1.md" VALIDATION = PKG + "AMRAL_LUC_FC_Round_03_VALIDATION.json" SNAPSHOT = TREE / "data" / "external" / "round03-citations.json" LOG = TREE / "data" / "gate-logs" / "run006-round03-placement-certificate.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" ANCHORS = { "B1": [r"Q_{\sigma,\phi}=R_\phiS^{(1-\sigma)/2},", r"h_K(Q^Tu_\theta)=h_K(\phi-\theta)."], "B3": [r"\|t_M^\star\|\le\frac{2L}{\cos\Delta_\theta}.", r"\|t^\star_{\sigma,\phi}\|\le2L."], "B5": [r"\eta_M=L\left(1+\frac{2}{\cos(\pi/M)}\right)\frac{\pi}{M}.", r"\rho_P=R_K\frac{\pi}{P}\le\frac{\pi}{P}.", r"G_{M,P}-\rho_P\leM_U(K)\leG_{M,P}+\eta_M,"], "B6": [r"U=\left\{(x,y):\frac{x^2}{0.72^2}+\frac{y^2}{0.52^2}\le1\right\}.", r"r_K(\theta)=\frac12+0.22\cos3\theta+0.10\sin5\theta.", r"M=64,\qquadP=48."], "B1b": [r"FORsigmain{+1,-1}:"], } REFS = {4: {"kind": "crossref", "doi": "10.1515/9781400873173"}} CITE_OPTS = {4: {}} # ---------------------------------------------------------------- the geometry def body(coeffs): """centred constant-width support function from odd-mode coefficients {n: (a, b)} of r""" def h(theta): v = 0.5 * np.ones_like(theta, dtype=float) for n, (a, b) in coeffs.items(): v = v + (a * np.cos(n * theta) + b * np.sin(n * theta)) / (1 - n * n) return v return h def ellipse(a, b): return lambda theta: np.sqrt((a * np.cos(theta)) ** 2 + (b * np.sin(theta)) ** 2) def grid_margin(hK, hU, sigma, phi, M, law): """m_{sigma,M}(phi): the finite-grid LP, primal and dual, independently of any package code. law(sigma, phi, theta) gives the argument at which h_K is read for orientation (sigma, phi).""" th = 2 * np.pi * np.arange(M) / M a = hK(law(sigma, phi, th)) - hU(th) ux, uy = np.cos(th), np.sin(th) # primal: minimise z s.t. a_j + t.u_j <= z primal = linprog(c=[0, 0, 1], A_ub=np.stack([ux, uy, -np.ones(M)], axis=1), b_ub=-a, bounds=[(None, None)] * 3, method="highs") # dual: maximise sum lambda_j a_j s.t. lambda >= 0, sum lambda = 1, sum lambda u = 0 dual = linprog(c=-a, A_eq=np.stack([np.ones(M), ux, uy]), b_eq=[1, 0, 0], bounds=[(0, None)] * M, method="highs-ds") return {"primal": primal.fun, "t": primal.x[:2], "dual": -dual.fun, "lam": dual.x, "theta": th} def G(hK, hU, M, P, law): best = None for sigma in (+1, -1): for l in range(P): m = grid_margin(hK, hU, sigma, 2 * np.pi * l / P, M, law)["primal"] if best is None or m < best[0] - 1e-15: best = (m, sigma, l) return best def proper_law(sigma, phi, theta): return theta - phi if sigma == +1 else phi - theta # ---------------------------------------------------------------- checks TH, PH, X1, X2 = sp.symbols("theta phi x1 x2", real=True) def b1_reflection(w): out = [] R = lambda a: sp.Matrix([[sp.cos(a), -sp.sin(a)], [sp.sin(a), sp.cos(a)]]) S = sp.Matrix([[1, 0], [0, -1]]) u = lambda a: sp.Matrix([sp.cos(a), sp.sin(a)]) for sigma in (+1, -1): Q = R(PH) * S ** ((1 - sigma) // 2) if sp.simplify(Q.det() - sigma) != 0: out.append(f"sigma={sigma}: det Q is not sigma") v = sp.simplify(Q.T * u(TH)) target = u(w["law"](sigma, PH, TH)) if sp.simplify(v - target) != sp.zeros(2, 1): out.append(f"sigma={sigma}: Q^T u_theta is not u at the claimed angle") return out RNG_SEED = 20260924 def chiral_cover(R0, e2, a2, e3, a3): """a round cover without mirror symmetry: h = R0 + e2 cos(2t+a2) + e3 cos(3t+a3); convex because R0 > 3 e2 + 8 e3""" return lambda t: R0 + e2 * np.cos(2 * t + a2) + e3 * np.cos(3 * t + a3) def random_instances(n): """Three regimes, so that orientation and reflection actually matter somewhere: ellipses (their minimal width tends to bind for every orientation), round covers without mirror symmetry, and round covers with a strongly triangular target.""" rng = np.random.default_rng(RNG_SEED) out = [] for i in range(n): amp = lambda A: tuple(A * rng.uniform(0, 1) * np.array([np.cos(p), np.sin(p)]) for p in [rng.uniform(0, 2 * np.pi)])[0] coeffs = {3: amp(0.30), 5: amp(0.12), 7: amp(0.05)} # |r - 1/2| <= 0.47: legal regime = i % 3 if regime == 0: a, b = sorted(rng.uniform(0.52, 0.8, 2), reverse=True) out.append((coeffs, ellipse(float(a), float(b)), 0.0 + float(a))) else: R0 = float(rng.uniform(0.52, 0.6)) e2, e3 = float(rng.uniform(0, 0.02)), float(rng.uniform(0, 0.01)) hU = chiral_cover(R0, e2, float(rng.uniform(0, 6.3)), e3, float(rng.uniform(0, 6.3))) out.append((coeffs, hU, R0 + e2 + e3)) return out def b2_duality(w): out, stats = [], {"lps": 0, "two": 0, "three": 0} for coeffs, hU, _ in random_instances(12): hK = body(coeffs) for sigma in (+1, -1): for phi in np.linspace(0, 2 * np.pi, 7, endpoint=False): r = grid_margin(hK, hU, sigma, phi, 96, w["law"]) stats["lps"] += 1 if abs(r["primal"] - r["dual"]) > 1e-9: out.append(f"primal {r['primal']:.12f} != dual {r['dual']:.12f}") nz = np.flatnonzero(r["lam"] > 1e-12) if len(nz) not in w["active_sizes"]: out.append(f"dual vertex with {len(nz)} nonzero weights") elif len(nz) == 2: stats["two"] += 1 i, j = nz if (j - i) % 96 != 48 or abs(r["lam"][i] - 0.5) > 1e-9: out.append("2-active dual witness is not an antipodal pair at 1/2") else: stats["three"] += 1 w["b2_stats"] = stats return out def b3_translation(w): out = [] for coeffs, hU, RU in random_instances(12): hK = body(coeffs) L = 1.0 + RU # R_K <= 1; R_U bounds max h_U for sigma in (+1, -1): for phi in np.linspace(0, 2 * np.pi, 5, endpoint=False): M = 64 r = grid_margin(hK, hU, sigma, phi, M, proper_law) if np.linalg.norm(r["t"]) > w["t_bound"](L, M) + 1e-12: out.append(f"||t*_M|| = {np.linalg.norm(r['t']):.4f} > bound {w['t_bound'](L, M):.4f}") return out def eta(L, M): return L * (1 + 2 / math.cos(math.pi / M)) * math.pi / M def b4_bracket(w): """necessary conditions of Theorem 17.1 on two grids of one instance: G_c - rho_c <= M_U(K) <= G_f + eta_f and G_f - rho_f <= M_U(K) <= G_c + eta_c.""" out, rows = [], [] for coeffs, hU, RU in random_instances(6): hK = body(coeffs) L = 1.0 + RU coarse, fine = (16, 12), (256, 96) Gc = G(hK, hU, *coarse, proper_law)[0] Gf = G(hK, hU, *fine, proper_law)[0] lo_c, hi_c = Gc - w["rho"](coarse[1]), Gc + w["eta"](L, coarse[0]) lo_f, hi_f = Gf - w["rho"](fine[1]), Gf + w["eta"](L, fine[0]) rows.append({"coarse": [lo_c, hi_c], "fine": [lo_f, hi_f]}) if max(lo_c, lo_f) > min(hi_c, hi_f) + 1e-12: out.append(f"brackets [{lo_c:.4f},{hi_c:.4f}] and [{lo_f:.4f},{hi_f:.4f}] are disjoint") w["b4_rows"] = rows return out def b5_constants(w): out = [] v = w["validation"]["sanity_check"] L = 1.0 + 0.72 checks = {"eta_support_upper_error": w["eta"](L, 64), "rho_orientation_lower_error": w["rho"](48)} for key, val in checks.items(): if abs(v[key] - val) > 1e-12: out.append(f"{key}: recorded {v[key]}, formula gives {val}") G0 = v["coarse_grid_G"] if abs(v["analytic_lower_bound_for_true_margin"] - (G0 - w["rho"](48))) > 1e-12: out.append("recorded lower bound is not G - rho_P") if abs(v["analytic_upper_bound_for_true_margin"] - (G0 + w["eta"](L, 64))) > 1e-12: out.append("recorded upper bound is not G + eta_M") return out SANITY_K = {3: (0.22, 0.0), 5: (0.0, 0.10)} def b6_sanity(w): out = [] v = w["validation"]["sanity_check"] hK, hU = body(SANITY_K), ellipse(0.72, 0.52) th = np.linspace(0, 2 * np.pi, 200001) r = 0.5 + 0.22 * np.cos(3 * th) + 0.10 * np.sin(5 * th) if not (r.min() > 0 and r.max() < 1): out.append("sanity target is not legal") Gc, sc, lc = G(hK, hU, 64, 48, w["law"]) Gr, sr, lr = G(hK, hU, 512, 192, w["law"]) w["b6"] = {"G_coarse": Gc, "coarse_sigma": sc, "coarse_index": lc, "G_reference": Gr, "reference_sigma": sr, "reference_index": lr, "r_range": [float(r.min()), float(r.max())]} for key, mine in (("coarse_grid_G", Gc), ("dense_reference_grid_value", Gr)): if abs(v[key] - mine) > 1e-9: out.append(f"{key}: recorded {v[key]}, recomputed {mine}") L = 1.72 if not (Gc - w["rho"](48) <= Gr + w["eta"](L, 512) and Gr - w["rho"](192) <= Gc + w["eta"](L, 64)): out.append("coarse and reference brackets disjoint") return out def b7_width(w): """For any placement, the antipodal pair along U's minor axis gives max(a(pi/2)+t_y, a(3pi/2)-t_y) >= (a(pi/2)+a(3pi/2))/2 = (1 - 2*0.52)/2 = -0.02, because h_K(v) + h_K(-v) = 1 for unit constant width. So M_U(K) >= -0.02. Above: a placement is found whose continuous margin is -0.02 up to the resolution of a dense theta sweep with local refinement.""" hK, hU = body(SANITY_K), ellipse(0.72, 0.52) lower = (1 - 2 * 0.52) / 2 best = None for sigma in (+1, -1): for l in range(0, 90): phi = 2 * np.pi * l / 90 r = grid_margin(hK, hU, sigma, phi, 2048, proper_law) if best is None or r["primal"] < best[0]: best = (r["primal"], sigma, phi, r["t"]) _, sigma, phi, t = best t = grid_margin(hK, hU, sigma, phi, 1 << 16, proper_law)["t"] # refine the translation n = 2_000_000 th = 2 * np.pi * np.arange(n) / n sampled = float(np.max(hK(proper_law(sigma, phi, th)) + t[0] * np.cos(th) + t[1] * np.sin(th) - hU(th))) # between samples the function rises by at most its angular Lipschitz constant times half a step lip = 1.72 + float(np.hypot(*t)) rigorous = sampled + lip * np.pi / n w["b7"] = {"lower_bound": lower, "sampled_margin_at_placement": sampled, "rigorous_upper_bound": rigorous, "sigma": sigma, "phi": phi, "t": [float(t[0]), float(t[1])]} out = [] if abs(lower - w["width_claim"]) > 1e-15: out.append(f"width bound {lower} != {w['width_claim']}") if not (lower - 1e-12 <= sampled and rigorous <= lower + w["width_tol"]): out.append(f"margin bracket [{lower:.9f}, {rigorous:.9f}] wider than {w['width_tol']}") return out def b8_package(w): out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf, text in (("round03", DOC, w["text"]), ("state_crystal", CRYSTAL, w["crystal"])): rec = v[key] _, size, digest = leaves[leaf] if rec["sha256"] != digest or rec["bytes"] != size: out.append(f"{key}: recorded sha256/bytes differ from the archive") if rec["double_dollar_count"] != text.count("$$"): out.append(f"{key}: recorded {rec['double_dollar_count']} $$, document has {text.count('$$')}") return out CHIRAL_K = {3: (0.30, 0.0), 5: (0.0, 0.12)} def b9_reflection_matters(w): """Why the reflection branch cannot be skipped. K is chiral; U is K's mirror image grown by eps. Reflected, K fits exactly with margin -eps (placement exhibited). Restricted to rotations and translations, Theorem 17.1's lower side, applied to the sigma = +1 branch alone, proves K does not fit - so a certificate that skipped sigma = -1 would report the wrong verdict for this pair.""" hK, eps = body(CHIRAL_K), w["b9_eps"] hU = lambda t: hK(-t) + eps th = np.linspace(0, 2 * np.pi, 100001) a = hK(w["law"](-1, 0.0, th)) - hU(th) reflected_fit = float(np.max(np.abs(a + eps))) RK = float(np.max(hK(th))) + (2 * np.pi / 100000) / 2 # h_K is 1-Lipschitz in angle P, M = 720, 512 Gp = min(grid_margin(hK, hU, +1, 2 * np.pi * l / P, M, w["law"])["primal"] for l in range(P)) lower = Gp - RK * np.pi / P w["b9"] = {"eps": eps, "reflected_placement_residual": reflected_fit, "R_K": RK, "G_proper_only": Gp, "rho_P": RK * np.pi / P, "proper_only_lower_bound": lower} out = [] if reflected_fit > 1e-12: out.append(f"the reflected placement does not give margin -eps exactly (residual {reflected_fit:.2e})") if not lower > 0: out.append(f"proper motions alone are not certified to fail (lower bound {lower:.6f})") return out # ---------------------------------------------------------------- registry (Round 03) R03_DEFINITIONS = { "EXPLICIT": ("contextual", "the reflection branch is enumerated as its own discrete case (sec. 3, 16, 29)"), "R01-CORRECTION-001": ("not-a-status", "the identifier of the correction sec. 8 records against Round 01 sec. 22"), "RECORDED": ("contextual", "the correction is recorded without overwriting Round 01 (Round 00 sec. 23.1)"), } PBCT = "PASS by cited theorem" R03_REVIEWS = [ ("PROVED", "Continuous translation dual", "analytic", PBCT, "Thm 6.1; subdifferential of a max of affine maps + Caratheodory; B2 on instances"), ("PROVED", "Finite support LP", "analytic", PBCT, "sec. 10-11; LP duality; B2"), ("PROVED", "Support-grid error", "analytic", PBCT, "sec. 12-13; R_K <= 1 rests on the Steiner point; B3, B5"), ("PROVED", "Orientation Lipschitz", "analytic", PBCT, "sec. 15"), ("PROVED", "Full placement bracket", "analytic", PBCT, "Thm 17.1; B4 attacks it on instances, no violation"), ("PROVED", "Shape + placement fixed-cover certificate", "analytic", PBCT, "sec. 20-23"), ("PASS", "SANITY", "computation", "PASS", "sec. 30 reproduced (B6), but the example's margin is -0.02 at every orientation in both branches: " "it cannot detect an orientation or reflection error (B7)"), ("PASS", "Numerical sanity", "computation", "PASS", "= SANITY"), ("CLOSED", "FIXED-COVER FINITE CERTIFICATE SCHEMA", "analytic", PBCT, "sec. 17-29"), ("COMPUTE-DEFERRED", "C03-4：Independent verifier", "n/a", "n/a", "C03-1..4 correctly deferred"), ("OPEN", "GLOBAL LEBESGUE OPTIMIZATION", "n/a", "n/a", ""), ("OPEN", "Global problem", "n/a", "n/a", ""), ("NONE", "New Lebesgue bound", "reading", "PASS", "none claimed"), ("EXPLICIT", "Reflection branch", "analytic", "PASS", "sec. 3 law (B1); both branches enumerated in sec. 16 and 29"), ("R01-CORRECTION-001", "", "reading", "PASS", "the correction is right; RUN-004 reached it independently"), ("RECORDED", "Round 01 active-branch correction", "reading", "PASS", ""), ] def r1_registry(w): return registry.completeness(w["registry"], "R03", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "A1": gate.citations_check(CITE_OPTS), "B1": b1_reflection, "B2": b2_duality, "B3": b3_translation, "B4": b4_bracket, "B5": b5_constants, "B6": b6_sanity, "B7": b7_width, "B8": b8_package, "B9": b9_reflection_matters, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "A1": {"text", "snapshot"}, "B1": {"law"}, "B2": {"law", "active_sizes"}, "B3": {"t_bound"}, "B4": {"rho", "eta"}, "B5": {"validation", "rho", "eta"}, "B6": {"validation", "law", "rho", "eta"}, "B7": {"width_claim", "width_tol"}, "B8": {"validation", "text", "crystal", "manifest"}, "B9": {"law", "b9_eps"}, "R1": {"registry", "definitions", "reviews"}} def claims(): return { "law": proper_law, # sec. 3: theta - phi, or phi - theta for sigma = -1 "active_sizes": {2, 3}, # sec. 7 "t_bound": lambda L, M: 2 * L / math.cos(math.pi / M), # sec. 12 "eta": eta, # sec. 13 "rho": lambda P: math.pi / P, # sec. 17, with R_K <= 1 "width_claim": -0.02, "width_tol": 1e-5, "b9_eps": 0.002, } def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, VALIDATION} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} return (got[DOC].decode("utf-8"), got[CRYSTAL].decode("utf-8"), json.loads(got[VALIDATION]), json.loads(MANIFEST.read_text(encoding="utf-8"))) def main(): ap = argparse.ArgumentParser() ap.add_argument("--refresh", action="store_true") ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() if args.refresh: recs = {str(n): gate.fetch_crossref(doi=r["doi"]) for n, r in REFS.items()} SNAPSHOT.write_text(json.dumps({"retrieved": datetime.date.today().isoformat(), "records": recs}, ensure_ascii=False, indent=1) + "\n", encoding="utf-8") snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8")) text, crystal, validation, manifest = load_inputs() def build(): return {"text": text, "crystal": crystal, "validation": json.loads(json.dumps(validation)), "manifest": manifest, "snapshot": json.loads(json.dumps(snapshot)), "registry": registry.load(), "definitions": dict(R03_DEFINITIONS), "reviews": list(R03_REVIEWS), **claims()} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {c: fn(w) for c, fn in CHECKS.items()} for c, f in results.items(): print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n {x}" for x in f[:6])) print("B2", w.get("b2_stats"), "| B6", w.get("b6"), "| B7", w.get("b7"), "| B9", w.get("b9")) if not args.drill: return # only a drill run writes the log val = validation["sanity_check"] sanity = lambda key, value: {"validation": {**validation, "sanity_check": {**val, key: value}}} pkg = lambda key, field, value: {"validation": {**validation, key: {**validation[key], field: value}}} rec = snapshot["records"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-law-rewritten", "control", {"law": lambda s, p, t: s * (t - p)}, set()), ("K2-eta-as-secant", "control", {"eta": lambda L, M: L * (1 + 2 * (1 / math.cos(math.pi / M))) * math.pi / M}, set()), ("K3-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K4-record-float-noise", "control", sanity("coarse_grid_G", val["coarse_grid_G"] + 1e-15), set()), ("M1-reflection-law-ignored", "mutation", {"law": lambda s, p, t: t - p}, {"B1", "B9"}), ("M2-both-branches-reflected", "mutation", {"law": lambda s, p, t: p - t}, {"B1", "B9"}), ("M3-only-3-active", "mutation", {"active_sizes": {3}}, {"B2"}), ("M4-translation-bound-tiny", "mutation", {"t_bound": lambda L, M: 1e-6}, {"B3"}), ("M5-eta-missing-factor", "mutation", {"eta": lambda L, M: L * (1 + 1 / math.cos(math.pi / M)) * math.pi / M}, {"B5"}), ("M6-rho-halved", "mutation", {"rho": lambda P: math.pi / (2 * P)}, {"B5"}), # added after blinding B4 found no plant naming it: with no error terms the two # brackets collapse to the two grid values, which differ - on the random instances # (B4), and on the sanity instance too, where they differ in the last bit (B6) ("M6b-errors-dropped", "mutation", {"rho": lambda P: 0.0, "eta": lambda L, M: 0.0}, {"B4", "B5", "B6"}), ("M7-recorded-G", "mutation", sanity("coarse_grid_G", -0.03), {"B5", "B6"}), ("M8-recorded-reference", "mutation", sanity("dense_reference_grid_value", -0.021), {"B6"}), ("M9-width-claim", "mutation", {"width_claim": -0.03}, {"B7"}), ("M10-eps-too-large", "mutation", {"b9_eps": 0.006}, {"B9"}), ("M11-doc-eta-edited", "mutation", {"text": text.replace(r"\frac{2}{\cos(\pi/M)}", r"\frac{1}{\cos(\pi/M)}")}, {"A0"}), ("M12-package-sha", "mutation", pkg("round03", "sha256", "0" * 64), {"B8"}), ("M13-ref-title", "mutation", {"snapshot": {**snapshot, "records": {**rec, "4": {**rec["4"], "title": "Convex Geometry"}}}}, {"A1"}), ("M14-review-dropped", "mutation", {"reviews": list(R03_REVIEWS[1:])}, {"R1"}), ("M15-definition-dropped", "mutation", {"definitions": {k: v for k, v in R03_DEFINITIONS.items() if k != "EXPLICIT"}}, {"R1"}), ] if args.blind: # only the plants naming the blinded check decide whether the drill sees it 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-006", "subject": "Round 03: the fixed-cover placement certificate", "document": DOC, "snapshot_retrieved": snapshot["retrieved"], "rng_seed": RNG_SEED, "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, "b2_stats": w.get("b2_stats"), "b4_rows": w.get("b4_rows"), "b6": w.get("b6"), "b7": w.get("b7"), "b9": w.get("b9"), "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("R03", "RUN-006", R03_DEFINITIONS, R03_REVIEWS) print(f"registry: {len(R03_DEFINITIONS)} definitions, {len(R03_REVIEWS)} reviews recorded for R03") if __name__ == "__main__": main()