"""The figures the crystallized paper adds up, counts or quotes, which no single gate log holds. python code/paper_figures.py (from lebesgue-verification-xuanheng/; needs data/source/) Writes data/paper-figures.json. It runs nothing of the programme and computes no mathematics of its own; it reads what the 68 runs already wrote, the runs' own code, and the archive. Its entries are of five kinds and never mixed: sums a sum, a difference, a ratio, a reciprocal or a sign change of fields of the gate logs; each entry names the fields it reads and asserts what it relies on (every leaf certified, no failure). counts counts over the inventory of the 68 reports (crystal/data/inventory.json, by SHA-256), over the drill records of the gate logs — for the whole tree, and for the runs each paper cites — and over the input manifest. parameters a run's grid sizes and precisions, read from its code as written. unlogged values a run's own code computes and checks, but its gate log does not record: the run's own function, imported and evaluated at the run's own inputs. No check is re-run. quoted_from_programme figures the paper cites from the programme's own documents, as the document writes them, with the document, its SHA-256 and the line. Nothing here recomputed them; the shared checker counts them apart from recomputed evidence. Re-run in the recorded environment, the file is byte-identical. """ import hashlib import json import platform import re import sys from decimal import Decimal from importlib import metadata from pathlib import Path TREE = Path(__file__).resolve().parents[1] LOGS = TREE / "data" / "gate-logs" OUT = TREE / "data" / "paper-figures.json" INVENTORY = TREE / "crystal" / "data" / "inventory.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" sys.path.insert(0, str(TREE / "code")) import corpus # noqa: E402 def log(prefix): (path,) = LOGS.glob(f"{prefix}-*.json") return json.loads(path.read_text(encoding="utf-8")) def field(prefix, *keys): v = log(prefix) for k in keys: v = v[k] return v def path_of(prefix, *keys): return f"{prefix} " + ".".join(str(k) for k in keys) def certified_sum(parts): """parts: [(prefix, keys to a record)]; a record is {area, certified, failures} or a list [area, certified, failures, escalated, least]. The sum is of certified leaves, and every leaf must be.""" total, read = 0, [] for prefix, keys in parts: r = field(prefix, *keys) area, cert, fail = (r["area"], r["certified"], r["failures"]) if isinstance(r, dict) else r[:3] assert cert == area and fail == 0, (prefix, keys, r) total += cert read.append(path_of(prefix, *keys)) return {"value": total, "rule": "sum of certified area leaves; each record has every leaf certified and no failure", "reads": read} def sums(): s = {} s["f3_erosion_area_leaves"] = certified_sum([("run047", ("w4", "c10")), ("run047", ("w4", "c11"))]) s["root6217_cycles_12_14_area_leaves"] = certified_sum( [("run048", ("w4", c)) for c in ("c12", "c13", "c14")]) s["root6217_cycles_15_17_area_leaves"] = certified_sum( [("run049", ("w4", "exact")), ("run049", ("w5", "h131", "exact")), ("run049", ("w5", "h129", "exact"))]) s["root6217_area_leaves"] = { "value": s["root6217_cycles_12_14_area_leaves"]["value"] + s["root6217_cycles_15_17_area_leaves"]["value"], "rule": "sum of the two entries above", "reads": ["root6217_cycles_12_14_area_leaves", "root6217_cycles_15_17_area_leaves"]} roots = [field("run047", "w1", c) for c in ("c10", "c11")] assert all(ok for _, ok in roots) s["f3_roots_closed"] = {"value": sum(n for n, _ in roots), "rule": "sum of the root counts of the two erosion certificates", "reads": [path_of("run047", "w1", c) for c in ("c10", "c11")]} verts = [field("run037", "w1", c, "vertices")[1] for c in ("47", "48")] s["rhcert_stored_vertices"] = {"value": sum(verts), "rule": "sum of the stored vertices of the cell 47 and cell 48 certificates", "reads": [path_of("run037", "w1", c, "vertices") for c in ("47", "48")]} barrier = Decimal(str(field("run049", "w2", "exact"))) a3 = Decimal(str(find_key(log("run061"), "A3plus"))) s["barrier_above_A3plus"] = {"value": float(barrier - a3), "rule": "difference, in decimal arithmetic", "reads": [path_of("run049", "w2", "exact"), "run061 A3plus"]} abar = Decimal(find_key(log("run002"), "upper")) s["anchored_cover_radius"] = {"value": float(2 * abar), "as_decimal": str(2 * abar), "rule": "R = 2 times the published upper bound, in decimal arithmetic", "reads": ["run002 upper"]} m = field("run057", "w3", "margin_72") assert m < 0 s["subgradient_shortfall_72"] = {"value": -m, "rule": "the negated (negative) margin over 72 directions", "reads": [path_of("run057", "w3", "margin_72")]} r = field("run005", "k5_ratios") big = max(r, key=int) s["smoothing_bound_over_moment_bound"] = {"value": 1 / r[big], "rule": "reciprocal of the ratio at the largest N logged", "reads": [path_of("run005", "k5_ratios", big)]} c4 = field("run007", "c4_rows") for key, label in (("eps_global_R", "the radius bound 2 Abar"), ("eps_true_R", "each cover's true radius")): r = {cover: row[key] / row["excess"] for cover, row in c4.items()} s[f"epsilon_over_actual_excess ({label})"] = { "least": min(r.values()), "largest": max(r.values()), "by_cover": r, "rule": "ratio of the bound to the actual Hausdorff excess, per cover", "reads": [path_of("run007", "c4_rows", c, k) for c in c4 for k in (key, "excess")]} c5 = field("run007", "c5_rows") s["steiner_against_support_area"] = { "value": max(abs(row["area_P_gamma_support"] - row["area_P_gamma_steiner"]) for row in c5.values()), "rule": "largest difference between Steiner's formula and the support-function area, over the covers", "reads": [path_of("run007", "c5_rows", c, k) for c in c5 for k in ("area_P_gamma_support", "area_P_gamma_steiner")]} w2 = field("run008", "w2") s["second_rung_dense_hull_against_exact"] = { "value": abs(w2["exact"] - w2["hull_dense"]), "rule": "difference", "reads": [path_of("run008", "w2", k) for k in ("exact", "hull_dense")]} n1, n3 = field("run008", "n1_rows"), field("run008", "n3_rows") tight = [row["eps_round04"] / row["eps_b"] for row in n1] gaps = [(row["smallest_member"] - row["LB_cell"], row["M"]) for row in n3] assert all(g > 0 for g, _ in gaps) s["saturation_cells"] = { "cells": len(n3), "covers": len({row["cover"] for row in n3}), "grids": len({row["M"] for row in n3}), "eps_b_tighter_least": min(tight), "eps_b_tighter_largest": max(tight), "closest_bound_to_smallest_member": min(gaps)[0], "closest_at_M": min(gaps)[1], "rule": "counts of the logged cells; ratios eps_round04 / eps_b; least smallest_member - LB_cell", "reads": ["run008 n1_rows", "run008 n3_rows"]} w3 = field("run010", "w3", "rows") s["recorded_J13_above_minimum"] = { "value": w3["13"]["package_sampled"] - w3["13"]["J"], "rule": "difference", "reads": [path_of("run010", "w3", "rows", "13", k) for k in ("package_sampled", "J")]} w4 = field("run010", "w4") s["fixed_seed_lift_above_four_body"] = { "value": w4["fixed_seed_J7"] - w4["four_body_search"], "rule": "difference", "reads": [path_of("run010", "w4", k) for k in ("fixed_seed_J7", "four_body_search")]} for leaf in ("seed + best B7", "four-body optimum"): w = field("run012", "w5", "widest_closing_half_width", leaf) assert w["core"] > w["rep"] > 0 s[f"core_over_representative_widest_cell ({leaf})"] = { "value": w["core"] / w["rep"], "rule": "ratio of the widest cells the exact core and the representative close", "reads": [path_of("run012", "w5", "widest_closing_half_width", leaf, k) for k in ("core", "rep")]} return s def find_key(v, key): """the one value under `key` anywhere in a log; refuses if there are several different ones""" found = [] def walk(x): if isinstance(x, dict): for k, y in x.items(): if k == key and not isinstance(y, (dict, list)): found.append(y) walk(y) elif isinstance(x, list): for y in x: walk(y) walk(v) assert found and len(set(map(str, found))) == 1, (key, found) return found[0] def counts(): raw = INVENTORY.read_bytes() inv = json.loads(raw) items = [i for r in inv for i in r["items"]] def first(i): a = i.get("audit") return re.match(r"relabelled from '([^']+)'", a).group(1) if a else i["strength"] def tally(keyf, xs): out = {} for x in xs: out[keyf(x)] = out.get(keyf(x), 0) + 1 return dict(sorted(out.items())) moved = [i for i in items if i.get("audit")] inventory = { "file": "crystal/data/inventory.json", "sha256": hashlib.sha256(raw).hexdigest(), "runs": len(inv), "items": len(items), "correction_rows": sum(len(r["corrections"]) for r in inv), "open_item_rows": sum(len(r["open_items"]) for r in inv), "by_strength": tally(lambda i: i["strength"], items), "by_strength_before_audit": tally(first, items), "moved_by_audit": len(moved), "moves": [{"from": a, "to": b, "items": n} for (a, b), n in sorted(tally(lambda i: (first(i), i["strength"]), moved).items())], } man = json.loads(MANIFEST.read_text(encoding="utf-8")) size = sum(leaf[1] for leaf in man["leaves"]) archive = {"leaves": len(man["leaves"]), "bytes": size, "megabytes": round(size / 10**6, 1), "rule": "decimal megabytes, one place"} by_paper = {} for paper, runs in PAPER_RUNS.items(): d = drill_over(runs) assert d["runs"] == len(runs), (paper, d["runs"]) by_paper[paper] = {"runs_named": [f"run{n:03d}" for n in runs], **d} return {"inventory": inventory, "drill": drill_over(), "drill_by_paper": by_paper, "archive": archive} # the runs each crystallized paper names as its checks; its drill figures are summed over exactly these PAPER_RUNS = {"certified-finite-reduction": [2, *range(4, 13), 41, 42]} def drill_over(runs=None): drill = {"runs": 0, "checks": 0, "plants": 0, "caught_by_named_checks": 0, "controls": 0, "controls_undisturbed": 0, "must_stay_green": 0, "must_stay_green_held": 0} for p in sorted(LOGS.glob("run*.json")): if runs is not None and int(p.name[3:6]) not in runs: continue g = json.loads(p.read_text(encoding="utf-8")) d = g.get("drill") if not isinstance(d, dict) or "plants" not in d: continue drill["runs"] += 1 drill["checks"] += len(g.get("checks") or ()) drill["plants"] += d.get("plants") or 0 drill["caught_by_named_checks"] += d.get("plants_caught_by_named_checks") or 0 drill["controls"] += d.get("controls") or 0 drill["controls_undisturbed"] += d.get("controls_undisturbed") or 0 drill["must_stay_green"] += d.get("must_stay_green_assertions") or 0 drill["must_stay_green_held"] += d.get("must_stay_green_held") or 0 return drill def code_of(stem): (path,) = (TREE / "code").glob(f"{stem}_*.py") return path, path.read_text(encoding="utf-8") def parameters(): src = (TREE / "code" / "run030_round27_interval_replay.py").read_text(encoding="utf-8") bits = int(re.search(r"^P = (\d+)$", src, re.M).group(1)) assert re.search(r"^ONE = 1 << P$", src, re.M) out = {"integer_interval_bits": {"value": bits, "reads": "code/run030_round27_interval_replay.py: ONE = 1 << P", "used_by": ["run030", "run031", "run045", "run047"]}} p4, s4 = code_of("run004") line = re.search(r"^ thetas = np\.linspace\(0, 2 \* np\.pi, (\d+)\)$", s4, re.M) modes = re.search(r"^ m = np\.arange\(1, (\d+), 2\)", s4, re.M) out["reuleaux_reconstruction_grid"] = {"directions": int(line.group(1)), "largest_odd_m": int(modes.group(1)) - 1, "reads": f"code/{p4.name}: n1_reconstruction", "used_by": ["run004"]} p6, s6 = code_of("run006") pm = re.search(r"^ P, M = (\d+), (\d+)$", s6, re.M) out["reflection_counterexample_grid"] = {"orientations_P": int(pm.group(1)), "directions_M": int(pm.group(2)), "reads": f"code/{p6.name}: P, M", "used_by": ["run006"]} dense = re.search(r"^ Gr, sr, lr = G\(hK, hU, (\d+), (\d+), w\[\"law\"\]\)$", s6, re.M) out["dense_reference_grid"] = {"directions_M": int(dense.group(1)), "orientations_P": int(dense.group(2)), "reads": f"code/{p6.name}: the dense reference G", "used_by": ["run006"]} for name, stem, func, pattern, value in GRIDS: path, src = code_of(stem) body = function_source(src, func) if func else src m = re.search(pattern, body, re.M) assert m, (name, stem, func) out[name] = {**value(m), "reads": f"code/{path.name}" + (f": {func}" if func else ""), "used_by": [stem]} return out def function_source(src, name): i = src.index(f"\ndef {name}(") j = src.find("\ndef ", i + 1) return src[i:j if j > 0 else len(src)] # grids and sample counts the paper states, each read from the run's script as written; a pattern that no # longer matches fails the file, so a changed script cannot leave a stale figure behind GRIDS = [ ("curvature_inversion_odd_modes", "run004", None, r"^ odd = \[([\d, ]+)\]$", lambda m: {"largest_odd_mode": max(int(x) for x in m.group(1).split(","))}), ("translation_bound_lps", "run006", "b3_translation", r"random_instances\((\d+)\):\n.*\n.*\n for sigma in \(\+1, -1\):\n" r" for phi in np\.linspace\(0, 2 \* np\.pi, (\d+), endpoint=False\):", lambda m: {"instances": int(m.group(1)), "branches": 2, "orientations": int(m.group(2)), "lps": int(m.group(1)) * 2 * int(m.group(2))}), ("bracket_grids", "run006", "b4_bracket", r"coarse, fine = \((\d+), (\d+)\), \((\d+), (\d+)\)", lambda m: {"coarse_M": int(m.group(1)), "coarse_P": int(m.group(2)), "fine_M": int(m.group(3)), "fine_P": int(m.group(4))}), ("test_instance", "run006", None, r"^SANITY_K = \{3: \(([\d.]+), 0\.0\), 5: \(0\.0, ([\d.]+)\)\}\n(?:.*\n)*? hK, hU = body\(SANITY_K\), " r"ellipse\(([\d.]+), ([\d.]+)\)", lambda m: {"cos3_coefficient": m.group(1), "sin5_coefficient": m.group(2), "semi_axes": [m.group(3), m.group(4)], "minor_width": str(2 * Decimal(m.group(4)))}), ("compiler_run_q", "run005", None, r"^ q = mp\.mpf\(\"([\d.]+)\"\) / (\d+)$", lambda m: {"q": f"{m.group(1)}/{m.group(2)}"}), ("cover_test_grid", "run007", None, r"P, _, _ = outer_polygon\(h, (\d+), ([\de.-]+), up\)", lambda m: {"M": int(m.group(1)), "q": m.group(2)}), ("sharp_radius_reference_polygon", "run041", None, r"^ n = 1 << (\d+)$", lambda m: {"sides_log2": int(m.group(1)), "sides": 1 << int(m.group(1))}), ("offset_placements", "run008", None, r"for d in \(([\d., ]+)\) for a in np\.linspace\(0, 2 \* math\.pi, (\d+), endpoint=False\)", lambda m: {"distances": len(m.group(1).split(",")), "angles": int(m.group(2)), "offsets": len(m.group(1).split(",")) * int(m.group(2))}), ("gauge_rotations", "run009", "w4_gauge", r"for _ in range\((\d+)\):", lambda m: {"rotations": int(m.group(1))}), ("exact_dual_grid", "run009", None, r"^ M, P = (\d+), (\d+)$", lambda m: {"M": int(m.group(1)), "P": int(m.group(2))}), ("motion_bound_placements", "run011", "w2_motion", r"for n in \(([\d, ]+)\)\}\n for k in range\((\d+)\):(?:.*\n)*? for _ in range\((\d+)\):\n(?:.*\n)*?" r" for _ in range\((\d+)\):", lambda m: {"bodies": len(m.group(1).split(",")) + int(m.group(2)), "boxes_per_body": int(m.group(3)), "placements_per_box": int(m.group(4)), "placements": (len(m.group(1).split(",")) + int(m.group(2))) * int(m.group(3)) * int(m.group(4))}), ("tree_identity_forests", "run011", "w5_trees", r"for _ in range\((\d+)\):", lambda m: {"forests": int(m.group(1))}), ] def unlogged(): import sympy as sp import run005_round02_finite_compiler as r5 import run006_round03_placement_certificate as r6 import run042_dlmvc_deep_passes as r42 out = {} c5 = r5.claims() c8 = r5.jackson_coeffs(8) out["jackson_multipliers_N8"] = {"mode_3": str(c8[3]), "mode_5": str(c8[5]), "computes": "run005 jackson_coeffs(8), the exact multipliers K9 uses"} for N in (256,): e = r5.sym_mp(c5["E_N"](sp.Integer(N))) half = r5.mu2(N) / 2 assert half <= e out[f"smoothing_bound_E_{N}"] = {"value": float(e), "computes": "run005 claims()['E_N'], as K5 and K6 do"} out[f"exact_half_second_moment_{N}"] = {"value": float(half), "computes": "run005 mu2(N) / 2, as K5 does"} L = 1.0 + 0.72 out["eta_64_test_instance"] = {"value": r6.eta(L, 64), "computes": "run006 eta(1 + 0.72, 64), as B5 does"} b = r42.budget(r42.ABAR) out["epsilon_deep"] = {"value": b["epsilon_deep"], "computes": "run042 budget(ABAR)['epsilon_deep'], as W1 does"} import math import run007_round04_cover_compiler as r7 c7 = r7.claims() R = c7["R_global"] grid = parameters()["cover_test_grid"] e = float(c7["eps"](R, math.pi / grid["M"], float(grid["q"]))) out["beta_as_used"] = {"value": float(c7["beta"](R, e)), "epsilon": e, "computes": "run007 claims()['beta'] at R = 2 Abar and the cover grid, as C7 does"} return out def environment(): def series(v): return ".".join(v.split(".")[:2]) full = {"python": platform.python_version(), **{m: metadata.version(m) for m in ("mpmath", "numpy", "scipy", "sympy")}} return {"about": "the interpreter and libraries this file was written with", "versions": full, "series": {k: series(v) for k, v in full.items()}} # what the paper quotes from the programme: (figure, document file name, text as the document writes it) QUOTES = [ ("tight reference A_ref (Cycle 16)", "UESFCM_Lebesgue_Cycle_16_Tight_Reference_and_Local_Secant_v0.1.md", "0.8349865"), ("stated slack of the tight reference (Cycle 16)", "UESFCM_Lebesgue_Cycle_16_Tight_Reference_and_Local_Secant_v0.1.md", "6.5385446698911637e-08"), ("separator constant s_7 (Cycle 03)", "UESFCM_Lebesgue_Cycle_03_Orbit_Localization_and_Scalar_Closure_v0.1.md", "0.00938484"), ("least centre area of the global pilot (Round 16)", "AMRAL_Lebesgue_Finite_Closure_Round_16_Global_Pilot_v0.1.md", "0.8356828349502634"), ("area inflation bound beta as used (Round 04 package)", "AMRAL_LUC_FC_Round_04_VALIDATION.json", "0.9063953966591665"), ("lens growth coefficient (BCODR LUC 04)", "BCODR_LUC_04_True_Overlap_Germ_Tangent_Decomposition_v0.1.md", "0.747599042164318"), ("far-branch gradient g_3, whose negative is the multiplier eta_3 by the document's g_3 + eta_3 = 0 (LESR Paper 07)", "LESR_Paper07_Root6217_Barrier_Shape_Reconstruction_v0.1.md", "-0.122791062735083228947666632271676747712689174"), ("the document's equation for the multiplier (LESR Paper 07)", "LESR_Paper07_Root6217_Barrier_Shape_Reconstruction_v0.1.md", r"g_3+\eta_3=0"), ("A_ref - m(0) (LESR Paper 08)", "LESR_Paper08_Positive_Rotation_Certificate_Reduction_v0.1.md", r"3.8944077590\times10^{-7}"), ("inner-core factor lambda_b as recorded (Round 04 deep audit, Pass 04 package)", "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_04_VALIDATION.json", "0.9882053662605436"), ("homothetic-core area lower bound as recorded (Pass 04 package)", "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_04_VALIDATION.json", "0.8268069547848553"), ("sharp cell radius as recorded (Pass 04 package)", "AMRAL_LUC_FC_Verification_Round_04_Deep_Audit_Pass_04_VALIDATION.json", "0.0059677037497217755"), ] def quotes(): names = {name for _, name, _ in QUOTES} blobs = {n: corpus.source_bytes(n) for n in corpus.SOURCES} assert not corpus.check_pins(blobs), corpus.check_pins(blobs) docs = {} for leaf, data in corpus.walk_sources(blobs, keep=lambda leaf: leaf.name in names): if data is not None: assert leaf.name not in docs, f"two leaves named {leaf.name}" docs[leaf.name] = (leaf, data.decode("utf-8")) out = [] for figure, name, text in QUOTES: leaf, body = docs[name] hits = [(n, line) for n, line in enumerate(body.splitlines(), 1) if text in line] assert hits, (name, text) n, line = hits[0] i = line.index(text) q = {"as_written": text, "line": line[max(0, i - 100):i + len(text) + 60].strip()} sci = re.fullmatch(r"(-?\d+\.\d+)\\times10\^\{(-?\d+)\}", text) if sci: q["reads_as"] = f"{sci.group(1)}e{sci.group(2)}" # the same figure in e-notation out.append({"figure": figure, "document": leaf.id, "document_sha256": leaf.sha256, "at": f"L{n}", "quoted_from_programme": q}) # the document's own equation g_3 + eta_3 = 0 turns its g_3 into the multiplier the paper names g3 = next(x for x in out if x["figure"].startswith("far-branch gradient g_3")) assert any(x["quoted_from_programme"]["as_written"] == r"g_3+\eta_3=0" for x in out) g3["quoted_from_programme"]["implies"] = {"eta_3": g3["quoted_from_programme"]["as_written"].lstrip("-")} return out def main(): figures = {"schema": "lebesgue-paper-figures.v1", "about": "figures of the crystallized paper that no single gate log holds; see code/paper_figures.py", "sums": sums(), **counts(), "parameters": parameters(), "unlogged": unlogged(), "environment": environment(), "quotes": quotes()} OUT.write_text(json.dumps(figures, ensure_ascii=False, indent=1) + "\n", encoding="utf-8", newline="\n") print("wrote", OUT.relative_to(TREE).as_posix()) for k, v in figures["sums"].items(): print(f" {k:40} {v.get('value', {a: b for a, b in v.items() if a not in ('rule', 'reads', 'by_cover')})}") print(" inventory", {k: figures["inventory"][k] for k in ("runs", "items", "correction_rows", "moved_by_audit")}) print(" drill", figures["drill"]) print(" archive", figures["archive"]) print(" quotes", len(figures["quotes"])) if __name__ == "__main__": main()