"""RUN-049 - UESFCM Cycles 15-17: root 6217's boundary locking, its upper references, and the competitive-core closures. Cycle 15 rejects global radial monotonicity out of the F3 circle, proves radial convexity for fixed boundary parameters (Fary-Redei), certifies an explicit feasible upper reference A_ref = 0.835 by a 20,000-direction outer polygon, and proves a two-colour boundary-locking criterion (SECANT-LOCKED, AREF-PRUNED). Cycle 16 tightens the reference to 0.8349865 by a padded 500,000-direction polygon, adds a local-secant lemma, and restricts the responsibility to the 68 open cells. Cycle 17 closes five of them against the tight reference with a bit-tree certificate, and two (131, 129) against A3+ with hierarchical prefix-tree certificates: 68 -> 61. Here the lemmas are read, the upper references rebuilt (the 20,000-direction polygon also at 50 digits), the secant diagnostics recomputed, and all three certificates replayed as in RUN-047: decoded, every leaf's witness bound rebuilt, every area leaf certified in exact arithmetic with this tree's exact eroded cores. Checks A0 anchors the numbers below occur in the three documents as written W1 lemmas radial convexity along random rays; Cycle 15's radial counterexample W2 references the outer polygons of Cycles 15 and 16 against the exact hull, with and without the hand-over normals W3 secants the secant diagnostics at the contact and on Cycle 12's profile; the samples below the tight reference W4 aref5 Cycle 17's five-tree certificate against 0.8349865: decoded, the witness bound, exact certification W5 hierarchy roots 131 and 129: the tries prefix-free and complete, the leaf boxes, the witness bound, exact W6 ledger 76 -> 68 -> 61; the 68-cell search diagnostic; the share of root 6217 closed only in search W7 crystals the three state crystals W8 code the four verifiers, read after the rebuild and never run P1 package the VALIDATION records; the dependency copies Usage: python code/run049_uesfcm_cycles_15_17.py [--drill] [--blind CID] """ import argparse import base64 import copy import hashlib import inspect import io import json import math import re from fractions import Fraction from multiprocessing import Pool import mpmath import numpy as np import gate import run030_round27_interval_replay as r30 import run044_uesfcm_cycles_01_03 as r44 import run046_uesfcm_cycles_07_09 as r46 import run047_uesfcm_cycles_10_11 as r47 import run048_uesfcm_cycles_12_14 as r48 from corpus import SOURCES, TREE, source_bytes, walk_sources FOLDER = "main.zip!/UESFCM/" PKG = {i: FOLDER + f"UESFCM_Lebesgue_Cycle_{i:02d}_Package_v0.1.zip!/" for i in (7, 10, 11, 12, 14, 15, 16, 17)} DOCS = {15: PKG[15] + "UESFCM_Lebesgue_Cycle_15_Corrected_Boundary_Locking_v0.1.md", 16: PKG[16] + "UESFCM_Lebesgue_Cycle_16_Tight_Reference_and_Local_Secant_v0.1.md", 17: PKG[17] + "UESFCM_Lebesgue_Cycle_17_Hierarchical_Competitive_Core_Closure_v0.1.md"} DATA = {"aref15": PKG[15] + "UESFCM_Lebesgue_Cycle_15_Aref_Upper_Certificate.json", "diag15": PKG[15] + "UESFCM_Lebesgue_Cycle_15_Boundary_Locking_Diagnostic.json", "aref16": PKG[16] + "UESFCM_Lebesgue_Cycle_16_Tight_Aref_Certificate.json", "diag16": PKG[16] + "UESFCM_Lebesgue_Cycle_16_Tight_Sublevel_Diagnostic.json", "aref5": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Aref5_Certificate.json", "h131": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Root131_Hierarchical_Certificate.json", "h129": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Root129_Hierarchical_Certificate.json", "core": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Competitive_Core_Summary.json", "profile": PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_Rotation_Profile.json"} NPZ = {"remaining76": PKG[12] + "UESFCM_Lebesgue_Cycle_12_6217_Remaining_76_Roots.npz", "remaining61": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Remaining_61_Root6217_Cells.npz", "minsearch": PKG[17] + "UESFCM_Lebesgue_Cycle_17_68Cell_MinSearch_Diagnostic.npz", "frontier": PKG[7] + "UESFCM_Lebesgue_Cycle_07_F3_Unresolved_Frontier.npz", "two": PKG[11] + "UESFCM_Lebesgue_Cycle_11_TwoRoot_Hard_Frontier.npz"} CERT14 = PKG[14] + "UESFCM_Lebesgue_Cycle_14_RotationTail8_F3_Certificate.json" CODE = {15: PKG[15] + "UESFCM_Lebesgue_Cycle_15_Verify_Aref_Upper.py", 16: PKG[16] + "UESFCM_Lebesgue_Cycle_16_Verify_Tight_Aref.py", "17a": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Verify_Aref5.py", "17h": PKG[17] + "UESFCM_Lebesgue_Cycle_17_Verify_Hierarchical_F3.py"} COPIES = {PKG[16] + "dependencies/UESFCM_Lebesgue_Cycle_12_6217_Remaining_76_Roots.npz": NPZ["remaining76"], PKG[16] + "dependencies/UESFCM_Lebesgue_Cycle_14_Formal_Closure_Summary.json": PKG[14] + "UESFCM_Lebesgue_Cycle_14_Formal_Closure_Summary.json", PKG[17] + "dependencies/UESFCM_Lebesgue_Cycle_10_Verify_27Root_F3.py": PKG[10] + "UESFCM_Lebesgue_Cycle_10_Verify_27Root_F3.py"} CRYSTALS = {i: PKG[i] + f"UESFCM_Lebesgue_State_Crystal_Cycle_{i:02d}_v0.1.json" for i in (15, 16, 17)} VALIDATIONS = {i: PKG[i] + f"UESFCM_Lebesgue_Cycle_{i:02d}_VALIDATION.json" for i in (15, 16, 17)} LOG = TREE / "data" / "gate-logs" / "run049-uesfcm-cycles-15-17.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" CACHE = TREE / "data" / "cache" / "run049-searches.json" # data/cache is not committed A3, S_F3, X30, ETA = r47.A3, r47.S_F3, r47.X30, r47.ETA X3S = X30 - S_F3 AREF, AREF_TIGHT = 0.835, 0.8349865 X5S = "0.019770946347947549143855079363215531030154538977642259806485879349844408697473001" ROOT = 6217 WORKERS, CHUNK = 6, 1500 def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = (set(DOCS.values()) | set(DATA.values()) | set(NPZ.values()) | {CERT14} | set(CODE.values()) | set(COPIES) | set(COPIES.values()) | set(CRYSTALS.values()) | set(VALIDATIONS.values())) listing, got = [], {} for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want): listing.append(leaf.id) if d is not None: got[leaf.id] = d rows = {row[0]: row for row in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"]} npz = lambda k: {name: a.tolist() for name, a in np.load(io.BytesIO(got[NPZ[k]])).items()} # lists: the drill compares by == front = {name: a for name, a in np.load(io.BytesIO(got[NPZ["frontier"]])).items()} two = npz("two") sub = [i for i, p in enumerate(two["parent_root"]) if p == ROOT] return {"texts": {i: got[DOCS[i]].decode("utf-8") for i in DOCS}, "code": {i: got[CODE[i]].decode("utf-8") for i in CODE}, **{k: json.loads(got[v]) for k, v in DATA.items()}, **{k: npz(k) for k in ("remaining76", "remaining61", "minsearch")}, "cert14": json.loads(got[CERT14]), "root": [front["centers"][ROOT].tolist(), front["halfwidths"][ROOT].tolist()], "subroots": {"centers": [two["centers"][i] for i in sub], "halfwidths": [two["halfwidths"][i] for i in sub]}, "crystals": {i: json.loads(got[CRYSTALS[i]]) for i in CRYSTALS}, "validations": {i: json.loads(got[VALIDATIONS[i]]) for i in VALIDATIONS}, "packages": {i: sorted(x.split(PKG[i])[-1] for x in listing if x.startswith(PKG[i])) for i in (15, 16, 17)}, "files": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want}} # ---------------------------------------------------------------- the upper references def outer_polygon(pieces, th, pad=0.0): """the polygon of the supporting lines at the directions th, every support raised by pad (RUN-044's cancellation-free edge lengths, the sum exactly rounded)""" th = np.unique(np.mod(np.asarray(th, dtype=float), 2 * np.pi)) hv = r44.support(pieces)(th) + pad dn = np.roll(th, -1) - th dn[-1] += 2 * np.pi dp = th - np.roll(th, 1) dp[0] += 2 * np.pi ell = (np.roll(hv, -1) - hv + 2 * hv * np.sin(dn / 2) ** 2) / np.sin(dn) + (np.roll(hv, 1) - hv + 2 * hv * np.sin(dp / 2) ** 2) / np.sin(dp) return 0.5 * math.fsum((hv * ell).tolist()) def outer_mp(n_dir, dps=50): """Cycle 15's polygon at dps digits: at every direction the largest support over all seventeen pieces""" mp = mpmath.mp mp.dps = dps two_pi = 2 * mp.pi x3, x5 = mp.mpf("-0.01215883209899") - mp.mpf("0.00882"), mp.mpf(X5S) def piece(k): if k == 0: return (mp.mpf(0), mp.mpf(0)), mp.mpf(1) / 2, None n, x, off = (3, x3, 1) if k < 7 else (5, x5, 7) R = 1 / (2 * mpmath.cos(mp.pi / (2 * n))) j = (k - off) % n V = (x + R * mpmath.cos(two_pi * j / n), R * mpmath.sin(two_pi * j / n)) return (V, mp.mpf(0), None) if k - off < n else (V, mp.mpf(1), (two_pi * j / n + mp.pi, mp.pi / (2 * n))) pm = [piece(k) for k in range(17)] def sup(t): ct, st, best = mpmath.cos(t), mpmath.sin(t), None for (cx, cy), r, rg in pm: if rg is not None and abs((t - rg[0] + mp.pi) % two_pi - mp.pi) > rg[1]: continue val = cx * ct + cy * st + r best = val if best is None or val > best else best return best h = [sup(two_pi * k / n_dir) for k in range(n_dir)] d = two_pi / n_dir cd, sd = mpmath.cos(d), mpmath.sin(d) area = mpmath.fsum(h[k] * ((h[k - 1] - h[k] * cd) / sd + (h[(k + 1) % n_dir] - h[k] * cd) / sd) for k in range(n_dir)) / 2 out = mpmath.nstr(area, 45) mp.dps = 15 return out def outer_scan(): v = [X3S, 0.0, 0.0, float(X5S), 0.0] P = r44.base_pieces(v) ho = np.asarray(r44.handovers(P), dtype=float) uni = lambda n: 2 * np.pi * np.arange(n) / n return {"exact": float(r46.area(v)), "c15": outer_polygon(P, uni(20000)), "c15_mp": outer_mp(20000), "c16_padded": outer_polygon(P, uni(500000), 1e-8), "c16_bare": outer_polygon(P, uni(500000)), "handovers": len(ho), "c15_with_handovers": outer_polygon(P, np.concatenate([uni(20000), ho])), "c16_with_handovers": outer_polygon(P, np.concatenate([uni(500000), ho]))} # ---------------------------------------------------------------- the radial function and the secants def radial(rho, x5, y5, alpha, r): """f_q(r): B3 at t3^0 + r (cos alpha, sin alpha), B5 turned by rho at (x5, y5)""" return r48.area([X30 + r * math.cos(alpha), r * math.sin(alpha), rho, x5, y5], 16384) def secant_scan(profile, diag15, root): """at the contact: f(s), f(0), f(s - 1e-4) and the outward slope; on Cycle 12's 27 samples: f(s) - f(0); Cycle 15's counterexample: f(s), the outward slope, the least f on its ray inside the box; second differences of f along random rays""" out = {} q = (0.0, float(X5S), 0.0, math.pi) fs, f0, fm = radial(*q, S_F3), radial(*q, 0.0), radial(*q, S_F3 - 1e-4) out["contact"] = {"fs": fs, "f0": f0, "local": fs - fm, "slope": (radial(*q, S_F3 + 1e-6) - fs) / 1e-6} rows = [] for s in profile["samples"]: a = math.atan2(s["y3"], s["x3"] - X30) rows.append([s["rho"], radial(s["rho"], s["x5"], s["y5"], a, S_F3), radial(s["rho"], s["x5"], s["y5"], a, 0.0)]) out["profile"] = rows g = diag15["global_monotonicity_counterexample"] q = (g["rho5"], g["x5"], g["y5"], g["alpha"]) fs = radial(*q, S_F3) C, H = root hi_x3, hi_y3, lo_x3 = C[0] + H[0], C[1] + H[1], C[0] - H[0] ca, sa = math.cos(q[3]), math.sin(q[3]) ends = [t for t in ((lo_x3 - X30) / ca if ca < 0 else math.inf, (hi_x3 - X30) / ca if ca > 0 else math.inf, hi_y3 / sa if sa > 0 else math.inf)] rmax = min(ends) a, b, gr = S_F3, rmax, (math.sqrt(5) - 1) / 2 c1, c2 = b - gr * (b - a), a + gr * (b - a) f1, f2 = radial(*q, c1), radial(*q, c2) for _ in range(60): if f1 < f2: b, c2, f2 = c2, c1, f1 c1 = b - gr * (b - a) f1 = radial(*q, c1) else: a, c1, f1 = c1, c2, f2 c2 = a + gr * (b - a) f2 = radial(*q, c2) rmin = (a + b) / 2 out["counterexample"] = {"fs": fs, "forward": {str(h): (radial(*q, S_F3 + h) - fs) / h for h in (1e-7, 1e-5)}, "backward": (fs - radial(*q, S_F3 - 1e-7)) / 1e-7, "rmax": rmax, "rmin": rmin, "ray_min": min(fs, radial(*q, rmin))} rng = np.random.default_rng(15) worst = math.inf for _ in range(200): rho = rng.random() * 2 * H[2] x5, y5 = C[3] + H[3] * (2 * rng.random() - 1), C[4] + H[4] * (2 * rng.random() - 1) alpha, r = math.pi / 2 + rng.random() * math.pi / 2, 0.002 + rng.random() * 0.012 t = 5e-4 f = [radial(rho, x5, y5, alpha, r + k * t) for k in (-1, 0, 1)] worst = min(worst, (f[0] - 2 * f[1] + f[2]) / t ** 2) out["convexity"] = worst return out # ---------------------------------------------------------------- the certificates def hier_leaves(cert): """every leaf of a prefix-tree certificate: its type and its box, rebuilt from the root by Cycle 10's split""" out = [] for leaf in cert["leaves"]: c, h = list(cert["root"]["center"]), list(cert["root"]["halfwidth"]) for b in leaf["path"]: (c1, h1), (c2, h2), _ = r47.split(c, h) c, h = (c1, h1) if b == "0" else (c2, h2) out.append((leaf["type"], c, h)) return out def certified_leaves(task): """a chunk of area leaves certified in exact arithmetic against a threshold (RUN-047's certify, the directions raised until the leaf passes)""" label, leaves, threshold = task shift = Fraction(threshold) - r47.A3_EXACT out = {"label": label, "area": 0, "certified": 0, "failures": 0, "escalated": 0, "least": None} for c, h in leaves: out["area"] += 1 margin, used = None, None for n_dir in r47.DIRECTIONS: m, fail = r47.certify(c, h, n_dir) out["failures"] += fail if m is not None and m - shift > 0: margin, used = m - shift, n_dir break out["escalated"] += used != r47.DIRECTIONS[0] if margin is not None: out["certified"] += 1 if out["least"] is None or margin < Fraction(out["least"][0]): out["least"] = [f"{margin.numerator}/{margin.denominator}", c, h, used] return out def certificate_scan(aref5, h131, h129): """the witness bound on every leaf (against 0.8349865 for Aref5, A3+ for the prefix trees); the NOT-F3 boxes in exact rationals; then every area leaf certified in exact arithmetic on a pool""" groups = {} wit = {} thr5 = aref5["constants"]["THRESHOLD"] leaves5, per_tree = [], [] for t in aref5["trees"]: area, notf3 = r48.area_leaves(t, "c10") tl = math.inf for c, h, _ in area: v = r47.witness_bound(c, h)[0] - thr5 tl = min(tl, v) leaves5.append((c, h, v, t["frontier_index"])) per_tree.append([t["frontier_index"], tl]) groups.setdefault("aref5", []).extend((c, h) for c, h, _ in area) groups.setdefault("aref5_notf3", []).extend((c, h) for c, h, _ in notf3) least = min(leaves5, key=lambda x: x[2]) wit["aref5"] = {"leaves": len(leaves5), "failing": sum(x[2] - ETA <= 0 for x in leaves5), "least": [least[2], least[3]], "per_tree": per_tree} for name, cert in (("h131", h131), ("h129", h129)): rows = hier_leaves(cert) area = [(c, h) for ty, c, h in rows if ty == "A"] vals = [r47.witness_bound(c, h)[0] - A3 for c, h in area] wit[name] = {"leaves": len(area), "failing": sum(v - ETA <= 0 for v in vals), "least": min(vals)} groups[name] = area groups[name + "_notf3"] = [(c, h) for ty, c, h in rows if ty == "N"] notf3 = {} for name in ("aref5", "h131", "h129"): inside, least = 0, math.inf for c, h in groups[name + "_notf3"]: far2 = (abs(Fraction(c[0]) - r47.X30_EXACT) + Fraction(h[0])) ** 2 + (abs(Fraction(c[1])) + Fraction(h[1])) ** 2 inside += far2 < r47.S_EXACT ** 2 least = min(least, float(r47.S_EXACT ** 2 - far2) / (float(r47.S_EXACT) + math.sqrt(float(far2)))) notf3[name] = [len(groups[name + "_notf3"]), inside, least] tasks = [] for name, thr in (("aref5", str(thr5)), ("h131", "0.834781191"), ("h129", "0.834781191")): L = groups[name] tasks += [(name, L[k:k + CHUNK], thr) for k in range(0, len(L), CHUNK)] with Pool(WORKERS) as pool: rows = pool.map(certified_leaves, tasks, chunksize=1) exact = {} for name in ("aref5", "h131", "h129"): mine = [r for r in rows if r["label"] == name] lst = min((r["least"] for r in mine if r["least"]), key=lambda x: Fraction(x[0])) exact[name] = {k: sum(r[k] for r in mine) for k in ("area", "certified", "failures", "escalated")} exact[name]["least"] = [float(Fraction(lst[0])), lst[3]] return {"witness": wit, "notf3": notf3, "exact": exact} # ---------------------------------------------------------------- the ledger def minsearch_scan(ms): """the 68 cells' stored minimizers: the exact hull there, d3, and whether the point lies in its cell""" out = [] for c, h, sol in zip(ms["centers"], ms["halfwidths"], ms["sol"]): out.append({"area": r48.area(sol, 16384), "d3": math.hypot(sol[0] - X30, sol[1] - 0.0), "in_cell": all(abs(sol[i] - c[i]) <= h[i] * (1 + 1e-12) for i in range(5))}) return out def _key(name, fn, extra=""): 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[name]: digest.update(inspect.getsource(helper).encode()) for path in (r8.__file__, r9.__file__, r30.__file__): digest.update(open(path, "rb").read()) digest.update(extra.encode()) return digest.hexdigest() HELPERS = {"outer": (outer_polygon, outer_mp, r44.support, r44.handovers, r46.area), "secants": (radial, r48.area), "certificates": (hier_leaves, certified_leaves, r47.split, r47.certify, r47.witness_bound, r48.area_leaves, r48.decode), "minsearch": (r48.area,)} def searches(inputs): cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {} out = {} def get(name, fn, call, extra=""): key = _key(name, fn, extra) if cached.get(name, {}).get("key") != key: cached[name] = {"key": key, "value": call()} CACHE.parent.mkdir(parents=True, exist_ok=True) CACHE.write_text(json.dumps(cached, indent=1) + "\n", encoding="utf-8") out[name] = cached[name]["value"] tag = lambda *xs: hashlib.sha256(json.dumps(xs, sort_keys=True).encode()).hexdigest() get("outer", outer_scan, outer_scan) get("secants", secant_scan, lambda: secant_scan(inputs["profile"], inputs["diag15"], inputs["root"]), tag(inputs["profile"], inputs["diag15"], inputs["root"])) get("certificates", certificate_scan, lambda: certificate_scan(inputs["aref5"], inputs["h131"], inputs["h129"]), tag(inputs["aref5"], inputs["h131"], inputs["h129"])) get("minsearch", minsearch_scan, lambda: minsearch_scan(inputs["minsearch"]), tag(inputs["minsearch"])) return out def world(inputs): return {**inputs, "search": searches(inputs)} # ---------------------------------------------------------------- checks ANCHORS = { 15: {"W1": ["Itisfalse.", r"A(s,q)\approx0.83603912", r"\partial_r^+f_q(s)\approx-0.04569.", "`GLOBALRADIALMONOTONICITY:REJECTED`", "`RADIALCONVEXITYFORFIXEDq:PROVEDVIAFARY-REDEI`", "`TWO-COLOURBOUNDARY-LOCKINGCRITERION:PROVED`"], "W2": [r"A_{\mathrm{outer}}=0.8349939254427389050715183787649635047821<0.835.", "20{,}000", "`EXPLICITFEASIBLEA_REF<0.835:CERTIFIED`"], "W3": [r"\boxed{+0.0250.}", r"\boxed{9.88746\times10^{-6}.}", "`PROFILELOW-SUBLEVELMINSECANT:~9.887e-6`", "`LOW-SUBLEVELMINNUMERICALRADIALSLOPE:~+0.0250`"]}, 16: {"W2": [r"\boxed{500{,}000}", r"\boxed{10^{-8}}", r"\boxed{2\times10^{-8}}", r"\boxed{0.83498643461455335.}", r"A_{\mathrm{ref}}^{\mathrm{tight}}:=0.8349865.", r"\boxed{6.5385446698911637e-08.}", "paddedouterarea:0.83498641461455325", "`TIGHTA_REF:0.8349865`"], "W3": [r"f(s)-f(s-10^{-4})\approx3.27\times10^{-6},", r"\boxed{2/27}", r"\boxed{3.29\times10^{-5}.}", r"\approx-2.88\times10^{-5}.", "`27-POINTPROFILEBELOWTIGHTA_REF:2/27`"], "W6": ["Allotherregionshavealreadybeeneliminatedbyfinitecertificates.", "`FORMALREMAININGROOT6217CELLS:68`"]}, 17: {"W4": [r"\boxed{28,\36,\68,\144,\155.}", r"\boxed{61{,}487}", "30{,}467", r"\boxed{2.582831171160649\times10^{-9}>0.}", "`A_REF5CERTIFICATENODES:61487`"], "W5": [r"\boxed{40{,}859}", "38{,}893", "1{,}966", "40{,}858", r"\boxed{1.239644498163273\times10^{-9}>0.}", r"\boxed{48{,}590}", "46{,}151", "2{,}439", r"\boxed{6.127131246813633\times10^{-9}>0.}", "`ROOT131TERMINALLEAVES:40859`", "`ROOT129TERMINALLEAVES:48590`"], "W6": [r"\boxed{68\to61.}", r"\boxed{131,\129,\125,\152,\150.}", r"\boxed{0.8349862484449208.}", r"2.31\times10^{-6}", r"\boxed{125,\152,\150.}", "`FORMALREMAININGCELLS:61`"]}, } CLAIMS = { "lemma_claim": {"convexity": 2.9, "counterexample": [-2e-09, -0.04569, -0.04569, -0.04569, 0.093, 1.6e-07, 7.2e-09, 0.8360391072, 4e-10, True]}, "reference_claim": {"candidate": [True, True, 71], "c15": [8e-16, 43], "c16": [2e-15, 2e-15], "exact": 0.8349861105592, "true_slack": [1.389e-05, 3.894e-07], "excess": [7.8e-06, 2.7e-07, 3.3e-08], "with_handovers": [17, 3.1e-09, 4.9e-12]}, "secant_claim": {"contact": [3.27e-06, 3.8e-05, 0.213], "profile_low": [8, 9.88424e-06, -3e-09, 8], "below_tight": [2, 2, True]}, "aref5_claim": {"trees": [5, [28, 36, 68, 144, 155], []], "totals": [61487, 30467, 279], "witness": [30467, 0, 3.5828319e-09, 155, 3e-16], "exact": [30467, 30467, 0, 0, 2.656e-05], "notf3": [279, 279, 1.93e-06]}, "hierarchy_claim": {"h131": {"structure": [40859, 40859, 0, 40858, True, True], "types": [38893, 1966, 38893, 1966], "witness": [38893, 0, 1.2396455e-09], "exact": [38893, 38893, 0, 0, 3.022e-05], "notf3": [1966, 1966, 8.37e-06]}, "h129": {"structure": [48590, 48590, 0, 48589, True, True], "types": [46151, 2439, 46151, 2439], "witness": [46151, 0, 6.1271319e-09], "exact": [46151, 46151, 0, 0, 3.183e-05], "notf3": [2439, 2439, 8.37e-06]}}, "ledger_claim": {"ledger": [68, True, [28, 36, 68, 129, 131, 144, 155], True, True], "minsearch": [1e-15, 68, [[14, -6.5e-08], [28, -2.3e-12]], [131, 129, 125, 152, 150], True, True, [131], [131, 129, 125, 152, 150]], "outside_200": 0.4415}, "crystal_claim": {"C15": ["CLOSED", True, "OPEN"], "C16": [68, True], "C17": [68, True, True, True]}, "code_facts": {"lines": {15: 72, 16: 93, "17a": 91, "17h": 91}, "defs": {15: ["reuleaux_piece_data_mp", "support_piece_mp", "main"], 16: ["regular_reuleaux", "main"], "17a": ["pair_lt", "quicksort_idx", "cross", "hull_area_numba", "unpack"], "17h": ["pair_lt", "quicksort_idx", "cross", "hull_area_numba", "main"]}, "c15_dps": ["70"], "c16_longdouble": True, "c10_from_package": {"17a": True, "17h": True}, "ships_c10": True, "hier_checks": {"leaf is prefix of another": True, "incomplete binary coverage": True, "bad NOT-F3 leaf": True}}, "package_claim": {"C15": True, "C16": True, "C17": True, "statuses": True, "replays": True, "manifest": True, "copies": True, "unrecorded": ["UESFCM_Lebesgue_Cycle_17_68Cell_MinSearch_Diagnostic.npz", "UESFCM_Lebesgue_Cycle_17_VALIDATION.json"]}, } 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_lemmas(w): """Cycle 15 sec. 2-3: radial convexity (second differences along random rays in the box); the counterexample to global radial monotonicity, recomputed at its stored configuration""" s, g = w["search"]["secants"], w["diag15"]["global_monotonicity_counterexample"] ce = s["counterexample"] got = {"convexity": sig(s["convexity"], 2), "counterexample": [sig(ce["fs"] - g["boundary_area"], 1), sig(ce["forward"]["1e-07"], 4), sig(ce["backward"], 4), sig(g["approx_outward_radial_slope"], 4), sig(ce["forward"]["1e-05"], 2), sig(ce["rmin"] - S_F3, 2), sig(ce["fs"] - ce["ray_min"], 2), sig(ce["ray_min"], 10), sig(ce["ray_min"] - g["ray_min_search"], 1), bool(ce["ray_min"] > AREF)]} w["w1"] = got return [] if got == w["lemma_claim"] else [f"the lemmas: {got}"] def w2_references(w): """Cycles 15-16: the outer polygons against the stated areas, the exact hull at the candidate, and the same polygons with the hull's hand-over normals added""" o, c15, c16 = w["search"]["outer"], w["aref15"], w["aref16"] stated15, stated16 = c15["outer_polygon"]["area_upper"], c16["outer_polygon"] close = lambda a, b: abs(mpmath.mpf(a) - mpmath.mpf(b)) < mpmath.mpf(10) ** -68 mpmath.mp.dps = 90 cand = [close(c15["candidate"]["x5"], X5S), c16["candidate"]["x5"] == X5S, len(c15["candidate"]["x5"]) - 2] mpmath.mp.dps = 15 got = {"candidate": cand, "c15": [sig(o["c15"] - float(stated15), 1), _common_digits(o["c15_mp"], stated15)], "c16": [sig(o["c16_padded"] - float(stated16["longdouble_area_before_final_safety"]), 1), sig(o["c16_padded"] + stated16["final_area_safety"] - float(stated16["certified_upper_under_error_contract"]), 1)], "exact": sig(o["exact"], 13), "true_slack": [sig(AREF - o["exact"], 4), sig(AREF_TIGHT - o["exact"], 4)], "excess": [sig(o["c15"] - o["exact"], 2), sig(o["c16_bare"] - o["exact"], 2), sig(o["c16_padded"] - o["c16_bare"], 2)], "with_handovers": [o["handovers"], sig(o["c15_with_handovers"] - o["exact"], 2), sig(o["c16_with_handovers"] - o["exact"], 2)]} w["w2"] = got return [] if got == w["reference_claim"] else [f"the references: {got}"] def _common_digits(a, b): """how many leading decimal digits of two decimal strings agree, after '0.'""" k = 0 while k < min(len(a), len(b)) and a[k] == b[k]: k += 1 return max(0, k - 2) def w3_secants(w): """Cycle 16 sec. 13: the local secant at the contact; Cycle 15 sec. 13: f(s) - f(0) on the profile samples at or below 0.835; Cycle 16 sec. 9: the samples below the tight reference""" s, d15, d16, prof = w["search"]["secants"], w["diag15"], w["diag16"], w["profile"] low = [fs - f0 for _, fs, f0 in s["profile"] if fs <= AREF] got = {"contact": [sig(s["contact"]["local"], 3), sig(s["contact"]["fs"] - s["contact"]["f0"], 3), sig(s["contact"]["slope"], 3)], "profile_low": [len(low), sig(min(low), 6), sig(min(low) - d15["rotation_profile_low_sublevel_secant"]["minimum_f_s_minus_f_0"], 1), d15["rotation_profile_low_sublevel_secant"]["sample_count"]], "below_tight": [sum(x["area_min_search"] < AREF_TIGHT for x in prof["samples"]), d16["cycle12_rotation_profile"]["samples_below_tight_A_ref"], [x["rho"] for x in prof["samples"] if x["area_min_search"] < AREF_TIGHT] == d16["cycle12_rotation_profile"]["sample_rhos_below_tight_A_ref"]]} w["w3"] = got return [] if got == w["secant_claim"] else [f"the secants: {got}"] def w4_aref5(w): """Cycle 17 sec. 3: the five trees decoded with Cycle 10's split; every leaf's witness bound against 0.8349865; the stored minima; exact certification against the same threshold""" a, C = w["aref5"], w["search"]["certificates"] stats = [r48.tree_stats(t, "c10") for t in a["trees"]] wrong = [t["frontier_index"] for t, s in zip(a["trees"], stats) if not s["full"] or any(t[k] != s[k] for k in ("node_count", "area_leaf_count", "not_f3_leaf_count", "max_depth"))] wi, ex, nf = C["witness"]["aref5"], C["exact"]["aref5"], C["notf3"]["aref5"] stored = {t["frontier_index"]: t["min_raw_search_slack"] for t in a["trees"]} got = {"trees": [len(a["trees"]), sorted(t["frontier_index"] for t in a["trees"]), wrong], "totals": [sum(s["node_count"] for s in stats), sum(s["area_leaf_count"] for s in stats), sum(s["not_f3_leaf_count"] for s in stats)], "witness": [wi["leaves"], wi["failing"], sig(wi["least"][0], 8), wi["least"][1], sig(max(abs(v - stored[i]) for i, v in wi["per_tree"]), 1)], "exact": [ex["area"], ex["certified"], ex["failures"], ex["escalated"], sig(ex["least"][0], 4)], "notf3": [nf[0], nf[1], sig(nf[2], 3)]} w["w4"] = got return [] if got == w["aref5_claim"] else [f"the Aref5 certificate: {got}"] def w5_hierarchy(w): """Cycle 17 sec. 7-10: each trie prefix-free and complete; its counts; every NOT-F3 box inside the ball; every area leaf's witness bound; exact certification against A3+""" C, got = w["search"]["certificates"], {} for name in ("h131", "h129"): cert = w[name] paths = [x["path"] for x in cert["leaves"]] ps = set(paths) internal = {p[:k] for p in paths for k in range(len(p))} complete = all(all((q + b) in ps or (q + b) in internal for b in "01") for q in internal) types = [x["type"] for x in cert["leaves"]] wi, ex, nf = C["witness"][name], C["exact"][name], C["notf3"][name] got[name] = {"structure": [len(paths), len(ps), sum(1 for p in paths for k in range(len(p)) if p[:k] in ps), len(internal), complete, cert["summary"]["total_nodes"] == len(paths) + len(internal)], "types": [types.count("A"), types.count("N"), cert["summary"]["area_leaves"], cert["summary"]["not_f3_leaves"]], "witness": [wi["leaves"], wi["failing"], sig(wi["least"] - ETA, 8)], "exact": [ex["area"], ex["certified"], ex["failures"], ex["escalated"], sig(ex["least"][0], 4)], "notf3": [nf[0], nf[1], sig(nf[2], 3)]} w["w5"] = got return [] if got == w["hierarchy_claim"] else [f"the prefix trees: {got}"] def w6_ledger(w): """76 - 8 = 68 - 7 = 61, row for row; the 68-cell search diagnostic at its stored points; the share of root 6217's box that lies outside the 200 subroots, closed only in Cycle 11's search""" r76, r61, ms, core = w["remaining76"], w["remaining61"], w["minsearch"], w["core"] c14 = sorted(t["frontier_index"] for t in w["cert14"]["trees"]) c17 = sorted([t["frontier_index"] for t in w["aref5"]["trees"]] + [w["h131"]["root"]["frontier_index"], w["h129"]["root"]["frontier_index"]]) open68 = sorted(set(r76["local_index"]) - set(c14)) rows = lambda z: {i: (c, h) for i, c, h in zip(z["local_index"], z["centers"], z["halfwidths"])} R76, R61 = rows(r76), rows(r61) mine = w["search"]["minsearch"] order = sorted(range(len(ms["local_index"])), key=lambda k: ms["min_search"][k]) top = [{"local_index": ms["local_index"][k], "candidate_area": ms["min_search"][k]} for k in order[:10]] sub = w["subroots"] (C, H) = w["root"] vol = lambda h: Fraction(1) * Fraction(2 * h[0]) * Fraction(2 * h[1]) * Fraction(2 * h[2]) * Fraction(2 * h[3]) * Fraction(2 * h[4]) share = float(sum(vol(h) for h in sub["halfwidths"]) / vol(H)) got = {"ledger": [len(open68), sorted(ms["local_index"]) == open68, c17, sorted(r61["local_index"]) == sorted(set(open68) - set(c17)), all(R61[i] == R76[i] for i in R61)], "minsearch": [sig(max(abs(x["area"] - m) for x, m in zip(mine, ms["min_search"])), 1), sum(x["in_cell"] for x in mine), sorted([ms["local_index"][k], sig(x["d3"] - S_F3, 2)] for k, x in enumerate(mine) if x["d3"] < S_F3 - 1e-12), [ms["local_index"][k] for k in order[:5]], [x["local_index"] for x in core["multi_start_exact_envelope_search"]["ranked_top_10"]] == [t["local_index"] for t in top], max(abs(x["candidate_area"] - t["candidate_area"]) for x, t in zip(core["multi_start_exact_envelope_search"]["ranked_top_10"], top)) == 0.0, [ms["local_index"][k] for k in order if ms["min_search"][k] < AREF_TIGHT], [ms["local_index"][k] for k in order if ms["min_search"][k] <= AREF]], "outside_200": sig(1 - share, 4)} w["w6"] = got return [] if got == w["ledger_claim"] else [f"the ledger: {got}"] def w7_crystals(w): c15, c16, c17 = (w["crystals"][i] for i in (15, 16, 17)) got = {"C15": [c15["root_6217"]["gate_A_rho0"], c15["root_6217"]["boundary_locking"]["A_ref"] == AREF, c15["root_6217"]["boundary_locking"]["formal_cover_certificate"]], "C16": [c16["root_6217"]["formal_remaining_cells"], c16["root_6217"]["tight_A_ref"]["value"] == AREF_TIGHT], "C17": [c17["root_6217"]["formal_cells_before"], c17["root_6217"]["formal_Aref_closed"] == sorted(t["frontier_index"] for t in w["aref5"]["trees"]), sorted(c17["root_6217"]["formal_target_closed"]) == sorted([w["h131"]["root"]["frontier_index"], w["h129"]["root"]["frontier_index"]]), c17["root_6217"]["formal_cells_remaining"] == len(w["remaining61"]["local_index"])]} w["w7"] = got return [] if got == w["crystal_claim"] else [f"the crystals: {got}"] def w8_code(w): code = w["code"] got = {"lines": {i: t.count("\n") for i, t in code.items()}, "defs": {i: re.findall(r"^def (\w+)", t, re.M) for i, t in code.items()}, "c15_dps": re.findall(r"mp\.mp\.dps=(\d+)", code[15]), "c16_longdouble": "np.longdouble" in code[16], "c10_from_package": {i: "'dependencies'" in code[i] and "HERE" in code[i] for i in ("17a", "17h")}, "ships_c10": any("Verify_27Root" in x for x in w["packages"][17]), "hier_checks": {k: k in code["17h"] for k in ("leaf is prefix of another", "incomplete binary coverage", "bad NOT-F3 leaf")}} w["w8"] = got return [] if got == w["code_facts"] else [f"the verifiers: {got}"] VALIDATED = {15: {"paper_sha256": DOCS[15], "Aref_certificate_sha256": DATA["aref15"], "Aref_verifier_sha256": CODE[15], "diagnostic_sha256": DATA["diag15"], "state_sha256": CRYSTALS[15]}, 16: {"paper_sha256": DOCS[16], "tight_Aref_certificate_sha256": DATA["aref16"], "tight_Aref_verifier_sha256": CODE[16], "diagnostic_sha256": DATA["diag16"], "state_sha256": CRYSTALS[16]}} def p1_package(w): files = w["files"] sha = lambda k: hashlib.sha256(files[k]).hexdigest() v15, v16, v17 = (w["validations"][i] for i in (15, 16, 17)) by_name = {k.split("!/")[-1]: k for k in files if k.startswith(PKG[17])} checks = {**{f"C{i}": [w["validations"][i][k] == sha(f) for k, f in VALIDATED[i].items()] for i in (15, 16)}, "C17": [v17[k] == sha(by_name[k[:-len("_sha256")]]) for k in v17 if k.endswith("_sha256")], "statuses": [v["status"] == "PASS" for v in (v15, v16, v17)], "replays": [v17["independent_replay"]["Aref5"]["nodes"] == sum(r48.tree_stats(t, "c10")["node_count"] for t in w["aref5"]["trees"]), v17["independent_replay"]["root131"]["terminal_leaves"] == len(w["h131"]["leaves"]), v17["independent_replay"]["root129"]["terminal_leaves"] == len(w["h129"]["leaves"])], "manifest": [w["manifest_rows"][k][2] == sha(k) for k in sorted(files)], "copies": [files[c] == files[o] for c, o in COPIES.items()]} got = {k: all(v) for k, v in checks.items()} got["unrecorded"] = sorted(x for x in w["packages"][17] if not x.startswith("dependencies/") and f"{x}_sha256" not in v17) w["p1"] = got return [k for k, v in checks.items() if not all(v)] + ([] if got == w["package_claim"] else [f"the package: {got}"]) CHECKS = {"A0": a0_anchors, "W1": w1_lemmas, "W2": w2_references, "W3": w3_secants, "W4": w4_aref5, "W5": w5_hierarchy, "W6": w6_ledger, "W7": w7_crystals, "W8": w8_code, "P1": p1_package} DEPENDS = {"A0": {"texts"}, "W1": {"search", "diag15", "aref15", "lemma_claim"}, "W2": {"search", "aref15", "aref16", "reference_claim"}, "W3": {"search", "diag15", "diag16", "profile", "secant_claim"}, "W4": {"aref5", "search", "aref5_claim"}, "W5": {"h131", "h129", "search", "hierarchy_claim"}, "W6": {"remaining76", "remaining61", "minsearch", "core", "cert14", "aref5", "h131", "h129", "search", "subroots", "root", "ledger_claim"}, "W7": {"crystals", "aref5", "h131", "h129", "remaining61", "crystal_claim"}, "W8": {"code", "packages", "code_facts"}, "P1": {"validations", "files", "manifest_rows", "packages", "aref5", "h131", "h129", "package_claim"}} def drill_cases(base): def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x texts, s = base["texts"], base["search"] def area_digit(x): a = x["outer_polygon"]["area_upper"] x["outer_polygon"]["area_upper"] = a[:20] + ("1" if a[20] != "1" else "2") + a[21:] def flip_type(x): k = next(i for i, leaf in enumerate(x["leaves"]) if leaf["type"] == "N") x["leaves"][k]["type"] = "A" def swap_top(x): r = x["multi_start_exact_envelope_search"]["ranked_top_10"] r[0], r[1] = r[1], r[0] r61 = base["remaining61"] return [ ("K0-unmodified", "control", {}, set()), ("K1-crlf", "control", {"texts": {i: t.replace("\n", "\r\n") for i, t in texts.items()}, "code": {i: t.replace("\n", "\r\n") for i, 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-aref5-nodes-text", "mutation", {"texts": {**texts, 17: texts[17].replace("61{,}487", "61{,}488")}}, {"A0"}), ("M2-counterexample-slope", "mutation", {"diag15": edit(base["diag15"], lambda x: x["global_monotonicity_counterexample"].update(approx_outward_radial_slope=-0.05))}, {"W1"}), ("M3-ray-convexity", "mutation", {"search": edit(s, lambda x: x["secants"].update(convexity=-1.0))}, {"W1"}), ("M4-c15-area-digit", "mutation", {"aref15": edit(base["aref15"], area_digit)}, {"W2"}), ("M5-c16-padded-area", "mutation", {"aref16": edit(base["aref16"], lambda x: x["outer_polygon"].update(longdouble_area_before_final_safety="0.83498641461455"))}, {"W2"}), ("M6-exact-hull", "mutation", {"search": edit(s, lambda x: x["outer"].update(exact=x["outer"]["exact"] + 1e-9))}, {"W2"}), ("M7-profile-secant", "mutation", {"diag15": edit(base["diag15"], lambda x: x["rotation_profile_low_sublevel_secant"].update(minimum_f_s_minus_f_0=9.9e-06))}, {"W3"}), ("M8-profile-sample", "mutation", {"profile": edit(base["profile"], lambda x: x["samples"][1].update(area_min_search=0.83499))}, {"W3"}), ("M9-aref5-tree-count", "mutation", {"aref5": edit(base["aref5"], lambda x: x["trees"][0].update(area_leaf_count=x["trees"][0]["area_leaf_count"] + 1))}, {"W4"}), ("M10-aref5-exact", "mutation", {"search": edit(s, lambda x: x["certificates"]["exact"]["aref5"]["least"].__setitem__(0, -1e-9))}, {"W4"}), ("M11-h131-leaf-dropped", "mutation", {"h131": edit(base["h131"], lambda x: x["leaves"].pop())}, {"W5", "P1"}), ("M12-h129-leaf-type", "mutation", {"h129": edit(base["h129"], flip_type)}, {"W5"}), ("M13-h131-witness", "mutation", {"search": edit(s, lambda x: x["certificates"]["witness"]["h131"].update(failing=1))}, {"W5"}), ("M14-remaining-index", "mutation", {"remaining61": {**r61, "local_index": r61["local_index"][1:]}}, {"W6", "W7"}), ("M15-minsearch-value", "mutation", {"minsearch": {**base["minsearch"], "min_search": [base["minsearch"]["min_search"][0] + 1e-6] + base["minsearch"]["min_search"][1:]}}, {"W6"}), ("M16-ranking", "mutation", {"core": edit(base["core"], swap_top)}, {"W6"}), ("M17-crystal-cells", "mutation", {"crystals": edit(base["crystals"], lambda x: x[16]["root_6217"].update(formal_remaining_cells=67))}, {"W7"}), ("M18-hier-verifier", "mutation", {"code": {**base["code"], "17h": base["code"]["17h"].replace("incomplete binary coverage", "coverage")}}, {"W8"}), ("M19-validation-digest", "mutation", {"validations": edit(base["validations"], lambda x: x[16].update(diagnostic_sha256="0" * 64))}, {"P1"}), ("M20-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-049", "subject": "UESFCM Cycles 15-17: root 6217's boundary locking, its upper references, and the competitive-core closures", "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()