"""RUN-020 - Round 17: the residual D3 quotient and certified-prune-gain scheduling. Round 17 finds a residual D3 symmetry of the normalized D + B3 + B5 placement space (the 2pi/3 turn and the mirror), proves every orbit meets the 60-degree wedge 0 <= arg t3 <= pi/3, and roots the pilot there: an enclosing rectangle and a SYM prune y3- > sqrt3 x3+. It then prices split schedulers by the children they certify at once (CPG): unrestricted, windowed to parents near the target, and windowed only from depth 10. Here the group and the wedge are checked, the D3 tree is rebuilt, the CPG runs are rebuilt first from the text and then with the rules only the code states (read after that reconstruction), and the comparisons are re-read at equal cell size and with one rule changed at a time. Checks A0 anchors the formulas and numbers below occur in Round 17 as written W1 group sec. 1-2, 5: r^3 = s^2 = e and srs = r^-1 on configurations; the area's invariance, exact and sampled (120 directions; 40 are not turn-invariant) W2 wedge sec. 3-4: every orbit has a representative in the wedge and the root box, given the a-priori exclusion |t5| <= t5*; q-dagger's representative sits in a HARD cell of both D3 trees W3 pilot sec. 6: the D3 official tree, sampled and exact; at depth 16 its cells are the full root's depth-18 cells, and there the gain is ~73%, not 47% / 33% W4 schedulers sec. 8-13: the four CPG runs and the tail probe, with the code's rules; what each unstated rule changes; the override rule against the activation depth; the tail window with exact cores W5 numbers sec. 11-15: the package's fractions, factors and entropy bits from its counts; the text's rounding P1 package summary, reference copy, stdout, tail probe, spec and crystal agree; the stored conclusion contradicting the stored data P2 package VALIDATION against the archive; the reference code and its .pyc R1 registry Round 17's judgments reviewed, first-used statuses defined Usage: python code/run020_round17_d3_cpg.py [--drill] [--blind CID] """ import argparse import copy import hashlib import inspect import json import math import re import struct from multiprocessing import Pool import numpy as np 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 from corpus import SOURCES, TREE, source_bytes, walk_sources from run009_round06_witness_exchange import placed_reuleaux from run010_round07_minimizer_atlas import d_star, t_text from run013_round10_reference_dry_run import contact_points PKG = "main.zip!/AMRAL_LUC_FC_Round_17_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_17_D3_CPG_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_17_v0.1.md" VALIDATION = PKG + "AMRAL_LUC_FC_Round_17_VALIDATION.json" SUMMARY = PKG + "AMRAL_LUC_FC_Round_17_PILOT_SUMMARY.json" SPEC = PKG + "AMRAL_LUC_FC_Round_17_PRODUCTION_SCHEDULER_SPEC.json" REF = PKG + "AMRAL_LUC_FC_Round_17_reference/" REF_SUMMARY = REF + "round17_pilot_summary.json" STDOUT = REF + "pilot_stdout.json" TAIL = REF + "tail_window_probe.json" PILOT = REF + "round17_symmetry_cpg_pilot.py" TAILPY = REF + "tail_window_probe.py" BASEPY = REF + "round16_base_pilot.py" PYC = REF + "__pycache__/round16_base_pilot.cpython-313.pyc" R16CODE = "main.zip!/AMRAL_LUC_FC_Round_16_Package_v0.1.zip!/AMRAL_LUC_FC_Round_16_global_pilot.py" RUN019 = TREE / "data" / "gate-logs" / "run019-round16-global-pilot.json" LOG = TREE / "data" / "gate-logs" / "run020-round17-d3-cpg.json" CACHE = TREE / "data" / "cache" / "run020-schedulers.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, TM = 0.835, 0.8365 GATE = T - 0.025 S3 = math.sqrt(3.0) P5 = 2 * math.pi / 5 ANCHORS = { "W1": [r"\boxed{A(q)=A(rq)}.", r"\boxed{A(q)=A(sq)}.", r"r^3=e,\qquads^2=e,\qquadsrs=r^{-1}.", r"\boxed{G\congD_3},", r"|G|=6.", r"6.661e-16.", r"8.882e-16.", r"samples：20。"], "W2": [r"\boxed{0\le\theta_3\le\pi/3}.", r"0\le\argt_3\le\pi/3.", r"\boxed{\min_{q\in\mathcalQ_{\rmfull}}A(q)=\min_{q\in\mathcalQ_{D_3}}A(q)}.", r"0\lex_3\let_3^\star,", r"0\ley_3\le\frac{\sqrt3}{2}t_3^\star.", r"\boxed{y_3\le\sqrt3\,x_3}.", r"\boxed{y^-_3>\sqrt3\,x^+_3},"], "W3": [r"23455\text{nodes},\qquad4112\text{HARD}.", r"\boxed{12357\text{nodes}},", r"\boxed{2766\text{HARD}}.", r"\boxed{47.32\%\text{fewernodes}},", r"\boxed{32.73\%\text{fewerHARD}}."], "W4": [r"C\subseteqC_0\cupC_1,", r"P(a)=\mathbf1[C^-_a\text{certified}]+\mathbf1[C^+_a\text{certified}].", r"\boxed{\max_aP(a)}.", r"1.$\min(L_-,L_+)$；", r"2.$L_-+L_+$；", r"3.childHausdorffradius；", r"2975\text{nodes},\qquad1210\text{HARD},", r"\boxed{L(C)\geT-\gamma},", r"\gamma=0.025.", r"L(C)\ge0.81.", r"N=2975,\quadH=1210,\quadE=14719.", r"N=4173,\quadH=863,\quadE=8424.", r"8625\text{nodes},\qquad1862\text{HARD}.", r"\boxed{N=9997},", r"\boxed{H=2048}.", r"只有officialsplit立即closure0children，且parent已進proof-nearwindow時，才評估alternateaxes。", r"-depth$<10$：純official；", r"-depth$\ge10$：若$L(C)\ge0.81$且officialclosure0child，才允許CPGoverride。", r"d_{\rmactivate}=10"], "W5": [r"**42.77%**", r"**42.45%**", r"\boxed{30.20\%\text{fewernodes}},", r"\boxed{32.68\%\text{fewerHARD}}.", r"1.82\times.", r"\boxed{10.72\%}.", r"\boxed{19.10\%\text{fewernodes}},", r"\boxed{25.96\%\text{fewerHARD}}.", r"2.02\times.", r"理論上2bits足夠表示axis"], } # ---------------------------------------------------------------- the group and the wedge def mirror(q): return np.array([q[0], -q[1], (-q[2]) % P5, q[3], -q[4]]) def turn(q, k=1): return r19.turn(np.asarray(q, dtype=float), k) def phi_gap(a, b): d = (a - b) % P5 return min(d, P5 - d) def q_gap(a, b): return max(max(abs(a[i] - b[i]) for i in (0, 1, 3, 4)), phi_gap(a[2], b[2])) def images(q): q = np.asarray(q, dtype=float) return {name: g for name, g in (("e", q), ("r", turn(q)), ("r2", turn(q, 2)), ("s", mirror(q)), ("sr", mirror(turn(q))), ("sr2", mirror(turn(q, 2))))} def representative(q, slack=1e-12): """the image of q whose t3 lies in the wedge 0 <= arg t3 <= pi/3 (t3 = 0 lies in it)""" best = None for name, g in images(q).items(): th = math.atan2(g[1], g[0]) if math.hypot(g[0], g[1]) == 0.0 or -slack <= th <= math.pi / 3 + slack: return name, g return best def d3_root(): t3, t5 = t_text(3, d_star(TM)), t_text(5, d_star(TM)) return (np.array([t3 / 2, S3 / 4 * t3, math.pi / 5, 0.0, 0.0]), np.array([t3 / 2, S3 / 4 * t3, math.pi / 5, t5, t5])) def sym(c, h, eps): """sec. 4: the cell lies wholly above the ray y3 = sqrt3 x3 (the code adds eps = 1e-15)""" return (c[1] - h[1]) > S3 * (c[0] + h[0]) + eps def sampled_area(q, n): th = 2 * np.pi * np.arange(n) / n disc = 0.5 * np.stack([np.cos(th), np.sin(th)], axis=1) return float(ConvexHull(np.vstack([disc, contact_points(placed_reuleaux(3, 0.0, q[:2]), th), contact_points(placed_reuleaux(5, q[2], q[3:5]), th)])).volume) # ---------------------------------------------------------------- the schedulers def _modes(args): return r19.modes(*args) def children(c, h, a): hh = h.copy() hh[a] /= 2 lo, hi = c.copy(), c.copy() lo[a] -= hh[a] hi[a] += hh[a] return (lo, hh), (hi, hh) def evaluate(cells, exact, pool, eps, out, count): jobs, where = [], [] for key, pair in cells.items(): for k, (cc, hh) in enumerate(pair): if sym(cc, hh, eps): where.append((key, k, None, hh)) else: where.append((key, k, len(jobs), hh)) jobs.append((cc.tolist(), hh.tolist(), exact)) vals = pool.map(_modes, jobs, chunksize=16) if jobs else [] if count: out["evals"] += len(jobs) res = {} for key, k, idx, hh in where: tau = r19.tau_f3(hh) item = (1, 1.0e9, tau, ("SYM", 1.0e9, None, None)) if idx is None else \ (int(vals[idx][0] is not None), vals[idx][1], tau, vals[idx]) res.setdefault(key, [None, None])[k] = item return res def emit(depth, exact, policy, pool, min_depth=0, eps=1e-15, rule=None): """policy: official | cpg_full | cpg_window | tail. The CPG variants evaluate the official children at the parent; a SYM child is certified with L = 1e9. cpg_full and cpg_window override on a larger key (cert, min L, sum L, -tau, -axis), cpg_window stopping at the first alternate certifying both children; tail overrides only with an alternate that certifies a child, on (cert, min L, sum L), stopping likewise. rule = 'key' | 'cert' swaps the window's override rule; min_depth delays either window.""" rule = rule or ("cert" if policy == "tail" else "key") c0, h0 = d3_root() level = [("", c0, h0, None)] out = {"nodes": 0, "SYM": 0, "APR": 0, "REP": 0, "CORE": 0, "HARD": 0, "evals": 0, "overrides": 0} hard = [] for d in range(depth + 1): keep = [] for p, c, h, pre in level: out["nodes"] += 1 if sym(c, h, eps): out["SYM"] += 1 else: keep.append((p, c, h, pre)) todo = [i for i, x in enumerate(keep) if x[3] is None] vals = pool.map(_modes, [(keep[i][1].tolist(), keep[i][2].tolist(), exact) for i in todo], chunksize=32) out["evals"] += len(todo) got = dict(zip(todo, vals)) opened = [] for i, (p, c, h, pre) in enumerate(keep): v = pre if pre is not None else got[i] if v[0]: out[v[0]] += 1 elif d == depth: out["HARD"] += 1 hard.append(p) else: opened.append((p, c, h, v[1])) if policy == "official": level = [(p + str(k), cc, hh, None) for p, c, h, lb in opened for k, (cc, hh) in enumerate(children(c, h, r19.official_axis(h)))] continue res = evaluate({(j, r19.official_axis(h)): children(c, h, r19.official_axis(h)) for j, (p, c, h, lb) in enumerate(opened)}, exact, pool, eps, out, True) alt = {} for j, (p, c, h, lb) in enumerate(opened): ao = r19.official_axis(h) allow = policy == "cpg_full" or (d >= min_depth and sum(x[0] for x in res[(j, ao)]) == 0 and lb >= GATE) if allow: alt.update({(j, a): children(c, h, a) for a in range(5) if a != ao}) ares = evaluate(alt, exact, pool, eps, out, False) nxt = [] for j, (p, c, h, lb) in enumerate(opened): ao = r19.official_axis(h) axis, r = ao, res[(j, ao)] key = lambda rr, a: (sum(x[0] for x in rr), min(x[1] for x in rr), sum(x[1] for x in rr), -rr[0][2], -a) alts = [a for a in range(5) if (j, a) in ares] if alts and (policy == "cpg_full" or rule == "key"): best = (key(r, ao), ao) for a in alts: rr = ares[(j, a)] out["evals"] += sum(1 for x in rr if x[3][0] != "SYM") if key(rr, a) > best[0]: best = (key(rr, a), a) if policy != "cpg_full" and sum(x[0] for x in rr) == 2: break axis = best[1] elif alts: best = None for a in alts: rr = ares[(j, a)] out["evals"] += sum(1 for x in rr if x[3][0] != "SYM") cert = sum(x[0] for x in rr) if cert > 0: if best is None or key(rr, a)[:3] > best[0]: best = (key(rr, a)[:3], a) if cert == 2: break if best is not None: axis = best[1] if axis != ao: out["overrides"] += 1 r = ares[(j, axis)] nxt += [(p + str(k), cc, hh, r[k][3]) for k, (cc, hh) in enumerate(children(c, h, axis))] level = nxt return out, hard RUNS = { # name: (depth, exact, policy, min_depth, eps, rule) "official": (16, False, "official", 0, 1e-15, None), "official_exact": (16, True, "official", 0, 1e-15, None), "cpg_window_16": (16, False, "cpg_window", 0, 1e-15, None), "cpg_full_14": (14, False, "cpg_full", 0, 1e-15, None), "cpg_window_14": (14, False, "cpg_window", 0, 1e-15, None), "tail_16": (16, False, "tail", 10, 1e-15, None), "cpg_full_14_no_margin": (14, False, "cpg_full", 0, 0.0, None), "key_rule_from_10": (16, False, "cpg_window", 10, 1e-15, "key"), "cert_rule_from_0": (16, False, "tail", 0, 1e-15, "cert"), "tail_16_exact": (16, True, "tail", 10, 1e-15, None), } def compute(): with Pool(14) as pool: out = {} for name, (depth, exact, policy, md, eps, rule) in RUNS.items(): counts, hard = emit(depth, exact, policy, pool, md, eps, rule) out[name] = {"counts": counts, "hard": hard if policy == "official" else None} return out def _code_key(): digest = hashlib.sha256() for fn in (d3_root, sym, _modes, children, evaluate, emit, compute): digest.update(inspect.getsource(fn).encode()) digest.update(json.dumps(RUNS, sort_keys=True).encode()) for mod in (r8, r9, r11, r12, r13, r19): digest.update(open(mod.__file__, "rb").read()) return digest.hexdigest() _COMPUTED = {} def computed(): key = _code_key() 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())) 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] def path_of(q, depth=16): """the official D3 tree's depth-d cell holding q: the split sequence is the same on a level""" c, h = d3_root() seq = r19.split_sequence(h, r19.official_axis, depth) bits = [] for a in seq: h = h.copy() h[a] /= 2 bit = int(q[a] >= c[a]) c = c.copy() c[a] += h[a] if bit else -h[a] bits.append(str(bit)) return "".join(bits) # ---------------------------------------------------------------- checks def w1_group(w): out, tr = [], w["turn"] rng = np.random.default_rng(17) c0, h0 = r19.root(TM) rel = 0.0 for _ in range(40): q = c0 + rng.uniform(-1, 1, 5) * h0 rel = max(rel, q_gap(tr(tr(tr(q))), q), q_gap(mirror(mirror(q)), q), q_gap(mirror(tr(mirror(q))), tr(tr(q)))) if rel > 1e-12: out.append(f"r^3 = s^2 = e, srs = r^-1 fail by {rel:.1e}") exact = 0.0 for _ in range(6): q = c0 + rng.uniform(-1, 1, 5) * h0 a = r19.base_area(q) exact = max(exact, abs(r19.base_area(mirror(q)) - a), abs(r19.base_area(tr(q)) - a)) if exact > 1e-13: out.append(f"the exact area moves by {exact:.1e} under the mirror or the turn") grid = {} for n in (40, 120): m = t = 0.0 for _ in range(20): q = c0 + rng.uniform(-1, 1, 5) * h0 a = sampled_area(q, n) m = max(m, abs(sampled_area(mirror(q), n) - a)) t = max(t, abs(sampled_area(tr(q), n) - a), abs(sampled_area(tr(tr(q)), n) - a)) grid[n] = {"mirror": m, "turn": t} if max(grid[120].values()) > 1e-13: out.append(f"120 directions: the sampled area moves by {max(grid[120].values()):.1e}") if (grid[40]["turn"] <= 1e-13) != w["n40_turn_invariant"] or grid[40]["mirror"] > 1e-13: out.append(f"40 directions: mirror {grid[40]['mirror']:.1e}, turn {grid[40]['turn']:.1e}") w["w1"] = {"relations_worst": rel, "exact_area_worst": exact, "sampled": grid} return out def w2_wedge(w): out = [] t3, t5 = t_text(3, d_star(TM)), t_text(5, d_star(TM)) c, h = d3_root() lo, hi = c - h, c + h rng = np.random.default_rng(170) pts = [] for _ in range(4000): r3, a3 = t3 * math.sqrt(rng.uniform()), rng.uniform(-math.pi, math.pi) r5, a5 = t5 * math.sqrt(rng.uniform()), rng.uniform(-math.pi, math.pi) pts.append(np.array([r3 * math.cos(a3), r3 * math.sin(a3), rng.uniform(0, P5), r5 * math.cos(a5), r5 * math.sin(a5)])) for k in range(6): # the wedge's edges and their images, and t3 = 0 pts.append(np.array([t3 / 2 * math.cos(k * math.pi / 3), t3 / 2 * math.sin(k * math.pi / 3), 0.3, 0.05, -0.02])) pts.append(np.array([0.0, 0.0, 0.7, -0.1, 0.1])) bad = [] for q in pts: rep = representative(q, w["slack"]) if rep is None: bad.append("no image in the wedge") continue g = rep[1] box = all(lo[i] - 1e-12 <= g[i] <= hi[i] + 1e-12 for i in (0, 1, 3, 4)) and -1e-12 <= g[2] < P5 + 1e-12 if not box or abs(math.hypot(g[3], g[4]) - math.hypot(q[3], q[4])) > 1e-14 or g[1] > S3 * g[0] + 1e-12: bad.append(f"representative {rep[0]} of {np.round(q, 4)} leaves the root") if bad: out.append(f"{len(bad)} of {len(pts)} configurations: {bad[:2]}") # the representative keeps |t5|, which is what keeps it in the box: from the square's corner it leaves corner = np.array([-0.1, 0.05, 0.2, t5, t5]) # arg t3 = 153 deg: the representative turns t5 g = representative(corner, w["slack"])[1] leaves = max(abs(g[3]), abs(g[4])) > t5 + 1e-12 if leaves != w["needs_radial_exclusion"]: out.append("the wedge needs the a-priori exclusion |t5| <= t5* to stay in the root box: " f"{'it does' if leaves else 'it does not'}") q = np.array([*r19.QDAG[:2], r19.QDAG[2] % P5, *r19.QDAG[3:]]) name, g = representative(q, w["slack"]) p = path_of(g) held = all(p in set(w["computed"][k]["hard"]) for k in ("official", "official_exact")) if held != w["qdag_rep_hard"]: out.append(f"q-dagger's representative {name} (arg t3 = {math.atan2(g[1], g[0]):.9f}) is in cell {p}, " f"HARD in both trees: {held}") w["w2"] = {"configurations": len(pts), "corner_representative_t5": [g for g in representative(corner, w["slack"])[1][3:5]], "qdag_representative": name, "qdag_rep_arg_t3": math.atan2(g[1], g[0]), "qdag_rep_below_edge": math.pi / 3 - math.atan2(g[1], g[0]), "qdag_rep_cell": p} return out def row(c): return [c["nodes"], c["evals"], c["SYM"], c["CORE"], c["HARD"], c["overrides"]] def summary_row(r): return [r["nodes"], r["lower_bound_evaluations"], r["counts"]["SYM"], r["counts"]["CORE"], r["counts"]["HARD"], r["overrides"]] def w3_pilot(w): out, comp = [], w["computed"] runs = {(r["root_kind"], r["depth"], r["scheduler"]): r for r in w["summary"]["runs"]} mine = row(comp["official"]["counts"]) if mine != summary_row(runs[("d3", 16, "official")]): out.append(f"D3 official depth 16: rebuilt {mine}, package {summary_row(runs[('d3', 16, 'official')])}") ex = comp["official_exact"]["counts"] if [ex["nodes"], ex["SYM"], ex["CORE"], ex["HARD"]] != w["exact_official"]: out.append(f"exact cores: {[ex['nodes'], ex['SYM'], ex['CORE'], ex['HARD']]}, recorded {w['exact_official']}") _, hd = d3_root() _, hf = r19.root(TM) for a in r19.split_sequence(hd, r19.official_axis, 16): hd[a] /= 2 for a in r19.split_sequence(hf, r19.official_axis, 18): hf[a] /= 2 if abs(r19.tau_f3(hd) - r19.tau_f3(hf)) > 1e-15 or any(abs(hd[i] - hf[i]) > 1e-15 for i in (0, 2, 3, 4)): out.append("the D3 root's depth-16 cells are not the full root's depth-18 cells") full = w["run019"]["w4"] matched = {} for key, d3 in (("sampled", comp["official"]["counts"]), ("exact", comp["official_exact"]["counts"])): f = full[key]["official@18"] matched[key] = [round(1 - d3["nodes"] / f[0], 4), round(1 - d3["HARD"] / f[4], 4)] if matched != w["matched"]: out.append(f"at equal cell size the D3 root saves {matched}, recorded {w['matched']}") w["w3"] = {"d3_depth16_halves": list(hd), "full_depth18_halves": list(hf), "tau": r19.tau_f3(hd), "matched_reduction": matched, "exact_official": ex} return out def w4_schedulers(w): out, comp = [], w["computed"] runs = {(r["root_kind"], r["depth"], r["scheduler"]): r for r in w["summary"]["runs"]} for name, key in (("cpg_window_16", ("d3", 16, "cpg_window")), ("cpg_full_14", ("d3", 14, "cpg_full")), ("cpg_window_14", ("d3", 14, "cpg_window"))): if row(comp[name]["counts"]) != summary_row(runs[key]): out.append(f"{name}: rebuilt {row(comp[name]['counts'])}, package {summary_row(runs[key])}") tail = comp["tail_16"]["counts"] t = w["tail"] internal = tail["nodes"] - sum(tail[k] for k in ("SYM", "APR", "REP", "CORE", "HARD")) if row(tail) != summary_row(t) or abs(tail["overrides"] / internal - t["override_fraction_of_internal_nodes"]) > 1e-15: out.append(f"tail window: rebuilt {row(tail)}, probe {summary_row(t)}") margin = row(comp["cpg_full_14_no_margin"]["counts"]) != row(comp["cpg_full_14"]["counts"]) if margin != w["sym_margin_matters"]: out.append(f"the SYM margin {'changes' if margin else 'does not change'} full CPG") pairs = {"key rule": ("cpg_window_16", "key_rule_from_10"), "cert rule": ("cert_rule_from_0", "tail_16")} worse = {} for rule, (a, b) in pairs.items(): x, y = comp[a]["counts"], comp[b]["counts"] worse[rule] = all(y[m] >= x[m] for m in ("nodes", "evals", "overrides", "HARD")) and \ any(y[m] > x[m] for m in ("nodes", "evals", "overrides", "HARD")) if all(worse.values()) != w["depth10_worse_everywhere"]: out.append(f"activating at depth 10 rather than the root is worse on every count: {worse}") eo, et = comp["official_exact"]["counts"], comp["tail_16_exact"]["counts"] beats = et["nodes"] < eo["nodes"] and et["HARD"] < eo["HARD"] if beats != w["tail_beats_official_exact"]: out.append(f"with exact cores the tail window {'beats' if beats else 'does not beat'} official") w["w4"] = {name: row(comp[name]["counts"]) for name in RUNS} w["w4"]["columns"] = ["nodes", "evals", "SYM", "CORE", "HARD", "overrides"] return out def w5_numbers(w): out, s, sq = [], w["summary"], gate.squash(w["text"]) runs = {(r["root_kind"], r["depth"], r["scheduler"]): r for r in s["runs"]} o16, w16 = runs[("d3", 16, "official")], runs[("d3", 16, "cpg_window")] f14, w14 = runs[("d3", 14, "cpg_full")], runs[("d3", 14, "cpg_window")] full, tail = s["full_depth16_baseline"], s["tail_window_depth16"] red = lambda a, b, k: (a[k] - b[k]) / a[k] want = { ("depth16_d3_official_vs_full", "node_reduction_fraction"): red(full, o16, "nodes"), ("depth16_d3_official_vs_full", "hard_reduction_fraction"): red(full, o16, "hard"), ("depth16_windowed_cpg_vs_d3_official", "node_reduction_fraction"): red(o16, w16, "nodes"), ("depth16_windowed_cpg_vs_d3_official", "hard_reduction_fraction"): red(o16, w16, "hard"), ("depth16_windowed_cpg_vs_d3_official", "emitter_eval_increase_factor"): w16["lower_bound_evaluations"] / o16["lower_bound_evaluations"], ("depth16_windowed_cpg_vs_d3_official", "wall_time_increase_factor"): w16["seconds"] / o16["seconds"], ("depth14_window_vs_full_cpg", "window_node_increase_fraction"): (w14["nodes"] - f14["nodes"]) / f14["nodes"], ("depth14_window_vs_full_cpg", "window_eval_reduction_fraction"): red(f14, w14, "lower_bound_evaluations"), ("depth14_window_vs_full_cpg", "window_wall_reduction_fraction"): red(f14, w14, "seconds"), ("tail_window_vs_d3_official", "node_reduction_fraction"): red(o16, tail, "nodes"), ("tail_window_vs_d3_official", "hard_reduction_fraction"): red(o16, tail, "hard"), ("tail_window_vs_d3_official", "eval_increase_factor"): tail["lower_bound_evaluations"] / o16["lower_bound_evaluations"], } for (block, key), val in want.items(): if abs(s[block][key] - val) > 1e-15: out.append(f"{block}.{key} = {s[block][key]!r}, its counts give {val!r}") if s["depth14_window_vs_full_cpg"]["same_hard_count"] != (w14["hard"] == f14["hard"]): out.append("same_hard_count disagrees with the counts") for r in list(s["runs"]) + [tail]: leaves = sum(r["counts"].values()) internal = r["nodes"] - leaves f = r["overrides"] / internal if internal else 0.0 if abs(f - r["override_fraction_of_internal_nodes"]) > 1e-15: out.append(f"{r.get('scheduler', 'tail')}: override fraction {r['override_fraction_of_internal_nodes']!r}, counts give {f!r}") if "idealized_entropy_control_bits" in r: H = -(f * math.log2(f) + (1 - f) * math.log2(1 - f)) if 0 < f < 1 else 0.0 bits = r["nodes"] + H * internal + 2 * r["overrides"] if abs(bits - r["idealized_entropy_control_bits"]) > 1e-9: out.append(f"{r['scheduler']}: entropy bits {r['idealized_entropy_control_bits']!r}, counts give {bits!r}") pct = [want[("depth16_d3_official_vs_full", "node_reduction_fraction")], want[("depth16_d3_official_vs_full", "hard_reduction_fraction")], want[("depth16_windowed_cpg_vs_d3_official", "node_reduction_fraction")], want[("depth16_windowed_cpg_vs_d3_official", "hard_reduction_fraction")], want[("tail_window_vs_d3_official", "node_reduction_fraction")], want[("tail_window_vs_d3_official", "hard_reduction_fraction")], want[("depth14_window_vs_full_cpg", "window_eval_reduction_fraction")], want[("depth14_window_vs_full_cpg", "window_wall_reduction_fraction")], tail["override_fraction_of_internal_nodes"]] for x in pct: if f"{100 * x:.2f}\\%" not in sq and f"**{100 * x:.2f}%**" not in sq: out.append(f"the text does not carry {100 * x:.2f}%") for x in (want[("depth16_windowed_cpg_vs_d3_official", "emitter_eval_increase_factor")], want[("tail_window_vs_d3_official", "eval_increase_factor")]): if f"{x:.2f}\\times." not in sq: out.append(f"the text does not carry {x:.2f}x") if math.ceil(math.log2(4)) != 2: out.append("four override axes need more than 2 bits") w["w5"] = {"recomputed": {f"{a}.{b}": v for (a, b), v in want.items()}} return out def p1_package(w): out, s = [], w["summary"] if s != w["ref_summary"]: out.append("the summary is not the reference directory's copy") extra = {"tail_window_depth16", "tail_window_vs_d3_official"} stripped = {k: v for k, v in s.items() if k not in extra} stripped["conclusions"] = s["conclusions"][:6] if stripped != w["stdout"]: out.append("the summary is not the pilot's stdout plus the tail blocks and a seventh conclusion") if w["tail"] != s["tail_window_depth16"]: out.append("the tail probe's file is not the summary's tail block") sp = w["spec"] sch = sp["split_scheduler"] if (sch["gamma"], sch["activation_depth"], sp["target"], sp["master_target"]) != (0.025, 10, s["target"], s["master_target"]) \ or abs(w["tail"]["gate"] - (sp["target"] - sch["gamma"])) > 1e-15: out.append("the scheduler spec's parameters differ from the summary's") if sp["root_semantics"]["canonical_condition"] != s["d3_symmetry"]["canonical_t3_wedge"] \ or sp["root_semantics"]["sym_prune"] != s["d3_symmetry"]["sym_prune"]: out.append("the spec's root semantics differ from the summary's") cr = gate.squash(w["crystal"]) runs = {(r["root_kind"], r["depth"], r["scheduler"]): r for r in s["runs"]} o16, t = runs[("d3", 16, "official")], s["tail_window_depth16"] frags = [f"{s['full_depth16_baseline']['nodes']}\\text{{nodes}},\\quad{s['full_depth16_baseline']['hard']}\\text{{HARD}}.", f"\\boxed{{{o16['nodes']}\\text{{nodes}},\\quad{o16['hard']}\\text{{HARD}}}}.", f"\\boxed{{{t['nodes']}\\text{{nodes}},\\quad{t['hard']}\\text{{HARD}}}}.", "L(C)\\ge0.81,", f"{100 * s['tail_window_vs_d3_official']['node_reduction_fraction']:.1f}%fewernodes", f"{100 * s['tail_window_vs_d3_official']['hard_reduction_fraction']:.1f}%fewerHARD", f"≈{100 * t['override_fraction_of_internal_nodes']:.1f}%", f"{100 * s['depth16_d3_official_vs_full']['node_reduction_fraction']:.1f}%fewernodes", f"{100 * s['depth16_d3_official_vs_full']['hard_reduction_fraction']:.1f}%fewerHARD"] out += [f"the crystal lacks {f}" for f in frags if f not in cr] stated = any("retained the depth-14 HARD count" in c for c in s["conclusions"]) contradicts = stated and not s["depth14_window_vs_full_cpg"]["same_hard_count"] if contradicts != w["stored_conclusion_contradicts"]: out.append(f"the stored conclusion on the depth-14 HARD count {'contradicts' if contradicts else 'agrees with'} " "the stored comparison") return out def p2_package(w): out, leaves = [], {row_[0]: row_ for row_ in w["manifest"]["leaves"]} v = w["validation"] for rec, leaf_id, text in ((v["round17"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"])): _, size, digest = leaves[leaf_id] if rec["sha256"] != digest or rec["bytes"] != size: out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive") n = text.count("$$") if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0): out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}") if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)): out.append(f"{rec['file']}: unicode-escape flag differs") if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)): out.append(f"{rec['file']}: bracket-delimiter flag differs") for key, leaf_id in (("pilot_summary_sha256", SUMMARY), ("scheduler_spec_sha256", SPEC), ("pilot_script_sha256", PILOT), ("tail_probe_sha256", TAILPY)): if v[key] != leaves[leaf_id][2]: out.append(f"{key}: recorded digest differs from the archive") s, k = w["summary"], v["key_results"] sym = s["symmetry_numeric_check"] got = {"symmetry_max_numeric_difference": max(sym["max_reflection_area_difference"], sym["max_120deg_rotation_area_difference"]), "d3_depth16_node_reduction": s["depth16_d3_official_vs_full"]["node_reduction_fraction"], "d3_depth16_hard_reduction": s["depth16_d3_official_vs_full"]["hard_reduction_fraction"], "tail_window_depth16_node_reduction": s["tail_window_vs_d3_official"]["node_reduction_fraction"], "tail_window_depth16_hard_reduction": s["tail_window_vs_d3_official"]["hard_reduction_fraction"], "tail_override_fraction": s["tail_window_vs_d3_official"]["override_fraction"]} if got != k: out.append(f"VALIDATION's key results differ from the summary's: {k} vs {got}") if leaves[BASEPY][2] != leaves[R16CODE][2]: out.append("the reference's round16_base_pilot.py is not Round 16's code") pyc = w["pyc"] magic, flags = pyc[:4].hex(), struct.unpack(" sqrt3 x3+ misses the closed wedge; the code's 1e-15 margin keeps cells touching its edge (W4)"), ("PASS", "Symmetry implementation sanity", "computation", "PASS", "W1: 120 directions are invariant under the turn; the pilot's own 40 are not, and its bound moves by 1.1e-3"), ("PASS", "$D_3$ global pilot", "computation", "PASS", "W3: rebuilt exactly; the equal-depth comparison understates the gain - the D3 root's depth-16 cells are the " "full root's depth-18 cells, where it removes 72.9% of nodes and 73.5% of HARD leaves (73.8% / 74.7% exact)"), ("IMPLEMENTED", "CPG", "computation", "PASS", "W4: rebuilt exactly with the code's SYM margin; without it full CPG at depth 14 has 2943 nodes, not 2975"), ("PILOT-PASS", "Windowed CPG", "computation", "PASS", "W4: rebuilt exactly; it overrides on any better key even when no child is certified, which is not the rule the " "production spec states"), ("PILOT-PASS / PRODUCTION CANDIDATE", "Tail-window CPG", "computation", "PARTIAL", "rebuilt exactly (W4); still ahead of official with exact cores; but its edge in overrides over the windowed CPG " "comes from a different override rule, and the same rule from the root is better on every count"), ("STILL OPEN / COMPUTE-DEFERRED", "Global $0.8350$ theorem", "n/a", "n/a", ""), ] def r1_registry(w): return registry.completeness(w["registry"], "R17", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_group, "W2": w2_wedge, "W3": w3_pilot, "W4": w4_schedulers, "W5": w5_numbers, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"turn", "n40_turn_invariant"}, "W2": {"computed", "slack", "needs_radial_exclusion", "qdag_rep_hard"}, "W3": {"computed", "summary", "run019", "exact_official", "matched"}, "W4": {"computed", "summary", "tail", "sym_margin_matters", "depth10_worse_everywhere", "tail_beats_official_exact"}, "W5": {"summary", "text"}, "P1": {"summary", "ref_summary", "stdout", "tail", "spec", "crystal", "stored_conclusion_contradicts"}, "P2": {"validation", "manifest", "text", "crystal", "summary", "code", "pyc", "pilot_reads_outside"}, "R1": {"registry", "definitions", "reviews"}} CLAIMS = { "n40_turn_invariant": False, "slack": 1e-12, "needs_radial_exclusion": True, "qdag_rep_hard": True, "exact_official": [10967, 100, 3045, 2339], "matched": {"sampled": [0.7293, 0.7353], "exact": [0.7383, 0.7467]}, "sym_margin_matters": True, "depth10_worse_everywhere": True, "tail_beats_official_exact": True, "stored_conclusion_contradicts": True, "pilot_reads_outside": True, } def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, VALIDATION, SUMMARY, SPEC, REF_SUMMARY, STDOUT, TAIL, PILOT, PYC} 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"), "validation": json.loads(got[VALIDATION]), "summary": json.loads(got[SUMMARY]), "spec": json.loads(got[SPEC]), "ref_summary": json.loads(got[REF_SUMMARY]), "stdout": json.loads(got[STDOUT]), "tail": json.loads(got[TAIL]), "code": got[PILOT].decode("utf-8"), "pyc": got[PYC][:16], "run019": json.loads(RUN019.read_text(encoding="utf-8")), "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() def build(): return {**copy.deepcopy(inputs), "computed": results_computed, "registry": registry.load(), "definitions": dict(R17_DEFINITIONS), "reviews": list(R17_REVIEWS), **copy.deepcopy(CLAIMS), "turn": turn} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {c: fn(w) for c, fn in CHECKS.items()} for c, f in results.items(): print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n {x}" for x in f[:6])) for key in ("w1", "w2", "w3", "w4", "p2"): print(key, json.dumps(w.get(key), default=float)[:900]) if not args.drill: return s = inputs["summary"] bumped = copy.deepcopy(s) bumped["runs"][0]["nodes"] += 1 frac = copy.deepcopy(s) frac["depth16_windowed_cpg_vs_d3_official"]["node_reduction_fraction"] += 1e-4 tail = copy.deepcopy(inputs["tail"]) tail["overrides"] += 1 spec = copy.deepcopy(inputs["spec"]) spec["split_scheduler"]["gamma"] = 0.02 cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()), ("K2-turn-by-8pi-over-3", "control", {"turn": lambda q, k=1: r19.turn(np.asarray(q, dtype=float), 4 * k)}, set()), ("K3-wedge-slack-1e-11", "control", {"slack": 1e-11}, set()), ("M1-doc-d3-nodes", "mutation", {"text": inputs["text"].replace("\\boxed{12357\\text{ nodes}}", "\\boxed{12358\\text{ nodes}}")}, {"A0"}), ("M2-turn-leaves-phi", "mutation", {"turn": lambda q, k=1: np.array([*r19.turn(np.asarray(q, dtype=float), k)[:2], q[2], *r19.turn(np.asarray(q, dtype=float), k)[3:]])}, {"W1"}), ("M3-40-directions-invariant", "mutation", {"n40_turn_invariant": True}, {"W1"}), ("M4-wedge-needs-no-exclusion", "mutation", {"needs_radial_exclusion": False}, {"W2"}), ("M5-qdag-representative-closed", "mutation", {"qdag_rep_hard": False}, {"W2"}), ("M6-summary-d3-nodes", "mutation", {"summary": bumped}, {"W3", "W5", "P1"}), ("M7-exact-official-hard", "mutation", {"exact_official": [10967, 100, 3045, 2340]}, {"W3"}), ("M8-matched-as-equal-depth", "mutation", {"matched": {"sampled": [0.4732, 0.3273], "exact": [0.7383, 0.7467]}}, {"W3"}), ("M9-tail-overrides", "mutation", {"tail": tail}, {"W4", "P1"}), ("M10-sym-margin-immaterial", "mutation", {"sym_margin_matters": False}, {"W4"}), ("M11-depth10-helps", "mutation", {"depth10_worse_everywhere": False}, {"W4"}), ("M12-tail-loses-exact", "mutation", {"tail_beats_official_exact": False}, {"W4"}), ("M13-summary-fraction", "mutation", {"summary": frac}, {"W5", "P1"}), ("M14-spec-gamma", "mutation", {"spec": spec}, {"P1"}), ("M15-conclusion-consistent", "mutation", {"stored_conclusion_contradicts": False}, {"P1"}), ("M16-pilot-digest", "mutation", {"validation": {**inputs["validation"], "pilot_script_sha256": "0" * 64}}, {"P2"}), ("M17-pilot-self-contained", "mutation", {"pilot_reads_outside": False}, {"P2"}), ("M18-review-dropped", "mutation", {"reviews": list(R17_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-020", "subject": "Round 17: the residual D3 quotient and certified-prune-gain scheduling", "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", "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("R17", "RUN-020", R17_DEFINITIONS, R17_REVIEWS) print(f"registry: {len(R17_DEFINITIONS)} definitions, {len(R17_REVIEWS)} reviews recorded for R17") if __name__ == "__main__": main()