"""RUN-036 - Round 33: cross-backend enclosure dominance, and the depth-30 batch. Round 33 proves that a second backend's core enclosures need only be checked for containment in the first's - centre rectangles inside, radius lower bound no smaller - for every exact rational point the first certifies to be certified by the second as well, and audits that for cells 47 and 48 over their unique witness-core states (1564 and 1574, not 9228 and 9285 leaves): 0 failures. Cell 48 gets its tree and an mpmath ledger (9285/9285) and marker 48 its replays; cells 68, 75 and 76 get their trees. It then keeps cells 47 and 48 below publication-candidate, because the ledgers keep only PASS, density and margin, not the polygons the dominance would transfer. Here the theorem is read, the unique states counted on this tree's own lifts, cells 48, 68, 75 and 76 lifted again and cell 48's leaves certified on their intended boxes, and marker 48 set against Round 29's file and this tree's certificate. Checks A0 anchors the numbers and formulas below occur in Round 33 as written W1 dominance sec. 1-4, 7: the theorem, read; the unique witness-core states on this tree's lifts W2 trees sec. 5, 11: cells 48, 68, 75 and 76 lifted here against their trees and manifests W3 emitter sec. 5: cell 48's leaves certified on their intended boxes at the ledger's density W4 marker sec. 6: marker 48 against Round 29's file and this tree's certificate W5 entity sec. 8-10: what the ledgers keep, the hull vertex totals, and what a regeneration recovers W6 dashboard sec. 11-13: the stage counts and the batch W7 code what the package ships, read after the rebuild and never run P1 package the status files, the spec, the dominance files, the dashboard, the batch and the crystal agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 33's judgments reviewed Usage: python code/run036_round33_dominance.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import json import re from fractions import Fraction from multiprocessing import Pool 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 run023_round20_mixed_escalation as r23 import run027_round24_residual_joint as r27 import run029_round26_full_atlas as r29 import run030_round27_interval_replay as r30 import run031_round28_exact_root as r31 import run032_round29_marker_upper as r32 import run034_round31_mpfr_replay as r34 import run035_round32_bulk_wave as r35 from corpus import SOURCES, TREE, source_bytes, walk_sources from run010_round07_minimizer_atlas import d_star, t_text PKG = "main.zip!/AMRAL_LUC_FC_Round_33_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_33_Cross_Backend_Dominance_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_33_v0.1.md" SPEC = PKG + "AMRAL_LUC_FC_Round_33_CROSS_BACKEND_DOMINANCE_SPEC.json" STATUS = {n: PKG + f"AMRAL_LUC_FC_Round_33_CELL{n}_STATUS.json" for n in (47, 48)} BATCH = PKG + "AMRAL_LUC_FC_Round_33_DEPTH30_BATCH_STATUS.json" DASH = PKG + "AMRAL_LUC_FC_Round_33_COVERAGE_DASHBOARD.json" SCOPE = PKG + "AMRAL_LUC_FC_Round_33_SCOPE_LEDGER.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_33_VALIDATION.json" REF = PKG + "AMRAL_LUC_FC_Round_33_reference/" DOMINANCE = {n: REF + f"AMRAL_LUC_FC_Round_33_CROSS_BACKEND_DOMINANCE_CELL{n}.json" for n in (47, 48)} MARKER48_A1 = REF + "AMRAL_LUC_FC_Round_33_MARKER48_A1.json" MARKER48 = r32.REF + "marker_48.json" LOG = TREE / "data" / "gate-logs" / "run036-round33-dominance.json" CACHE = TREE / "data" / "cache" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T = 0.835 LIFTED = (68, 75, 76) BATCH30 = (47, 48, 68, 69, 70, 75, 76) def lift_compute(paths): """each cell lifted here to depth 30 (RUN-030's lift under the package's pad): its leaves' paths and areas""" with Pool(14) as pool: return {n: [[p, area] for p, _, _, area in r30.leaves_with_paths(pool, *(lambda b: (b["center"], b["half"]))(r35.cell_box(path)), 30)] for n, path in sorted(paths.items())} def lifts_computed(paths): return r35._cached("run036-lifts.json", [lift_compute, r35.cell_box, r30.leaves_with_paths, r8, r9, r11, r12, r13, r19, r23, r27, r30, json.dumps(sorted(paths.items())).encode()], lambda: lift_compute(paths)) def marker_compute(m): return {"certificate": r32.certify(([Fraction(x) for x in m["q_rational"]], m["final"]["density"])), "polygons": r34.marker_polygons(m)} def marker_computed(m): """RUN-032's certificate for marker 48, and its exact polygon under the package's normals and ceiling""" return r35._cached("run036-marker48.json", [marker_compute, r32.certify, r32.half_planes, r32.outer_area, r32.support_hi, r34.marker_polygons, r34.full_area, r34.package_normals, r8, r9, r19, r30, r31, json.dumps([m["q_rational"], m["final"]["density"]]).encode()], lambda: marker_compute(m)) def unique_states(paths): """the witness-core states of a tree's leaves: the rotation and the half-widths, which fix a core's unit corners and its radius; the translation only shifts them""" tn = t_text(7, d_star(r31.TM)) seq = r31.float_sequence(tn, 30) return len({(wc[0], tuple(wh)) for wc, wh in (r31.float_box(p, seq, tn) for p in paths)}) def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} r32ref = r35.REF want = {MARKER48, r29.LEDGER, r35.REF + "cell47_mpmath_leaf_ledger.json", r35.REF + "cell47_topology.bin", r35.REF + "cell47_axis_stream_2bit.bin"} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id.startswith(PKG) or l.id in want) if d is not None} sha = lambda b: hashlib.sha256(b).hexdigest() cells = {} for n in (47, 48, 68, 75, 76): c = {"manifest": json.loads(got[REF + f"cell{n}_manifest.json"]), "topology": got[REF + f"cell{n}_topology.bin"], "axes": got[REF + f"cell{n}_axis_stream_2bit.bin"], "digests": {k: sha(got[REF + f"cell{n}_{k}"]) for k in ("topology.bin", "axis_stream_2bit.bin")}} if n in (47, 48): c["mpmath"] = json.loads(got[REF + f"cell{n}_mpmath_leaf_ledger.json"]) c["mpmath_bytes"] = got[REF + f"cell{n}_mpmath_leaf_ledger.json"] c["digests"]["mpmath_leaf_ledger.json"] = sha(c["mpmath_bytes"]) cells[str(n)] = c return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "spec": json.loads(got[SPEC]), "status": {n: json.loads(got[p]) for n, p in STATUS.items()}, "batch": json.loads(got[BATCH]), "dashboard": json.loads(got[DASH]), "scope": json.loads(got[SCOPE]), "validation": json.loads(got[VALIDATION]), "dominance": {n: json.loads(got[p]) for n, p in DOMINANCE.items()}, "marker48_a1": json.loads(got[MARKER48_A1]), "marker48": json.loads(got[MARKER48]), "cells": cells, "ledger26": json.loads(got[r29.LEDGER]), "round32_cell47": {k: sha(got[r32ref + f"cell47_{k}"]) for k in ("mpmath_leaf_ledger.json", "topology.bin", "axis_stream_2bit.bin")}, "code": {k[len(REF):]: v.decode("utf-8") for k, v in got.items() if k.startswith(REF) and k.endswith(".py")}, "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} def world(inputs): c = inputs["cells"] computed = {n: r35.cell_computed(int(n), c[n]["manifest"]["base_path"], c[n]["mpmath_bytes"]) for n in ("47", "48")} lifts = lifts_computed({str(n): c[str(n)]["manifest"]["base_path"] for n in LIFTED}) return {**inputs, "computed": computed, "lifts": lifts, "marker_mine": marker_computed(inputs["marker48"]), "states": {**{n: unique_states([p for p, _ in computed[n]["leaves"]]) for n in computed}, **{n: unique_states([p for p, _ in v]) for n, v in lifts.items()}}} ANCHORS = { "W1": [r"R^B_j\subseteqR^A_j", r"\rho_B\ge\rho_A,", r"\sup_{c\inR^A_j}\|p-c\|<\rho_A,", r"p\inG_A^{\rmcert}\Rightarrowp\inG_B^{\rmcert}.", r"P\subseteqG_B.", r"exactrationalshoelacearea与backend无关。", r"9228\text{leaves}\to1564\text{uniquewitness-corestates}", r"9285\text{leaves}\to1574\text{uniquewitness-corestates}", r"\boxed{1564}.", r"\boxed{1574}.", r"6\times", r"\boxed{\text{PASS},\quad0\text{failures}.}", r"2.15\times10^{-64}>0.", r"47/48\text{backenddominance皆完全PASS}."], "W2": [r"18569\text{nodes},", r"9285\text{leaves},", r"47,48,68,69,70,75,76.", r"18509\text{nodes},\qquad9255\text{leaves}.", r"21895\text{nodes},\qquad10948\text{leaves}.", r"21863\text{nodes},\qquad10932\text{leaves}."], "W3": [r"\boxed{9285/9285\text{PASS}}", r"-256:824-512:3438-1024:3725-2048:1065-4096:183-8192:43-16384:7", r"1.03164\times10^{-7}>0."], "W4": [r"0.8349325735415322.", r"6.74265\times10^{-5}."], "W5": [r"Round32emitter没有持久化每个leaf的：", r"2.16\times10^6.", r"2.11\times10^6.", r"16\text{bytes/vertex}.", r"\text{finitecertificateentitypersistence}."], "W6": [r"\boxed{4/77}.", r"\{69,70\}.", r"\{47,48,69,70\}", r"4/77\approx5.19\%.", r"2/77\approx2.60\%."], "P1": [r"a_{\mathrm{Leb}}\ge0.835\text{NOTCERTIFIED}."], } CLAIMS = { # [this tree's states, the audit's, this tree's leaves, the audit's]; leaves per state; the audits' own results (recorded, # not recomputed: they rest on MPFR) "dominance_claim": {"premises": [True, True], "proof": [True, True], "states": {"47": [1564, 1564, 9228, 9228], "48": [1574, 1574, 9285, 9285]}, "ratio": [5.9, 5.9], "results": {"47": ["PASS", 0, 2.1500046539032408e-64], "48": ["PASS", 0, 2.1500046539032408e-64]}}, # counts [decoded nodes, leaves, internal; the manifest's three; its bits; this tree's leaves] "trees_claim": { "48": {"counts": [18569, 9285, 9284, 18569, 9285, 9284, 18569, 9285], "leaf_paths_equal": True, "depth": [30, 30], "axes_high_first": True, "base": [True, True], "digests": [True, True], "least_slack": ["110101101001101011111010", 1.160243198e-07, 2e-16]}, "68": {"counts": [18509, 9255, 9254, 18509, 9255, 9254, 18509, 9255], "leaf_paths_equal": True, "depth": [30, 30], "axes_high_first": True, "base": [True, True], "digests": [True, True], "least_slack": ["00111011001001010000010", 3.260004866e-08, 0.0]}, "75": {"counts": [21895, 10948, 10947, 21895, 10948, 10947, 21895, 10948], "leaf_paths_equal": True, "depth": [30, 30], "axes_high_first": True, "base": [True, True], "digests": [True, True], "least_slack": ["11010110100110111101000001111", 7.800966129e-08, 1e-16]}, "76": {"counts": [21863, 10932, 10931, 21863, 10932, 10931, 21863, 10932], "leaf_paths_equal": True, "depth": [30, 30], "axes_high_first": True, "base": [True, True], "digests": [True, True], "least_slack": ["11010110110100101111001110011", 3.630034273e-08, 0.0]}, "47": {"round32_bytes": [True, True, True]}}, "emitter_claim": {"pass": 9285, "refused": 0, "hull_equal": 9285, "margin_difference": 2.3e-16, "least": ["110101101001101011111010", 16384, 1.0316417843733946e-07], "bands": [9285, 9285], "density_counts": {"256": 824, "512": 3438, "1024": 3725, "2048": 1065, "4096": 183, "8192": 43, "16384": 7}}, # [area, active, numerator bits, denominator bits]; this tree's certificate [normals, margin, exact margin] "marker_claim": {"record": [True, True, True, True, True], "every_constraint": [0.8349325735415322, 2601, 42878, 42879], "is_replay": True, "float_reduced": [0.8349325735415322, 2560, 41557, 41557], "is_round29": True, "mine": [128, 4.028306961197044e-05, 0.00010222745468868588], "status_margins": [True]}, # [hull counts regenerated here, largest margin difference] "entity_claim": {"47": {"fields": ["density", "index", "margin_decimal", "path", "status", "vertices"], "vertices": 2163069, "raw_mb": 34.6, "regenerated": [9228, 2.6e-16]}, "48": {"fields": ["density", "index", "margin_decimal", "path", "status", "vertices"], "vertices": 2109700, "raw_mb": 33.8, "regenerated": [9285, 2.3e-16]}}, "dashboard_claim": {"cells": [[69, 70], [47, 48, 69, 70], [47, 48], [68, 75, 76]], "counts": [True, True, True, True, True], "geometry": [66, 11, 51], "batch": {"47": ["CROSS-BACKEND-ENCLOSURE-AUDITED-PROTOTYPE", 9228], "48": ["CROSS-BACKEND-ENCLOSURE-AUDITED-PROTOTYPE", 9285], "68": ["SHARDIZED-ARITHMETIC-PENDING", 9255], "69": ["PUBLICATION-CANDIDATE-SHARD", None], "70": ["PUBLICATION-CANDIDATE-SHARD", None], "75": ["SHARDIZED-ARITHMETIC-PENDING", 10948], "76": ["SHARDIZED-ARITHMETIC-PENDING", 10932]}, "batch_leaves": True, "batch_slack": True, "batch_counts": [2, 2, 3, True, True]}, "code_facts": {"lines": 108, "absolute_path": True, "opens": ["AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json", "AMRAL_LUC_FC_Round_29_reference/marker_{cell:02d}.json", "AMRAL_LUC_FC_Round_31_MPFR_ROOT_REPLAY.json", "AMRAL_LUC_FC_Round_32_cell{cell:02d}", "AMRAL_LUC_FC_Round_33_CROSS_BACKEND_DOMINANCE_CELL{cell}.json", "axis_stream_2bit.bin", "manifest.json", "topology.bin"], "not_in_archive": ["AMRAL_LUC_FC_Round_32_cell{cell:02d}"], "key_is_rotation_and_halfwidths": True, "translation_per_leaf": True, "a_by_decimal_strings": True, "b_by_round31_wrapper": True, "gain_is_min_over_states": True}, } def near(a, b, tol): return abs(a - b) <= tol def sig(x, n=4): return float(f"{x:.{n - 1}e}") def w1_dominance(w): """sec. 1-4, 7: the theorem, read - a supremum over a subset is no larger, and rho_A <= rho_B - and the audits' sizes: the unique witness-core states (rotation and half-widths) on this tree's own lifts; the audits' own results, which rest on MPFR, are not recomputed here""" out, sp = [], w["spec"] st = sp["statement"] got = {"premises": [any("subset of R^A_j" in p for p in st["premises"]), any("rho_B >= rho_A" in p for p in st["premises"])], "proof": ["sup over R^B_j distance <= sup over R^A_j distance" in " ".join(sp["proof_sketch"]), "backend-independent" in " ".join(sp["proof_sketch"])], "states": {n: [w["states"][n], w["dominance"][int(n)]["unique_witness_core_states"], len(w["computed"][n]["leaves"]), w["dominance"][int(n)]["leaf_count"]] for n in ("47", "48")}, "ratio": [sig(len(w["computed"][n]["leaves"]) / w["states"][n], 3) for n in ("47", "48")], "results": {str(n): [d["status"], d["witness_core_failures"], d["minimum_rho_lower_gain_B_minus_A"]] for n, d in sorted(w["dominance"].items())}} if not all(got["premises"] + got["proof"]) or any(v[0] != v[1] or v[2] != v[3] for v in got["states"].values()) or got != w["dominance_claim"]: out.append(f"the dominance: {got}") w["w1"] = got return out def w2_trees(w): """sec. 5, 11: cells 48, 68, 75 and 76 lifted here to depth 30 - node, leaf and internal counts, the leaf paths, the 2-bit axis stream, the depth, the digests and the least slack against their trees and manifests; cell 47's files are Round 32's""" out, got = [], {} tn = t_text(7, d_star(r31.TM)) seq = r31.float_sequence(tn, 30) trees = {"48": w["computed"]["48"]["leaves"], **w["lifts"]} for n in ("48", "68", "75", "76"): c, m = w["cells"][n], w["cells"][n]["manifest"] try: nodes = r31.decode_topology(c["topology"], m["nodes"]) except ValueError as e: got[n] = {"topology": str(e)} continue internal = [p for p, b in nodes if b] leaves = [p for p, b in nodes if not b] slack = min((a - r30.PKG_PAD - T, p) for p, a in trees[n]) got[n] = {"counts": [len(nodes), len(leaves), len(internal), m["nodes"], m["leaves"], m["internal_nodes"], m["topology_bits"], len(trees[n])], "leaf_paths_equal": sorted(leaves) == sorted(p for p, _ in trees[n]), "depth": [max(map(len, leaves)), m["closure_depth"]], "axes_high_first": r31.decode_axes(c["axes"], len(internal), True) == [seq[len(p)][0] for p in internal], "base": [r31.base_axes(m["base_path"])[0] == m["base_axis_trace"], m["base_path"] == w["ledger26"]["cells"][int(n)]["path"]], "digests": [m["topology_sha256"] == c["digests"]["topology.bin"], m["axis_sha256"] == c["digests"]["axis_stream_2bit.bin"]], "least_slack": [slack[1], sig(slack[0], 10), sig(abs(slack[0] - m["worst_reference_slack"]), 1)]} c47 = w["cells"]["47"] got["47"] = {"round32_bytes": [c47["digests"][k] == w["round32_cell47"][k] for k in ("mpmath_leaf_ledger.json", "topology.bin", "axis_stream_2bit.bin")]} ok = all("counts" in v and v["leaf_paths_equal"] and v["axes_high_first"] and all(v["base"]) and all(v["digests"]) and v["least_slack"][2] < 1e-14 and v["counts"][0] == v["counts"][3] == v["counts"][6] and v["counts"][1] == v["counts"][4] == v["counts"][7] and v["counts"][2] == v["counts"][5] for k, v in got.items() if k != "47") and all(got["47"]["round32_bytes"]) if not ok or got != w["trees_claim"]: out.append(f"the trees: {got}") w["w2"] = got return out def w3_emitter(w): """sec. 5: cell 48's leaves certified here on their intended boxes at the ledger's density; the start bands""" out, comp, led = [], w["computed"]["48"], w["cells"]["48"]["mpmath"] byp = {x["path"]: x for x in led} area = dict((p, a) for p, a in comp["leaves"]) res = {p: r for (p, _), r in zip(comp["leaves"], comp["results"])} at = {p: r["ledger"] for p, r in res.items()} rule = [x["density"] == (max(r35.start_band(area[x["path"]] - r30.PKG_PAD - T), res[x["path"]]["least"]["n"]) if res[x["path"]]["least"] else None) for x in led if x["path"] in res] least = min(led, key=lambda x: x["margin_decimal"]) got = {"pass": sum(r["pass"] for r in at.values()), "refused": sum(r["failures"] for r in at.values()), "hull_equal": sum(at[p]["hull"] == x["vertices"] for p, x in byp.items() if p in at), "margin_difference": sig(max(abs(at[p]["margin"] - x["margin_decimal"]) for p, x in byp.items() if p in at), 2), "least": [least["path"], least["density"], least["margin_decimal"]], "bands": [sum(rule), len(rule)], "density_counts": {str(k): v for k, v in sorted(collections.Counter(x["density"] for x in led).items())}} if got["pass"] != len(led) or got["refused"] or got["hull_equal"] != len(led) or got["margin_difference"] > 1e-15 or got != w["emitter_claim"]: out.append(f"cell 48's ledger: {got}") w["w3"] = got return out def w4_marker(w): """sec. 6: marker 48's replay record against Round 29's file; its exact polygon under the package's normals and ceiling, every constraint kept and float-reduced; this tree's certificate""" out, rec, f, mine = [], w["marker48_a1"]["markers"][0], w["marker48"]["final"], w["marker_mine"] poly = mine["polygons"] got = {"record": [rec["cell"] == 48, rec["density"] == f["density"] == rec["full_constraint_count"], rec["outer_area_decimal"] == f["outer_area_decimal"], rec["margin_decimal"] == f["margin_decimal"], w["marker48_a1"]["status"] == "PASS"], "every_constraint": poly["full"], "is_replay": poly["full"][:2] == [rec["outer_area_decimal"], rec["exact_active_constraints"]], "float_reduced": poly["reduced"], "is_round29": poly["reduced"] == [f["outer_area_decimal"], f["active_constraints"], f["outer_area_num_bits"], f["outer_area_den_bits"]], "mine": [mine["certificate"]["ladder"]["N"], mine["certificate"]["ladder"]["margin"], T - mine["certificate"]["exact"]], "status_margins": [w["status"][48]["marker_upper"]["MPFR_margin_decimal"] == f["margin_decimal"]]} if not all(got["record"]) or not got["is_replay"] or not got["is_round29"] or not all(got["status_margins"]) or got != w["marker_claim"]: out.append(f"marker 48: {got}") w["w4"] = got return out def w5_entity(w): """sec. 8-10: what the ledgers keep per leaf; the hull vertex totals and their raw size at 16 bytes a vertex; and what an independent regeneration recovers from density and rule alone - the hull counts and margins of every leaf (W3 here, RUN-035 W3 for cell 47)""" out, got = [], {} for n in ("47", "48"): led = w["cells"][n]["mpmath"] comp = w["computed"][n] at = {p: r["ledger"] for (p, _), r in zip(comp["leaves"], comp["results"])} total = sum(x["vertices"] for x in led) got[n] = {"fields": sorted(set().union(*(x.keys() for x in led))), "vertices": total, "raw_mb": sig(16 * total / 1e6, 3), "regenerated": [sum(at[x["path"]]["hull"] == x["vertices"] for x in led), sig(max(abs(at[x["path"]]["margin"] - x["margin_decimal"]) for x in led), 2)]} if any(v["regenerated"][0] != len(w["cells"][n]["mpmath"]) for n, v in got.items()) or got != w["entity_claim"]: out.append(f"the certificate entities: {got}") w["w5"] = got return out def w6_dashboard(w): """sec. 11-13: the stage counts - two candidates, four arithmetic-closed-or-better, 62 geometry-complete cells at a lower stage - and the depth-30 batch: every cell in it has a tree, 68, 75 and 76 with the least slack this tree's lifts give""" out, d, b = [], w["dashboard"], w["batch"] ar = d["arithmetic_pipeline"] pc, ac = sorted(ar["publication_candidate_cells"]), sorted(ar["arithmetic_closed_or_better_cells"]) slack = {n: min(a - r30.PKG_PAD - T for _, a in w["lifts"][n]) for n in w["lifts"]} got = {"cells": [pc, ac, sorted(ar["cross_backend_enclosure_audited_cells"]), sorted(ar["shardized_arithmetic_pending_depth30_cells"])], "counts": [ar["publication_candidate_count"] == len(pc), ar["arithmetic_closed_or_better_count"] == len(ac), ar["geometry_complete_arithmetic_pending_or_lower_stage_count"] == d["geometry"]["known_complete"] - len(ac), near(ar["publication_candidate_fraction_global"], len(pc) / 77, 1e-15), near(ar["arithmetic_closed_or_better_fraction_global"], len(ac) / 77, 1e-15)], "geometry": [d["geometry"]["known_complete"], d["geometry"]["residual"], d["geometry"]["latest_exact_common_budget"]["complete"]], "batch": {n: [v["status"], v.get("leaves")] for n, v in sorted(b["cells"].items(), key=lambda x: int(x[0]))}, "batch_leaves": all(b["cells"][str(n)]["leaves"] == len(w["lifts"][str(n)]) for n in LIFTED) and all(b["cells"][str(n)]["leaves"] == len(w["computed"][str(n)]["leaves"]) for n in (47, 48)), "batch_slack": all(near(slack[str(n)], b["cells"][str(n)]["worst_reference_slack"], 1e-14) for n in LIFTED), "batch_counts": [b["publication_candidate_count_in_batch"], b["cross_backend_enclosure_audited_count_in_batch"], b["shardized_arithmetic_pending_count_in_batch"], sorted(map(int, b["cells"])) == list(BATCH30), b["all_depth30_cells_have_finite_topology"]]} if not all(got["counts"]) or not got["batch_leaves"] or not got["batch_slack"] or got != w["dashboard_claim"]: out.append(f"the dashboard: {got}") w["w6"] = got return out def w7_code(w): """what the package ships, read after the rebuild and never run: the dominance audit""" src = w["code"]["r33_enclosure_dominance.py"] leaves = [row[0] for row in w["manifest"]["leaves"]] opened = sorted(set(re.findall(r"ROOT\s*/\s*f?[\"']([^\"']+)[\"']", src)) | set(re.findall(r"SD\s*/\s*[\"']([^\"']+)[\"']", src))) facts = {"lines": src.count("\n"), "absolute_path": bool(re.search(r"(?:Path\(|insert\(0,)\s*[\"']/", src)), "opens": opened, "not_in_archive": sorted(u for u in opened if not any(u.split("/")[0].split("{")[0].rstrip("_") in leaf for leaf in leaves)), "key_is_rotation_and_halfwidths": "key=(ca[0].lo,ca[0].hi,ha[0].lo,ha[0].hi,ha[1].lo,ha[1].hi,ha[2].lo,ha[2].hi,cb[0].lo,cb[0].hi,hb[0].lo,hb[0].hi" in src, "translation_per_leaf": "trans_ok &= all(contains(ca[i],cb[i]) and contains(ha[i],hb[i]) for i in range(3))" in src, "a_by_decimal_strings": "mp.iv.mpf([fs(e.lo),fs(e.hi)])" in src, "b_by_round31_wrapper": "from r31_mpfr_backend import" in src, "gain_is_min_over_states": "min_rho_gain=gain if min_rho_gain is None else min(min_rho_gain,gain)" in src} w["w7"] = facts return [] if facts == w["code_facts"] else [f"the script: {facts}"] def p1_package(w): out, sp, st, dom = [], w["spec"], w["status"], w["dominance"] for n in (47, 48): if sp["audits"][f"cell{n}"] != dom[n] or st[n]["cross_backend_dominance"] != dom[n]: out.append(f"cell {n}: the spec's and the status file's audit against the dominance file") led, s, m = w["cells"][str(n)]["mpmath"], st[n], w["cells"][str(n)]["manifest"] least = min(led, key=lambda x: x["margin_decimal"]) lm = s["lower_mpmath"] if (lm["leaves_total"], lm["leaves_pass"], lm["inconclusive"], lm["minimum_margin_decimal"], lm["minimum_margin_path"], lm["ledger_sha256"]) \ != (len(led), sum(x["status"] == "PASS" for x in led), sum(x["status"] != "PASS" for x in led), least["margin_decimal"], least["path"], w["cells"][str(n)]["digests"]["mpmath_leaf_ledger.json"]) \ or ("density_counts" in lm and lm["density_counts"] != {str(k): v for k, v in collections.Counter(x["density"] for x in led).items()}) \ or s["geometry"] != m or s["publication_candidate"] is not False or s["status"] != "CROSS-BACKEND-ENCLOSURE-AUDITED-PROTOTYPE": out.append(f"cell {n}: the status file against its ledger and manifest") d, b = w["dashboard"], w["batch"] if sorted(d["arithmetic_pipeline"]["cross_backend_enclosure_audited_cells"]) != [n for n in (47, 48) if st[n]["status"].startswith("CROSS-BACKEND")] \ or [b["cells"][str(n)]["status"] for n in (47, 48)] != [st[n]["status"] for n in (47, 48)] or d["global_lebesgue_claim"]: out.append("the dashboard and the batch against the status files") ids = [e["id"] for e in w["scope"]["entries"]] if ids != ["R33-CERT-ENTITY-001", "R33-GEOMETRY-SCOPE-001"] or "Cells47/48 remain below PUBLICATION-CANDIDATE" not in w["scope"]["entries"][0]["effect"]: out.append("the scope ledger") crystal = gate.squash(w["crystal"]) for frag in ("9228leaves→1564uniqueB7corestates.", "9285leaves→1574uniqueB7corestates.", r"\boxed{\{47,48,69,70\}}", "9285/9285mpmathlowerPASS."): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"audits": {n: dom[n]["status"] for n in (47, 48)}} 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 (("round33", 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["file"] != leaf_id.split("/")[-1] \ 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 (("dominance_spec_sha256", SPEC), ("cell47_status_sha256", STATUS[47]), ("cell48_status_sha256", STATUS[48]), ("depth30_batch_sha256", BATCH), ("coverage_dashboard_sha256", DASH), ("scope_ledger_sha256", SCOPE), ("cell47_ledger_sha256", REF + "cell47_mpmath_leaf_ledger.json"), ("cell48_ledger_sha256", REF + "cell48_mpmath_leaf_ledger.json")): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") c, dom, st, b, d = w["cells"], w["dominance"], w["status"], w["batch"], w["dashboard"] kc = {"cell47_lower_9228": len(c["47"]["mpmath"]) == 9228 and all(x["status"] == "PASS" for x in c["47"]["mpmath"]), "cell47_dominance_pass": dom[47]["status"] == "PASS", "cell48_lower_9285": len(c["48"]["mpmath"]) == 9285, "cell48_all_lower_pass": all(x["status"] == "PASS" for x in c["48"]["mpmath"]), "cell48_marker_A1_pass": w["marker48_a1"]["status"] == "PASS", "cell48_marker_MPFR_pass": st[48]["marker_upper"]["MPFR_status"] == "PASS", "cell48_dominance_pass": dom[48]["status"] == "PASS", "batch68_shardized": b["cells"]["68"]["status"] == "SHARDIZED-ARITHMETIC-PENDING", "batch75_shardized": b["cells"]["75"]["status"] == "SHARDIZED-ARITHMETIC-PENDING", "batch76_shardized": b["cells"]["76"]["status"] == "SHARDIZED-ARITHMETIC-PENDING", "publication_candidates_still_2": d["arithmetic_pipeline"]["publication_candidate_count"] == 2, "no_global_claim": d["global_lebesgue_claim"] is False} if kc != v["checks"] or v["status"] != "PASS": out.append(f"VALIDATION checks {kc}") w["p2"] = kc return out _DOM = ("the MPFR enclosures are not recomputed here (no MPFR on this machine); the audit's logic holds - each rotation and " "half-width state once, every leaf's translation checked (W7) - its state counts are this tree's (W1), the root nesting it " "rests on RUN-034's, and every leaf of both cells is certified here directly (W3, RUN-035)") _AUD = ("the MPFR side is not recomputed here (no MPFR on this machine); the root nesting it rests on holds (RUN-034 W1), and every " "leaf of the cell is certified here directly (W3, RUN-035)") _L48 = "9,285 of 9,285 here too on this tree's own lift, the ledger's hull counts, margins within a few units in the last place (W2, W3)" _M48 = ("the replay row is Round 29's marker file, and the full polygon under the package's normals is rebuilt here - its area and " "its active count (W4); the MPFR replay's record is not shipped") _ROOTC = ("t3, t5 and t7: the MPFR intervals lie inside Round 28's (RUN-034 W1); pi and sqrt 3: the MPFR intervals are not shipped, " "and MPFR is not on this machine") R33_REVIEWS = [ ("PASS", "4. Cell47 dominance audit", "computation", "UNMEASURED", _AUD), ("PASS", "4. Cell47 dominance audit", "computation", "UNMEASURED", _AUD), ("PASS", "4. Cell47 dominance audit", "computation", "UNMEASURED", _AUD), ("PASS", "4. Cell47 dominance audit", "computation", "UNMEASURED", _AUD), ("PASS", "7. Cell48 dominance audit", "computation", "PARTIAL", _ROOTC), ("PASS", "7. Cell48 dominance audit", "computation", "UNMEASURED", _AUD), ("PASS", "7. Cell48 dominance audit", "computation", "UNMEASURED", _AUD), ("PASS", "9285/9285", "computation", "PASS", _L48), ("PASS", "", "computation", "PARTIAL", _ROOTC), ("PASS", "9285/9285", "computation", "PASS", _L48), ("PASS", "", "computation", "PASS", _M48), ("PASS", "", "computation", "UNMEASURED", "the MPFR replay's record is not shipped and MPFR is not on this machine; the polygon it computes is rebuilt here exactly (W4)"), ("PASS", "47/48 backend dominance皆完全", "computation", "UNMEASURED", _DOM), ("PASS", "independent exact polar upper replay", "computation", "PASS", _M48), ("PASS", "MPFR upper replay", "computation", "UNMEASURED", "the MPFR replay's record is not shipped and MPFR is not on this machine; the polygon it computes is rebuilt here exactly (W4)"), ("PUBLICATION-CANDIDATE", "8. Certificate-Entity Gap", "reading", "PASS", "true: not raised - the ledgers keep no polygon (W5); a regeneration from density and rule recovers every hull count and margin (W5)"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ] def r1_registry(w): return registry.completeness(w["registry"], "R33", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_dominance, "W2": w2_trees, "W3": w3_emitter, "W4": w4_marker, "W5": w5_entity, "W6": w6_dashboard, "W7": w7_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"spec", "dominance", "states", "computed", "dominance_claim"}, "W2": {"cells", "computed", "lifts", "ledger26", "round32_cell47", "trees_claim"}, "W3": {"cells", "computed", "emitter_claim"}, "W4": {"marker48_a1", "marker48", "marker_mine", "status", "marker_claim"}, "W5": {"cells", "computed", "entity_claim"}, "W6": {"dashboard", "batch", "lifts", "computed", "dashboard_claim"}, "W7": {"code", "manifest", "code_facts"}, "P1": {"spec", "status", "dominance", "cells", "dashboard", "batch", "scope", "crystal"}, "P2": {"validation", "manifest", "text", "crystal", "cells", "dominance", "status", "batch", "dashboard", "marker48_a1"}, "R1": {"registry", "definitions", "reviews"}} def drill_cases(base): text, c = base["text"], base["cells"] def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x def fail_leaf(comp): comp["48"]["results"][0]["ledger"]["pass"] = False return [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-spec-keys-sorted", "control", {"spec": json.loads(json.dumps(base["spec"], sort_keys=True))}, set()), ("K3-batch-keys-sorted", "control", {"batch": json.loads(json.dumps(base["batch"], sort_keys=True))}, set()), ("M1-doc-states", "mutation", {"text": text.replace(r"\boxed{1574}", r"\boxed{1575}")}, {"A0"}), ("M2-state-count", "mutation", {"dominance": edit(base["dominance"], lambda x: x[47].update(unique_witness_core_states=1565))}, {"W1", "P1"}), ("M3-topology-bit", "mutation", {"cells": edit(c, lambda x: x["75"].update(topology=bytes([x["75"]["topology"][0] ^ 1]) + x["75"]["topology"][1:]))}, {"W2"}), ("M4-manifest-slack", "mutation", {"cells": edit(c, lambda x: x["68"]["manifest"].update(worst_reference_slack=3.3e-8))}, {"W2"}), ("M5-ledger-margin", "mutation", {"cells": edit(c, lambda x: x["48"]["mpmath"][50].update(margin_decimal=x["48"]["mpmath"][50]["margin_decimal"] + 1e-12))}, {"W3", "W5"}), ("M6-certificate", "mutation", {"computed": edit(base["computed"], fail_leaf)}, {"W3"}), ("M7-marker-area", "mutation", {"marker48_a1": edit(base["marker48_a1"], lambda x: x["markers"][0].update(outer_area_decimal=0.8349325735415323))}, {"W4"}), ("M8-ledger-vertices", "mutation", {"cells": edit(c, lambda x: x["47"]["mpmath"][7].update(vertices=x["47"]["mpmath"][7]["vertices"] + 1))}, {"W5"}), ("M9-dashboard-count", "mutation", {"dashboard": edit(base["dashboard"], lambda x: x["arithmetic_pipeline"].update(geometry_complete_arithmetic_pending_or_lower_stage_count=63))}, {"W6"}), ("M10-batch-slack", "mutation", {"batch": edit(base["batch"], lambda x: x["cells"]["76"].update(worst_reference_slack=3.7e-8))}, {"W6"}), ("M11-code-claim", "mutation", {"code_facts": {}}, {"W7"}), ("M12-status-margin", "mutation", {"status": edit(base["status"], lambda x: x[48]["lower_mpmath"].update(minimum_margin_decimal=1.0e-7))}, {"P1"}), ("M13-crystal", "mutation", {"crystal": base["crystal"].replace("1574 unique", "1575 unique")}, {"P1"}), ("M14-validation-digest", "mutation", {"validation": {**base["validation"], "scope_ledger_sha256": "0" * 64}}, {"P2"}), ("M15-validation-check", "mutation", {"validation": {**base["validation"], "checks": {**base["validation"]["checks"], "batch75_shardized": False}}}, {"P2"}), ("M16-review-dropped", "mutation", {"reviews": list(R33_REVIEWS[1:])}, {"R1"}), ] def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() base = world(load_inputs()) def build(): return {**base, "registry": registry.load(), "definitions": {}, "reviews": list(R33_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)) if not args.drill: return cases = drill_cases(base) if args.blind: cases = [c for c in cases if args.blind in c[3]] d = gate.run_drill(build, CHECKS, DEPENDS, cases) summary = gate.summarize(d, CHECKS) print(gate.report_drill(summary)) for x in d: if not x["ok"]: print(" DRILL FAIL", x) if args.blind: n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"]) print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)") return log = {"run": "RUN-036", "subject": "Round 33: cross-backend enclosure dominance, and the depth-30 batch", "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("R33", "RUN-036", {}, R33_REVIEWS) print(f"registry: {len(R33_REVIEWS)} reviews recorded for R33") if __name__ == "__main__": main()