"""RUN-024 - Round 21: the B7 lift-tail atlas and counterexample-guided witness synthesis. Round 21 takes the open leaves of B7's lift tree on the tracked branch's depth-50 cell - 1046, 1397 and 2143 at lift depths 22, 24 and 26 - and reads them as an adversarial placement atlas: a phase lock arg t7 ~ 7 phi7 that tightens with depth, two lobes, and a ridge of area-minimising placements in the same two channels. It then designs witnesses against that atlas as a shape-versus-placement minimax (a cutting-plane loop, with a finite-tail optimism theorem), and tests a legal 7-fold family, smooth 7-fold witnesses, nearby irregular Reuleaux heptagons and a k = 3 symmetry-breaking pilot against regular B7: none beats it. Here the atlas is rebuilt box by box, the same boxes are bounded with exact cores, the ridge is scanned over the whole phase period, B7 and the smooth family are searched again with exact or bracketed areas, and the package - which ships no computing code - is read for what it records. Checks A0 anchors the numbers and formulas below occur in Round 21 as written W1 volumes sec. 1-2: the depth-50 cell; B7's sampled tree at lift depths 22, 24, 26 W2 atlas sec. 3-5, 7: the 2143 depth-26 boxes, the phase-lock and radius quantiles, the two lobes W3 ridge sec. 6: the area-minimising ridge over the whole phase period; the package's two ridge points W4 exact the same tail with exact cores: every depth-26 box closes; the tree closes W5 theorems sec. 8-11: finite-tail optimism; the legal 7-fold family; the cutting-plane record W6 baselines sec. 12-13: regular B7 and the smooth 7-fold family at q-dagger, searched again with exact or bracketed areas W7 unrecorded sec. 14-17: what the package records of its synthesised shapes W8 code what the package ships P1 package atlas, synthesis summary, crystal and text agree P2 package VALIDATION against the archive; its key checks from the data R1 registry Round 21's judgments reviewed, first-used statuses defined Usage: python code/run024_round21_lift_tail_synthesis.py [--drill] [--blind CID] """ import argparse import copy import hashlib import inspect import json import math from multiprocessing import Pool import numpy as np from scipy.optimize import minimize from scipy.spatial import ConvexHull import gate import registry import run008_round05_saturation_gate as r8 import run009_round06_witness_exchange as r9 import run011_round08_conditional_lift as r11 import run012_round09_adaptive_atlas as r12 import run013_round10_reference_dry_run as r13 import run019_round16_global_pilot as r19 import run020_round17_d3_cpg as r20 import run022_round19_necessity_lift as r22 import run023_round20_mixed_escalation as r23 from corpus import SOURCES, TREE, source_bytes, walk_sources from run009_round06_witness_exchange import placed_disc, placed_reuleaux from run010_round07_minimizer_atlas import d_star, t_text from run012_round09_adaptive_atlas import pieces_support from run013_round10_reference_dry_run import contact_points PKG = "main.zip!/AMRAL_LUC_FC_Round_21_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_21_Lift_Tail_Synthesis_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_21_v0.1.md" ATLAS = PKG + "AMRAL_LUC_FC_Round_21_TAIL_ATLAS.json" SYNTH = PKG + "AMRAL_LUC_FC_Round_21_SYNTHESIS_SUMMARY.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_21_VALIDATION.json" BOXES = PKG + "AMRAL_LUC_FC_Round_21_reference/B7_tail_boxes_depth26.json" ENTRY = PKG + "AMRAL_LUC_FC_Round_21_reference/round21_repro_entry.py" LOG = TREE / "data" / "gate-logs" / "run024-round21-lift-tail-synthesis.json" CACHE = TREE / "data" / "cache" / "run024-tail.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, TM = 0.835, 0.8365 RIDGE_GRID, SEARCH_STARTS, SEED = 64, 28, 20260925 LOBES = (2.5255, 5.8819) # sec. 5's two lobe centres of 7 phi, used only to split the boxes ANCHORS = { "W1": [r"\tau_{\rmbase}\approx3.82517\times10^{-4}.", r"1046/2^{22}\approx2.494\times10^{-4}.", r"1397/2^{24}\approx8.327\times10^{-5}.", r"\boxed{2143/2^{26}\approx3.193\times10^{-5}.}"], "W2": [r"\boxed{\delta_{\rmlock}=\operatorname{wrap}(\argt_7-7\phi_7).}", r"0.1886\to0.1372\to0.1081", r"0.4785\to0.3330\to0.2446.", r"7\phi\approx2.5255,", r"\argt\approx2.5536,", r"|t|\approx0.01213.", r"7\phi\approx5.8819,", r"\argt\approx5.8989,", r"|t|\approx0.01248.", r"$$1000$$", r"$$1143$$", r"0.98\text{–}0.99.", r"|t_{23}|\approx3.19\times10^{-4}.", r"|t_7|\sim0.012."], "W5": [r"\boxed{v_{m+1}\lev_m.}", r"P_m\subseteq\mathcalP,", r"h_{\lambda,a,\psi}=(1-\lambda)h_{B_7}+\lambda/2+a\cos(7\theta+\psi).", r"\boxed{|a|\le\lambda/96.}", r"$k=7$harmoniccurvatureamplitude為$48|a|$"], "W6": [r"\boxed{0.83712806.}", r"h(\theta)=1/2+a\cos7\theta.", r"a=0.0103", r"0.8369528,"], "W7": [r"0.8377708.", r"\boxed{0.8369560.}", r"0.8370455;", r"0.8371292;", r"0.8371286.", r"0.83697744,", r"0.83628622."], } CLAIMS = { "tail": {"22": [1046, 2.494e-4], "24": [1397, 8.327e-5], "26": [2143, 3.193e-5]}, "lock_text": {"median": [0.1886, 0.1372, 0.1081], "q95": [0.4785, 0.3330, 0.2446]}, "lobes_text": [[1000, 2.5255, 2.5536, 0.01213], [1143, 5.8819, 5.8989, 0.01248]], "mean_phi_is_phase7_centre_over_7": True, # this tree's, not the text's "ridge_minima": [[0.3506, 0.8371407193], [0.8415, 0.8371653077]], "package_ridge_points_are_minima": False, "exact_tail": {"boxes_closed": 2143, "least_bound": 0.8358005576, "closes_at": 21, "nodes": 2509, "open_18_19_20": [100, 39, 35]}, "b7_at_qdagger": {"at_package_point": 0.8371347054, "search_min": 0.8371339787}, "package_values_below_true_minimum": True, "smooth_lower_ends": {"0.006": 0.8362553547, "0.008": 0.8366196654, "0.009": 0.8367774562, "0.01": 0.8369189114, "0.0103": 0.8369581551}, "shapes_recorded": False, "ships_computing_code": False, } # ---------------------------------------------------------------- the tail (sec. 1-5) def tail(c, h, exact, pool, max_depth, keep): """B7's lift tree on a base cell, level by level (RUN-023's rule), keeping the open boxes - path, centre, half-widths, bound - at the depths in keep""" base = r19.cores(np.asarray(c, dtype=float), np.asarray(h, dtype=float)) tn = t_text(7, d_star(TM)) level = [("", (math.pi / 7, 0.0, 0.0), (math.pi / 7, tn, tn))] out, nodes, closed = {"per": {}}, 0, 0 for d in range(max_depth + 1): vals = pool.map(r23.lift_value, [(7, wc, wh, base, exact) for _, wc, wh in level], chunksize=16) nodes += len(level) open_ = [(p, wc, wh, lb) for (p, wc, wh), lb in zip(level, vals) if lb < T] closed += len(level) - len(open_) out["per"][d] = [nodes, closed, len(open_)] if d in keep: out[d] = [[p, list(wc), list(wh), lb] for p, wc, wh, lb in open_] if not open_ or d == max_depth: break nxt = [] for p, wc, wh, lb in open_: trial = [] for a in range(3): hh = list(wh) hh[a] /= 2 trial.append(r23.delta_n(7, hh)) a = int(np.argmin(trial)) hh = list(wh) hh[a] /= 2 lo, hi = list(wc), list(wc) lo[a] -= hh[a] hi[a] += hh[a] nxt += [(p + "0", tuple(lo), tuple(hh)), (p + "1", tuple(hi), tuple(hh))] level = nxt return out def wrap(a): return (a + math.pi) % (2 * math.pi) - math.pi def lock(g): """sec. 3: the phase lock wrap(arg t7 - 7 phi7) of a placement""" return wrap(math.atan2(g[2], g[1]) - 7 * g[0]) def circular(angles): s, c = float(np.mean(np.sin(angles))), float(np.mean(np.cos(angles))) return math.atan2(s, c) % (2 * math.pi), math.hypot(s, c) def lobes(boxes): """split by the nearer of sec. 5's two centres of 7 phi, and describe each lobe""" out = [] for k in (0, 1): lb = [b for b in boxes if (abs(wrap(7 * b[1][0] - LOBES[0])) < abs(wrap(7 * b[1][0] - LOBES[1]))) == (k == 0)] p7, ta = circular([7 * b[1][0] for b in lb]), circular([math.atan2(b[1][2], b[1][1]) for b in lb]) out.append({"count": len(lb), "phase7_circular_center": p7[0], "phase7_resultant": p7[1], "translation_angle_center": ta[0], "translation_angle_resultant": ta[1], "mean_translation_radius": float(np.mean([math.hypot(b[1][1], b[1][2]) for b in lb])), "mean_phi": float(np.mean([b[1][0] for b in lb])), "mean_tx": float(np.mean([b[1][1] for b in lb])), "mean_ty": float(np.mean([b[1][2] for b in lb]))}) return out # ---------------------------------------------------------------- the ridge (sec. 6) and the baselines (sec. 12-13) def _ridge(args): """min over (x7, y7) of the exact hull area at a fixed phase, from three starts""" base_q, phi, starts = args best = None for x0 in starts: r = minimize(lambda xy: r23.area4(base_q, 7, (phi, xy[0], xy[1])), x0, method="Nelder-Mead", options={"xatol": 1e-11, "fatol": 1e-14, "maxfev": 3000}) if best is None or r.fun < best[0]: best = [float(r.fun), [float(v) for v in r.x]] return best def _b7_search(args): q, g0 = args r = minimize(lambda g: r23.area4(q, 7, g), g0, method="Nelder-Mead", options={"xatol": 1e-12, "fatol": 1e-14, "maxiter": 4000, "maxfev": 6000}) return [float(r.fun), [float(v) for v in r.x]] def smooth_parts(q, a, g, N): """the base's contact points and support at N directions, and the smooth witness h = 1/2 + a cos 7(theta - phi) placed at g""" th = 2 * np.pi * np.arange(N) / N q = np.asarray(q, dtype=float) base = [placed_disc(), placed_reuleaux(3, 0.0, q[:2]), placed_reuleaux(5, q[2], q[3:5])] phi, x, y = g h = 0.5 + a * np.cos(7 * (th - phi)) + x * np.cos(th) + y * np.sin(th) hp = -7 * a * np.sin(7 * (th - phi)) - x * np.sin(th) + y * np.cos(th) pts = np.stack([h * np.cos(th) - hp * np.sin(th), h * np.sin(th) + hp * np.cos(th)], axis=1) return th, base, h, pts def smooth_inner(q, a, g, N): """the hull of the contact points at N directions: below the hull's area""" th, base, h, pts = smooth_parts(q, a, g, N) return float(ConvexHull(np.vstack([contact_points(p, th) for p in base] + [pts])).volume) def smooth_outer(q, a, g, N): """the polygon of the N support lines: above it (RUN-022's cancellation-free form)""" th, base, h, pts = smooth_parts(q, a, g, N) hh = np.maximum(np.stack([pieces_support(p, th) for p in base]).max(axis=0), h) d = 2 * np.pi / N e = ((np.roll(hh, 1) - hh) + (np.roll(hh, -1) - hh) + 4 * hh * math.sin(d / 2) ** 2) / math.sin(d) return 0.5 * math.fsum(hh * e) def _smooth_search(args): q, a, g0, N = args r = minimize(lambda g: smooth_inner(q, a, g, N), g0, method="Nelder-Mead", options={"xatol": 1e-10, "fatol": 1e-13, "maxiter": 3000, "maxfev": 4000}) return [float(r.fun), [float(v) for v in r.x]] def compute(atlas, synth): out = {} rng = np.random.default_rng(SEED) with Pool(14) as pool: c50, h50, path50 = r23.branch(50) out["cell"] = {"center": list(c50), "half": list(h50), "tau": r19.tau_f3(h50), "path": path50} s = tail(c50, h50, False, pool, 26, {22, 24, 26}) out["sampled"] = {"per": s["per"], "open": {str(d): s[d] for d in (22, 24, 26)}} base = r19.cores(np.asarray(c50), np.asarray(h50)) out["exact_bounds_26"] = pool.map(r23.lift_value, [(7, b[1], b[2], base, True) for b in s[26]], chunksize=8) e = tail(c50, h50, True, pool, 34, {18, 19, 20}) out["exact"] = {"per": e["per"], "open": {str(d): e[d] for d in (18, 19, 20)}} starts = [[-0.0106, 0.0071], [0.0113, -0.0056], [0.0, 0.0]] grid = [2 * math.pi / 7 * k / RIDGE_GRID for k in range(RIDGE_GRID)] out["ridge"] = {"grid": grid, "min": pool.map(_ridge, [(atlas["base_center"], phi, starts) for phi in grid])} out["ridge_package"] = [[r23.area4(atlas["base_center"], 7, (rl["phi"], rl["tx"], rl["ty"])), pool.apply(_ridge, ((atlas["base_center"], rl["phi"], [[rl["tx"], rl["ty"]]]),))] for rl in atlas["area_minimizing_ridge_lobes"]] q = synth["base_configuration"]["q"] g = synth["regular_B7_reference"]["placement"] b7 = pool.map(_b7_search, [(q, g)] + [(q, [rng.uniform(0, 2 * math.pi / 7), rng.uniform(-0.02, 0.02), rng.uniform(-0.02, 0.02)]) for _ in range(SEARCH_STARTS - 1)]) out["b7"] = {"at_package_point": r23.area4(q, 7, g), "from_package": b7[0], "best": min(b7)} out["smooth"] = {} for trial in synth["smooth_7fold_trials"]: a = trial["a"] res = pool.map(_smooth_search, [(q, a, [rng.uniform(0, 2 * math.pi / 7), rng.uniform(-0.02, 0.02), rng.uniform(-0.02, 0.02)], 8000) for _ in range(14)]) best = min(res) fine = pool.apply(_smooth_search, ((q, a, best[1], 40000),)) out["smooth"][str(a)] = {"coarse": best, "fine": fine, "inner": smooth_inner(q, a, fine[1], 80000), "outer": smooth_outer(q, a, fine[1], 80000)} return out def _code_key(files): digest = hashlib.sha256() for fn in (tail, wrap, lock, circular, _ridge, _b7_search, smooth_parts, smooth_inner, smooth_outer, _smooth_search, compute): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r11, r12, r13, r19, r20, r22, r23): digest.update(open(mod.__file__, "rb").read()) digest.update(files) digest.update(repr((RIDGE_GRID, SEARCH_STARTS, SEED)).encode()) return digest.hexdigest() _COMPUTED = {} def computed(atlas, synth, key_bytes): key = _code_key(key_bytes) if key not in _COMPUTED: if CACHE.exists(): cached = json.loads(CACHE.read_text(encoding="utf-8")) if cached.get("key") == key: _COMPUTED[key] = cached["results"] if key not in _COMPUTED: _COMPUTED[key] = json.loads(json.dumps(compute(atlas, synth))) CACHE.parent.mkdir(parents=True, exist_ok=True) CACHE.write_text(json.dumps({"key": key, "results": _COMPUTED[key]}) + "\n", encoding="utf-8") return _COMPUTED[key] # ---------------------------------------------------------------- checks def near(a, b, tol): return abs(a - b) <= tol def w1_volumes(w): out, comp, at = [], w["computed"], w["atlas"] cell = comp["cell"] if max(abs(a - b) for a, b in zip(cell["center"] + cell["half"], at["base_center"] + at["base_halfwidth"])) > 1e-15 \ or not near(cell["tau"], at["base_tau"], 1e-18): out.append("the atlas's base cell is not the track's depth-50 cell") got = {} for d in ("22", "24", "26"): nodes, closed, open_ = comp["sampled"]["per"][d] rec, txt = at["depth_summary"][d], w["tail"][d] halves = {tuple(b[2]) for b in comp["sampled"]["open"][d]} got[d] = [nodes, closed, open_, open_ / 2 ** int(d)] if [nodes, closed, open_] != [rec["nodes"], rec["cert_leaves"], rec["pending_count"]] \ or rec["pending_volume_fraction"] != open_ / 2 ** int(d) or open_ != txt[0] \ or not near(open_ / 2 ** int(d), txt[1], 5e-4 * txt[1]) or len(halves) != 1 \ or max(abs(a - b) for a, b in zip(next(iter(halves)), rec["box_halfwidth"])) > 1e-15: out.append(f"depth {d}: rebuilt {nodes, closed, open_}, atlas {rec['nodes'], rec['cert_leaves'], rec['pending_count']}") w["w1"] = {"cell_path": cell["path"], "tau": cell["tau"], "depths": got} return out def w2_atlas(w): out, comp, at = [], w["computed"], w["atlas"] op = comp["sampled"]["open"] mine = {b[0]: b for b in op["26"]} theirs = {b["path"]: b for b in w["boxes"]["boxes"]} if set(mine) != set(theirs) or w["boxes"]["depth"] != 26: out.append(f"depth-26 boxes: {len(mine)} rebuilt, {len(theirs)} in the package") worst = max((max(max(abs(a - b) for a, b in zip(mine[p][1] + mine[p][2], theirs[p]["center"] + theirs[p]["half"])), abs(mine[p][3] - theirs[p]["lower"])) for p in theirs if p in mine), default=1.0) if worst > 1e-14: out.append(f"depth-26 boxes differ by {worst:.2e}") medians, q95 = [], [] for d in ("22", "24", "26"): rec = at["depth_summary"][d] radius = [math.hypot(b[1][1], b[1][2]) for b in op[d]] lk = [abs(lock(b[1])) for b in op[d]] for key, vals, table in (("translation_radius_quantiles", radius, rec["translation_radius_quantiles"]), ("phase_lock_abs_quantiles", lk, rec["phase_lock_abs_quantiles"])): for k, v in table.items(): if not near(float(np.quantile(vals, float(k[1:]) / 100)), v, 1e-14): out.append(f"depth {d}: {key} {k}") medians.append(float(np.median(lk))) q95.append(float(np.quantile(lk, 0.95))) if any(not near(m, t, 5e-5) for m, t in zip(medians + q95, w["lock_text"]["median"] + w["lock_text"]["q95"])) \ or not (medians[0] > medians[1] > medians[2]): out.append(f"phase-lock medians {medians}, 95% {q95}") lb = lobes(op["26"]) for mine_l, ref, txt in zip(lb, at["depth26_two_lobes"], w["lobes_text"]): for k in ("count", "phase7_circular_center", "phase7_resultant", "translation_angle_center", "translation_angle_resultant", "mean_translation_radius", "mean_tx", "mean_ty"): if not near(mine_l[k], ref[k], 1e-12): out.append(f"lobe {txt[0]}: {k} {mine_l[k]!r} against {ref[k]!r}") if mine_l["count"] != txt[0] or not near(mine_l["phase7_circular_center"], txt[1], 5e-5) \ or not near(mine_l["translation_angle_center"], txt[2], 5e-5) or not near(mine_l["mean_translation_radius"], txt[3], 5e-6): out.append(f"lobe {txt[0]} against the text") is_centre = near(ref["mean_phi"], ref["phase7_circular_center"] / 7, 1e-15) and not near(ref["mean_phi"], mine_l["mean_phi"], 1e-12) if is_centre != w["mean_phi_is_phase7_centre_over_7"]: out.append("what the atlas calls mean_phi") if sum(l["count"] for l in lb) != len(op["26"]) or min(l["phase7_resultant"] for l in lb) < 0.98: out.append("the lobes do not cover the tail, or are not concentrated") w["w2"] = {"lock_medians": medians, "lock_q95": q95, "lobes": lb, "box_worst": worst} return out def w3_ridge(w): out, comp, at = [], w["computed"], w["atlas"] grid, mins = comp["ridge"]["grid"], [m[0] for m in comp["ridge"]["min"]] n = len(grid) local = sorted([(mins[k], grid[k]) for k in range(n) if mins[k] < mins[k - 1] and mins[k] < mins[(k + 1) % n]]) got = [[phi, m] for m, phi in local] step = 2 * math.pi / 7 / n if len(got) != 2 or any(not near(g[0], c[0], step) or not near(g[1], c[1], 5e-10) for g, c in zip(sorted(got), w["ridge_minima"])): out.append(f"the ridge's local minima {got}") if any(min(abs(wrap(7 * g[0] - c)) for c in LOBES) > 7 * step for g in got): out.append("a ridge minimum outside sec. 5's two channels") pk = [] for (at_pkg, polished), rl in zip(comp["ridge_package"], at["area_minimizing_ridge_lobes"]): pk.append({"phi": rl["phi"], "package": rl["area"], "at_package_point": at_pkg, "polished": polished[0], "channel_minimum": min(m for m, phi in local if abs(wrap(7 * phi - 7 * rl["phi"])) < 1)}) if not near(at_pkg, rl["area"], 1e-14): out.append(f"the ridge point at phi {rl['phi']}: area {at_pkg!r}, package {rl['area']!r}") minima = all(p["package"] <= p["channel_minimum"] + 1e-12 for p in pk) if minima != w["package_ridge_points_are_minima"]: out.append(f"the package's ridge points against the channel minima: {pk}") w["w3"] = {"local_minima": got, "package_points": pk} return out def w4_exact(w): out, comp, cl = [], w["computed"], w["exact_tail"] bounds = comp["exact_bounds_26"] closed = sum(v >= T for v in bounds) per = comp["exact"]["per"] last = max(per, key=int) opens = [len(comp["exact"]["open"][d]) for d in ("18", "19", "20")] if closed != cl["boxes_closed"] or not near(min(bounds), cl["least_bound"], 5e-11) \ or [int(last), per[last][0], per[last][2]] != [cl["closes_at"], cl["nodes"], 0] or opens != cl["open_18_19_20"]: out.append(f"exact cores: {closed} boxes closed, least {min(bounds)!r}; tree {last, per[last]}; open {opens}") sampled = [b[3] for b in comp["sampled"]["open"]["26"]] gap = min(e - s for e, s in zip(bounds, sampled)) w["w4"] = {"boxes_closed": closed, "least_exact_bound": min(bounds), "least_gain_over_sampled": gap, "closes_at": int(last), "nodes": per[last][0], "open_18_19_20": opens, "open_20_lobes": [l["count"] for l in lobes(comp["exact"]["open"]["20"])]} return out def w5_theorems(w): """sec. 10 by inclusion; sec. 11's family checked numerically; the cutting-plane record""" out = [] cp = w["synth"]["cutting_plane_7fold_preserving"] train = [x["training_score"] for x in cp] fresh = [x["fresh_oracle_min"] for x in cp] if any(b > a for a, b in zip(train, train[1:])) or any(f > t for f, t in zip(fresh, train)): out.append(f"the cutting-plane record breaks the theorem's direction: {train}, {fresh}") rng = np.random.default_rng(SEED) th = 2 * np.pi * np.arange(4096) / 4096 h7 = pieces_support(placed_reuleaux(7, 0.0, (0.0, 0.0)), th) worst_width, worst_rho, broken = 0.0, np.inf, 0 for _ in range(64): lam, psi = rng.uniform(0.01, 0.2), rng.uniform(0, 2 * math.pi) for a, legal in ((lam / 96 * rng.uniform(-1, 1), True), (lam / 96 * 1.02, False)): h = (1 - lam) * h7 + lam / 2 + a * np.cos(7 * th + psi) worst_width = max(worst_width, float(np.max(np.abs(h + np.roll(h, 2048) - 1)))) # the smooth part's radius of curvature; B7's own contributes a nonnegative measure rho = lam / 2 - 48 * a * np.cos(7 * th + psi) if legal: worst_rho = min(worst_rho, float(rho.min())) else: broken += float(rho.min()) < 0 curv = {str(x["a"]): x["curvature_min"] for x in w["synth"]["smooth_7fold_trials"]} if worst_width > 1e-12 or worst_rho < -1e-15 or broken != 64 \ or any(not near(v, 0.5 - 48 * float(a), 5e-4) for a, v in curv.items()): out.append(f"the 7-fold family: width error {worst_width:.2e}, least legal rho {worst_rho:.2e}, broken {broken}") w["w5"] = {"width_error": worst_width, "least_legal_curvature": worst_rho, "over_the_bound_breaks": broken} return out def w6_baselines(w): out, comp, syn, cl = [], w["computed"], w["synth"], w["b7_at_qdagger"] b7 = comp["b7"] ref = syn["regular_B7_reference"]["searched_min"] if not near(b7["at_package_point"], cl["at_package_point"], 5e-11) or not near(b7["best"][0], cl["search_min"], 5e-11): out.append(f"B7 at q-dagger: {b7['at_package_point']!r} at the package's point, {b7['best'][0]!r} searched") below = [ref < b7["best"][0] - 1e-9] smooth = {} for trial in syn["smooth_7fold_trials"]: s = comp["smooth"][str(trial["a"])] smooth[str(trial["a"])] = {"package": trial["searched_min"], "inner": s["inner"], "outer": s["outer"], "package_below_by": s["inner"] - trial["searched_min"]} below.append(trial["searched_min"] < s["inner"] - 1e-9) if not near(s["inner"], w["smooth_lower_ends"][str(trial["a"])], 5e-10) or not s["inner"] <= s["outer"] \ or not s["outer"] < b7["best"][0]: out.append(f"a = {trial['a']}: bracket [{s['inner']!r}, {s['outer']!r}]") if all(below) != w["package_values_below_true_minimum"]: out.append(f"the package's minima against the true ones: {below}") w["w6"] = {"b7": {"package": ref, "at_package_point": b7["at_package_point"], "polished_from_package": b7["from_package"][0], "search_min": b7["best"][0], "package_below_by": b7["best"][0] - ref}, "smooth": smooth} return out def w7_unrecorded(w): """the synthesised shapes behind sec. 14, 16, 17: what the package keeps of them""" syn = w["synth"] keys = json.dumps({k: v for k, v in syn.items() if k in ("cutting_plane_7fold_preserving", "nearby_irregular_Reuleaux7_exploration", "symmetry_breaking_k3_pilot")}) recorded = any(k in keys for k in ("coefficients", "shape", "fourier", "support", "vertices", "lambda", "psi")) cp = syn["cutting_plane_7fold_preserving"] gap = abs(cp[-1]["fresh_oracle_min"] - syn["regular_B7_reference"]["searched_min"]) bias = min(v["package_below_by"] for v in w["w6"]["smooth"].values()) if w.get("w6") else None w["w7"] = {"shapes_recorded": recorded, "final_oracle_minus_baseline": gap, "smallest_measured_bias": bias} return [] if recorded == w["shapes_recorded"] else [f"shape parameters recorded: {recorded}"] def w8_code(w): import re code = w["entry_code"] computes = any(k in code for k in ("minimize", "ConvexHull", "def ", "import numpy", "scipy")) reads_outside = bool(re.search(r"Path\(\"/", code)) w["w8"] = {"computes": computes, "reads_outside_package": reads_outside, "lines": code.count("\n")} return [] if (computes or not reads_outside) == w["ships_computing_code"] else [f"the shipped script: {w['w8']}"] def p1_package(w): out, text, at, syn = [], w["text"], w["atlas"], w["synth"] ds = at["depth_summary"] med = [round(ds[d]["phase_lock_abs_quantiles"]["q50"], 4) for d in ("22", "24", "26")] q95 = [round(ds[d]["phase_lock_abs_quantiles"]["q95"], 4) for d in ("22", "24", "26")] if med != w["lock_text"]["median"] or q95 != w["lock_text"]["q95"]: out.append(f"sec. 4 against the atlas: {med}, {q95}") for lb, txt in zip(at["depth26_two_lobes"], w["lobes_text"]): if [lb["count"], round(lb["phase7_circular_center"], 4), round(lb["translation_angle_center"], 4), round(lb["mean_translation_radius"], 5)] != txt: out.append(f"sec. 5 against the atlas: lobe {txt[0]}") vals = {"0.83712806": syn["regular_B7_reference"]["searched_min"], "0.8369528": syn["smooth_7fold_trials"][-1]["searched_min"], "0.8377708": syn["cutting_plane_7fold_preserving"][0]["training_score"], "0.8369560": syn["cutting_plane_7fold_preserving"][0]["fresh_oracle_min"], "0.8370455": syn["cutting_plane_7fold_preserving"][1]["fresh_oracle_min"], "0.8371292": syn["cutting_plane_7fold_preserving"][2]["fresh_oracle_min"], "0.8371286": syn["cutting_plane_7fold_preserving"][3]["fresh_oracle_min"], "0.83697744": syn["nearby_irregular_Reuleaux7_exploration"]["best_robust_min_found"], "0.83628622": syn["symmetry_breaking_k3_pilot"]["best_robust_min_found"]} for s, v in vals.items(): if round(v, len(s) - 2) != float(s): out.append(f"the text's {s} against the summary's {v}") crystal = gate.squash(w["crystal"]) for frag in ("d220.1886", "d240.1372", "d260.1081", r"7\phi\approx2.5255", r"7\phi\approx5.8819", r"\sim0.83712806.", "~0.83777", "~0.83696", "0.8371286.", r"|a|\le\lambda/96."): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"sec4": [med, q95]} return out def p2_package(w): import re out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf_id, text in (("round21", DOC, w["text"]), ("state_crystal", CRYSTAL, w["crystal"])): rec, (_, size, digest) = v[key], leaves[leaf_id] n = text.count("$$") if rec["sha256"] != digest or rec["bytes"] != size or not rec["utf8"] \ or rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0) \ or rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)) \ or rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)): out.append(f"VALIDATION {key} against the archive and the document") for key, leaf_id in (("tail_atlas_sha256", ATLAS), ("synthesis_summary_sha256", SYNTH), ("raw_depth26_tail_sha256", BOXES)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") at, syn = w["atlas"], w["synth"] ds = at["depth_summary"] ref = syn["regular_B7_reference"]["searched_min"] kc = {"depth26_pending_count": ds["26"]["pending_count"], "two_lobes_cover_all": sum(l["count"] for l in at["depth26_two_lobes"]) == ds["26"]["pending_count"], "phase_lock_tightens": ds["22"]["phase_lock_abs_quantiles"]["q50"] > ds["24"]["phase_lock_abs_quantiles"]["q50"] > ds["26"]["phase_lock_abs_quantiles"]["q50"], "regular_B7_beats_tested_smooth7": all(x["searched_min"] < ref for x in syn["smooth_7fold_trials"]), "cutting_plane_final_oracle_near_regular": abs(syn["cutting_plane_7fold_preserving"][-1]["fresh_oracle_min"] - ref) < 1e-5, "irregular_exploration_did_not_beat_regular": syn["nearby_irregular_Reuleaux7_exploration"]["best_robust_min_found"] < ref} if kc != v["key_checks"] or v["status"] != "PASS": out.append(f"VALIDATION key checks {kc}") w["p2"] = kc return out R21_DEFINITIONS = { "NOT FOUND": ("in-line", "sec. 0, 21: no instance turned up in the searches this round ran"), "FORMALIZED + IMPLEMENTED": ("in-line", "sec. 21: stated as a protocol (sec. 8-10) and run (sec. 14)"), } R21_REVIEWS = [ ("CLOSED", "B7 LIFT-TAIL ATLAS", "computation", "PARTIAL", "the atlas rebuilds box by box (W1, W2), but it is the pilot's sampled tail: with exact cores all 2143 depth-26 boxes " "close, the least by 8.0e-4, and B7 closes the cell at lift depth 21 (W4)"), ("CLOSED", "COUNTEREXAMPLE-GUIDED SYNTHESIS LOOP", "reading", "PASS", "a sound protocol (sec. 8-10); its runs are recorded as scores only (W7)"), ("NOT FOUND", "NEW SUPERIOR WITNESS", "computation", "PARTIAL", "true of the smooth 7-fold family, rebuilt here with bracketed areas (W6); the other candidates are not recorded (W7)"), ("STILL COMPUTE-DEFERRED", "a_{Leb}≥0.8350", "n/a", "n/a", "sec. 0's boxed summary; read from census v5 on (RUN-003)"), ("VERIFIED-COMPUTATIONAL-PILOT", "B7 lift-tail atlas", "computation", "PASS", "every count, box, quantile and lobe statistic rebuilds exactly (W1, W2) - as the pilot's sampled tail (W4)"), ("NUMERICAL-EVIDENCE", "Two-lobe phase lock", "computation", "PASS", "rebuilt (W2); the ridge scan finds exactly two channels, at 7 phi 2.45 and 5.89 (W3)"), ("FORMALIZED + IMPLEMENTED", "Cutting-plane witness synthesis", "reading", "PARTIAL", "formalized soundly; implemented by code the package does not ship, on shapes it does not record (W7, W8)"), ("PROVED", "Finite-tail optimism theorem", "analytic", "PASS", "min over a subset is at least the min over the set, and it can only fall as the subset grows; the record agrees (W5)"), ("PROVED", "7-fold legal deformation family", "analytic", "PASS", "width 1 exactly and radius of curvature at least lambda/2 - 48|a| (W5)"), ("NOT FOUND", "superior 7-fold witness", "computation", "PARTIAL", "the smooth family rebuilds below B7 by at least 1.8e-4 (W6); the cutting-plane shapes are not recorded (W7)"), ("NOT FOUND", "nearby irregular Reuleaux7 improvement", "n/a", "UNMEASURED", "the 30 candidates and 6 re-searched are not recorded (W7)"), ("NUMERICAL-EVIDENCE", "regular B7 local minimax interpretation", "computation", "PARTIAL", "B7's own value is measured with an area that sits 5.9e-6 below its true minimum (W6); the final cutting-plane oracle " "is 5.3e-7 from it, inside that error"), ("COMPUTE-DEFERRED", "global $0.8350$", "n/a", "n/a", ""), ] def r1_registry(w): return registry.completeness(w["registry"], "R21", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_volumes, "W2": w2_atlas, "W3": w3_ridge, "W4": w4_exact, "W5": w5_theorems, "W6": w6_baselines, "W7": w7_unrecorded, "W8": w8_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"computed", "atlas", "tail"}, "W2": {"computed", "atlas", "boxes", "lock_text", "lobes_text", "mean_phi_is_phase7_centre_over_7"}, "W3": {"computed", "atlas", "ridge_minima", "package_ridge_points_are_minima"}, "W4": {"computed", "exact_tail"}, "W5": {"synth"}, "W6": {"computed", "synth", "b7_at_qdagger", "package_values_below_true_minimum", "smooth_lower_ends"}, "W7": {"synth", "shapes_recorded", "computed", "b7_at_qdagger", "package_values_below_true_minimum", "smooth_lower_ends"}, "W8": {"entry_code", "ships_computing_code"}, "P1": {"text", "atlas", "synth", "crystal", "lock_text", "lobes_text"}, "P2": {"validation", "manifest", "text", "crystal", "atlas", "synth"}, "R1": {"registry", "definitions", "reviews"}} def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, ATLAS, SYNTH, VALIDATION, BOXES, ENTRY} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "atlas": json.loads(got[ATLAS]), "synth": json.loads(got[SYNTH]), "validation": json.loads(got[VALIDATION]), "boxes": json.loads(got[BOXES]), "entry_code": got[ENTRY].decode("utf-8"), "key_bytes": got[ATLAS] + got[SYNTH], "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() inputs = load_inputs() results_computed = computed(inputs["atlas"], inputs["synth"], inputs["key_bytes"]) def build(): return {**{k: v for k, v in inputs.items() if k != "key_bytes"}, "computed": results_computed, "registry": registry.load(), "definitions": dict(R21_DEFINITIONS), "reviews": list(R21_REVIEWS), **copy.deepcopy(CLAIMS)} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {} for c, fn in CHECKS.items(): results[c] = fn(w) 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", "p2"): print(key, json.dumps(w.get(key), default=float, ensure_ascii=False)[:900]) if not args.drill: return atlas, syn, boxes = inputs["atlas"], inputs["synth"], inputs["boxes"] at_count = copy.deepcopy(atlas) at_count["depth_summary"]["24"]["cert_leaves"] += 1 at_lobe = copy.deepcopy(atlas) at_lobe["depth26_two_lobes"][1]["translation_angle_center"] += 1e-9 at_ridge = copy.deepcopy(atlas) at_ridge["area_minimizing_ridge_lobes"][0]["area"] -= 1e-9 bx = copy.deepcopy(boxes) bx["boxes"][100]["lower"] += 1e-10 syn_cp = copy.deepcopy(syn) syn_cp["cutting_plane_7fold_preserving"][2]["training_score"] = 0.8374 syn_curv = copy.deepcopy(syn) syn_curv["smooth_7fold_trials"][1]["curvature_min"] = 0.126 syn_ref = copy.deepcopy(syn) syn_ref["regular_B7_reference"]["searched_min"] = 0.8371345 syn_shape = copy.deepcopy(syn) syn_shape["nearby_irregular_Reuleaux7_exploration"]["support_coefficients"] = [0.5, 0.0] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()), ("K2-boxes-reordered", "control", {"boxes": {**boxes, "boxes": list(reversed(boxes["boxes"]))}}, set()), ("K3-atlas-keys-sorted", "control", {"atlas": json.loads(json.dumps(atlas, sort_keys=True))}, set()), ("M1-doc-lobe-count", "mutation", {"text": inputs["text"].replace("$$\n1143\n$$", "$$\n1142\n$$")}, {"A0"}), ("M2-atlas-cert-count", "mutation", {"atlas": at_count}, {"W1"}), ("M3-text-fraction", "mutation", {"tail": {**CLAIMS["tail"], "24": [1397, 8.4e-5]}}, {"W1"}), ("M4-box-bound", "mutation", {"boxes": bx}, {"W2"}), ("M5-lobe-angle", "mutation", {"atlas": at_lobe}, {"W2"}), ("M6-mean-phi-reading", "mutation", {"mean_phi_is_phase7_centre_over_7": False}, {"W2"}), ("M7-ridge-claim", "mutation", {"ridge_minima": [[0.3506, 0.8371407193], [0.8415, 0.8371663077]]}, {"W3"}), ("M8-package-ridge-area", "mutation", {"atlas": at_ridge}, {"W3"}), ("M9-exact-tail", "mutation", {"exact_tail": {**CLAIMS["exact_tail"], "closes_at": 22}}, {"W4"}), ("M10-cutting-plane-record", "mutation", {"synth": syn_cp}, {"W5"}), ("M11-curvature-record", "mutation", {"synth": syn_curv}, {"W5"}), ("M12-b7-reference", "mutation", {"synth": syn_ref}, {"W6", "P1"}), ("M13-smooth-claim", "mutation", {"smooth_lower_ends": {**CLAIMS["smooth_lower_ends"], "0.009": 0.8367774462}}, {"W6"}), ("M14-shapes-recorded", "mutation", {"synth": syn_shape}, {"W7"}), ("M15-entry-computes", "mutation", {"entry_code": inputs["entry_code"] + "\nimport scipy\n"}, {"W8"}), ("M16-validation-digest", "mutation", {"validation": {**inputs["validation"], "tail_atlas_sha256": "0" * 64}}, {"P2"}), ("M17-review-dropped", "mutation", {"reviews": list(R21_REVIEWS[1:])}, {"R1"}), ] 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-024", "subject": "Round 21: the B7 lift-tail atlas and counterexample-guided witness synthesis", "document": DOC, "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "w6", "w7", "w8", "p1", "p2")}, "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("R21", "RUN-024", R21_DEFINITIONS, R21_REVIEWS) print(f"registry: {len(R21_DEFINITIONS)} definitions, {len(R21_REVIEWS)} reviews recorded for R21") if __name__ == "__main__": main()