"""RUN-023 - Round 20: necessity-marked mixed lift shards and adaptive witness escalation. Round 20 writes Round 19's necessity markers into a mixed base/lift shard: four depth-40 marked cells, each with B7, B11 and B19 lift trees to depth 12 that keep their open leaves. It proves a negative filter - one legal placement of a witness K whose hull, with the base, has an outer bound below T disqualifies K as the cell's sole closer - and applies it: B23 on cell-00. It compares witnesses by shallow pending fractions, by 3-D placement-search minima and, on the tracked branch's depth-50 cell, by how fast their lift tails contract, and turns that into an escalation policy. Here every tree, count, marker, placement and bracket is rebuilt from the text and the manifest - the shipped package has no code - the streams are re-emitted, this tree runs its own placement search, and the same lifts are run with exact cores. Checks A0 anchors the numbers and formulas below occur in Round 20 as written W1 markers sec. 1-2, 15: the four cells are Round 19's four lowest depth-40 centres; boxes, markers, exact / inner / outer; the manifest and the schema W2 lifts sec. 15-16: the twelve lift trees rebuilt - counts, worst slacks - and their streams re-emitted byte for byte, under one convention only W3 negative sec. 3-6: the counterexample theorem; B23 on cell-00, exact and bracket W4 search sec. 9: the nine recorded placements; this tree's own search W5 efficiency sec. 7-8: the eight-cell and four-cell depth-12 scans W6 deep the benchmark's depth-14/16 comparison on two depth-40 cells W7 tail sec. 11-13: the depth-50 cell's lift tails; B7 with exact cores to closure W8 code what the package ships to replay its claims P1 package benchmark, manifest, summary, policy, crystal and text agree P2 package VALIDATION against the archive; its key checks from the data R1 registry Round 20's judgments reviewed, first-used statuses defined Usage: python code/run023_round20_mixed_escalation.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 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 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 run011_round08_conditional_lift import placed_vertices from run012_round09_adaptive_atlas import core_pieces, pieces_support from run013_round10_reference_dry_run import contact_points PKG = "main.zip!/AMRAL_LUC_FC_Round_20_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_20_Mixed_Witness_Escalation_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_20_v0.1.md" BENCH = PKG + "AMRAL_LUC_FC_Round_20_BENCHMARK_SUMMARY.json" SCHEMA = PKG + "AMRAL_LUC_FC_Round_20_MIXED_SHARD_SCHEMA.json" POLICY = PKG + "AMRAL_LUC_FC_Round_20_ESCALATION_POLICY.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_20_VALIDATION.json" SHARD = PKG + "AMRAL_LUC_FC_Round_20_reference/mixed_shard/" LOG = TREE / "data" / "gate-logs" / "run023-round20-mixed-escalation.json" CACHE = TREE / "data" / "cache" / "run023-lifts.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, TS, TM = 0.835, 0.8350002, 0.8365 ODD = (7, 9, 11, 13, 15, 17, 19, 21, 23) SEARCH_STARTS, SEARCH_SEED = 28, 20260925 ANCHORS = { "W1": ["4個depth-40necessity-markedbasecells", r"\boxed{\texttt{theorem\_ready=false}.}"], "W2": [r"\boxed{\texttt{REFERENCE-MIXED-SHARD-VERIFIED}}"], "W3": [r"P_d>0,", r"J_{B_7}(H)= T: closed += 1 out["worst"] = lb - T if out["worst"] is None else min(out["worst"], lb - T) if keep_tree: out["tree"][p] = "C" continue open_here += 1 if d == max_depth: if keep_tree: out["tree"][p] = "P" continue if keep_tree: out["tree"][p] = "I" trial = [] for a in range(3): hh = list(wh) hh[a] /= 2 trial.append(delta_n(n, 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))] out["per"][d] = [nodes, closed, open_here] level = nxt if not level: break return out def at(per, d): """a max-depth-d probe's (nodes, closed leaves, open leaves), read off a deeper run (keys are strings once the run has been cached); a tree closed earlier is whole""" if str(d) in per: return tuple(per[str(d)]) last = per[max(per, key=int)] return last[0], last[1], 0 def preorder(tree, low_first): topo, tags = [], [] def walk(p): s = tree[p] topo.append(1 if s == "I" else 0) if s == "I": for k in ("0", "1") if low_first else ("1", "0"): walk(p + k) else: tags.append(s) walk("") return topo, tags def pack(bits, msb): out = bytearray((len(bits) + 7) // 8) for i, b in enumerate(bits): if b: out[i // 8] |= (1 << (7 - i % 8)) if msb else (1 << (i % 8)) return bytes(out) def emit(tree, low_first, msb, cert_bit): topo, tags = preorder(tree, low_first) return pack(topo, msb), pack([cert_bit if s == "C" else 1 - cert_bit for s in tags], msb) # ---------------------------------------------------------------- the base and a witness placement (sec. 4-5, 9) def area4(q, n, g): q = np.asarray(q, dtype=float) return r19.exact_area(placed_disc() + placed_reuleaux(3, 0.0, q[:2]) + placed_reuleaux(5, q[2], q[3:5]) + placed_reuleaux(n, g[0], g[1:3])) def bracket4(q, n, g, N=20000): """RUN-022's 20k bracket with a fourth body: the package's inner polygon and the cancellation-free outer polygon""" th = 2 * np.pi * np.arange(N) / N q = np.asarray(q, dtype=float) parts = [placed_disc(), placed_reuleaux(3, 0.0, q[:2]), placed_reuleaux(5, q[2], q[3:5]), placed_reuleaux(n, g[0], g[1:3])] hs = np.stack([pieces_support(p, th) for p in parts]) win = np.argmax(hs, axis=0) pts = np.stack([contact_points(p, th) for p in parts])[win, np.arange(N)] inner = 0.5 * math.fsum(pts[:, 0] * np.roll(pts[:, 1], -1) - np.roll(pts[:, 0], -1) * pts[:, 1]) h = hs.max(axis=0) d = 2 * np.pi / N edge = ((np.roll(h, 1) - h) + (np.roll(h, -1) - h) + 4 * h * math.sin(d / 2) ** 2) / math.sin(d) return inner, 0.5 * math.fsum(h * edge) def _placement(args): q, n, g = args return [area4(q, n, g), *bracket4(q, n, g)] def _search(args): """one start of this tree's placement search: Nelder-Mead on the exact hull area""" q, n, g0 = args r = minimize(lambda g: area4(q, n, 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]] # ---------------------------------------------------------------- Round 19's cells def branch(depth): """the tracked branch's cell at a depth - the official split from the D3 root, keeping the child that holds q-dagger's image - and its path""" q = r22.canonical()[1] c, h = r20.d3_root() path = "" for _ in range(depth): a = r19.official_axis(h) bit = int(q[a] >= c[a]) c, h = r20.children(c, h, a)[bit] path += str(bit) return c, h, path def box(path): """a cell of the D3 root from its path (bit 1 the upper child)""" c, h = r20.d3_root() for bit in path: c, h = r20.children(c, h, r19.official_axis(h))[int(bit)] return c, h def compute(man, placements): out = {} with Pool(14) as pool: c31, h31, prefix = branch(31) nodes, pend = r22.refine(c31, h31, 31, 40, TS, pool) ex = pool.map(r19.base_area, [x[1] for x in pend], chunksize=4) below = [(prefix + x[0], x[1], x[2], e) for x, e in zip(pend, ex) if e < T] brk = pool.map(r22._bracket, [x[1] for x in below]) out["segment"] = [{"path": p, "center": cc, "half": hh, "exact": e, "inner": b[1], "outer": b[2]} for (p, cc, hh, e), b in zip(below, brk)] out["reference"] = [] for cell in man["base_cells"]: cc, hh = cell["base_center"], cell["base_halfwidth"] rec = {"id": cell["base_cell_id"], "lifts": {}} for lf in cell["lifts"]: r = lift(cc, hh, lf["n"], False, pool, 12, keep_tree=True) rec["lifts"][str(lf["n"])] = {"per": r["per"], "worst": r["worst"], "streams": {f"{int(lo)}{int(m)}{cb}": [s.hex() for s in emit(r["tree"], lo, m, cb)] for lo in (True, False) for m in (True, False) for cb in (0, 1)}, "open_depths": sorted({len(p) for p, s in r["tree"].items() if s == "P"})} rec["scan"] = {str(n): lift(cc, hh, n, False, pool, 12)["per"] for n in ODD} out["reference"].append(rec) low = sorted(out["segment"], key=lambda x: x["outer"])[:8] out["eight"] = {"paths": [x["path"] for x in low], "scan": {str(n): [lift(x["center"], x["half"], n, False, pool, 12)["per"] for x in low] for n in (7, 9, 11)}} low_exact = sorted(out["segment"], key=lambda x: x["exact"])[:8] out["eight_by_exact"] = {str(n): [lift(x["center"], x["half"], n, False, pool, 12)["per"] for x in low_exact] for n in (7, 9)} out["deep"] = {} for x in sorted(out["segment"], key=lambda x: x["exact"])[:2]: out["deep"][x["path"]] = {str(n): lift(x["center"], x["half"], n, False, pool, 16)["per"] for n in (7, 9, 11, 13)} c50, h50, _ = branch(50) out["depth50"] = {"tau": r19.tau_f3(h50), "sampled": {str(n): lift(c50, h50, n, False, pool, d)["per"] for n, d in ((7, 26), (11, 22), (13, 20), (19, 20), (21, 20))}} out["exact_close"] = {} cells = [("track50", c50, h50), ("track46", *branch(46)[:2]), ("track43", *branch(43)[:2])] cells += [(cell["base_cell_id"], cell["base_center"], cell["base_halfwidth"]) for cell in man["base_cells"]] for label, cc, hh in cells: r = lift(cc, hh, 7, True, pool, 34) out["exact_close"][label] = {"per": r["per"], "worst": r["worst"]} q00 = man["base_cells"][0]["base_center"] out["placements"] = {str(n): pool.apply(_placement, ((q00, n, g),)) for n, g in placements.items()} out["search"] = {} rng = np.random.default_rng(SEARCH_SEED) for n in ODD: starts = [[rng.uniform(0, 2 * math.pi / n), rng.uniform(-0.02, 0.02), rng.uniform(-0.02, 0.02)] for _ in range(SEARCH_STARTS)] starts.append(list(placements[n])) # and a polish of the package's own minimum res = pool.map(_search, [(q00, n, g) for g in starts]) best = min(res) out["search"][str(n)] = {"best": best, "from_package": res[-1], "random_best": min(res[:-1]), "below_T": [r for r in res if r[0] < T], "best_brackets": list(bracket4(q00, n, best[1]))} return out def _code_key(files): digest = hashlib.sha256() for fn in (rn, delta_n, lift_value, lift, preorder, pack, emit, area4, bracket4, _placement, _search, branch, box, compute): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r11, r12, r13, r19, r20, r22): digest.update(open(mod.__file__, "rb").read()) digest.update(files) digest.update(repr((SEARCH_STARTS, SEARCH_SEED)).encode()) return digest.hexdigest() _COMPUTED = {} def computed(man, placements, 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(man, placements))) 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_markers(w): """the four cells are Round 19's four lowest depth-40 centres; their boxes and markers""" out, man, comp = [], w["manifest_r20"], w["computed"] seg = {x["path"]: x for x in comp["segment"]} lowest = [x["path"] for x in sorted(comp["segment"], key=lambda x: x["exact"])[:4]] cells = {c["base_cell_id"]: c for c in man["base_cells"]} if sorted(cells) != ["cell-00", "cell-01", "cell-02", "cell-03"] \ or [cells[f"cell-0{k}"]["base_path"] for k in range(4)] != lowest: out.append(f"the cells are not Round 19's four lowest depth-40 centres: {lowest}") worst = {"box": 0.0, "exact": 0.0, "inner": 0.0, "outer": 0.0} for cid, cell in cells.items(): s = seg.get(cell["base_path"]) if s is None: out.append(f"{cid}: its path is not a depth-40 cell below T") continue c, h = box(cell["base_path"]) worst["box"] = max(worst["box"], max(abs(a - b) for a, b in zip(list(c) + list(h), cell["base_center"] + cell["base_halfwidth"]))) mk = cell["marker"] if mk["q"] != cell["base_center"] or mk["target"] != T or not near(cell["base_tau"], r19.tau_f3(np.array(cell["base_halfwidth"])), 1e-15): out.append(f"{cid}: marker point, target or tau") for k, mine in (("exact", s["exact"]), ("inner", s["inner"]), ("outer", s["outer"])): worst[k] = max(worst[k], abs(mine - mk[f"{k}_area"])) if not s["outer"] < T: out.append(f"{cid}: the outer bracket is not below T") if worst["box"] > 1e-15 or worst["exact"] > 5e-15 or max(worst["inner"], worst["outer"]) > 1e-12: out.append(f"marker values: worst differences {worst}") want = {"magic": "LUCFC20-MIXED", "global_lebesgue_claim": False, "target": T, "master_target": TM, "theorem_ready": False} if any(man.get(k) != v for k, v in want.items()) or any(k not in man for k in w["schema"]["required"]) \ or w["schema"]["properties"]["magic"]["const"] != man["magic"]: out.append("the manifest's header against the schema") w["w1"] = {"cells": {cid: c["base_path"] for cid, c in cells.items()}, "worst": worst} return out def w2_lifts(w): """the twelve lift trees rebuilt, and their streams re-emitted""" out, man, comp, vs = [], w["manifest_r20"], w["computed"], w["verification"] rebuilt = {r["id"]: r for r in comp["reference"]} summary = {c["base_cell_id"]: {l["witness"]: l for l in c["lifts"]} for c in vs["cells"]} conventions, worst = set(), 0.0 for cell in man["base_cells"]: cid = cell["base_cell_id"] for lf in cell["lifts"]: r = rebuilt[cid]["lifts"][str(lf["n"])] nodes, closed, open_ = at(r["per"], 12) if (nodes, closed, open_) != (lf["nodes"], lf["cert_leaves"], lf["pending_leaves"]) \ or lf["pending_fraction"] != open_ / 4096 or r["open_depths"] not in ([12], []): out.append(f"{cid} {lf['witness']}: rebuilt {nodes, closed, open_}, manifest " f"{lf['nodes'], lf['cert_leaves'], lf['pending_leaves']}") sm = summary[cid][lf["witness"]] worst = max(worst, abs(r["worst"] - sm["worst_cert_slack"])) topo, tags = w["streams"][lf["topology"]["path"]], w["streams"][lf["leaf_tags"]["path"]] if hashlib.sha256(topo).hexdigest() != lf["topology"]["sha256"] or hashlib.sha256(tags).hexdigest() != lf["leaf_tags"]["sha256"] \ or lf["topology"]["bits"] != nodes or lf["leaf_tags"]["bits"] != closed + open_: out.append(f"{cid} {lf['witness']}: a stream's digest or bit count") conventions.add(frozenset(k for k, (tp, tg) in r["streams"].items() if bytes.fromhex(tp) == topo and bytes.fromhex(tg) == tags)) names = {"110": ["lower child first", "most significant bit first", "CERT 0, PENDING 1"]} if conventions != {frozenset({"110"})} or names["110"] != w["stream_convention"]: out.append(f"the streams re-emit under {[sorted(c) for c in conventions]}") if worst > 1e-12: out.append(f"worst CERT slacks differ from the summary's by {worst:.2e}") w["w2"] = {"conventions_matching": [sorted(c) for c in conventions], "slack_worst_difference": worst} return out def w3_negative(w): """sec. 4-5: the counterexample theorem, and B23 on cell-00""" out, cl = [], w["b23"] ev = w["manifest_r20"]["negative_witness_evidence"] comp = w["computed"]["placements"]["23"] g = [ev[0]["placement"][k] for k in ("phi", "tx", "ty")] exact, inner, outer = comp if len(ev) != 1 or ev[0]["base_cell_id"] != "cell-00" or ev[0]["witness"] != "B23" \ or not near(exact, ev[0]["exact_area"], 5e-15) or not near(outer, ev[0]["outer_area"], 1e-12) or not outer < T: out.append(f"B23: exact {exact!r}, outer {outer!r}; manifest {ev[0]['exact_area']}, {ev[0]['outer_area']}") if max(abs(a - b) for a, b in zip(g, cl["g"])) > 5e-7 or not near(exact, cl["exact"], 5e-9) or not near(outer, cl["outer"], 5e-9): out.append(f"B23 against the text: {g}, {exact}, {outer}") if not (inner <= exact <= outer) or not (0 <= g[0] < 2 * math.pi / 23): out.append("B23: bracket order, or the phase outside B23's period") w["w3"] = {"placement": g, "exact": exact, "inner": inner, "outer": outer, "margin_below_T": T - outer} return out def w4_search(w): """sec. 9: the nine recorded placements, and this tree's own search""" out, comp, bench = [], w["computed"], w["bench"] got = {} for rec in bench["placement_search_on_cell00"]: n = int(rec["witness"][1:]) exact, inner, outer = comp["placements"][str(n)] if not near(exact, rec["exact_search"], 5e-15) or not near(outer, rec["outer"], 1e-12) \ or not near(inner, rec["inner"], 1e-12) or (outer < T) != rec["outer_below_target"]: out.append(f"B{n}: rebuilt {exact}, {outer}; recorded {rec['exact_search']}, {rec['outer']}") if not near(exact, w["search_text"][n], 5e-9): out.append(f"B{n}: text {w['search_text'][n]}") s = comp["search"][str(n)] got[n] = {"package": rec["exact_search"], "this_search": s["best"][0], "improvement": rec["exact_search"] - s["best"][0], "starts_below_T": len(s["below_T"]), "best_outer": s["best_brackets"][1]} if s["best"][0] > rec["exact_search"] + 1e-12: out.append(f"B{n}: this tree's search stops above the package's minimum") if not near(s["best"][0], w["own_search"][n], 5e-11): out.append(f"B{n}: this tree's search found {s['best'][0]!r}, claimed {w['own_search'][n]}") new = [n for n in got if n != 23 and got[n]["best_outer"] < T] if (not new) != w["own_search_finds_no_new_disqualification"]: out.append(f"new disqualifications: {new}") w["w4"] = got return out def w5_efficiency(w): """sec. 7: the eight-cell and four-cell depth-12 scans""" out, comp, b = [], w["computed"], w["bench"]["shallow_depth12_certificate_efficiency"] eight = {} for n in (7, 9, 11): per = [at(p, 12) for p in comp["eight"]["scan"][str(n)]] mine = {"mean_nodes": sum(x[0] for x in per) / 8, "mean_pending": sum(x[2] for x in per) / 8, "max_pending": max(x[2] for x in per), "mean_pending_fraction": sum(x[2] for x in per) / 8 / 4096} theirs = {k: b["eight_cell_B7_B9_B11"][f"B{n}"][k] for k in mine} if mine != theirs or not near(mine["mean_pending"], w["eight"][n], 0.05): out.append(f"eight cells, B{n}: {mine}, benchmark {theirs}, text {w['eight'][n]}") eight[n] = mine by_exact = {n: sum(at(p, 12)[2] for p in comp["eight_by_exact"][str(n)]) / 8 for n in (7, 9)} differs = any(by_exact[n] != eight[n]["mean_pending"] for n in (7, 9)) if differs != w["eight_are_lowest_outer_not_lowest_exact"]: out.append(f"the eight lowest by exact centre give {by_exact}") four = {} ref = {r["id"]: r for r in comp["reference"]} for n in (7, 9, 11, 13, 15, 17, 19): per = [at(ref[f"cell-0{k}"]["scan"][str(n)], 12) for k in range(4)] want = b["four_cell_odd_scan_B7_to_B19"][f"B{n}"]["per_cell"] if [{"nodes": x[0], "pending": x[2]} for x in per] != want: out.append(f"four cells, B{n}: {per}") four[n] = sum(x[2] for x in per) / 4 for n in (21, 23): four[n] = sum(at(ref[f"cell-0{k}"]["scan"][str(n)], 12)[2] for k in range(4)) / 4 if four[n] != b["additional_B21_B23_mean_pending"][f"B{n}"]: out.append(f"four cells, B{n}: mean pending {four[n]}") if any(four[n] != v for n, v in w["four"].items()): out.append(f"four-cell means against the text: {four}") w["w5"] = {"eight": eight, "eight_by_lowest_exact": by_exact, "four_mean_pending": four} return out def w6_deep(w): """the benchmark's depth-14 and -16 probes on the two lowest depth-40 cells""" out, comp = [], w["computed"] for row in w["bench"]["deep_certificate_comparison"]: mine = comp["deep"].get(row["path"]) if mine is None: out.append(f"{row['path']}: not one of the two lowest cells") continue for pr in row["probes"]: got = at(mine[pr["witness"][1:]], pr["max_depth"]) if got != (pr["nodes"], pr["cert_leaves"], pr["pending_leaves"]) or pr["pending_fraction"] != got[2] / 2 ** pr["max_depth"]: out.append(f"{row['path'][-6:]} {pr['witness']} depth {pr['max_depth']}: {got}") w["w6"] = {"probes": sum(len(r["probes"]) for r in w["bench"]["deep_certificate_comparison"])} return out def w7_tail(w): """sec. 11-12: the depth-50 cell's lift tails, and B7 with exact cores to closure""" out, comp, tail = [], w["computed"], w["bench"]["fine_depth50_tail"] d50 = comp["depth50"] if not near(d50["tau"], tail["tau"], 1e-18): out.append("the depth-50 cell's tau") table = {} for wit, recs in tail.items(): if not wit.startswith("B"): continue for d, rec in recs.items(): nodes, closed, open_ = at(d50["sampled"][wit[1:]], int(d)) table.setdefault(wit, {})[d] = [nodes, open_] if (nodes, open_) != (rec["nodes"], rec["pending"]) or rec["fraction"] != open_ / 2 ** int(d): out.append(f"{wit} depth {d}: rebuilt {nodes, open_}, benchmark {rec['nodes'], rec['pending']}") for d, fr in w["tail_fractions"].items(): for n, pct in fr.items(): if not near(100 * table[f"B{n}"][d][1] / 2 ** int(d), pct, 5e-4 if pct < 0.1 else 5e-4 * 10): out.append(f"B{n} at depth {d}: {100 * table[f'B{n}'][d][1] / 2 ** int(d):.4f}%, text {pct}%") for d, u in w["u"].items(): if not near(table["B7"][d][1] / 2 ** int(d), u, 5e-4 * u): out.append(f"u_{d}: {table['B7'][d][1] / 2 ** int(d):.4e}, text {u}") omits = "13" not in {str(n) for n in w["tail_fractions"]["18"]} and \ table["B13"]["18"][1] >= max(table[f"B{n}"]["18"][1] for n in (7, 11, 19, 21)) if omits != w["text_depth18_omits_B13"]: out.append("the text's depth-18 list") opens = [table["B7"][d][1] for d in ("18", "20", "22", "24", "26")] if (opens == sorted(opens)) != w["sampled_open_leaves_grow"]: out.append(f"B7's open leaves by depth: {opens}") closes = {} for label, r in comp["exact_close"].items(): last = max(r["per"], key=int) closes[label] = [int(last), r["per"][last][0], r["per"][last][2], r["worst"]] for label, (depth, nodes) in w["exact_close"].items(): if closes[label][:3] != [depth, nodes, 0]: out.append(f"B7 with exact cores on {label}: {closes[label]}") if any(v[2] != 0 or v[3] is None or v[3] <= 0 for v in closes.values()): out.append(f"B7 with exact cores leaves a cell open: {closes}") w["w7"] = {"sampled": table, "exact_cores_close": closes} return out def w8_code(w): """what the package ships to replay itself""" leaves = [row[0] for row in w["manifest"]["leaves"] if row[0].startswith(PKG)] facts = {"ships_code": any(p.endswith(".py") for p in leaves), "schema_types_base_cells": "items" in w["schema"]["properties"]["base_cells"], "manifest_states_encoding": any(k in json.dumps(w["manifest_r20"]) for k in ("bit_order", "msb", "encoding", "child_order"))} w["w8"] = {**facts, "package_files": len(leaves)} return [f"{k}: {v}, expected {w['code_facts'][k]}" for k, v in facts.items() if v != w["code_facts"][k]] def p1_package(w): out, b, man, vs, text = [], w["bench"], w["manifest_r20"], w["verification"], w["text"] if b["mixed_shard_verification"] != vs: out.append("the benchmark's verification block is not the summary") s = {c["base_cell_id"]: c for c in vs["cells"]} for cell in man["base_cells"]: sc = s.get(cell["base_cell_id"]) if sc is None or sc["marker_outer"] != cell["marker"]["outer_area"] or \ [(l["witness"], l["nodes"], l["cert_leaves"], l["pending_leaves"]) for l in sc["lifts"]] != \ [(l["witness"], l["nodes"], l["cert_leaves"], l["pending_leaves"]) for l in cell["lifts"]]: out.append(f"{cell['base_cell_id']}: manifest against the summary") if vs["B23_counterexample"]["outer"] != man["negative_witness_evidence"][0]["outer_area"]: out.append("B23: the summary against the manifest") rec = {int(r["witness"][1:]): r["exact_search"] for r in b["placement_search_on_cell00"]} if any(round(rec[n], 8) != v for n, v in w["search_text"].items()): out.append("sec. 9 against the benchmark") tail = b["fine_depth50_tail"]["B7"] if any(not near(tail[d]["fraction"], u, 5e-4 * u) for d, u in w["u"].items()): out.append("sec. 12 against the benchmark") crystal = gate.squash(w["crystal"]) listed = [n for n in ODD if f"-B{n}0.83" in crystal] for n in listed: if f"-B{n}{rec[n]:.5f}" not in crystal: out.append(f"crystal: B{n}") pol = w["policy"] import re text_states = re.findall(r"^- `([A-Z\-]+)`", text.split("# 2. State semantics")[1].split("# 3.")[0], re.M) matches = pol["states"] == text_states if matches != w["policy_matches_text"]: out.append(f"the escalation policy's states {pol['states']} against sec. 2's {text_states}") statuses = {cell["marker"]["status"] for cell in man["base_cells"]} | {l["status"] for cell in man["base_cells"] for l in cell["lifts"]} \ | {e["status"] for e in man["negative_witness_evidence"]} w["p1"] = {"crystal_lists": listed, "crystal_omits": [n for n in ODD if n not in listed], "policy_states": pol["states"], "text_states": text_states, "manifest_statuses_in_neither": sorted(s for s in statuses if s not in pol["states"] and s not in text_states)} 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 (("round20", 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 (("mixed_shard_manifest_sha256", SHARD + "manifest.json"), ("mixed_shard_verification_sha256", SHARD + "verification_summary.json"), ("benchmark_sha256", BENCH), ("schema_sha256", SCHEMA), ("policy_sha256", POLICY)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") man, vs = w["manifest_r20"], w["verification"] kc = {"four_markers_valid": len(vs["cells"]) == 4 and all(c["marker_valid"] and c["marker_outer"] < T for c in vs["cells"]), "mixed_shard_not_theorem_ready": man["theorem_ready"] is False and vs["theorem_ready"] is False, "B23_counterexample_replays": vs["B23_counterexample"]["outer_below_target"] is True, "partial_lifts_preserve_pending": all(l["pending_leaves"] > 0 and l["status"] == "PARTIAL-UNRESOLVED" for c in man["base_cells"] for l in c["lifts"])} if kc != v["key_checks"] or v["status"] != "PASS": out.append(f"VALIDATION key checks {kc}") w["p2"] = kc return out R20_DEFINITIONS = { "CURRENT CERTIFICATE INCOMPLETE": ("in-line", "sec. 3: what open lift leaves at a depth show - nothing about the witness"), "IMPLEMENTED + REPLAYED": ("in-line", "sec. 21: implemented, and replayed by an independent verifier"), "NOT YET ACHIEVED": ("in-line", "sec. 21: not reached so far"), "REJECTED AS INFERENCE": ("in-line", "sec. 6, 21: a rule of inference this round refuses"), "NO-COUNTEREXAMPLE-FOUND": ("in-line", "sec. 6: the only thing a search that finds no placement below T may record"), "VIABLE-PROVED": ("in-line", "sec. 6: the label such a search may not claim"), "WITNESS-DISQUALIFIED": ("in-line", "sec. 2, 14: a witness with a verified placement whose outer hull area is below T, " "so it cannot close the cell alone"), "REFERENCE-MIXED-SHARD-VERIFIED": ("in-line", "sec. 16: the reference mixed shard replayed - markers, lift trees, every " "CERT and PENDING leaf, the B23 counterexample - with theorem_ready false"), } R20_REVIEWS = [ ("CLOSED", "MIXED SHARD GRAMMAR", "reading", "PARTIAL", "the twelve lift trees rebuild and re-emit byte for byte (W2), but only under a stream convention stated nowhere, the " "schema leaves the base-cell record untyped, and no replay code is shipped (W8)"), ("CLOSED", "WITNESS NEGATIVE FILTER", "analytic", "PASS", "sec. 4 by one line: a placement below T bounds J_K from above (W3)"), ("PILOT-CALIBRATED", "ADAPTIVE ESCALATION", "computation", "PASS", "every scan it is calibrated on rebuilds (W4-W7); a calibration on the pilot's sampled cores, with which B7 closes " "none of these cells and exact cores close all"), ("STILL COMPUTE-DEFERRED", "a_{Leb}≥0.8350", "n/a", "n/a", "sec. 0's boxed summary; read from census v5 on (RUN-003)"), ("CURRENT CERTIFICATE INCOMPLETE", "", "analytic", "PASS", "sec. 3: open leaves bound nothing from above; with exact cores the same B7 trees close (W7)"), ("REFERENCE-MIXED-SHARD-VERIFIED", "", "computation", "PASS", "rebuilt here: markers (W1), the twelve trees and streams (W2), B23 (W3); the package's own replay code is not shipped (W8)"), ("IMPLEMENTED + REPLAYED", "Mixed shard grammar", "computation", "PARTIAL", "replayed here (W1-W3), not by anything in the package: no code is shipped, and the stream convention is found only by trial"), ("IMPLEMENTED", "Necessity markers in mixed shard", "computation", "PASS", "the four markers are Round 19's four lowest depth-40 centres, their outer brackets below T (W1)"), ("IMPLEMENTED", "Partial lift semantics", "computation", "PASS", "every PENDING leaf is at depth 12, and theorem_ready is false (W2)"), ("PROVED", "Witness negative theorem", "analytic", "PASS", "sec. 4 (W3)"), ("VERIFIED-COMPUTATIONAL-PILOT", "B23 negative example", "computation", "PASS", "exact 0.83492540257395, outer 0.8349443917869175 below T by 5.6e-5 (W3)"), ("REJECTED AS INFERENCE", "Absence-of-counterexample -> viability", "analytic", "PASS", "rightly: the sampled trees keep open leaves where exact cores close, so no search outcome certifies anything (W7)"), ("NUMERICAL-EVIDENCE", "Horizon-dependent ranking", "computation", "PARTIAL", "the depth-18 and -20 fractions rebuild exactly (W7), but they rank the pilot's sampled lift bound: its open leaves grow " "with depth for B7 (653 to 2143), while exact cores close B7 on the same cell at depth 21"), ("NOT YET ACHIEVED", "B7 full closure of marked cell", "computation", "PARTIAL", "true of the pilot's sampled bound, whose open leaves grow with depth; with exact cores B7 closes the depth-50 cell at " "lift depth 21 and cell-00 at depth 30, in floating arithmetic (W7)"), ("COMPUTE-DEFERRED", "Global $0.8350$", "n/a", "n/a", ""), ("NO-COUNTEREXAMPLE-FOUND", "6. Absence of counterexample has no positive proof value", "n/a", "n/a", "a label of sec. 6, defined there; not a judgment"), ("VIABLE-PROVED", "6. Absence of counterexample has no positive proof value", "n/a", "n/a", "a label of sec. 6, defined there; not a judgment"), ("WITNESS-DISQUALIFIED", "N1 — Negative Filter", "n/a", "n/a", "a state of sec. 14, defined there; not a judgment"), ] def r1_registry(w): return registry.completeness(w["registry"], "R20", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_markers, "W2": w2_lifts, "W3": w3_negative, "W4": w4_search, "W5": w5_efficiency, "W6": w6_deep, "W7": w7_tail, "W8": w8_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"computed", "manifest_r20", "schema"}, "W2": {"computed", "manifest_r20", "verification", "streams", "stream_convention"}, "W3": {"computed", "manifest_r20", "b23"}, "W4": {"computed", "bench", "search_text", "own_search_finds_no_new_disqualification", "own_search"}, "W5": {"computed", "bench", "eight", "four", "eight_are_lowest_outer_not_lowest_exact"}, "W6": {"computed", "bench"}, "W7": {"computed", "bench", "tail_fractions", "u", "text_depth18_omits_B13", "sampled_open_leaves_grow", "exact_close"}, "W8": {"manifest", "schema", "manifest_r20", "code_facts"}, "P1": {"bench", "manifest_r20", "verification", "text", "crystal", "policy", "policy_matches_text", "search_text", "u"}, "P2": {"validation", "manifest", "text", "crystal", "manifest_r20", "verification"}, "R1": {"registry", "definitions", "reviews"}} def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, BENCH, SCHEMA, POLICY, VALIDATION, SHARD + "manifest.json", SHARD + "verification_summary.json"} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want or l.id.startswith(SHARD + "cell-")) if d is not None} streams = {k[len(SHARD):]: v for k, v in got.items() if k.startswith(SHARD + "cell-")} bench = json.loads(got[BENCH]) return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "bench": bench, "schema": json.loads(got[SCHEMA]), "policy": json.loads(got[POLICY]), "validation": json.loads(got[VALIDATION]), "manifest_r20": json.loads(got[SHARD + "manifest.json"]), "verification": json.loads(got[SHARD + "verification_summary.json"]), "streams": streams, "key_bytes": got[SHARD + "manifest.json"] + got[BENCH], "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() placements = {int(r["witness"][1:]): [r["phi"], r["tx"], r["ty"]] for r in inputs["bench"]["placement_search_on_cell00"]} results_computed = computed(inputs["manifest_r20"], placements, 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(R20_DEFINITIONS), "reviews": list(R20_REVIEWS), **copy.deepcopy(CLAIMS)} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {c: fn(w) for c, fn in CHECKS.items()} for c, f in results.items(): print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n {x}" for x in f[:6])) 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 man, bench, streams = inputs["manifest_r20"], inputs["bench"], inputs["streams"] marker = copy.deepcopy(man) marker["base_cells"][2]["marker"]["outer_area"] += 1e-9 count = copy.deepcopy(man) count["base_cells"][1]["lifts"][0]["pending_leaves"] += 1 flipped = dict(streams) k = man["base_cells"][3]["lifts"][2]["leaf_tags"]["path"] flipped[k] = bytes([streams[k][0] ^ 0x10]) + streams[k][1:] place = copy.deepcopy(bench) place["placement_search_on_cell00"][5]["exact_search"] += 1e-9 deep = copy.deepcopy(bench) deep["deep_certificate_comparison"][1]["probes"][3]["pending_leaves"] += 1 tail = copy.deepcopy(bench) tail["fine_depth50_tail"]["B7"]["26"]["pending"] += 1 policy = copy.deepcopy(inputs["policy"]) policy["states"] = ["BASE-CERTIFIED", "NECESSITY-MARKED", "LIFT-PROBE", "LIFT-ACTIVE", "LIFT-CERTIFIED", "WITNESS-DISQUALIFIED", "PENDING"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()), ("K2-cells-reordered", "control", {"manifest_r20": {**man, "base_cells": list(reversed(man["base_cells"]))}}, set()), ("K3-benchmark-keys-sorted", "control", {"bench": json.loads(json.dumps(bench, sort_keys=True))}, set()), ("M1-doc-b23-outer", "mutation", {"text": inputs["text"].replace("0.83494439<0.835", "0.83494438<0.835")}, {"A0"}), ("M2-marker-outer", "mutation", {"manifest_r20": marker}, {"W1", "P1"}), ("M3-lift-count", "mutation", {"manifest_r20": count}, {"W2", "P1"}), ("M4-stream-bit", "mutation", {"streams": flipped}, {"W2"}), ("M5-stream-convention", "mutation", {"stream_convention": ["higher child first", "most significant bit first", "CERT 0, PENDING 1"]}, {"W2"}), ("M6-b23-claim", "mutation", {"b23": {**CLAIMS["b23"], "outer": 0.83494539}}, {"W3"}), ("M7-recorded-placement", "mutation", {"bench": place}, {"W4"}), ("M8-new-disqualification", "mutation", {"own_search_finds_no_new_disqualification": False}, {"W4"}), ("M8b-own-search-value", "mutation", {"own_search": {**CLAIMS["own_search"], 19: 0.8354088638}}, {"W4"}), ("M9-eight-claim", "mutation", {"eight": {**CLAIMS["eight"], 7: 160.4}}, {"W5"}), ("M10-eight-selection", "mutation", {"eight_are_lowest_outer_not_lowest_exact": False}, {"W5"}), ("M11-deep-probe", "mutation", {"bench": deep}, {"W6"}), ("M12-tail-count", "mutation", {"bench": tail}, {"W7"}), ("M13-exact-closure", "mutation", {"exact_close": {**CLAIMS["exact_close"], "cell-00": [29, 18555]}}, {"W7"}), ("M14-open-leaves", "mutation", {"sampled_open_leaves_grow": False}, {"W7"}), ("M15-ships-code", "mutation", {"code_facts": {**CLAIMS["code_facts"], "ships_code": True}}, {"W8"}), ("M16-policy-states", "mutation", {"policy": policy}, {"P1"}), ("M17-validation-digest", "mutation", {"validation": {**inputs["validation"], "schema_sha256": "0" * 64}}, {"P2"}), ("M18-validation-check", "mutation", {"validation": {**inputs["validation"], "key_checks": {**inputs["validation"]["key_checks"], "B23_counterexample_replays": False}}}, {"P2"}), ("M19-review-dropped", "mutation", {"reviews": list(R20_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-023", "subject": "Round 20: necessity-marked mixed lift shards and adaptive witness escalation", "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("R20", "RUN-023", R20_DEFINITIONS, R20_REVIEWS) print(f"registry: {len(R20_DEFINITIONS)} definitions, {len(R20_REVIEWS)} reviews recorded for R20") if __name__ == "__main__": main()