"""RUN-032 - Round 29: the necessity markers' directed rational upper certificates and the first whole shard. Round 29 migrates all 77 necessity markers of the atlas to exact rational outer polygons: a rational point q_j inside each directed cell, integer normals, directed support upper bounds of the disc and the two Reuleaux bodies rounded up to 10^-26, the half-planes' intersection by an exact polar hull, and its exact area below 167/200 - 77/77 at 4096 to 32768 normals, the least margin 6.1062e-7 (marker 6). It notes that marker 47's new bound is "tighter" than its Round 26 reference (margin 7.5672e-6 against 2.89e-7), and it joins marker 70 - Round 28's cell - with its 9278 migrated B7 leaves into the first whole-shard prototype. Here every marker point is checked inside its directed cell, its base hull area computed exactly (the corrected kernel), and every marker certified again by this tree's own outer polygons: integer-interval support upper bounds (Machin's pi, Taylor enclosures), a uniform grid of integer normals and the normals of the hull's bridging edges, the half-planes intersected through their exact polar hull. Checks A0 anchors the numbers and formulas below occur in Round 29 as written W1 points sec. 1, 15: each marker point inside its directed cell; the official axes; no override W2 upper sec. 2-10: all 77 markers certified here, with the bridging normals; the least density W3 package sec. 10-13: the package's bounds against the exact areas - valid, and first order in the normal spacing at the bridging edges; marker 47's "tighter" W4 audit sec. 14: the three-marker independent replay against the marker files W5 shard sec. 16-22: marker 70 is Round 28's cell; the shard's lower half is Round 28's W6 code what the package ships, read after the rebuild and never run P1 package the summary, the spec, the ABI, the shard, the crystal and the text agree P2 package VALIDATION against the archive; its checks from the data R1 registry Round 29's judgments reviewed, first-used statuses defined Usage: python code/run032_round29_marker_upper.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import inspect import json import math from fractions import Fraction from multiprocessing import Pool import numpy as np from scipy.spatial import ConvexHull import gate import registry import run008_round05_saturation_gate as r8 import run009_round06_witness_exchange as r9 import run011_round08_conditional_lift as r11 import run012_round09_adaptive_atlas as r12 import run013_round10_reference_dry_run as r13 import run019_round16_global_pilot as r19 import run020_round17_d3_cpg as r20 import run022_round19_necessity_lift as r22 import run023_round20_mixed_escalation as r23 import run025_round22_fourier_pareto as r25 import run026_round23_portfolio_closure as r26 import run027_round24_residual_joint as r27 import run028_round25_closure_wave as r28 import run029_round26_full_atlas as r29 import run030_round27_interval_replay as r30 import run031_round28_exact_root as r31 from corpus import SOURCES, TREE, source_bytes, walk_sources from run009_round06_witness_exchange import placed_disc, placed_reuleaux from run030_round27_interval_replay import ONE, P, add, cos_sin, div_int, exact, mul from run031_round28_exact_root import PI, neg, radius, sqrt_iv, sub PKG = "main.zip!/AMRAL_LUC_FC_Round_29_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_29_Marker_Whole_Shard_ABI_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_29_v0.1.md" SUMMARY = PKG + "AMRAL_LUC_FC_Round_29_MARKER_MIGRATION_SUMMARY.json" SPEC = PKG + "AMRAL_LUC_FC_Round_29_MARKER_UPPER_SPEC.json" ABI = PKG + "AMRAL_LUC_FC_Round_29_WHOLE_SHARD_ABI.json" SHARD = PKG + "AMRAL_LUC_FC_Round_29_WHOLE_SHARD_70.json" AUDIT = PKG + "AMRAL_LUC_FC_Round_29_A1_MARKER_AUDIT.json" VALIDATION = PKG + "AMRAL_LUC_FC_Round_29_VALIDATION.json" REF = PKG + "AMRAL_LUC_FC_Round_29_reference/" LOG = TREE / "data" / "gate-logs" / "run032-round29-marker-upper.json" CACHE = TREE / "data" / "cache" / "run032-markers.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" T, T_EXACT = 0.835, Fraction(167, 200) LADDER = (128, 256, 512, 1024, 2048, 4096) SCALE = 1 << 30 # the uniform normals: round(2^30 (cos, sin)) at 2 pi k / N BRIDGE = 1 << 40 # a bridging normal: round(2^40 (cos, sin)) at the hand-over angle # ---------------------------------------------------------------- directed support upper bounds def reuleaux_iv(m, phi, tx, ty): """a Reuleaux m-gon of width 1 at an exact placement: its corners V_j = t + R_m (cos, sin)(phi + 2 pi j / m) enclosed, and for the arc about V_j (radius 1) the centre of the normals it carries, -(cos, sin)(phi + 2 pi j / m), with cos(pi / 2m), the cosine of their half-width""" R = radius(m) corners, centres = [], [] for j in range(m): cs, sn = cos_sin(add(phi, div_int((2 * j * PI[0], 2 * j * PI[1]), m))) corners.append((add(tx, mul(R, cs)), add(ty, mul(R, sn)))) centres.append((neg(cs), neg(sn))) return corners, centres, cos_sin(div_int(PI, 2 * m))[0] def dot_hi(n, v): return mul(exact(n[0]), v[0])[1] + mul(exact(n[1]), v[1])[1] def dot_lo(n, v): return mul(exact(n[0]), v[0])[0] + mul(exact(n[1]), v[1])[0] def support_hi(n, body, norm): """h_B(n) from above for an integer normal n: the corners' n.V_j, and n.V_k + |n| for every arc whose range of normals may hold n - it is certainly out only when n.c_k < |n| cos(pi / 2m) at the ends""" corners, centres, cw = body best = max(dot_hi(n, v) for v in corners) bound = mul(norm, cw) for v, c in zip(corners, centres): if dot_hi(n, c) >= bound[0]: best = max(best, dot_hi(n, v) + norm[1]) return best def base_bodies(q): """the disc and the two Reuleaux bodies at an exact marker point q = (x3, y3, phi5, x5, y5)""" return (reuleaux_iv(3, exact(0), exact(q[0]), exact(q[1])), reuleaux_iv(5, exact(q[2]), exact(q[3]), exact(q[4]))) def half_planes(normals, bodies): """n.x <= H / 2^P for each integer normal: H the base hull's support upper, max of the disc's |n| / 2 and the two bodies'""" out = [] for n in normals: norm = sqrt_iv(exact(n[0] * n[0] + n[1] * n[1])) out.append(max(-(-norm[1] // 2), *(support_hi(n, b, norm) for b in bodies))) return out # ---------------------------------------------------------------- the exact outer polygon def outer_area(normals, H): """the half-planes' intersection through the polar hull of n_i / H_i (the origin is inside - the disc is), exactly: a float hull proposes the active constraints (dropping any only enlarges the polygon), Andrew's chain on the exact polar points keeps them, and the vertices are consecutive lines' crossings""" pts = np.array([[n[0] / (h / ONE), n[1] / (h / ONE)] for n, h in zip(normals, H)]) cand = sorted(set(ConvexHull(pts).vertices.tolist())) polar = sorted((Fraction(normals[i][0] * ONE, H[i]), Fraction(normals[i][1] * ONE, H[i]), i) for i in cand) def cross(o, a, b): return (a[0] - o[0]) * (b[1] - o[1]) - (a[1] - o[1]) * (b[0] - o[0]) lower, upper = [], [] for p in polar: while len(lower) >= 2 and cross(lower[-2], lower[-1], p) <= 0: lower.pop() lower.append(p) for p in reversed(polar): while len(upper) >= 2 and cross(upper[-2], upper[-1], p) <= 0: upper.pop() upper.append(p) active = [p[2] for p in lower[:-1] + upper[:-1]] verts = [] for i, j in zip(active, active[1:] + active[:1]): (a1, b1), (a2, b2) = normals[i], normals[j] det = a1 * b2 - a2 * b1 verts.append((Fraction(H[i] * b2 - H[j] * b1, ONE * det), Fraction(a1 * H[j] - a2 * H[i], ONE * det))) twice = sum(x1 * y2 - x2 * y1 for (x1, y1), (x2, y2) in zip(verts, verts[1:] + verts[:1])) return twice / 2, len(active) def uniform_normals(N): th = 2 * np.pi * np.arange(N) / N out = [] for c, s in zip(np.cos(th), np.sin(th)): a, b = round(SCALE * float(c)), round(SCALE * float(s)) g = math.gcd(a, b) out.append((a // g, b // g)) return out def bridge_normals(qf): """the normals of the base hull's straight bridging edges: the verified envelope's hand-overs between different bodies (disc, B3, B5), each as round(2^40 (cos, sin))""" parts = [placed_disc(), placed_reuleaux(3, 0.0, qf[:2]), placed_reuleaux(5, qf[2], qf[3:5])] raw, body = [], [] for b, p in enumerate(parts): raw += p body += [b] * len(p) for turn in r19.TURNS: # as exact_area: a refused envelope is retried at another turn pieces = r19.turned(raw, turn) C = np.array([p[0] for p in pieces], dtype=float) rho = np.array([p[1] for p in pieces], dtype=float) ranged = [(k, p[2]) for k, p in enumerate(pieces) if p[2] is not None] def owner(t, C=C, rho=rho, ranged=ranged): V = C @ np.stack([np.cos(t), np.sin(t)]) + rho[:, None] for k, (mid, half) in ranged: V[k, np.abs(r8.wrap(t - mid)) > half] = -np.inf return np.argmax(V, axis=0) try: cuts, owners = r8.envelope(owner, 1024, len(pieces)) except RuntimeError: continue segs = r8.verify_segments(C, rho, [p[2] for p in pieces], r8.segments(cuts, owners)) out = [] for (a, _, k), (_, _, k2) in zip(segs, segs[-1:] + segs[:-1]): if body[k] != body[k2]: out.append((round(BRIDGE * math.cos(a - turn)), round(BRIDGE * math.sin(a - turn)))) return out raise RuntimeError("envelope refused at every turn") def certify(args): """one marker: the exact area at its point (the corrected kernel), and this tree's outer polygon on the ladder of uniform normals plus the bridging normals, to the first that clears 167/200; with the uniform normals alone at the package's density, to compare""" q, pkg_density = args qf = np.array([float(x) for x in q]) bodies = base_bodies(q) bridges = bridge_normals(qf) out = {"exact": r19.base_area(qf), "bridges": len(bridges), "ladder": None} for N in LADDER: normals = uniform_normals(N) + bridges area, active = outer_area(normals, half_planes(normals, bodies)) if area < T_EXACT: out["ladder"] = {"N": N, "active": active, "margin": float(T_EXACT - area), "area": float(area)} break for key, N in (("uniform", pkg_density), ("uniform_half", pkg_density // 2)): normals = uniform_normals(N) area, active = outer_area(normals, half_planes(normals, bodies)) out[key] = {"N": N, "active": active, "margin": float(T_EXACT - area), "area": float(area)} return out def compute(markers): with Pool(14) as pool: return pool.map(certify, [([Fraction(x) for x in m["q_rational"]], m["final"]["density"]) for m in markers], chunksize=1) def computed(markers): digest = hashlib.sha256() for fn in (reuleaux_iv, dot_hi, dot_lo, support_hi, base_bodies, half_planes, outer_area, uniform_normals, bridge_normals, certify, compute): digest.update(inspect.getsource(fn).encode()) for mod in (r8, r9, r11, r12, r13, r19, r30, r31): digest.update(open(mod.__file__, "rb").read()) digest.update(json.dumps([[m["q_rational"], m["final"]["density"]] for m in markers]).encode()) key = digest.hexdigest() if CACHE.exists(): cached = json.loads(CACHE.read_text(encoding="utf-8")) if cached.get("key") == key: return cached["results"] results = json.loads(json.dumps(compute(markers))) CACHE.parent.mkdir(parents=True, exist_ok=True) CACHE.write_text(json.dumps({"key": key, "results": results}) + "\n", encoding="utf-8") return results def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {r29.LEDGER, r31.ROOTREC, r31.BULK, r31.LEAVES, r31.TOPO, r31.AXES} 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} markers = sorted((json.loads(v) for k, v in got.items() if k.startswith(REF + "marker_")), key=lambda m: m["cell"]) return {"text": got[DOC].decode("utf-8"), "crystal": got[CRYSTAL].decode("utf-8"), "summary": json.loads(got[SUMMARY]), "spec": json.loads(got[SPEC]), "abi": json.loads(got[ABI]), "shard": json.loads(got[SHARD]), "audit": json.loads(got[AUDIT]), "validation": json.loads(got[VALIDATION]), "markers": markers, "marker70_sha256": hashlib.sha256(got[REF + "marker_70.json"]).hexdigest(), "r28": {name: hashlib.sha256(got[leaf]).hexdigest() for name, leaf in (("root", r31.ROOTREC), ("topology", r31.TOPO), ("axes", r31.AXES), ("ledger", r31.LEAVES))}, "bulk28": json.loads(got[r31.BULK]), "rootrec28": json.loads(got[r31.ROOTREC]), "code": {k[len(PKG):]: v.decode("utf-8") for k, v in got.items() if k.startswith(PKG) and k.endswith(".py")}, "ledger26": json.loads(got[r29.LEDGER]), "manifest": json.loads(MANIFEST.read_text(encoding="utf-8"))} ANCHORS = { "W1": [r"q_{j,k}\in[\ell_k^{\rmhi},u_k^{\rmlo}]", r"77/77markers的rationalpoint皆安全位於directedcellinterior。", r"\boxed{\text{cellswithCPGoverride}=0.}"], "W2": [r"$$h_D(n)=\frac12\|n\|.$$", r"$$\pi/n.$$", r"\boxed{\widehath_{B_n}(n)\geh_{B_n}(n).}", r"$$H(q)=\operatorname{conv}(D\cupB_3\cupB_5).$$", r"\boxed{H_i=\left\lceil10^{26}\widehath_H(n_i)\right\rceil.}", r"\boxed{n_i\cdotx\leH_i/10^{26}.}", r"\boxed{H(q)\subseteqP.}", r"\boxed{A(H(q))\leA(P).}", r"$$A(P)<167/200,$$", r"\boxed{A(H(q))<0.835.}", r"$$p_i=n_i/h_i.$$", r"\boxed{77/77\text{PASS}.}"], "W3": [r"-4096：21markers；-8192：39；-16384：16；-32768：1。", r"\boxed{6.1062\times10^{-7}>0.}", r"\boxed{3.5043\times10^{-5}.}", r"$$U_6^{\rmrat}\approx0.8349993893782748.$$", r"$$0.835-U_{47}^{\rmref}\approx2.89\times10^{-7}.$$", r"$$U_{47}^{\rmrat}\approx0.834992432807.$$", r"\boxed{7.5672\times10^{-6}.}", r"新的outerconstruction反而更緊", r"沒有marker需要：$$65536.$$"], "W4": [r"\boxed{\texttt{A1-MARKER-SAMPLE-PASS}.}"], "W5": [r"0001110001100111000100010001001111011111", r"$$\boxed{70}.$$", r"$$U_{70}^{\rmrat}\approx0.83490750145<0.835,$$", r"$$\approx0.8349075014501105.$$", r"\boxed{9.24985\times10^{-5}.}", r"\boxed{\texttt{publication\_candidate=false}}"], "P1": [r"a_{\mathrm{Leb}}\ge0.835:\text{NOTCERTIFIED}"], } CLAIMS = { # every point strictly inside its directed cell, within 7 units in the last place of this tree's stored centre "points": {"markers": 77, "inside": 77, "axes_equal": 77, "ids_path_order": True, "centre_ulps": 7}, # this tree's outer polygons with the 11 bridging normals: 128 normals certify 51 markers, 256 the rest; the thinnest, # certified and exact, is marker 47 "upper": {"certified": 77, "ladder": {"128": 51, "256": 26}, "least": [47, 1.4996147563446147e-06], "exact_least": [47, 1.856783932985273e-05], "bridges": [11], "all_below_exact": True}, # the package's 77 areas are upper bounds; its active counts are this tree's at its densities; halving the density # multiplies the loss by 1.3-5.5 (first order at the bridging edges, as the offsets fall); 73 final densities are the # start rule's, 4 escalated; marker 47's reference and package losses "package": {"valid_upper": 77, "counts_equal": 77, "area_difference": 1.2598866394597508e-10, "loss_ratio": [1.3132319981728813, 5.51429571444892], "start_rule": [73, 4], "marker47": {"reference_loss": 1.8279320929348586e-05, "package_loss": 1.1000646286118965e-05, "exact_margin": 1.856783932985273e-05}, "least_package": [6, 6.106217252494817e-07]}, # [marker, density, area, margin as the file's; the replay's active count, the emitter's] "audit_claim": {"rows": [[6, True, True, True, 4962, 4900], [47, True, True, True, 10255, 10204], [70, True, True, True, 1317, 1284]], "status": "PASS", "same_in_summary": True}, "shard_claim": {"path": True, "point": True, "axes": True, "upper": True, "lower": True, "flags": True}, "code_facts": {"r29_marker_a1_verify.py": {"lines": 92, "absolute_path": True, "uses": ["AMRAL_LUC_FC_Round_29_A1_MARKER_AUDIT.json", "AMRAL_LUC_FC_Round_29_reference"], "not_in_archive": [], "normal_scale": 9, "sector_support": True, "start_from_reference_margin": False}, "r29_marker_migrate.py": {"lines": 190, "absolute_path": True, "uses": ["AMRAL_LUC_FC_Round_26_FULL_ATLAS_LEDGER.json", "AMRAL_LUC_FC_Round_28_ROOT_RECONSTRUCTION.json", "AMRAL_LUC_FC_Round_29_reference", "r25_incremental_wave.py"], "not_in_archive": [], "normal_scale": 9, "sector_support": True, "start_from_reference_margin": True}}, } def near(a, b, tol): return abs(a - b) <= tol def directed_cells(w): """each marker's directed cell (RUN-031's root and intended boxes) along its own path and axes""" sc = r31.root_scales() out = [] for m in w["markers"]: axes, c, h = r31.base_axes(m["path"]) lo, hi = r31.fractions(m["path"], axes, 5) bc, bh = r31.directed_box(lo, hi, r31.BASE, sc) out.append((axes, c, bc, bh)) return out def w1_points(w): """sec. 1, 15: every marker point strictly inside its directed cell; the official axes; the ids are the atlas's path order; each point is its cell's stored centre, rationalized""" out = [] paths = sorted(c["path"] for c in w["ledger26"]["cells"]) inside = axes_equal = 0 far = 0.0 for m, (axes, c, bc, bh) in zip(w["markers"], directed_cells(w)): q = [Fraction(x) for x in m["q_rational"]] low, high = [sub(x, y) for x, y in zip(bc, bh)], [add(x, y) for x, y in zip(bc, bh)] inside += all(Fraction(l[1], ONE) < v < Fraction(u[0], ONE) for v, l, u in zip(q, low, high)) axes_equal += axes == m["axis_trace"] and m["override_count"] == 0 far = max(far, max(abs(float(v) - x) / math.ulp(x) for v, x in zip(q, c) if x)) ids = [paths.index(m["path"]) for m in w["markers"]] == [m["cell"] for m in w["markers"]] got = {"markers": len(w["markers"]), "inside": inside, "axes_equal": axes_equal, "ids_path_order": ids, "centre_ulps": round(far)} if inside != 77 or axes_equal != 77 or not ids or len(w["markers"]) != 77 or got != w["points"]: out.append(f"the marker points: {got}") w["w1"] = got return out def w2_upper(w): """sec. 2-10: every marker certified by this tree's outer polygon - uniform normals and the bridging normals - at the least density on the ladder; the exact areas and margins""" out, res = [], w["computed"] ladder = collections.Counter(r["ladder"]["N"] if r["ladder"] else None for r in res) least = min(range(len(res)), key=lambda k: res[k]["ladder"]["margin"] if res[k]["ladder"] else -1) exact_least = min(range(len(res)), key=lambda k: T - res[k]["exact"]) got = {"certified": sum(r["ladder"] is not None for r in res), "ladder": {str(k): v for k, v in sorted(ladder.items(), key=lambda x: x[0] or 0)}, "least": [least, res[least]["ladder"]["margin"]], "exact_least": [exact_least, T - res[exact_least]["exact"]], "bridges": sorted(set(r["bridges"] for r in res)), "all_below_exact": all(r["ladder"]["area"] >= r["exact"] - 1e-12 for r in res if r["ladder"])} if got["certified"] != 77 or not got["all_below_exact"] or got != w["upper"]: out.append(f"this tree's certificates: {got}") w["w2"] = {**got, "margins": [r["ladder"]["margin"] for r in res], "exact_margins": [T - r["exact"] for r in res]} return out def w3_package(w): """sec. 10-13: the package's outer areas are upper bounds of the exact areas; this tree's uniform normals at the package's density reproduce its active counts and areas; the loss at half the density is about twice the loss at the full - first order in the spacing, from the bridging edges""" out, res, mk = [], w["computed"], w["markers"] valid = sum(m["final"]["outer_area_decimal"] >= r["exact"] for m, r in zip(mk, res)) counts = sum(m["final"]["active_constraints"] == r["uniform"]["active"] for m, r in zip(mk, res)) diff = max(abs(m["final"]["outer_area_decimal"] - r["uniform"]["area"]) for m, r in zip(mk, res)) ratios = [(r["uniform_half"]["area"] - r["exact"]) / (r["uniform"]["area"] - r["exact"]) for r in res] m47, r47 = mk[47], res[47] def start(m): """the emitter's first density, from the Round 26 reference margin (read in its code after the rebuild)""" return 2048 if m > 5e-4 else 4096 if m > 1e-4 else 8192 if m > 2e-5 else 16384 if m > 3e-6 else 32768 got = {"valid_upper": valid, "counts_equal": counts, "area_difference": diff, "loss_ratio": [min(ratios), max(ratios)], "start_rule": [sum(m["final"]["density"] == start(m["reference_marker_margin"]) for m in mk), sum(len(m["attempts"]) > 1 for m in mk)], "marker47": {"reference_loss": T - m47["reference_marker_margin"] - r47["exact"], "package_loss": m47["final"]["outer_area_decimal"] - r47["exact"], "exact_margin": T - r47["exact"]}, "least_package": [min(range(77), key=lambda k: mk[k]["final"]["margin_decimal"]), min(m["final"]["margin_decimal"] for m in mk)]} if valid != 77 or counts != 77 or diff > 1e-9 or got != w["package"]: out.append(f"the package's bounds: {got}") w["w3"] = {**got, "losses": [m["final"]["outer_area_decimal"] - r["exact"] for m, r in zip(mk, res)]} return out def w4_audit(w): """sec. 14: the independent replay of markers 6, 47 and 70 against their marker files""" out, aud, mk = [], w["audit"], w["markers"] rows = [] for a in aud["markers"]: f = mk[a["cell"]]["final"] rows.append([a["cell"], a["density"] == f["density"], a["outer_area_decimal"] == f["outer_area_decimal"], a["margin_decimal"] == f["margin_decimal"], a["exact_active_constraints"], f["active_constraints"]]) got = {"rows": rows, "status": aud["status"], "same_in_summary": aud["markers"] == w["summary"]["A1_marker_sample_audit"]["markers"]} if [r[0] for r in rows] != [6, 47, 70] or not all(r[1] and r[2] and r[3] for r in rows) or aud["status"] != "PASS" or not got["same_in_summary"] \ or got != w["audit_claim"]: out.append(f"the audit: {got}") w["w4"] = got return out def w5_shard(w): """sec. 16-22: marker 70 is Round 28's cell; the shard's upper half is marker 70's file, its lower half Round 28's certificate""" out, sh, mk = [], w["shard"], w["markers"] base, nm, b7 = sh["base_cell"], sh["necessity_marker"], sh["B7_lift"] m70 = mk[base["global_marker_id"]] bulk = w["bulk28"] got = {"path": base["path"] == m70["path"] == w["rootrec28"]["base_path"], "point": base["marker_point_q"] == m70["q_rational"], "axes": base["base_axis_trace"] == m70["axis_trace"] == w["rootrec28"]["base_axis_trace"], "upper": (nm["density"], nm["outer_area_decimal"], nm["margin_decimal"]) == (m70["final"]["density"], m70["final"]["outer_area_decimal"], m70["final"]["margin_decimal"]) and nm["certificate_sha256"] == w["marker70_sha256"], "lower": (b7["root_reconstruction_sha256"], b7["topology_sha256"], b7["axis_stream_sha256"], b7["leaf_ledger_sha256"]) == (w["r28"]["root"], w["r28"]["topology"], w["r28"]["axes"], w["r28"]["ledger"]) and (b7["leaf_count"], b7["leaf_pass_count"], b7["leaf_inconclusive_count"], b7["minimum_exact_rational_margin_decimal"]) == (bulk["leaves_total"], bulk["leaves_pass"], bulk["leaves_inconclusive"], bulk["minimum_exact_rational_margin_decimal"]), "flags": (sh["status"], sh["publication_candidate"], sh["theorem_ready"], sh["global_lebesgue_claim"]) == ("ARITHMETICALLY-CLOSED-WHOLE-SHARD-PROTOTYPE", False, False, False)} if not all(got.values()) or got != w["shard_claim"]: out.append(f"the shard: {got}") w["w5"] = got return out def w6_code(w): """what the package ships: two scripts, read after the rebuild and never run""" import re leaves = [row[0] for row in w["manifest"]["leaves"]] facts = {} for name, src in sorted(w["code"].items()): uses = sorted(set(re.findall(r"ROOT\s*/\s*'([^']+)'", src)) | set(re.findall(r"^import (r\d+_\w+)", src, re.M))) scale = re.search(r"(?:NORMAL_SCALE|SCALE)\s*=\s*10\*\*(\d+)", src) facts[name] = {"lines": src.count("\n"), "absolute_path": bool(re.search(r"(?:Path\(|=)\s*['\"]/", src)), "uses": uses, "not_in_archive": [u for u in uses if not any(u.split(".")[0] in leaf for leaf in leaves)], "normal_scale": int(scale.group(1)) if scale else None, "sector_support": "mp.iv.atan2(ivc(b),ivc(a))" in src, "start_from_reference_margin": "start=2048 if m>5e-4" in src} w["w6"] = facts return [] if facts == w["code_facts"] else [f"the scripts: {facts}"] def p1_package(w): out, s, mk, spec = [], w["summary"], w["markers"], w["spec"] margins = sorted(m["final"]["margin_decimal"] for m in mk) counts = {str(k): v for k, v in sorted(collections.Counter(m["final"]["density"] for m in mk).items())} low = min(mk, key=lambda m: m["final"]["margin_decimal"]) if (s["marker_count"], s["pass_count"], s["inconclusive_count"]) != (len(mk), sum(m["status"] == "DIRECTED-RATIONAL-UPPER-PASS" for m in mk), 0) \ or counts != s["density_counts"] or (low["cell"], low["final"]["margin_decimal"], low["final"]["outer_area_decimal"], low["final"]["density"]) \ != (s["minimum_margin"]["cell"], s["minimum_margin"]["margin_decimal"], s["minimum_margin"]["outer_area_decimal"], s["minimum_margin"]["density"]) \ or not near(float(np.median(margins)), s["median_margin_decimal"], 1e-18) or margins[-1] != s["maximum_margin_decimal"] \ or (s["base_path_override_stats"]["cells_with_override"], s["base_path_override_stats"]["maximum_override_count"]) != (0, max(m["override_count"] for m in mk)) \ or any(m["final"] != m["attempts"][-1] | {k: m["final"][k] for k in ("outer_area_fraction_sha256", "outer_area_num_bits", "outer_area_den_bits")} for m in mk) \ or any(not near(m["final"]["margin_decimal"], 0.835 - m["final"]["outer_area_decimal"], 2e-16) for m in mk): out.append("the summary against the 77 marker files") if spec["support_upper"]["rationalization"] != "ceil to a fixed rational denominator 10^26" or not spec["fail_closed"] \ or "dropping constraints enlarges the polygon" not in spec["outer_polygon"]["candidate_reduction"]: out.append("the upper spec") crystal = gate.squash(w["crystal"]) for frag in ("77/77", "6.1062", "70", "9278/9278"): if frag not in crystal: out.append(f"crystal: {frag}") w["p1"] = {"density_counts": counts, "median": float(np.median(margins))} return out def p2_package(w): import re out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf_id, text in (("round29", 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 (("marker_summary_sha256", SUMMARY), ("marker_upper_spec_sha256", SPEC), ("whole_shard_abi_sha256", ABI), ("whole_shard_70_sha256", SHARD), ("A1_marker_audit_sha256", AUDIT)): if v[key] != leaves[leaf_id][2]: out.append(f"VALIDATION {key} against the archive") s, sh, mk = w["summary"], w["shard"], w["markers"] kc = {"marker_count_77": len(mk) == s["marker_count"] == 77, "all_marker_pass": s["pass_count"] == 77, "no_marker_inconclusive": s["inconclusive_count"] == 0, "all_marker_paths_zero_override": all(m["override_count"] == 0 for m in mk), "marker_A1_sample_pass": w["audit"]["status"] == "PASS", "marker70_path_matches_round28": sh["base_cell"]["path"] == w["rootrec28"]["base_path"], "marker70_upper_pass": sh["necessity_marker"]["status"] == "DIRECTED-RATIONAL-UPPER-PASS", "round28_lower_all_pass": sh["B7_lift"]["leaf_pass_count"] == sh["B7_lift"]["leaf_count"], "whole_shard_not_publication_candidate": sh["publication_candidate"] is False, "whole_shard_not_theorem_ready": sh["theorem_ready"] is False, "no_global_claim": sh["global_lebesgue_claim"] is False} if kc != v["checks"] or v["status"] != "PASS": out.append(f"VALIDATION checks {kc}") w["p2"] = kc return out R29_DEFINITIONS = { "UPPER-INCONCLUSIVE": ("in-line", "sec. 0: a marker whose rational outer polygon does not fall below 167/200 at the densities tried"), "A1-MARKER-SAMPLE-PASS": ("in-line", "sec. 14: markers 6, 47 and 70 replayed by a second polygon path, all passing - a sample, not 77/77"), "ARITHMETICALLY-CLOSED-WHOLE-SHARD-PROTOTYPE": ("in-line", "sec. 0, 21: a shard whose marker upper and lift lower certificates both pass " "in exact / directed arithmetic, under a prototype backend"), "ARITHMETICALLY CLOSED": ("in-line", "sec. 0: the same, of the first whole-shard prototype"), "ARITHMETICALLY-CLOSED-PROTOTYPE": ("in-line", "sec. 23: local upper and lower arithmetic both PASS"), "PUBLICATION-CANDIDATE-SHARD": ("in-line", "sec. 26: a whole shard whose 9278 lower leaves also pass a second, independent replay"), "THEOREM-READY": ("in-line", "sec. 23: every global shard, the root and base atlas, the dependency merge, and no pending obligation"), } R29_REVIEWS = [ ("PASS", "19. Marker 70 upper", "computation", "PASS", "an upper bound - the exact area 0.83480184 lies below it; here it certifies with 128 normals once the bridging edges' normals " "are added (W2, W3)"), ("PASS", "77/77", "computation", "PASS", "77 of 77 here too, with 128 or 256 normals once the bridging edges' normals are added; the package's densities are start " "points from the reference margins (W2, W3)"), ("PASS", "", "computation", "PASS", "the three replays reproduce the marker files; the replay shares the emitter's support bounds and normals, skipping only " "its candidate reduction - a second polygon path, not a second arithmetic (W4, W6)"), ("PASS", "9278/9278", "computation", "PASS", "RUN-031 certified all 9278 leaves on their intended boxes"), ("PASS", "77/77 marker upper certificates", "computation", "PASS", "77 of 77 here too, with 128 or 256 normals once the bridging edges' normals are added; the package's densities are " "start points from the reference margins (W2, W3)"), ("CLOSED", "WHOLE-SHARD ARITHMETIC ABI", "reading", "PASS", "the five layers are defined, and the shard file carries each (W5)"), ("OPEN", "FULL A1 / PUBLICATION BACKEND", "reading", "PASS", "true: the replay covers three markers and no lower leaf"), ("COMPLETE", "77 NECESSITY MARKER UPPER MIGRATION", "computation", "PASS", "77 of 77 here too, with 128 or 256 normals once the bridging edges' normals are added; the package's densities are " "start points from the reference margins (W2, W3)"), ("PUBLICATION-CANDIDATE", "", "n/a", "n/a", "a state of sec. 23, defined there; not a judgment"), ("ARITHMETICALLY-CLOSED-PROTOTYPE", "", "n/a", "n/a", "a state of sec. 23, defined there; not a judgment"), ("PUBLICATION-CANDIDATE-SHARD", "", "n/a", "n/a", "a goal of sec. 26 for Round 30; not a judgment"), ("THEOREM-READY", "", "n/a", "n/a", "a state of sec. 23, defined there; not a judgment"), ("ARITHMETICALLY CLOSED", "FIRST WHOLE-SHARD PROTOTYPE", "computation", "PASS", "its upper half is marker 70's file, its lower half Round 28's certificate, both checked here and in RUN-031 (W5)"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("NOT CERTIFIED", "a_{Leb}≥0.835", "reading", "PASS", "true"), ("UPPER-INCONCLUSIVE", "0. 本輪摘要", "computation", "PASS", "none here either (W2)"), ("ARITHMETICALLY-CLOSED-WHOLE-SHARD-PROTOTYPE", "", "computation", "PASS", "its upper half is marker 70's file, its lower half Round 28's certificate, both checked here and in RUN-031 (W5)"), ("ARITHMETICALLY-CLOSED-WHOLE-SHARD-PROTOTYPE", "", "computation", "PASS", "its upper half is marker 70's file, its lower half Round 28's certificate, both checked here and in RUN-031 (W5)"), ("A1-MARKER-SAMPLE-PASS", "", "computation", "PASS", "the three replays reproduce the marker files; the replay shares the emitter's support bounds and normals, " "skipping only its candidate reduction (W4, W6)"), ] def r1_registry(w): return registry.completeness(w["registry"], "R29", w["definitions"], w["reviews"]) CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_points, "W2": w2_upper, "W3": w3_package, "W4": w4_audit, "W5": w5_shard, "W6": w6_code, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "W1": {"markers", "ledger26", "points"}, "W2": {"computed", "upper"}, "W3": {"computed", "markers", "package"}, "W4": {"audit", "markers", "summary", "audit_claim"}, "W5": {"shard", "markers", "marker70_sha256", "r28", "bulk28", "rootrec28", "shard_claim"}, "W6": {"code", "code_facts", "manifest"}, "P1": {"summary", "markers", "spec", "crystal"}, "P2": {"validation", "manifest", "text", "crystal", "summary", "shard", "markers", "audit", "rootrec28"}, "R1": {"registry", "definitions", "reviews"}} 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["markers"]) def build(): return {**inputs, "computed": results_computed, "registry": registry.load(), "definitions": dict(R29_DEFINITIONS), "reviews": list(R29_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", "p1", "p2"): print(key, json.dumps(w.get(key), default=float, ensure_ascii=False)[:1500]) if not args.drill: return mk, text = inputs["markers"], inputs["text"] def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x exact20 = results_computed[20]["exact"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-summary-keys-sorted", "control", {"summary": json.loads(json.dumps(inputs["summary"], sort_keys=True))}, set()), ("K3-shard-keys-sorted", "control", {"shard": json.loads(json.dumps(inputs["shard"], sort_keys=True))}, set()), ("M1-doc-margin", "mutation", {"text": text.replace(r"6.1062\times", r"6.1063\times")}, {"A0"}), ("M2-point-outside", "mutation", {"markers": edit(mk, lambda x: x[10]["q_rational"].__setitem__(0, "0/1"))}, {"W1"}), ("M3-axis-trace", "mutation", {"markers": edit(mk, lambda x: x[30]["axis_trace"].__setitem__(slice(0, 2), [3, 2]))}, {"W1"}), ("M4-upper-claim", "mutation", {"upper": {**CLAIMS["upper"], "certified": 76}}, {"W2"}), ("M5-area-below-exact", "mutation", {"markers": edit(mk, lambda x: x[20]["final"].update(outer_area_decimal=exact20 - 1e-9))}, {"W3", "P1"}), ("M6-package-claim", "mutation", {"package": {**CLAIMS["package"], "counts_equal": 76}}, {"W3"}), ("M7-audit-area", "mutation", {"audit": edit(inputs["audit"], lambda x: x["markers"][1].update(outer_area_decimal=x["markers"][1]["outer_area_decimal"] + 1e-12))}, {"W4"}), ("M8-shard-margin", "mutation", {"shard": edit(inputs["shard"], lambda x: x["necessity_marker"].update(margin_decimal=9.2e-5))}, {"W5"}), ("M9-shard-leaves", "mutation", {"shard": edit(inputs["shard"], lambda x: x["B7_lift"].update(leaf_count=9277))}, {"W5", "P2"}), ("M10-code-claim", "mutation", {"code_facts": {}}, {"W6"}), ("M11-summary-counts", "mutation", {"summary": {**inputs["summary"], "density_counts": {**inputs["summary"]["density_counts"], "32768": 2}}}, {"P1"}), ("M12-crystal", "mutation", {"crystal": inputs["crystal"].replace("77/77", "76/77")}, {"P1"}), ("M13-validation-digest", "mutation", {"validation": {**inputs["validation"], "whole_shard_70_sha256": "0" * 64}}, {"P2"}), ("M14-validation-check", "mutation", {"validation": {**inputs["validation"], "checks": {**inputs["validation"]["checks"], "no_marker_inconclusive": False}}}, {"P2"}), ("M15-review-dropped", "mutation", {"reviews": list(R29_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-032", "subject": "Round 29: the necessity markers' directed rational upper certificates and the first whole shard", "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", "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("R29", "RUN-032", R29_DEFINITIONS, R29_REVIEWS) print(f"registry: {len(R29_DEFINITIONS)} definitions, {len(R29_REVIEWS)} reviews recorded for R29") if __name__ == "__main__": main()