"""RUN-022 - Round 19: the lazy proof cascade, necessity markers and the base/lift switch. Round 19 continues Round 18's Tail-Window checkpoint from its 2048 pending roots. It evaluates the three one-sided bounds lazily - APR, then CORE, and REP only if both fail - and measures the saving on a fixed tree; it prices the continuation to depth 20 against Round 18's break-even; it rechecks, with an exact kernel, the depth-20 cells whose sampled centre falls below 0.835; it follows the official near-minimum configuration's canonical branch until an outer bracket proves a centre below 0.835; and it separates what such a point forces (no base-only closure along its branch) from when to spend a B7 lift on it. Here every tree is rebuilt - the A/B, both continuations, the tracked branch, the depth-31 segmentation, the B7 switch curve and its floor - the exact values come from this tree's own exact hull, and the shipped probe and exact kernel are read, after that, for what they do. Checks A0 anchors the numbers and formulas below occur in Round 19 as written W1 cascade sec. 1-4: Thm 2.1; the fixed-tree A/B from the 2048 roots - nodes, pending, REP calls eager and lazy; every accepted leaf closes by CORE W2 continuation sec. 5-7: the Tail-Window continuation 16 -> 18 -> 20 - nodes, SYM, CORE, pending, overrides, the probe's evaluation counts; kappa's arithmetic W3 depth 20 sec. 8-9: the 10114 depth-20 centres, sampled and exact; the 12 sampled candidates and their recheck; the profile W4 branch sec. 10-12: q-dagger's canonical image; the tracked branch row by row; the outer brackets and the first depth one falls below 0.835 W5 segment sec. 13-18: Thm 13.1; the depth-31 cell refined to depth 40 - nodes, pending, exact centres, brackets W6 switch sec. 16, 21-24, 27: the B7 depth-12 probes along the branch, the base-zero floor at depth 12 and 18, the fractions and the tau^0.70 fit W7 code sec. 3-8, 12, 17-22: what the shipped probe and exact kernel do, read after the rebuild P1 package benchmark, activation policy, crystal, summaries and profiles agree with each other and with the text P2 package VALIDATION against the archive; its key checks from the data R1 registry Round 19's judgments reviewed, first-used statuses defined Usage: python code/run022_round19_necessity_lift.py [--drill] [--blind CID] """ import argparse import copy import hashlib import inspect import json import math import re from multiprocessing import Pool import numpy as np 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 run021_round18_shard_emitter as r21 from corpus import SOURCES, TREE, source_bytes, walk_sources from run009_round06_witness_exchange import placed_disc, placed_reuleaux from run012_round09_adaptive_atlas import pieces_support from run013_round10_reference_dry_run import contact_points PKG = "main.zip!/AMRAL_LUC_FC_Round_19_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_19_Necessity_Lazy_Lift_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_19_v0.1.md" BENCH = PKG + "AMRAL_LUC_FC_Round_19_BENCHMARK_SUMMARY.json" POLICY = PKG + "AMRAL_LUC_FC_Round_19_ACTIVATION_POLICY.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_19_VALIDATION.json" REF = PKG + "AMRAL_LUC_FC_Round_19_reference/" PROBE = REF + "continuation_probe.py" KERNEL = REF + "official_exact_kernel_minimal.py" REFS = {k: REF + k + ".json" for k in ("official_seed_branch_track", "necessity_segmentation_brackets", "necessity_segmentation_exact_profile", "tail_depth18_summary", "tail_depth20_profile", "tail_depth20_summary")} LOG = TREE / "data" / "gate-logs" / "run022-round19-necessity-lift.json" CACHE = TREE / "data" / "cache" / "run022-continuations.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, TS = 0.835, 0.8350002 GATE = T - 0.025 # Round 18's gate for trying another axis ACTIVATE = 10 # ... from this depth on NB = 20000 # the brackets' support directions (sec. 12) SWITCH_DEPTHS = (20, 24, 28, 31, 34, 37, 40, 43, 46, 50) ANCHORS = { "W1": [r"\max\{L_{\rmAPR},L_{\rmREP},L_{\rmCORE}\}\geT.", r"\boxed{\text{APR}\to\text{CORE}\to\text{REP}}", r"13206\text{nodes},", r"4944\text{pending},", r"12659,", r"7.2903\text{s}.", r"10523.", r"6.8687\text{s}.", r"\boxed{16.87\%\text{REPcallseliminated}}", r"\boxed{5.78\%\text{wall-timereduction}.}"], "W2": [r"12634\text{nodes}.", r"4599\text{pending}.", r"22.7531\text{s}.", r"\boxed{11.11\text{ms}}", r"26455\text{nodes}.", r"10114\text{pending}.", r"55.3844\text{s}.", r"\boxed{78.1375\text{CPU-s}.}", r"\boxed{38.15\text{ms/originaldepth-16pendingroot}.}", r"14.41\text{ms}.", r"\boxed{2.65\times.}"], "W3": [r"A_{\rmsample}(q_c)<0.835.", r"0.83395139.", r"\boxed{0/12}", r"\boxed{0.83586503.}"], "W4": [r"0.0060794482,0.0105298389,0.4188548915,-0.0114949286,-0.0199175943", r"A(q^\dagger)=0.8347809459115.", r"0.8352534195.", r"0.8352704487>T.", r"\boxed{0.8349033738.}", r"\boxed{0.8349184947= threshold: return True, "APR", apr, False if core >= threshold: return True, "CORE", core, False vals = {"APR": apr, "CORE": core, "REP": rep(b, threshold)} mode = max(vals, key=vals.get) return vals[mode] >= threshold, mode, vals[mode], True def eager(b, threshold, rep_t): best = max(b[0], b[1], rep(b, rep_t)) return best >= threshold, best # ---------------------------------------------------------------- the continuations (sec. 3, 5-6) def continue_root(args): """one pending root continued to depth d1 as the shipped probe does it: the official split, or Round 18's Tail-Window rule, the parent re-evaluated at the target only when the official children certify none. Every evaluation is counted the probe's way and checked: lazy against eager, REP built at T against at T_search, the eager keys' axis""" path, c, h, d1, policy = args out = {"nodes": 0, "SYM": 0, "APR": 0, "CORE": 0, "REP": 0, "PENDING": 0, "overrides": 0, "evals": 0, "parent_evals": 0, "rep_lazy": 0, "rep_skipped": 0, "lazy_eager_differ": 0, "rep_at_T_differs": 0, "eager_axis_differs": 0, "pending": []} def ev(cc, hh, threshold=TS, parent=False): b = bounds(cc, hh) lz = lazy(b, threshold) out["evals"] += 1 out["parent_evals"] += parent out["rep_lazy"] += lz[3] out["rep_skipped"] += lz[0] and lz[1] == "CORE" ok_eager = eager(b, threshold, threshold)[0] out["lazy_eager_differ"] += ok_eager != lz[0] out["rep_at_T_differs"] += eager(b, threshold, T)[0] != ok_eager return b, lz stack = [(path, np.asarray(c, dtype=float), np.asarray(h, dtype=float), None)] while stack: p, c, h, pre = stack.pop() out["nodes"] += 1 if r20.sym(c, h, 1e-15): out["SYM"] += 1 continue if pre is None: pre = ev(c, h) b, (ok, mode, best, _) = pre if ok: out[mode] += 1 continue if len(p) >= d1: out["PENDING"] += 1 out["pending"].append([p, c.tolist(), h.tolist(), best, b[2], b[3]]) continue a = r19.official_axis(h) kids = r20.children(c, h, a) if policy == "official": stack += [(p + "1", *kids[1], None), (p + "0", *kids[0], None)] continue vals = [ev(cc, hh) for cc, hh in kids] if not any(v[1][0] for v in vals): parent = ev(c, h, T, parent=True) if len(p) >= ACTIVATE and parent[1][2] >= GATE: choice, choice_eager = None, None for alt in range(5): if alt == a: continue kk = r20.children(c, h, alt) vv = [ev(cc, hh) for cc, hh in kk] cert = sum(v[1][0] for v in vv) if cert <= 0: continue tie = (-r19.tau_f3(kk[0][1]), -alt) key = (cert, min(v[1][2] for v in vv), sum(v[1][2] for v in vv), *tie) eb = [eager(v[0], TS, TS)[1] for v in vv] key_eager = (cert, min(eb), sum(eb), *tie) if choice is None or key > choice[0]: choice = (key, alt, kk, vv) if choice_eager is None or key_eager > choice_eager[0]: choice_eager = (key_eager, alt) if cert == 2: break if choice is not None: kids, vals = choice[2], choice[3] out["overrides"] += 1 out["eager_axis_differs"] += choice_eager[1] != choice[1] stack += [(p + "1", *kids[1], vals[1]), (p + "0", *kids[0], vals[0])] return out def continuation(roots, d1, policy, pool): res = pool.map(continue_root, [(p, c, h, d1, policy) for p, c, h in roots], chunksize=8) tot = {k: sum(r[k] for r in res) for k in res[0] if k != "pending"} return tot, [x for r in res for x in r["pending"]] # ---------------------------------------------------------------- exact values and brackets (sec. 8, 12, 18) def bodies(q): q = np.asarray(q, dtype=float) return placed_disc() + placed_reuleaux(3, 0.0, q[:2]) + placed_reuleaux(5, q[2], q[3:5]) def brackets(q, n=NB): """sec. 12's 20k-direction bracket. Outer: the polygon of the n support lines, which holds the hull; each edge from its neighbours' support values, with 1 - cos d written 2 sin^2(d/2) (the plain form loses 7.5e-10 at n = 20000 to the rounding of cos d). Inner: the polygon through the contact point of the body that wins each direction, as the package draws it""" 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])] 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 _centre(args): """a pending cell's centre: the pilot's sampled area (plus its pad back) and the exact area""" q = np.asarray(args, dtype=float) return r19.sampled_hull([placed_reuleaux(3, 0.0, q[:2]), placed_reuleaux(5, q[2], q[3:5])]), r19.base_area(q) def _bounds(args): return bounds(*args) def _bracket(args): return [r19.base_area(args), *brackets(args)] # ---------------------------------------------------------------- the tracked branch (sec. 10-12) def canonical(): """q-dagger's image in the canonical wedge (Round 17's quotient)""" q = np.array([*r19.QDAG[:2], r19.QDAG[2] % r20.P5, *r19.QDAG[3:]]) name, g = r20.representative(q) return name, g def track(q, depth=50): """the official split from the D3 root, keeping the child that holds q""" c, h = r20.d3_root() rows, path = [], "" for d in range(depth + 1): if d: a = r19.official_axis(h) kids = r20.children(c, h, a) bit = int(q[a] >= c[a]) (c, h), path = kids[bit], path + str(bit) b = bounds(c, h) vals = {"APR": b[0], "REP": rep(b, T), "CORE": b[1]} mode = max(vals, key=vals.get) rows.append({"depth": d, "path": path, "center": c.tolist(), "half": h.tolist(), "contains_seed": bool(np.all(np.abs(q - c) <= h)), "exact": r19.base_area(c), "sampled": b[2], "tau": b[3], "lower_best": vals[mode], "lower_mode": mode, # the package's distance leaves the phase out: x3, y3, x5, y5 only "seed_distance": float(np.linalg.norm((q - c)[[0, 1, 3, 4]])), "brackets": list(brackets(c))}) return rows def refine(c0, h0, d0, d1, threshold, pool): """sec. 17: a cell refined by the official split to depth d1; closed cells drop out""" level, nodes, pending = [("", np.asarray(c0, dtype=float), np.asarray(h0, dtype=float))], 0, [] for d in range(d0, d1 + 1): nodes += len(level) keep = [x for x in level if not r20.sym(x[1], x[2], 1e-15)] bs = pool.map(_bounds, [(c.tolist(), h.tolist()) for _, c, h in keep], chunksize=8) nxt = [] for (p, c, h), b in zip(keep, bs): if lazy(b, threshold)[0]: continue if d == d1: pending.append([p, c.tolist(), h.tolist(), b[2], b[3]]) continue for k, (cc, hh) in enumerate(r20.children(c, h, r19.official_axis(h))): nxt.append((p + str(k), cc, hh)) level = nxt return nodes, pending def compute(tail_files): out = {} roots = [(p, c.tolist(), h.tolist()) for p, t, c, h in r21.decode_certificate(tail_files)["leaves"] if t == 2] out["roots"] = len(roots) with Pool(14) as pool: out["ab"] = continuation(roots, 18, "official", pool)[0] t18, p18 = continuation(roots, 18, "tail", pool) t20, p20 = continuation([(p, c, h) for p, c, h, *_ in p18], 20, "tail", pool) out["tail18"], out["tail20"] = t18, t20 cs = pool.map(_centre, [c for p, c, h, *_ in p20], chunksize=16) out["depth20"] = [[p, c, h, best, ca, tau, s, e] for (p, c, h, best, ca, tau), (s, e) in zip(p20, cs)] cand = [x for x in out["depth20"] if x[4] < T] out["depth20_brackets"] = pool.map(_bracket, [x[1] for x in cand]) name, q = canonical() out["canonical"] = {"name": name, "q": q.tolist(), "area": r19.base_area(q)} rows = track(q) out["track"] = rows r31 = rows[31] out["segment"] = {} for label, thr in (("TS", TS), ("T", T)): nodes, pend = refine(r31["center"], r31["half"], 31, 40, thr, pool) out["segment"][label] = {"nodes": nodes, "pending": pend} pend = out["segment"]["TS"]["pending"] ex = pool.map(r19.base_area, [x[1] for x in pend], chunksize=4) out["segment_exact"] = ex below = [x[1] for x, e in zip(pend, ex) if e < T] out["segment_brackets"] = pool.map(_bracket, below) out["switch"] = {str(d): r19.b7_probe(rows[d]["center"], rows[d]["half"], False, pool) for d in SWITCH_DEPTHS} out["floor"] = {str(k): r19.b7_probe(q, [0.0] * 5, False, pool, max_depth=k) for k in (12, 18)} # the same probes with exact cores: how much of the floor is the pilot's sampling out["switch_exact"] = {str(d): r19.b7_probe(rows[d]["center"], rows[d]["half"], True, pool) for d in SWITCH_DEPTHS} out["floor_exact"] = {str(k): r19.b7_probe(q, [0.0] * 5, True, pool, max_depth=k) for k in (12, 18)} return out def _code_key(files): digest = hashlib.sha256() for fn in (bounds, rep, lazy, eager, continue_root, continuation, bodies, brackets, _centre, _bounds, _bracket, canonical, track, refine, compute): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r11, r12, r13, r19, r20, r21): digest.update(open(mod.__file__, "rb").read()) for k in sorted(files): digest.update(k.encode() + files[k]) return digest.hexdigest() _COMPUTED = {} def computed(files): key = _code_key(files) 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(files))) 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_cascade(w): """Thm 2.1 on every evaluation of every tree here, and the fixed-tree A/B""" out, ab, cl = [], w["computed"]["ab"], w["ab"] runs = [w["computed"][k] for k in ("ab", "tail18", "tail20")] evals = sum(r["evals"] for r in runs) if any(r["lazy_eager_differ"] for r in runs): out.append("a cell where the lazy and the eager classifier disagree") if any(r["rep_at_T_differs"] for r in runs): out.append("REP built at T instead of T_search changes a classification") if any(r["eager_axis_differs"] for r in runs): out.append("eager values would pick another override axis") certified = ab["APR"] + ab["CORE"] + ab["REP"] got = {"nodes": ab["nodes"], "pending": ab["PENDING"], "rep_eager": ab["evals"], "rep_lazy": ab["rep_lazy"]} if got != {k: cl[k] for k in got}: out.append(f"A/B {got}, text {cl}") if (ab["CORE"] == certified == ab["rep_skipped"] and ab["APR"] == ab["REP"] == 0) != w["all_by_core"]: out.append(f"accepted leaves by mode: APR {ab['APR']}, CORE {ab['CORE']}, REP {ab['REP']}") cut = 1 - ab["rep_lazy"] / ab["evals"] wall = 1 - cl["seconds"][1] / cl["seconds"][0] if not near(cut, cl["rep_cut"], 5e-5) or not near(wall, cl["wall_cut"], 5e-5): out.append(f"REP cut {cut:.5f}, wall cut {wall:.5f}") w["w1"] = {"A/B": got, "SYM": ab["SYM"], "accepted_by": {k: ab[k] for k in ("APR", "CORE", "REP")}, "rep_cut": cut, "wall_cut_from_the_text's_timings": wall, "evaluations_checked": evals, "rep_at_T_changes_a_classification": sum(r["rep_at_T_differs"] for r in runs)} return out def w2_continuation(w): out, cl = [], w["continuation"] got = {} for key, summary in (("d18", "tail_depth18_summary"), ("d20", "tail_depth20_summary")): c = w["computed"]["tail18" if key == "d18" else "tail20"] s = w["refs"][summary] mine = {"nodes": c["nodes"], "SYM": c["SYM"], "APR": c["APR"], "REP": c["REP"], "CORE": c["CORE"], "PENDING": c["PENDING"], "overrides": c["overrides"]} theirs = {**s["counts"], "nodes": s["nodes"], "overrides": s["overrides"]} if mine != theirs: out.append(f"{key}: rebuilt {mine}, summary {theirs}") if mine["nodes"] != cl[key]["nodes"] or mine["PENDING"] != cl[key]["pending"]: out.append(f"{key}: rebuilt {mine['nodes']} nodes, {mine['PENDING']} pending; text {cl[key]}") calls = c["evals"] probe = {"calls": calls, "rep": c["rep_lazy"], "rep_skipped": c["rep_skipped"]} want = {k: s["stats"][k] for k in probe} if (probe == want) != w["evaluation_accounting"]: out.append(f"{key}: evaluations {probe}, the probe's {want}") got[key] = {**mine, "roots": w["computed"]["roots"] if key == "d18" else w["computed"]["tail18_pending"], "evaluations": calls, "of_them_parent_re-evaluations": c["parent_evals"], "rep_calls": c["rep_lazy"], "eager_keys_pick_another_axis": c["eager_axis_differs"]} roots18, roots20 = got["d18"]["roots"], got["d20"]["roots"] # sec. 5-6 call the counts new nodes; they are the trees' nodes, roots included include = all(got[k]["nodes"] == cl[k]["nodes"] != got[k]["nodes"] - got[k]["roots"] for k in ("d18", "d20")) if include != w["new_counts_include_roots"]: out.append(f"the 'new' node counts: roots included {include}") b = w["bench"]["continuation_cost"] s18, s20 = w["refs"]["tail_depth18_summary"]["seconds"], w["refs"]["tail_depth20_summary"]["seconds_sum_worker"] cum = s18 + s20 ms = 1000 * cum / roots18 be = 1000 * w["break_even_r18"] arith = {"cumulative": cum, "ms_per_root": ms, "ms_per_root_d18": 1000 * s18 / roots18, "break_even_ms": be, "ratio": ms / be} if not (near(cum, cl["cumulative"], 5e-5) and near(ms, cl["ms_per_root"], 5e-3) and near(be, cl["break_even_ms"], 5e-3) and near(ms / be, cl["ratio"], 5e-3) and near(arith["ms_per_root_d18"], cl["d18"]["ms_per_root"], 5e-3) and near(s18, cl["d18"]["seconds"], 5e-5) and near(s20, cl["d20"]["seconds"], 5e-5) and near(b["depth16_to20_cpu_seconds"], cum, 1e-9) and near(b["round18_break_even_seconds_per_saved_pending_leaf"], w["break_even_r18"], 1e-12)): out.append(f"kappa's arithmetic: {arith}") got["kappa"] = arith w["w2"] = got return out def w3_depth20(w): out, cl, rows = [], w["depth20"], w["computed"]["depth20"] prof = w["refs"]["tail_depth20_profile"] samp = np.array([x[4] for x in rows]) # the probe's centre area: the pilot's hull less its pad exact = np.array([x[7] for x in rows]) below = int(np.sum(samp < T)) cand = [x for x in rows if x[4] < T] ex_c = [x[7] for x in cand] got = {"pending": len(rows), "sampled_below": below, "sampled_min": float(samp.min()), "candidates_exact_min": min(ex_c) if ex_c else None, "candidates_exact_below": sum(e < T for e in ex_c), "candidates_outer_below": sum(b[2] < T for b in w["computed"]["depth20_brackets"]), "exact_below_among_all": int(np.sum(exact < T)), "sampled_minus_exact_max": float(np.max(samp - exact)), "exact_min_among_all": float(exact.min())} if below != cl["below"] or not near(got["sampled_min"], cl["sampled_min"], 5e-9) \ or got["candidates_exact_below"] != cl["exact_below"] or not near(got["candidates_exact_min"], cl["exact_min"], 5e-9): out.append(f"depth 20: {got}, text {cl}") if (got["sampled_minus_exact_max"] <= 0) != w["sampled_below_exact"]: out.append(f"a sampled centre above its exact value by {got['sampled_minus_exact_max']:.3g}") if got["exact_below_among_all"]: out.append(f"{got['exact_below_among_all']} exact centres below 0.835") # the profile, as its keys ask qs = {k: float(np.quantile(samp, float(k))) for k in prof["center_quantiles"]} bq = {k: float(np.quantile([x[3] for x in rows], float(k))) for k in prof["best_quantiles"]} tq = {k: float(np.quantile([x[5] for x in rows], float(k))) for k in prof["tau_quantiles"]} nc = {k: int(np.sum(samp <= T + float(k))) for k in prof["near_counts"]} bad = [k for k, v in qs.items() if not near(v, prof["center_quantiles"][k], 1e-12)] bad += [f"best {k}" for k, v in bq.items() if not near(v, prof["best_quantiles"][k], 1e-12)] bad += [f"tau {k}" for k, v in tq.items() if not near(v, prof["tau_quantiles"][k], 1e-12)] bad += [f"near {k}" for k, v in nc.items() if v != prof["near_counts"][k]] if prof["count"] != len(rows) or prof["center_below_target"] != below or not near(prof["center_min"], got["sampled_min"], 1e-12): bad.append("count / below / min") top = sorted(rows, key=lambda x: x[4])[:8] for mine, theirs in zip(top, prof["top8"]): if mine[0] != theirs["path"] or not near(mine[4], theirs["center_area"], 1e-12) \ or not near(mine[3], theirs["best"], 1e-12) or not near(mine[5], theirs["tau"], 1e-12) \ or max(abs(a - b) for a, b in zip(mine[1] + mine[2], theirs["center"] + theirs["half"])) > 1e-15: bad.append(f"top8 {theirs['path']}") if bad: out.append(f"the depth-20 profile: {bad[:6]}") w["w3"] = got return out def w4_branch(w): out, cl, comp = [], w, w["computed"] rows, theirs = comp["track"], w["refs"]["official_seed_branch_track"] can = comp["canonical"] q = np.array(can["q"]) if max(abs(a - b) for a, b in zip(q, theirs["canonicalization"]["q"])) > 1e-15 \ or max(abs(a - b) for a, b in zip(q, cl["qdagger"])) > 5e-11 \ or not near(math.atan2(q[1], q[0]), theirs["canonicalization"]["angle_t3"], 1e-15) \ or not near(can["area"], cl["qdagger_area"], 5e-14) \ or not near(can["area"], r19.base_area(np.array([*r19.QDAG[:2], r19.QDAG[2] % r20.P5, *r19.QDAG[3:]])), 1e-15): out.append(f"q-dagger's image {can}") worst = {"center": 0.0, "half": 0.0, "exact": 0.0, "sampled": 0.0, "tau": 0.0, "lower_best": 0.0, "seed_distance": 0.0} by_depth = {r["depth"]: r for r in theirs["rows"]} for mine in rows: row = by_depth.get(mine["depth"]) if row is None: out.append(f"depth {mine['depth']}: no row in the track") continue if mine["path"] != row["path"] or mine["lower_mode"] != row["lower_mode"] or mine["contains_seed"] != row["contains_seed"]: out.append(f"depth {row['depth']}: path, mode or containment differ") for k, rk in (("center", "center"), ("half", "half")): worst[k] = max(worst[k], max(abs(a - b) for a, b in zip(mine[k], row[rk]))) for k, rk in (("exact", "exact_center_area"), ("sampled", "sample_inner_center_area"), ("tau", "tau"), ("lower_best", "lower_best"), ("seed_distance", "seed_to_center_distance")): worst[k] = max(worst[k], abs(mine[k] - row[rk])) if len(rows) != len(theirs["rows"]) or max(worst.values()) > 1e-12: out.append(f"the track: worst differences {worst}") first = next((r["depth"] for r in rows if r["brackets"][1] < T), None) for d, (ex, up) in cl["brackets"].items(): r = rows[int(d)] if not near(r["exact"], ex, 5e-11) or not near(r["brackets"][1], up, 5e-9): out.append(f"depth {d}: exact {r['exact']!r}, outer {r['brackets'][1]!r}; text {ex}, {up}") if first != cl["first_sublevel"]: out.append(f"first outer bracket below 0.835 at depth {first}") if any(not (r["brackets"][0] <= r["exact"] <= r["brackets"][1]) for r in rows): out.append("an exact value outside its bracket") w["w4"] = {"canonical": can["name"], "q": can["q"], "area": can["area"], "rows": len(rows), "worst": worst, "first_outer_below": first, "by_depth": {r["depth"]: [r["exact"], *r["brackets"]] for r in rows if r["depth"] >= 28}} return out def w5_segment(w): out, cl, comp = [], w["segmentation"], w["computed"] seg = comp["segment"] pend, ex = seg["TS"]["pending"], comp["segment_exact"] brk = comp["segment_brackets"] below = [(x, e) for x, e in zip(pend, ex) if e < T] got = {"nodes": seg["TS"]["nodes"], "pending": len(pend), "nodes_at_T": seg["T"]["nodes"], "pending_at_T": len(seg["T"]["pending"]), "exact_below": len(below), "outer_below": sum(b[2] < T for b in brk), "exact_min": min(ex)} if {k: got[k] for k in cl} != cl or got["nodes_at_T"] != got["nodes"] or got["pending_at_T"] != got["pending"]: out.append(f"segmentation {got}, text {cl}") # the package's two files: every bracket, and the exact profile base = comp["track"][31]["path"] mine = {base + x[0]: (e, *b[1:]) for (x, _), b, e in zip(below, brk, [e for _, e in below])} theirs = w["refs"]["necessity_segmentation_brackets"] missing = [b["path"] for b in theirs if b["path"] not in mine] worst = max((max(abs(mine[b["path"]][0] - b["exact"]), abs(mine[b["path"]][1] - b["inner"]), abs(mine[b["path"]][2] - b["outer"])) for b in theirs if b["path"] in mine), default=0.0) flags = sum((mine[b["path"]][2] < T) != b["outer_below_target"] for b in theirs if b["path"] in mine) prof = w["refs"]["necessity_segmentation_exact_profile"] qs = {k: float(np.quantile(ex, float(k))) for k in prof["quantiles"]} low = sorted(zip(ex, pend), key=lambda t: t[0])[:len(prof["lowest20"])] lows = [(base + x[0], e, x[4], x[3]) for e, x in low] bad_low = [r["path"] for r, m in zip(prof["lowest20"], lows) if r["path"] != m[0] or not near(r["exact"], m[1], 1e-12) or not near(r["tau"], m[2], 1e-15) or not near(r["sample_inner"], m[3], 1e-12)] if missing or worst > 1e-9 or flags or len(theirs) != len(below) or prof["count"] != len(pend) \ or prof["below_target"] != len(below) or not near(prof["min"], min(ex), 1e-12) \ or any(not near(v, prof["quantiles"][k], 1e-12) for k, v in qs.items()) or bad_low: out.append(f"the package's segmentation files: {len(missing)} paths missing, worst {worst:.2e}, " f"{flags} flags, lowest20 {bad_low[:3]}") w["w5"] = {**got, "bracket_worst": worst, "bracket_paths_missing": len(missing), "bracket_path_lengths": sorted({len(b['path']) for b in theirs})} return out def w6_switch(w): out, comp, bench = [], w["computed"], w["bench"] cl, fr = w["switch"], w["fractions"] got = {d: [v["nodes"], v["closed"], v["unresolved"]] for d, v in comp["switch"].items()} want = {str(r["base_depth"]): [r["b7_depth12_nodes"], r["b7_depth12_closed_leaves"], r["b7_depth12_unresolved_leaves"]] for r in bench["b7_switch_curve_depth12"]} if got != want: out.append(f"the switch curve {got}, benchmark {want}") if any(got[d][2] != u for d, u in cl["curve"].items()) or got["31"][0] != cl["31"][0] or got["31"][2] != cl["31"][1]: out.append(f"the switch curve against the text's sec. 16 and 21") fl = {k: [v["nodes"], v["closed"], v["unresolved"]] for k, v in comp["floor"].items()} fb = bench["b7_exact_base_point_floor"] if fl != {k: [fb[f"depth{k}"][x] for x in ("nodes", "closed_leaves", "unresolved_leaves")] for k in ("12", "18")} \ or fl["12"][2] != cl["floor12"] or fl["18"][2] == 0: out.append(f"the base-zero floor {fl}") frac = {"31": 100 * got["31"][2] / 4096, "40": 100 * got["40"][2] / 4096, "46": 100 * got["46"][2] / 4096, "floor": 100 * fl["12"][2] / 4096} if any(not near(frac[k], fr[k], 5e-3) for k in fr): out.append(f"fractions {frac}") f0 = fl["12"][2] / 4096 taus = {str(r["base_depth"]): r["tau"] for r in bench["b7_switch_curve_depth12"]} rows = {str(r["depth"]): r for r in comp["track"]} def fit(depths): x = np.log([rows[d]["tau"] for d in depths]) y = np.log([got[d][2] / 4096 - f0 for d in depths]) return float(np.polyfit(x, y, 1)[0]) ten, nine = fit(list(got)), fit(list(cl["curve"])) if not (near(ten, w["exponent"], 0.01) and near(nine, w["exponent"], 0.01)): out.append(f"the tau exponent: ten points {ten:.3f}, the text's nine {nine:.3f}") if ("43" not in cl["curve"]) != w["curve_omits_43"]: out.append("the text's list of depths") if any(not near(rows[d]["tau"], taus[d], 1e-15) for d in taus): out.append("the curve's tau against the tracked branch") # with exact cores: every probe leaves fewer leaves open, and the floor falls most ex = {d: v["unresolved"] for d, v in comp["switch_exact"].items()} exf = {k: v["unresolved"] for k, v in comp["floor_exact"].items()} xl = w["exact_lift"] x = np.log([rows[d]["tau"] for d in ex]) ex_exp = float(np.polyfit(x, np.log([ex[d] / 4096 - exf["12"] / 4096 for d in ex]), 1)[0]) if ex != xl["curve"] or exf != {"12": xl["floor12"], "18": xl["floor18"]} or not near(ex_exp, xl["exponent"], 0.01) \ or any(ex[d] >= got[d][2] for d in ex) or any(exf[k] >= fl[k][2] for k in exf): out.append(f"exact cores: curve {ex}, floor {exf}, exponent {ex_exp:.3f}") w["w6"] = {"curve": got, "floor": fl, "fractions_percent": frac, "exponent_ten_points": ten, "exponent_text_nine": nine, "exact_cores": {"curve": {d: [v["nodes"], v["closed"], v["unresolved"]] for d, v in comp["switch_exact"].items()}, "floor": {k: [v["nodes"], v["closed"], v["unresolved"]] for k, v in comp["floor_exact"].items()}, "exponent": ex_exp}} return out def code_facts(probe, kernel, profile): """what the shipped probe and exact kernel do (read after the rebuild)""" parent = probe.find("parent=evalfn(") levels = [float(x) for x in re.search(r"qs=\[([^\]]*)\]", probe).group(1).split(",")] margins = [float(x) for x in re.search(r"for m in \[([^\]]*)\]", probe).group(1).split(",")] return { # it loads Round 18's emitter, verifier and checkpoint from an absolute path outside the package "reads_outside_package": bool(re.search(r"ROOT=Path\('/", probe)), "parent_only_when_children_fail": 0 < probe.find("if int(el['ok'])+int(er['ok'])>0: return") < parent, "parent_at_target": "parent=evalfn(c,h,stats,threshold=TARGET)" in probe, "probe_lift_depth": int(re.search(r"'probe':b7_probe\(x,(\d+)\)", probe).group(1)), # the depth-20 profile has quantile levels and margins the probe does not compute "profile_not_from_probe": sorted(map(float, profile["center_quantiles"])) != sorted(levels) and sorted(map(float, profile["near_counts"])) != sorted(margins), # nothing shipped tracks the branch, segments it, or runs the depth-12 curve "branch_segment_curve_not_shipped": not any(k in probe + kernel for k in ("representative", "seed_branch", "segment", "switch", "depth12")), "kernel_tangent_angles": "np.arccos(np.clip(-dr[ok]/M[ok],-1,1))" in kernel and "rw**2*(dt-np.sin(dt))" in kernel, } def w7_code(w): facts = code_facts(w["probe_code"], w["kernel_code"], w["refs"]["tail_depth20_profile"]) w["w7"] = facts 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, refs, text = [], w["bench"], w["refs"], w["text"] ab = b["lazy_proof_mode_ab"] if (ab["eager"]["nodes"], ab["lazy"]["nodes"], ab["eager"]["pending"], ab["lazy"]["pending"], ab["eager"]["rep_calls"], ab["lazy"]["rep_calls"], ab["lazy"]["rep_skipped"]) != (13206, 13206, 4944, 4944, 12659, 10523, 2136) \ or not near(ab["rep_call_reduction_fraction"], 1 - ab["lazy"]["rep_calls"] / ab["eager"]["rep_calls"], 1e-15) \ or not near(ab["wall_speedup_fraction"], 1 - ab["lazy"]["seconds"] / ab["eager"]["seconds"], 1e-15): out.append("the benchmark's A/B") cc = b["continuation_cost"] if cc["depth16_to18_cpu_seconds"] != refs["tail_depth18_summary"]["seconds"] \ or cc["depth18_to20_cpu_seconds_sum_workers"] != refs["tail_depth20_summary"]["seconds_sum_worker"] \ or not near(cc["cpu_seconds_per_original_depth16_pending_root_to20"], cc["depth16_to20_cpu_seconds"] / 2048, 1e-15) \ or not near(cc["ratio_vs_round18_break_even"], cc["cpu_seconds_per_original_depth16_pending_root_to20"] / cc["round18_break_even_seconds_per_saved_pending_leaf"], 1e-12): out.append("the benchmark's continuation cost against the summaries") d20, prof = b["depth20"], refs["tail_depth20_profile"] if (d20["pending"], d20["sample_inner_center_below_target"], d20["sample_inner_center_min"]) != \ (prof["count"], prof["center_below_target"], prof["center_min"]) or d20["pending"] != refs["tail_depth20_summary"]["pending_count"]: out.append("the benchmark's depth 20 against the profile") br, tr = b["official_near_minimum_branch"], refs["official_seed_branch_track"] rows = {r["depth"]: r for r in tr["rows"]} if br["canonicalized_configuration"] != tr["canonicalization"] \ or any(br[f"depth{d}"]["exact_center"] != rows[d]["exact_center_area"] or br[f"depth{d}"]["tau"] != rows[d]["tau"] for d in (30, 31)): out.append("the benchmark's branch against the track") seg, sp, sb = br["depth31_to40_base_refinement"], refs["necessity_segmentation_exact_profile"], refs["necessity_segmentation_brackets"] if (seg["pending_descendants"], seg["exact_center_below_target"], seg["outer_bracket_below_target"], seg["outer_bracket_tested_exact_sublevel_centers"]) != (sp["count"], sp["below_target"], sum(x["outer_below_target"] for x in sb), len(sb)): out.append("the benchmark's segmentation against its files") curve = {r["base_depth"]: r for r in b["b7_switch_curve_depth12"]} if any(curve[d]["exact_center_area"] != rows[d]["exact_center_area"] or curve[d]["tau"] != rows[d]["tau"] or curve[d]["b7_depth12_unresolved_volume_fraction"] != curve[d]["b7_depth12_unresolved_leaves"] / 4096 for d in curve): out.append("the switch curve's rows against the track") pol = w["policy"] states_text = re.findall(r"^([A-Z][A-Z\-]+)$", text.split("# 25. Recommended activation state machine")[1].split("# 26.")[0], re.M) payload_text = text.split("marker至少包含：")[1].split("```text")[1].split("```")[0].split("\n") matches = pol["frontier_states"] == states_text and len(pol["necessity_marker"]["marker_payload"]) == len([x for x in payload_text if x.strip()]) if matches != w["policy_matches_text"] or pol["proof_cascade"]["order"] != ["APR", "CORE", "REP"]: out.append(f"the activation policy: states {pol['frontier_states']} against the text's {states_text}") crystal = gate.squash(w["crystal"]) for frag in ("12659→10523", "13206nodes/4944pending", r"78.14\text{CPU-s}", r"38.15\text{ms/originalpendingroot}.", r"U_{\rmbracket}\approx0.83491849<0.835.", "561basenodes", "depth50:3.05%", "exactbasepoint:2.64%"): if frag not in crystal: out.append(f"crystal: {frag} not found") w["p1"] = {"policy_states": pol["frontier_states"], "text_states": states_text, "policy_payload": pol["necessity_marker"]["marker_payload"], "text_payload": [x.strip() for x in payload_text if x.strip()]} return out def p2_package(w): out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf_id, text in (("round19", 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 (("benchmark_summary_sha256", BENCH), ("activation_policy_sha256", POLICY)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") b = w["bench"] br = b["official_near_minimum_branch"] ab = b["lazy_proof_mode_ab"] kc = {"fixed_tree_lazy_same_nodes": ab["eager"]["nodes"] == ab["lazy"]["nodes"], "fixed_tree_lazy_same_pending": ab["eager"]["pending"] == ab["lazy"]["pending"], "lazy_rep_calls_lower": ab["lazy"]["rep_calls"] < ab["eager"]["rep_calls"], "depth20_sample_false_positive_correction": b["depth20"]["exact_recheck_of_12_sample_inner_sublevel_candidates"]["exact_below_target"] == 0 < b["depth20"]["sample_inner_center_below_target"], "tracked_first_sublevel_depth31": br["first_tracked_depth_with_outer_bracket_below_target"] == 31, "necessity_segmentation_outer_below_count": br["depth31_to40_base_refinement"]["outer_bracket_below_target"], "continuation_cost_exceeds_round18_break_even": b["continuation_cost"]["ratio_vs_round18_break_even"] > 1} if kc != v["key_checks"] or v["status"] != "PASS": out.append(f"VALIDATION key checks {kc}") w["p2"] = kc return out R19_DEFINITIONS = { "PILOT-CALIBRATED": ("in-line", "sec. 0, 21-26: tuned on the tracked branch's pilot data, not derived"), "BASE-UNRESOLVED": ("in-line", "sec. 19: a pending base cell with no certified sublevel point in it"), "NECESSITY-MARKED": ("in-line", "sec. 14, 19: a cell holding a point whose base area is certified below T; " "only its descendants that hold the point inherit the mark (sec. 15)"), "CORRECTION-R19-001": ("in-line", "sec. 9: the ledger entry retracting 'sampled centre below T' as a proof " "that the centre is below T"), "CENTER-SUBLEVEL-CERTIFIED-PILOT": ("in-line", "sec. 12: a cell whose centre has an outer bracket below T in " "the pilot's floating arithmetic, not yet in publication arithmetic"), "PROVED + A/B PASS": ("in-line", "sec. 30: a theorem, and a fixed-tree comparison agreeing with it"), "MEASURED": ("in-line", "sec. 30: a timing taken once, not a bound"), "VERIFIED-COMPUTATIONAL-PILOT": ("in-line", "sec. 30: a computation checked under the pilot's floating policy"), "IMPLEMENTED / PILOT PASS": ("in-line", "sec. 30: implemented, and run once on the tracked branch"), "NUMERICAL-EVIDENCE / SCHEDULER PARAMETER": ("in-line", "sec. 23-24, 30: an observed scale used to schedule, " "not a constant of a theorem"), "LIFT-EFFICIENCY-REGIME-PILOT": ("in-line", "sec. 23: tau of order 1e-3, where further base refinement stops " "helping the B7 lift much on the pilot branch"), } R19_REVIEWS = [ ("CLOSED", "LAZY PROOF CASCADE", "analytic", "PASS", "Thm 2.1 by cases; on every evaluation here the lazy and the eager classifier agree (W1)"), ("CLOSED", "NECESSITY-MARKER SEMANTICS", "analytic", "PASS", "Thm 13.1: a sound lower bound cannot exceed the infimum, which a point below T bounds (W5)"), ("PILOT-CALIBRATED", "BASE/LIFT SWITCH POLICY", "computation", "PASS", "the switch curve and its floor rebuild exactly (W6); a calibration on one branch and on the pilot's sampled " "cores, as it says - with exact cores every probe leaves fewer leaves open"), ("STILL COMPUTE-DEFERRED", "a_{Leb}≥0.8350", "n/a", "n/a", "sec. 0's boxed summary; read from census v5 on (RUN-003)"), ("PROVED + A/B PASS", "Lazy cascade", "analytic", "PASS", "Thm 2.1; the A/B rebuilds - 13206 nodes, 4944 pending, REP 12659 against 10523 (W1)"), ("MEASURED", "Continuation $\\kappa$", "computation", "PASS", "the trees rebuild exactly and kappa's arithmetic holds (W2); the timings are single runs, taken as recorded, " "and include the probe's re-evaluation of parents (8-9% of its evaluations), so kappa is if anything high"), ("CORRECTED", "Sample-inner sublevel interpretation", "computation", "PASS", "sampled never exceeds exact at depth 20, so the 12 candidates are all a sublevel centre could be, and none is (W3)"), ("VERIFIED-COMPUTATIONAL-PILOT", "Official exact-kernel center classification", "computation", "PASS", "this tree's exact hull: 0 of 12, the least 0.8358650284; 0 of all 10114 (W3)"), ("PROVED", "Necessity-Marker Theorem", "analytic", "PASS", "Thm 13.1 (W5)"), ("IMPLEMENTED / PILOT PASS", "Necessity segmentation", "computation", "PASS", "561 nodes, 256 pending, 85 exact centres below T, 77 with the outer bracket below T; every bracket of the " "package rebuilt (W5)"), ("NUMERICAL-EVIDENCE / SCHEDULER PARAMETER", "$\\tau\\sim10^{-3}$ lift-efficiency regime", "computation", "PARTIAL", "the fractions and the exponent rebuild for the pilot's sampled cores (W6); with exact cores the floor is 76 leaves, " "not 108, and the excess falls as tau^0.91, not tau^0.70 - the regime belongs to the sampling as much as to the lift"), ("COMPUTE-DEFERRED", "B7 global closure", "n/a", "n/a", "at the exact base point B7 leaves 412 leaves open at depth 18 " "with the pilot's cores, 7 with exact cores (W6)"), ("NOT YET CERTIFIED", "Global $a_{\\mathrm{Leb}}\\ge0.835$", "n/a", "n/a", ""), ("BASE-UNRESOLVED", "Base Frontier", "n/a", "n/a", "a frontier state of sec. 19, defined there; not a judgment"), ("NECESSITY-MARKED", "Necessity / Lift Frontier", "n/a", "n/a", "a frontier state of sec. 19, defined there; not a judgment"), ("CORRECTION-R19-001", "9. Correction ledger", "n/a", "n/a", "a ledger label of sec. 9, defined there; not a judgment"), ("LIFT-EFFICIENCY-REGIME-PILOT", "23. Diminishing base-refinement return", "computation", "PASS", "the depth-12 fractions fall toward the base-zero floor, 5.54, 3.93, 3.30 and 2.64 per cent (W6); with exact " "cores too, toward 1.86 per cent"), ("CENTER-SUBLEVEL-CERTIFIED-PILOT", "", "computation", "PASS", "at depth 31 the exact centre is 0.8349033738 and the 20k outer bracket 0.8349184947, the first below T on the " "branch (W4)"), ] def r1_registry(w): return registry.completeness(w["registry"], "R19", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_cascade, "W2": w2_continuation, "W3": w3_depth20, "W4": w4_branch, "W5": w5_segment, "W6": w6_switch, "W7": w7_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"computed", "ab", "all_by_core"}, "W2": {"computed", "refs", "continuation", "evaluation_accounting", "new_counts_include_roots", "bench", "break_even_r18"}, "W3": {"computed", "refs", "depth20", "sampled_below_exact"}, "W4": {"computed", "refs", "qdagger", "qdagger_area", "brackets", "first_sublevel"}, "W5": {"computed", "refs", "segmentation"}, "W6": {"computed", "bench", "switch", "fractions", "exponent", "curve_omits_43", "exact_lift"}, "W7": {"probe_code", "kernel_code", "code_facts", "refs"}, "P1": {"bench", "refs", "text", "policy", "policy_matches_text", "crystal"}, "P2": {"validation", "manifest", "text", "crystal", "bench"}, "R1": {"registry", "definitions", "reviews"}} def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, BENCH, POLICY, VALIDATION, PROBE, KERNEL, *REFS.values()} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} r18 = r21.load_inputs() cost = r18["cost"]["measured_reference"] return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "bench": json.loads(got[BENCH]), "policy": json.loads(got[POLICY]), "validation": json.loads(got[VALIDATION]), "probe_code": got[PROBE].decode("utf-8"), "kernel_code": got[KERNEL].decode("utf-8"), "refs": {k: json.loads(got[v]) for k, v in REFS.items()}, "tail_files": r18["certs"]["certificate_tail_window"], "break_even_r18": (cost["tail_window"]["E"] - cost["official"]["E"]) / 718, "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["tail_files"]) results_computed["tail18_pending"] = results_computed["tail18"]["PENDING"] def build(): return {**{k: v for k, v in inputs.items() if k != "tail_files"}, "computed": results_computed, "registry": registry.load(), "definitions": dict(R19_DEFINITIONS), "reviews": list(R19_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", "p1", "p2"): print(key, json.dumps(w.get(key), default=float, ensure_ascii=False)[:900]) if not args.drill: return refs = inputs["refs"] bench = copy.deepcopy(inputs["bench"]) bench["b7_switch_curve_depth12"][3]["b7_depth12_unresolved_leaves"] = 228 tail18 = copy.deepcopy(refs) tail18["tail_depth18_summary"]["overrides"] = 288 prof = copy.deepcopy(refs) prof["tail_depth20_profile"]["near_counts"]["0.001"] = 30 track_rows = copy.deepcopy(refs) track_rows["official_seed_branch_track"]["rows"][31]["exact_center_area"] += 1e-9 flag = copy.deepcopy(refs) flag["necessity_segmentation_brackets"][0]["outer_below_target"] = not flag["necessity_segmentation_brackets"][0]["outer_below_target"] policy = copy.deepcopy(inputs["policy"]) policy["frontier_states"] = ["BASE-UNRESOLVED", "NECESSITY-MARKED", "NECESSITY-SEGMENTED", "LIFT-ACTIVE", "LIFT-CERTIFIED"] policy["necessity_marker"]["marker_payload"] = policy["necessity_marker"]["marker_payload"] + ["target"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": inputs["text"].replace("\n", "\r\n")}, set()), ("K2-track-rows-reversed", "control", {"refs": {**refs, "official_seed_branch_track": {**refs["official_seed_branch_track"], "rows": list(reversed(refs["official_seed_branch_track"]["rows"]))}}}, set()), ("K3-brackets-reordered", "control", {"refs": {**refs, "necessity_segmentation_brackets": list(reversed(refs["necessity_segmentation_brackets"]))}}, set()), ("M1-doc-lazy-rep", "mutation", {"text": inputs["text"].replace("10523.", "10524.")}, {"A0"}), ("M2-lazy-rep-claim", "mutation", {"ab": {**CLAIMS["ab"], "rep_lazy": 10524}}, {"W1"}), ("M3-not-all-by-core", "mutation", {"all_by_core": False}, {"W1"}), ("M4-summary-overrides", "mutation", {"refs": tail18}, {"W2"}), ("M5-evaluation-accounting", "mutation", {"evaluation_accounting": False}, {"W2"}), ("M6-new-counts", "mutation", {"new_counts_include_roots": False}, {"W2"}), ("M7-break-even", "mutation", {"break_even_r18": 0.0145}, {"W2"}), ("M8-profile-near-count", "mutation", {"refs": prof}, {"W3"}), ("M9-sampled-above-exact", "mutation", {"sampled_below_exact": False}, {"W3"}), ("M10-track-row", "mutation", {"refs": track_rows}, {"W4", "P1"}), ("M11-first-sublevel", "mutation", {"first_sublevel": 30}, {"W4"}), ("M12-bracket-flag", "mutation", {"refs": flag}, {"W5", "P1"}), ("M13-segmentation-claim", "mutation", {"segmentation": {**CLAIMS["segmentation"], "outer_below": 78}}, {"W5"}), ("M14-switch-curve", "mutation", {"bench": bench}, {"W6", "P1"}), ("M15-exponent", "mutation", {"exponent": 0.75}, {"W6"}), ("M15b-exact-floor", "mutation", {"exact_lift": {**CLAIMS["exact_lift"], "floor18": 8}}, {"W6"}), ("M16-probe-lift-depth", "mutation", {"code_facts": {**CLAIMS["code_facts"], "probe_lift_depth": 12}}, {"W7"}), ("M17-policy-states", "mutation", {"policy": policy}, {"P1"}), ("M18-validation-digest", "mutation", {"validation": {**inputs["validation"], "benchmark_summary_sha256": "0" * 64}}, {"P2"}), ("M19-validation-check", "mutation", {"validation": {**inputs["validation"], "key_checks": {**inputs["validation"]["key_checks"], "necessity_segmentation_outer_below_count": 78}}}, {"P2"}), ("M20-review-dropped", "mutation", {"reviews": list(R19_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-022", "subject": "Round 19: the lazy proof cascade, necessity markers and the base/lift switch", "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", "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("R19", "RUN-022", R19_DEFINITIONS, R19_REVIEWS) print(f"registry: {len(R19_DEFINITIONS)} definitions, {len(R19_REVIEWS)} reviews recorded for R19") if __name__ == "__main__": main()