"""RUN-057 - LESR Paper 07: root-6217 barrier shape reconstruction. LESR Paper 07 (2026-09-20) reconstructs the root-6217 barrier as a controlled test of the LESR chain. From the contact equations it computes theta*, x5* and a second disk-B5 crossing alpha* to 55 digits; lists a 13-interval support signature, eight exposed bridges (three lengths), six triple-support lines with latent third contacts; sums the area from the signature to 65 digits; splits the surface-area measure into nonnegative witness pressures (B5 gets an atom b* at pi +- theta*) so that B5 balances in translation and rotation; reads off a B3 horizontal "subgradient" g3 = 2 (sin theta* - 1/2) < 0 balanced by the far-branch constraint x3 <= x3*; and concludes by convexity (sec. 16) that (x3*, x5*) minimizes the rho5 = 0 translation problem globally, then (sec. 17, by Cycle 12's symmetrization) all translations at rho5 = 0 within the far branch. It ships a certificate, a verifier, a compute-deferred list, a signature graph, plots, a state record and VALIDATION. It is evidence, not a canonical document. Here every constant is recomputed from the contact equations in mpmath, the signature against this tree's verified hull, and the KKT step against the area's measured directional derivatives. Checks A0 anchors the statements below occur in the document as written W1 constants sec. 1-4, 8, 10-13: theta*, x5*, alpha*, the bridges, b*, the B5 force, g3, the area and its 13 parts, from the contact equations (70 digits) - against the text, the certificate and VALIDATION W2 signature sec. 3-7: the verified hull at the barrier against the 13-interval table; the atoms; the six triple-support normals; the latent contacts; the least winner margin at the interval midpoints W3 kkt sec. 10-16: the pressure split and B5's balances; then F(x3, x5)'s measured directional derivatives against sec. 15's premise (the integral of the largest active rate) and against the claimed subgradient (g3, 0) - the worst direction, finite steps, the multipliers that do work W4 prior runs sec. 17: the symmetrization it rests on, against RUN-048 W5 records the certificate's statuses and the state against the sections; VALIDATION's replay W6 verifier the verifier, read after this rebuild and never run P1 package the VALIDATION record against the bytes and the archive Usage: python code/run057_lesr_paper07.py [--drill] [--blind CID] """ import argparse import copy import hashlib import inspect import json import math import re import mpmath as mp import numpy as np import gate import run046_uesfcm_cycles_07_09 as r46 from corpus import SOURCES, TREE, source_bytes, walk_sources from run053_lesr_paper03 import first_order, structure FOLDER = "main.zip!/LESR_Skew_Field_Variational/" PKG = FOLDER + "LESR_Paper07_Package_v0.1.zip!/" DOC = PKG + "LESR_Paper07_Root6217_Barrier_Shape_Reconstruction_v0.1.md" CERT = PKG + "LESR_Paper07_Barrier_Shape_Certificate_v0.1.json" VERIFIER = PKG + "LESR_Paper07_Verify_Barrier_Shape.py" PLOT = PKG + "LESR_Paper07_Barrier_Shape_Reconstruction.png" SIGPNG = PKG + "LESR_Paper07_Support_Signature_Graph_v0.1.png" SIGDOT = PKG + "LESR_Paper07_Support_Signature_Graph_v0.1.dot" TASKS = PKG + "LESR_Paper07_COMPUTE_DEFERRED_Tasks_v0.1.json" STATE = PKG + "LESR_State_Paper07_v0.1.json" VALIDATION = PKG + "LESR_Paper07_VALIDATION.json" PAPER08 = FOLDER + "LESR_Paper08_Package_v0.1.zip!/LESR_Paper08_Positive_Rotation_Certificate_Reduction_v0.1.md" LOG = TREE / "data" / "gate-logs" / "run057-lesr-paper07.json" LOG48 = TREE / "data" / "gate-logs" / "run048-uesfcm-cycles-12-14.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" CACHE = TREE / "data" / "cache" / "run057-searches.json" # data/cache is not committed # the constants as the text prints them (sec. 1, 2, 4, 8, 10, 11, 13) PRINTED = {"theta": "0.4540452162931832966751150439895469148442504536936533471", "x5": "0.01977094634794754914385507936321553103015453897764225981", "alpha": "0.848180369775584085040022340276448851992602952956868618", "Ltheta": "0.24402699852741554812952519030032421462301168", "Lalpha": "0.0998294599642212652279430328944230599803692883", "Lvert": "0.49188476115820359447636517572176149133140715", "area": "0.83498611055922409985066235655770059210182728925748306508259408038", "bstar": "0.0655836825508581909985249388028961008456583585", "margin": "0.178443315976557357131000251497428113777353322", "F5x": "0.117877515233001208663670207630118606859776859", "g3": "-0.122791062735083228947666632271676747712689174"} def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = (DOC, CERT, VERIFIER, PLOT, SIGPNG, SIGDOT, TASKS, STATE, VALIDATION) got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want + (PAPER08,)) if d is not None} rows = {row[0]: row for row in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"]} return {"text": got[DOC].decode("utf-8"), "cert": json.loads(got[CERT]), "verifier": got[VERIFIER].decode("utf-8"), "dot": got[SIGDOT].decode("utf-8"), "tasks": json.loads(got[TASKS]), "state": json.loads(got[STATE]), "validation": json.loads(got[VALIDATION]), "bytes": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want}, "paper08": got[PAPER08].decode("utf-8"), "log48": json.loads(LOG48.read_text(encoding="utf-8"))} # ---------------------------------------------------------------- the constants, from the contact equations def hp_constants(dps=70): """B3 (corners at 2 pi k / 3, radius 1/sqrt3) at (x3*, 0), x3* = x3^0 - s; B5 (corners at 2 pi k / 5, radius 1 / (2 cos(pi/10))) at (x5*, 0); the disc of radius 1/2. theta*: B3's corner v0 meets the disc; x5*: B5's arc about v3 supports at 1/2 at theta*; alpha*: that arc's other crossing of the disc in (theta*, 3 pi/10). The bridges as atoms (h'_next - h'_prev), b* from B5's horizontal balance, g3, the area by the analytic primitive over the 13 intervals, each piece's centre and radius, B5's vertical and rotation balances, and the least winner margin at the 13 midpoints over all 17 pieces""" mp.mp.dps = dps pi = mp.pi x3 = mp.mpf("-0.01215883209899") - mp.mpf("0.00882") R3, R5 = 1 / mp.sqrt(3), 1 / (2 * mp.cos(pi / 10)) c3 = R3 + x3 th = mp.acos(1 / (2 * c3)) x5 = (-mp.mpf(1) / 2 - R5 * mp.cos(6 * pi / 5 - th)) / mp.cos(th) V = [(x3 + R3 * mp.cos(2 * pi * k / 3), R3 * mp.sin(2 * pi * k / 3)) for k in range(3)] W = [(x5 + R5 * mp.cos(2 * pi * k / 5), R5 * mp.sin(2 * pi * k / 5)) for k in range(5)] f = lambda a: W[3][0] * mp.cos(a) + W[3][1] * mp.sin(a) + mp.mpf(1) / 2 grid = [th + (3 * pi / 10 - th) * k / 400 for k in range(1, 401)] roots = [mp.findroot(f, (a, b), solver="anderson") for a, b in zip(grid, grid[1:]) if f(a) * f(b) < 0] al = roots[0] up = lambda t: (-mp.sin(t), mp.cos(t)) dot = lambda p, q: p[0] * q[0] + p[1] * q[1] Lth, Lal, Lv = -dot(V[0], up(th)), dot(W[3], up(al)), W[1][0] - V[1][0] b = (mp.sin(3 * pi / 10) - mp.sin(al)) / mp.cos(th) D = ((mp.mpf(0), mp.mpf(0)), mp.mpf(1) / 2) sig = [(0, th, V[0], 0), (th, al, *D), (al, 3 * pi / 10, W[3], 1), (3 * pi / 10, pi / 2, W[1], 0), (pi / 2, 5 * pi / 6, V[1], 0), (5 * pi / 6, pi - th, V[0], 1), (pi - th, pi + th, *D), (pi + th, 7 * pi / 6, V[0], 1), (7 * pi / 6, 3 * pi / 2, V[2], 0), (3 * pi / 2, 17 * pi / 10, W[4], 0), (17 * pi / 10, 2 * pi - al, W[2], 1), (2 * pi - al, 2 * pi - th, *D), (2 * pi - th, 2 * pi, V[0], 0)] def part(a, b_, c, r): cn = mp.sqrt(c[0] ** 2 + c[1] ** 2) ang = mp.atan2(c[1], c[0]) if cn > 0 else mp.mpf(0) F = lambda t: cn ** 2 / 2 * mp.sin(2 * (t - ang)) + 2 * r * cn * mp.sin(t - ang) + r ** 2 * t return (F(b_) - F(a)) / 2 parts = [part(*s) for s in sig] # every piece: (centre, radius, range of normals or None) pieces = [(D[0], D[1], None)] + [(V[k], 0, None) for k in range(3)] + [(V[k], 1, (2 * pi * k / 3 + pi, pi / 6)) for k in range(3)] + \ [(W[k], 0, None) for k in range(5)] + [(W[k], 1, (2 * pi * k / 5 + pi, pi / 10)) for k in range(5)] def support(p, t): c, r, rg = p if rg is not None and abs(mp.fmod(t - rg[0] + 3 * pi, 2 * pi) - pi) > rg[1]: return None return c[0] * mp.cos(t) + c[1] * mp.sin(t) + r body = [0] + [3] * 6 + [5] * 10 margins, piece_margins = [], [] for a, b_, c, r in sig: t = (a + b_) / 2 vals = sorted(((x, body[i]) for i, x in enumerate(support(p, t) for p in pieces) if x is not None), key=lambda y: y[0], reverse=True) margins.append(vals[0][0] - next(x for x, bd in vals[1:] if bd != vals[0][1])) # against the other bodies piece_margins.append(vals[0][0] - vals[1][0]) # against every other piece # B5's vertical and rotation balance under the allocation: its arcs (density 1) and b* at pi -+ theta* on corners v2, v3 c5 = (x5, mp.mpf(0)) arcs5 = [(al, 3 * pi / 10, W[3]), (17 * pi / 10, 2 * pi - al, W[2])] fy = sum(mp.quad(mp.sin, [a, b_]) for a, b_, _ in arcs5) + b * (mp.sin(pi - th) + mp.sin(pi + th)) rel = lambda p: (p[0] - c5[0], p[1] - c5[1]) tau = sum(mp.quad(lambda t: dot(rel(w), up(t)), [a, b_]) for a, b_, w in arcs5) + b * (dot(rel(W[2]), up(pi - th)) + dot(rel(W[3]), up(pi + th))) fx = 2 * (mp.sin(3 * pi / 10) - mp.sin(al)) - 2 * b * mp.cos(th) s = lambda x: mp.nstr(x, dps - 5, strip_zeros=False) return {"theta": s(th), "x5": s(x5), "alpha": s(al), "roots": len(roots), "Ltheta": s(Lth), "Lalpha": s(Lal), "Lvert": s(Lv), "bstar": s(b), "margin": s(Lth - b), "F5x": s(2 * (mp.sin(3 * pi / 10) - mp.sin(al))), "g3": s(2 * (mp.sin(th) - mp.mpf(1) / 2)), "area": s(sum(parts)), "parts": [s(p) for p in parts], "pieces": [[s(c[0]), s(c[1]), s(mp.mpf(r))] for _, _, c, r in sig], "winner_margin": s(min(margins)), "piece_margin": s(min(piece_margins)), "balance": [s(fx), s(fy), s(tau)], "sin_below_half": bool(mp.sin(th) < mp.mpf(1) / 2), "c3_below_R3": bool(c3 < R3)} # ---------------------------------------------------------------- the signature, on this tree's verified hull X3F, X5F = -0.01215883209899 - 0.00882, 0.019770946347947549 VB = [X3F, 0.0, 0.0, X5F, 0.0] TABLE = ["B3v0", "D", "B5a3", "B5v1", "B3v1", "B3a0", "D", "B3a0", "B3v2", "B5v4", "B5a2", "D", "B3v0"] def signature_scan(): """the verified segments at the barrier (tie-level ones dropped), cycled to start at normal 0; their owners, their ends, the atoms and the active pieces at each hand-over""" st = structure(VB) S = sorted(((a % (2 * math.pi), b - a, k) for a, b, k in st["S"]), key=lambda x: x[0]) atoms = sorted(((x % (2 * math.pi), m, [r46.PIECE[j] for j in act]) for x, m, _, _, act in st["atoms"]), key=lambda x: x[0]) return {"owners": [r46.PIECE[k] for _, _, k in S], "starts": [a for a, _, _ in S], "atoms": [[x, m, act] for x, m, act in atoms]} # ---------------------------------------------------------------- the KKT step def kkt_scan(): """F(x3, x5) = area of conv(D, B3 + x3 e_x, B5 + x5 e_x), convex (Fary-Redei). At (x3*, x5*): the one-sided rates (F(v + t d) - F(v)) / t, t = 1e-7, in 72 directions, against sec. 15's premise (the least affine cost, the largest active rate at every normal: RUN-053's affine model) and against (g3, 0); the worst direction on a 0.6-rad window at 1/6000 rad; F(v + t d) - F(v) - t g.d there for t = 1e-6 .. 1e-2; the least rate over feasible directions (d3 <= 0); and over 720 directions the range of g3' for which (g3', 0) passes""" F = lambda a, b: r46.area([a, 0.0, 0.0, b, 0.0]) F0 = F(X3F, X5F) g3 = 2 * (math.sin(math.acos(1 / (2 * (1 / math.sqrt(3) + X3F)))) - 0.5) rate = lambda d, t=1e-7: (F(X3F + t * d[0], X5F + t * d[1]) - F0) / t st = structure(VB) rows = [] for k in range(72): d = (math.cos(2 * math.pi * k / 72), math.sin(2 * math.pi * k / 72)) rows.append({"measured": rate(d), "affine": first_order(st, VB, [d[0], 0.0, 0.0, d[1], 0.0])[1], "gd": g3 * d[0], "d3": d[0]}) worst = min(((rate((math.cos(p), math.sin(p))) - g3 * math.cos(p), p) for p in (3.3 + 0.6 * k / 3600 for k in range(3601)))) d = (math.cos(worst[1]), math.sin(worst[1])) steps = [F(X3F + t * d[0], X5F + t * d[1]) - F0 - t * g3 * d[0] for t in (1e-6, 1e-4, 1e-2)] lo, hi = -math.inf, math.inf for k in range(720): dk = (math.cos(2 * math.pi * k / 720), math.sin(2 * math.pi * k / 720)) r = rate(dk) if dk[0] < -1e-9: lo = max(lo, r / dk[0]) elif dk[0] > 1e-9: hi = min(hi, r / dk[0]) return {"g3": g3, "premise_gap": [min(r["affine"] - r["measured"] for r in rows), max(r["affine"] - r["measured"] for r in rows)], "margin_72": min(r["measured"] - r["gd"] for r in rows), "worst": list(worst), "steps": steps, "feasible_least": min(r["measured"] for r in rows if r["d3"] <= 1e-12), "valid": [lo, hi], "x3_right": rate((1.0, 0.0)), "x3_left": rate((-1.0, 0.0))} # ---------------------------------------------------------------- the cache def _key(name, fn, extra=""): import run008_round05_saturation_gate as r8 import run009_round06_witness_exchange as r9 import run052_lesr_paper02 as r52 import run053_lesr_paper03 as r53 digest = hashlib.sha256(inspect.getsource(fn).encode()) for helper in HELPERS[name]: digest.update(inspect.getsource(helper).encode()) for path in (r8.__file__, r9.__file__, r52.__file__, r53.__file__): digest.update(open(path, "rb").read()) digest.update(extra.encode()) return digest.hexdigest() HELPERS = {"constants": (), "signature": (r46.area,), "kkt": (r46.area, r46.hull)} def searches(): cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {} out = {} for name, fn in (("constants", hp_constants), ("signature", signature_scan), ("kkt", kkt_scan)): key = _key(name, fn) if cached.get(name, {}).get("key") != key: cached[name] = {"key": key, "value": json.loads(json.dumps(fn()))} CACHE.parent.mkdir(parents=True, exist_ok=True) CACHE.write_text(json.dumps(cached, indent=1) + "\n", encoding="utf-8") out[name] = cached[name]["value"] return out # ---------------------------------------------------------------- checks ANCHORS = {"A0": [PRINTED[k] for k in ("theta", "x5", "alpha", "Ltheta", "Lalpha", "Lvert", "area", "bstar", "margin", "F5x", "g3")] + [ r"0\in\partialF(x_3^\star,x_5^\star)+N_{\{x_3\lex_3^\star\}}.", r"A(x_3,0,0,x_5,0)\leA(x_3,y_3,0,x_5,y_5).", r"g_3+\eta_3=0.", "`DERIVEDGIVENTHERECONSTRUCTEDSUPPORTSIGNATURE`", r"m_{6217}(\rho)\gem_{6217}(0)"]} STATE_MAP = {"13 open normal intervals in the reconstructed support signature": (3, "FullCyclicSupportSignature"), "8 nonzero exposed bridge normals": (4, "NonzeroExposedBridges"), "6 triple-support lines total": (5, "SixTriple-SupportLines,NotOnlyFour"), "four nontrivial triple lines have latent B5 contact inside B3-disk bridge": (6, "WhytheFourNontrivialContactsRemainSpecial"), "vertical triple lines have latent disk contact inside B5-B3 bridge": (7, "VerticalTripleLinesHavetheOppositeLatentBody"), "surface-area measure admits a constructive nonnegative witness-pressure decomposition": (10, "AConstructivePressureDecomposition"), "B5 placement force/torque balances exactly by construction and reflection": (12, "$B_5$VerticalandRotationBalance"), "B3 horizontal subgradient is negative and balanced by the active x3 far-boundary normal": (13, "$B_3$HorizontalSubgradient"), "remaining exact shape obstruction is positive rotation": (18, "WhatRemainsOpen")} CLAIMS = { "constants_claim": {"text": {k: True for k in PRINTED}, "roots": 1, "certificate": [True] * 10, "parts": True, "pieces": True, "replay": [True] * 6}, "signature_claim": {"owners": True, "ends": True, "atoms": {"Lalpha": 2, "Ltheta": 4, "Lvert": 2, "zero": 4}, "triple": [0.454045, 1.570796, 2.687547, 3.595638, 4.712389, 5.82914], "winner_margin": [0.00526073, 0.000604651]}, "kkt_claim": {"split": [True, True], "balance": [True, True, True], "exact_sign": [True, True], "premise_gap": [0.265, 0.451], "margin_72": -0.0663, "worst": [-0.0696, 3.53], "steps": [-7e-08, -6.9e-06, -0.00025], "feasible_least": 0.0354, "valid": [-0.0477, -0.0474], "x3": [-0.0331, 0.213]}, "prior_claim": {"arc_least": [0.8349861106, 3.142], "barrier_is_least": True, "arc_certified": 0.013, "relies_on_symmetrization": True}, "records_claim": {"statuses": ["DERIVED_FROM_PRESSURE_DECOMPOSITION GIVEN_SIGNATURE", "CLOSED_GIVEN_SIGNATURE"], "closure_block": True, "unmapped": [], "facts": 9, "tasks": ["P07_INTERVAL_SIGNATURE_AUDIT", "P08_ROTATION_PROFILE_INTERVAL_DERIVATIVE", "P07_PRESSURE_CERT_RATIONALIZATION"], "dot_nodes": 13, "next": [True, False]}, "verifier_facts": {"lines": 152, "defs": ["regular_reuleaux", "b5arc3", "area_piece"], "classes": ["Body"], "midpoints_only": True, "fails": ["pressure allocation", "B3 KKT sign", "B5 stationarity", "triple tie"], "b5_by_definition": True, "area_evaluations": 1}, "package_claim": {"digests": [True] * 7, "unhashed": ["LESR_Paper07_Support_Signature_Graph_v0.1.dot"], "status": "PASS", "delimiters": [], "manifest": True}, } def sig(x, n=2): return float(f"{x:.{n - 1}e}") def agree(mine, printed): """the decimal digits printed, recomputed: |mine - printed| within one unit of the last printed digit""" mp.mp.dps = 90 places = len(printed.split(".")[1]) return bool(abs(mp.mpf(mine) - mp.mpf(printed)) <= mp.mpf(10) ** (-places)) def a0_anchors(w): text = gate.squash(w["text"]) return [f"anchor not found: {a[:60]}" for a in ANCHORS["A0"] if a not in text] def w1_constants(w): """the constants against the text's digits, the certificate's (to 60 places) and VALIDATION's replay""" s, c = w["search"]["constants"], w["cert"] cc, br, pc = c["constants"], c["transition_structure"]["bridge_lengths"], c["pressure_certificate"] near = lambda a, b, places=60: bool(abs(mp.mpf(a) - mp.mpf(b)) <= mp.mpf(10) ** (-places)) mp.mp.dps = 90 replay = dict(re.findall(r"^(.*?) = (.*)$", w["validation"]["fresh_replay_stdout"], re.M)) got = {"text": {k: agree(s[k], v) for k, v in PRINTED.items()}, "roots": s["roots"], "certificate": [near(s["theta"], cc["theta_star"]), near(s["x5"], cc["x5_star"]), near(s["alpha"], cc["alpha_star"]), near(s["area"], cc["area_barrier"]), near(s["Ltheta"], br["L_theta"]), near(s["Lalpha"], br["L_alpha"]), near(s["Lvert"], br["L_vertical"]), near(s["bstar"], pc["b_star"]), near(s["g3"], pc["B3_x_subgradient"]), near(s["F5x"], pc["B5_x_force_continuous"])], "parts": all(near(p, q["area_contribution"], 60) for p, q in zip(s["parts"], c["support_signature"])), "pieces": all(near(p[0], q["support_formula"]["cx"], 60) and near(p[1], q["support_formula"]["cy"], 60) and near(p[2], q["support_formula"]["r"], 60) for p, q in zip(s["pieces"], c["support_signature"])), "replay": [agree(s["theta"], replay["theta*"]), agree(s["alpha"], replay["alpha*"]), agree(s["x5"], replay["x5*"]), agree(s["area"], replay["area"]), agree(s["winner_margin"], replay["minimum midpoint winner margin"]), agree(s["bstar"], replay["b*"])]} w["w1"] = got return [] if got == w["constants_claim"] else [f"the constants: {got}"] def w2_signature(w): """the verified hull's owners are the table's; its hand-overs are the symbolic ends; eight atoms are bridges (four of length L_theta, two L_alpha, two L_vert) and four are zero; six normals have three bodies touching""" s, c = w["search"]["signature"], w["search"]["constants"] th, al = float(c["theta"]), float(c["alpha"]) # the hull's segments run round the circle, so B3's corner v0 is one segment across normal 0, which the table cuts # into its intervals 12 and 0: compare the 12 cyclic segments, starting at the disk's (theta*, alpha*) ends = sorted(x % (2 * math.pi) for x in (th, al, 3 * math.pi / 10, math.pi / 2, 5 * math.pi / 6, math.pi - th, math.pi + th, 7 * math.pi / 6, 3 * math.pi / 2, 17 * math.pi / 10, 2 * math.pi - al, 2 * math.pi - th)) starts = sorted(x % (2 * math.pi) for x in s["starts"]) i0 = min(range(len(s["starts"])), key=lambda i: abs(s["starts"][i] - th)) cyclic = s["owners"][i0:] + s["owners"][:i0] L = {float(c["Ltheta"]): "Ltheta", float(c["Lalpha"]): "Lalpha", float(c["Lvert"]): "Lvert"} kinds = [] for x, m, act in s["atoms"]: # a tangent hand-over is located to ~1e-8, so its atom (the gap in h') reads ~1e-8, not 0 k = next((name for val, name in L.items() if abs(m - val) < 1e-9), "zero" if m < 1e-6 else "other") kinds.append(k) bodies = lambda act: {a[:2] if a.startswith("B") else a for a in act} got = {"owners": cyclic == TABLE[1:12] + ["B3v0"], "ends": len(starts) == 12 and max(abs(a - b) for a, b in zip(starts, ends)) < 1e-7, "atoms": {k: kinds.count(k) for k in sorted(set(kinds))}, "triple": sorted(round(x, 6) for x, m, act in s["atoms"] if len({a[:2] for a in act}) == 3), "winner_margin": [sig(float(c["winner_margin"]), 6), sig(float(c["piece_margin"]), 6)]} w["w2"] = got return [] if got == w["signature_claim"] else [f"the signature: {got}"] def w3_kkt(w): """the split is nonnegative and B5 balances; g3 < 0 exactly. Sec. 15 says the area's directional derivative is the integral, against mu_h, of the largest active rate - it is not; (g3, 0) must satisfy g.d <= F'(v; d) in every direction - it does not; what holds is F' > 0 on the feasible directions, with a smaller multiplier""" s, c = w["search"]["kkt"], w["search"]["constants"] got = {"split": [mp.mpf(c["bstar"]) > 0, mp.mpf(c["margin"]) > 0], "balance": [abs(mp.mpf(x)) < mp.mpf(10) ** -60 for x in c["balance"]], "exact_sign": [c["c3_below_R3"], c["sin_below_half"]], "premise_gap": [round(x, 3) for x in s["premise_gap"]], "margin_72": sig(s["margin_72"], 3), "worst": [sig(s["worst"][0], 3), round(s["worst"][1], 2)], "steps": [sig(x, 2) for x in s["steps"]], "feasible_least": sig(s["feasible_least"], 3), "valid": [round(x, 4) for x in s["valid"]], "x3": [sig(s["x3_right"], 3), sig(s["x3_left"], 3)]} w["w3"] = got return [] if got == w["kkt_claim"] else [f"the kkt: {got}"] def w4_prior(w): """sec. 17 extends the slice minimum to all translations by Cycle 12's symmetrization y -> 0, which RUN-048 found does not keep d3 >= s; RUN-048's arc-side profile has its least value at the barrier itself""" l48 = w["log48"]["w6"] got = {"arc_least": l48["arc_least"][:2], "barrier_is_least": abs(l48["arc_least"][0] - round(float(w["search"]["constants"]["area"]), 10)) < 1e-9, "arc_certified": round(l48["coverage_arc"]["c12"] / sum(l48["coverage_arc"].values()), 3), "relies_on_symmetrization": "Cycle12alsoproved" in gate.squash(w["text"])} w["w4"] = got return [] if got == w["prior_claim"] else [f"the prior runs: {got}"] def w5_records(w): c, st, text = w["cert"], w["state"], gate.squash(w["text"]) got = {"statuses": [c["status"]["translation_KKT"], st["status"]["zero_rotation_translation_KKT"]], "closure_block": "ZERO_ROTATION_TRANSLATION_KKT=CLOSEDGIVENSIGNATURE" in text, "unmapped": [x for x in st["new_structural_facts"] if x not in STATE_MAP or f"#{STATE_MAP[x][0]}.{STATE_MAP[x][1]}" not in text], "facts": len(st["new_structural_facts"]), "tasks": [t["id"] for t in w["tasks"]["tasks"]], "dot_nodes": len(re.findall(r"^n\d+ \[", w["dot"], re.M)), "next": [st["next"] == "Paper 08 — Positive-Rotation Barrier Closure", "Positive-Rotation Barrier Closure" in w["paper08"][:300]]} w["w5"] = got return [] if got == w["records_claim"] else [f"the records: {got}"] def w6_verifier(w): """the verifier, read: it checks winners at the 13 midpoints only; its KKT tests are the sign of g3, b* inside (0, L_theta), and B5's residual - which is zero by the line that defines b*; no directional derivative of the area is taken anywhere, so sec. 15's step is not checked""" code = w["verifier"] got = {"lines": code.count("\n"), "defs": re.findall(r"^def (\w+)", code, re.M), "classes": re.findall(r"^class (\w+)", code, re.M), "midpoints_only": bool(re.search(r"m=\(a\+b\)/2", code)), "fails": re.findall(r'raise SystemExit\("FAIL ([^"]+)"\)', code), "b5_by_definition": bool(re.search(r"bstar=F5x/\(2\*mp\.cos\(theta\)\)", code)) and bool(re.search(r"res5=F5x-2\*bstar\*mp\.cos\(theta\)", code)), "area_evaluations": len(re.findall(r"area_piece\(\*p\)", code))} w["w6"] = got return [] if got == w["verifier_facts"] else [f"the verifier: {got}"] def p1_package(w): v, B = w["validation"], w["bytes"] sha = lambda b: hashlib.sha256(b).hexdigest() body = B[DOC].decode("utf-8") got = {"digests": [v["paper_sha256"] == sha(B[DOC]), v["certificate_sha256"] == sha(B[CERT]), v["verifier_sha256"] == sha(B[VERIFIER]), v["plot_sha256"] == sha(B[PLOT]), v["signature_graph_sha256"] == sha(B[SIGPNG]), v["state_sha256"] == sha(B[STATE]), v["tasks_sha256"] == sha(B[TASKS])], "unhashed": sorted(k.split("!/")[-1] for k in (SIGDOT,) if sha(B[k]) not in json.dumps(v)), "status": v["status"], "delimiters": sorted(set(re.findall(r"\\\(|\\\)|\\\[|\\\]", body))), "manifest": all(w["manifest_rows"][k][2] == sha(b) for k, b in B.items())} w["p1"] = got return [] if got == w["package_claim"] else [f"the package: {got}"] CHECKS = {"A0": a0_anchors, "W1": w1_constants, "W2": w2_signature, "W3": w3_kkt, "W4": w4_prior, "W5": w5_records, "W6": w6_verifier, "P1": p1_package} DEPENDS = {"A0": {"text"}, "W1": {"search", "cert", "validation", "constants_claim"}, "W2": {"search", "signature_claim"}, "W3": {"search", "kkt_claim"}, "W4": {"search", "log48", "text", "prior_claim"}, "W5": {"cert", "state", "text", "tasks", "dot", "paper08", "records_claim"}, "W6": {"verifier", "verifier_facts"}, "P1": {"validation", "bytes", "manifest_rows", "package_claim"}} def drill_cases(base): def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x text, s = base["text"], base["search"] return [ ("K0-unmodified", "control", {}, set()), ("K1-crlf", "control", {"text": text.replace("\n", "\r\n"), "verifier": base["verifier"].replace("\n", "\r\n"), "dot": base["dot"].replace("\n", "\r\n")}, set()), ("K2-validation-keys-sorted", "control", {"validation": json.loads(json.dumps(base["validation"], sort_keys=True))}, set()), ("M1-kkt-text", "mutation", {"text": text.replace("N_{\\{x_3\\le x_3^\\star\\}}", "N_{\\{x_3\\ge x_3^\\star\\}}", 1)}, {"A0"}), ("M2-certificate-alpha", "mutation", {"cert": edit(base["cert"], lambda x: x["constants"].update(alpha_star=x["constants"]["alpha_star"][:40] + "9" + x["constants"]["alpha_star"][41:]))}, {"W1"}), ("M3-replay-area", "mutation", {"validation": edit(base["validation"], lambda x: x.update(fresh_replay_stdout=x["fresh_replay_stdout"].replace("area = 0.8349861105", "area = 0.8349861106")))}, {"W1"}), ("M4-owner", "mutation", {"search": edit(s, lambda x: x["signature"]["owners"].__setitem__(1, "B5a4"))}, {"W2"}), ("M5-bridge", "mutation", {"search": edit(s, lambda x: x["signature"]["atoms"][0].__setitem__(1, 0.3))}, {"W2"}), ("M6-subgradient-holds", "mutation", {"search": edit(s, lambda x: x["kkt"].update(margin_72=0.001, worst=[0.0005, 3.53]))}, {"W3"}), ("M7-premise-holds", "mutation", {"search": edit(s, lambda x: x["kkt"].update(premise_gap=[0.0, 0.0]))}, {"W3"}), ("M8-arc-least", "mutation", {"log48": edit(base["log48"], lambda x: x["w6"].update(arc_least=[0.8349, 2.0, 0.0]))}, {"W4"}), ("M9-no-symmetrization", "mutation", {"text": text.replace("Cycle 12 also proved:", "It follows that:", 1)}, {"W4"}), ("M10-state-status", "mutation", {"state": edit(base["state"], lambda x: x["status"].update(zero_rotation_translation_KKT="OPEN"))}, {"W5"}), ("M11-task-dropped", "mutation", {"tasks": edit(base["tasks"], lambda x: x["tasks"].pop())}, {"W5"}), ("M12-verifier-derivative", "mutation", {"verifier": base["verifier"] + "\ndef directional(d, t):\n return (area_at(d, t) - A) / t\n"}, {"W6"}), ("M13-verifier-sample", "mutation", {"verifier": base["verifier"].replace("m=(a+b)/2", "m=a+(b-a)/3", 1)}, {"W6"}), ("M14-validation-digest", "mutation", {"validation": {**base["validation"], "certificate_sha256": "0" * 64}}, {"P1"}), ("M15-dot-bytes", "mutation", {"bytes": {**base["bytes"], SIGDOT: base["bytes"][SIGDOT] + b" "}}, {"P1"}), ] def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() base = {**load_inputs(), "search": searches()} def build(): return {**copy.deepcopy(base), **copy.deepcopy(CLAIMS)} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {} for c, fn in CHECKS.items(): try: results[c] = fn(w) except KeyError as e: results[c] = [f"claim missing: {e}"] 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"): print(key, "=", json.dumps(w.get(key), default=str, 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-057", "subject": "LESR Paper 07: root-6217 barrier shape reconstruction", "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")}, "drill": summary} LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8") if __name__ == "__main__": main()