"""RUN-011 - Round 08: the conditional-lift certificate compiler. Round 08 fixes the proof grammar for the 0.8350 milestone: a placement box moves a body by at most delta (motion bound), a convex core with C + delta B inside the box-centre body lies inside every placement of the box (common-core theorem), the Reuleaux erosion of Mishra's certificate is the special case with discs of radius 1 - delta, and a base atlas whose every leaf is base-pruned or closed by a complete witness lift tree proves Lambda >= T (nested soundness). It fixes B7's root for T = 0.835 and specifies the verifier. Its computation is deferred. The theorems are read in the report; here the constants are rebuilt, Mishra's lemmas read against the text, the motion bound and the cores tested on random boxes, and two lift leaves - at the seed and at the four-body optimum, in base cells the base bound cannot prune - computed with the inner-point lower bound the verifier would use. Checks A0 anchors the formulas and constants below occur in Round 08 as written A1 citations its references X1 paper sec. 1, 4, 16: Mishra's Lemmas 21-22 and Remark 24, his remark on reflections (after Lemma 17), and his sec. 5.2 tree identity W1 constants sec. 6-7, 19-20: R_7, t_7(0.835), the domains, the headroom and its ratio W2 motion sec. 1: d_H(gK, g0K) <= sqrt(hx^2 + hy^2) + 2 R_K sin(h_phi/2) on random boxes W3 cores sec. 2-4, 33: Reuleaux cores inside every placement; the emptiness threshold; the analytic support core of the package's sanity body W4 leaves sec. 8-9, 12: two lift leaves the base cannot prune, bounded below by inner points W5 trees sec. 16 V8: a binary forest with S seeds and L leaves has 2L - S nodes P1 package VALIDATION, LOCAL_COMPUTE_SPEC and CERTIFICATE_SCHEMA against the text; how often the package's sanity test S1 would expose a motion bound without its rotation term (recorded, not judged) P2 package the package's self-description of its files matches the archive R1 registry Round 08's judgments reviewed, first-used statuses defined Usage: python code/run011_round08_conditional_lift.py [--refresh] [--drill] [--blind CID] """ import argparse import datetime import json import math import re import numpy as np import sympy as sp from scipy.spatial import ConvexHull import gate import registry from corpus import SOURCES, TREE, source_bytes, walk_sources from run006_round03_placement_certificate import body from run008_round05_saturation_gate import R0, disc_samples, reuleaux_support, reuleaux_vertices from run009_round06_witness_exchange import hull_pieces, placed_disc, placed_reuleaux, rot from run010_round07_minimizer_atlas import d_star, t_text PKG = "main.zip!/AMRAL_LUC_FC_Round_08_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_08_Conditional_Lift_Certificate_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_08_v0.1.md" VALIDATION = PKG + "AMRAL_LUC_FC_Round_08_VALIDATION.json" SPEC = PKG + "AMRAL_LUC_FC_Round_08_LOCAL_COMPUTE_SPEC.json" SCHEMA = PKG + "AMRAL_LUC_FC_Round_08_CERTIFICATE_SCHEMA.json" SKELETON = PKG + "AMRAL_LUC_FC_Round_08_verifier_skeleton.py" SNAPSHOT = TREE / "data" / "external" / "round08-citations.json" ROUND07 = TREE / "data" / "external" / "round07-citations.json" RUN010 = TREE / "data" / "gate-logs" / "run010-round07-minimizer-atlas.json" LOG = TREE / "data" / "gate-logs" / "run011-round08-conditional-lift.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" ANCHORS = { "W1": [r"R_7=\frac{1}{2\sin(3\pi/7)}\approx0.512858431636.", r"|t_7|\le0.196935046771", r"0.8350-0.834781190917=0.000218809083", r"\approx6.83."], "W2": [r"d_H(K_0,K_g)\le\delta:=\sqrt{h_x^2+h_y^2}+2R_K\sin\frac{h_\phi}{2}."], "W3": [r"C=\bigcap_jB(V_j,1-\delta)", r"h(\theta)=\frac12+0.02\cos3\theta.", r"\frac12-0.16\cos3\theta\ge0.34."], "W4": [r"\operatorname{Area}H_{\mathrm{actual}}\ge\operatorname{Area}H_{\mathrm{core}}.", r"A_{\mathrm{inner}}-e_{\mathrm{fp}}\geT_1."], "W5": [r"N=2L-1", r"N=2L-S"], } REFS = {1: {"kind": "arxiv", "id": "2608.30538"}, 3: {"kind": "arxiv", "id": "1810.10089"}, 4: {"kind": "arxiv", "id": "2609.01284"}, 5: {"kind": "crossref", "doi": "10.1017/CBO9781139003858"}} CITE_OPTS = {n: {} for n in REFS} MISHRA_FACTS = { # short phrases only; matched in the full text of v2 "erosion": r"Then ⋂ j = 1 n D ¯ \( V j , 1 − δ \) ⊆ ⋂ j = 1 n D ¯ \( W j , 1 \)", "nonempty": r"The left-hand side is non-empty precisely when 1 − δ 1-\\delta is at least the circumradius", "delta3": r"moves by at most δ 3 = h x 2 \+ h y 2", "delta5": r"δ 5 = h x 2 \+ h y 2 \+ 2 R 5 sin \( h ρ / 2 \)", "thresholds": r"The thresholds are δ 3 = 0\.422649730810 \\delta_\{3\}=0\.422649730810 and δ 5 = 0\.474268887881", "reflections": r"Reflections need not be considered separately, since D D , B 3 B_\{3\} and B 5 B_\{5\} each have an " r"axis of symmetry", "forest": r"a forest of s s such trees with L L leaves in total has exactly 2 L − s 2L-s nodes", } # ---------------------------------------------------------------- geometry def support_of_points(P, th): return np.max(np.asarray(P) @ np.stack([np.cos(th), np.sin(th)]), axis=0) def motion_delta(hx, hy, hphi, RK): """sec. 1 (Mishra's Lemma 22): the most a point of a body within R_K of its centre moves""" return math.hypot(hx, hy) + 2 * RK * math.sin(hphi / 2) def reuleaux_core_points(V, rho, per_circle=4000): """inner points of the core, the intersection of the discs of radius rho about the corners V: points on each circle pulled in by a relative 1e-12, kept when within rho of every corner""" if rho <= 0: return np.zeros((0, 2)) t = 2 * np.pi * np.arange(per_circle) / per_circle circle = np.stack([np.cos(t), np.sin(t)], axis=1) pts = [] for v in V: cand = v + rho * (1 - 1e-12) * circle ok = np.all(np.linalg.norm(cand[:, None, :] - V[None, :, :], axis=2) <= rho, axis=1) pts.append(cand[ok]) return np.vstack(pts) def core_is_empty(V, rho): """whether the discs of radius rho about V fail to meet, searched on a fine grid round the corners' centroid (for a regular polygon the best point is its centre)""" c = V.mean(axis=0) g = np.linspace(-0.01, 0.01, 201) P = c + np.stack(np.meshgrid(g, g), axis=-1).reshape(-1, 2) return not bool(np.any(np.all(np.linalg.norm(P[:, None, :] - V[None, :, :], axis=2) <= rho, axis=1))) def placed_vertices(n, phi, t): return reuleaux_vertices(n) @ rot(phi).T + np.asarray(t, dtype=float) # S1's placement box, as the package's sanity script sets it (read after this tree's # reconstruction); with its R_K = 0.55 it reproduces the delta VALIDATION records S1_BOX, S1_RK = (0.0015, 0.0010, 0.006), 0.55 def s1_exposure(hx, hy, hp, samples=2000): """S1's body h = 1/2 + 0.02 cos 3t in S1's box, with a motion bound that has lost its rotation term: the worst support deficit over a grid of placements (box corners, five angles, 241 base angles) and the share of random placements showing any deficit""" h = lambda t: 0.5 + 0.02 * np.cos(3 * t) th = 2 * np.pi * np.arange(20000) / 20000 d = math.hypot(hx, hy) worst = math.inf for phi0 in np.linspace(0, 2 * np.pi / 3, 241): base = h(th - phi0) - d for dphi in (-hp, -hp / 2, 0.0, hp / 2, hp): for sx in (-1, 1): for sy in (-1, 1): worst = min(worst, float(np.min(h(th - phi0 - dphi) + sx * hx * np.cos(th) + sy * hy * np.sin(th) - base))) rng, hits = np.random.default_rng(87), 0 for _ in range(samples): phi0 = rng.uniform(0, 2 * np.pi) dphi, tx, ty = rng.uniform(-hp, hp), rng.uniform(-hx, hx), rng.uniform(-hy, hy) hits += bool(np.min(h(th - phi0 - dphi) + tx * np.cos(th) + ty * np.sin(th) - (h(th - phi0) - d)) < 0) return {"worst_deficit_without_rotation_term": worst, "random_placements_exposing": hits, "of": samples} def leaf(base_q, lift_x, hb, hl, rng, samples=120): """one lift leaf: base box = q +- hb in every coordinate, B7 box = lift_x +- hl. Returns the inner-point lower bounds of the base cores alone and of the common-core hull with B7, and the smallest exact hull over random placements in the product box (neither bound may exceed it).""" R3, R5, R7 = (1 / (2 * math.cos(math.pi / 6)), 1 / (2 * math.cos(math.pi / 10)), 1 / (2 * math.cos(math.pi / 14))) d3 = motion_delta(hb, hb, 0.0, R3) d5 = motion_delta(hb, hb, hb, R5) d7 = motion_delta(hl, hl, hl, R7) V3 = placed_vertices(3, 0.0, base_q[:2]) V5 = placed_vertices(5, base_q[2], base_q[3:5]) V7 = placed_vertices(7, lift_x[0], lift_x[1:3]) cores = [reuleaux_core_points(V, 1 - d) for V, d in ((V3, d3), (V5, d5), (V7, d7))] base = float(ConvexHull(np.vstack([disc_samples(20000)] + cores[:2])).volume) inner = float(ConvexHull(np.vstack([disc_samples(20000)] + cores)).volume) least = math.inf for _ in range(samples): q = np.asarray(base_q) + rng.uniform(-hb, hb, 5) x = np.asarray(lift_x) + rng.uniform(-hl, hl, 3) a = hull_pieces(placed_disc() + placed_reuleaux(3, 0.0, q[:2]) + placed_reuleaux(5, q[2], q[3:5]) + placed_reuleaux(7, x[0], x[1:3]), 2048)[0] least = min(least, a) return {"half_widths": [hb, hl], "deltas": [d3, d5, d7], "base_inner_lower": base, "inner_lower": inner, "least_sampled_actual": least, "loss": least - inner} # ---------------------------------------------------------------- checks def x1_paper(w): out, facts, claims = [], w["snapshot"]["mishra_fulltext"]["facts"], w["paper_claims"] for name, val in facts.items(): if val is None: out.append(f"Mishra's full text: {name} not found") if facts.get("thresholds"): found = [float(x) for x in re.findall(r"0\.\d{12}", facts["thresholds"])] for n, claimed in claims["core_thresholds"].items(): if not any(abs(f - claimed) < 5e-13 for f in found): # half a unit of the 12th decimal out.append(f"threshold for B{n}: {claimed} not in Mishra's Remark 24") return out def w1_constants(w): out = [] R7 = 1 / (2 * math.sin(3 * math.pi / 7)) if abs(R7 - w["R7"]) > 5e-13 or abs(R7 - 1 / (2 * math.cos(math.pi / 14))) > 1e-15: out.append(f"R_7 = {R7!r}, claimed {w['R7']}") t7 = t_text(7, d_star(0.835)) if abs(t7 - w["t7"]) > 5e-13: out.append(f"t_7(0.835) = {t7!r}, claimed {w['t7']}") need = 0.835 - 0.834781190917 if abs(need - w["headroom"]) > 5e-13: out.append(f"required increment {need!r}, claimed {w['headroom']}") ratio = (0.836494901 - 0.835) / need if abs(ratio - w["ratio"]) > 5e-3: out.append(f"ratio {ratio:.4f}, claimed {w['ratio']}") for n, claimed in w["core_thresholds"].items(): Rn = 1 / (2 * math.cos(math.pi / (2 * n))) if abs(1 - Rn - claimed) > 5e-13: out.append(f"core threshold 1 - R_{n} = {1 - Rn!r}, claimed {claimed}") w["w1"] = {"R7": R7, "t7": t7, "increment": need, "ratio": ratio} return out def w2_motion(w): """random boxes and placements; d_H measured as the sup of the support difference (sampled, plus the Lipschitz half-step R th-step)""" out, rng, worst = [], np.random.default_rng(81), 0.0 th = 2 * np.pi * np.arange(8192) / 8192 bodies = {n: (reuleaux_support(n), 1 / (2 * math.cos(math.pi / (2 * n)))) for n in (3, 5, 7)} for k in range(4): coeffs = {3: tuple(rng.uniform(-0.2, 0.2, 2)), 5: tuple(rng.uniform(-0.06, 0.06, 2))} hK = body(coeffs) RK = float(np.max(np.sqrt(hK(th) ** 2 + np.gradient(hK(th), th[1] - th[0]) ** 2))) + 1e-6 bodies[f"fourier-{k}"] = (hK, RK) for name, (hK, RK) in bodies.items(): for _ in range(40): hx, hy, hp = rng.uniform(0, 0.02, 3) phi0, t0 = rng.uniform(0, 2 * np.pi), rng.uniform(-0.1, 0.1, 2) delta = w["motion"](hx, hy, hp, RK) for _ in range(5): phi = phi0 + rng.uniform(-hp, hp) t = t0 + np.array([rng.uniform(-hx, hx), rng.uniform(-hy, hy)]) h0 = hK(th - phi0) + t0[0] * np.cos(th) + t0[1] * np.sin(th) h1 = hK(th - phi) + t[0] * np.cos(th) + t[1] * np.sin(th) d = float(np.max(np.abs(h1 - h0))) worst = max(worst, d / max(delta, 1e-15)) if d > delta + 1e-12: out.append(f"{name}: d_H {d:.6e} > delta {delta:.6e}") break w["w2"] = {"largest_dH_over_delta": worst} return out def w3_cores(w): out, rng = [], np.random.default_rng(83) for n in (3, 5, 7): Rn = 1 / (2 * math.cos(math.pi / (2 * n))) for _ in range(30): hx, hy, hp = rng.uniform(0, 0.03, 3) delta = w["motion"](hx, hy, hp, Rn) phi0, t0 = rng.uniform(0, 2 * np.pi), rng.uniform(-0.1, 0.1, 2) V0 = placed_vertices(n, phi0, t0) C = reuleaux_core_points(V0, w["core_radius"](delta), 1500) # C + delta B inside K0: every core point, pushed delta in any direction, is within 1 of every corner if len(C) and np.max(np.linalg.norm(C[:, None, :] - V0[None, :, :], axis=2)) > 1 - delta + 1e-12: out.append(f"B{n}: a core point is farther than 1 - delta from a corner") break for _ in range(5): V = placed_vertices(n, phi0 + rng.uniform(-hp, hp), t0 + np.array([rng.uniform(-hx, hx), rng.uniform(-hy, hy)])) if len(C) and np.max(np.linalg.norm(C[:, None, :] - V[None, :, :], axis=2)) > 1 + 1e-12: out.append(f"B{n}: a core point leaves a placement in its box") break # the core empties exactly at delta = 1 - R_n V0 = placed_vertices(n, 0.0, (0, 0)) if core_is_empty(V0, Rn + 1e-9) or not core_is_empty(V0, Rn - 1e-9): out.append(f"B{n}: the core does not empty at 1 - delta = R_n") # the package's analytic body: h = 1/2 + 0.02 cos 3t, curvature >= 0.34; the core h - delta hK = lambda t: 0.5 + 0.02 * np.cos(3 * t) th = 2 * np.pi * np.arange(8192) / 8192 RK = float(np.max(np.sqrt(hK(th) ** 2 + (0.06 * np.sin(3 * th)) ** 2))) worst_gap = math.inf for _ in range(300): hx, hy, hp = rng.uniform(0, 0.003, 3) delta = w["motion"](hx, hy, hp, RK) if 0.34 - delta <= 0: out.append("the analytic core loses convexity") break phi0, t0 = rng.uniform(0, 2 * np.pi), rng.uniform(-0.1, 0.1, 2) phi, t = phi0 + rng.uniform(-hp, hp), t0 + np.array([rng.uniform(-hx, hx), rng.uniform(-hy, hy)]) hC = hK(th - phi0) + t0[0] * np.cos(th) + t0[1] * np.sin(th) - delta hg = hK(th - phi) + t[0] * np.cos(th) + t[1] * np.sin(th) worst_gap = min(worst_gap, float(np.min(hg - hC))) if np.min(hg - hC) < -1e-12: out.append("the analytic core pokes out of a placement") break w["w3"] = {"analytic_core_min_support_gap": worst_gap, "R_K_analytic": RK} return out _LEAVES = {} _S1 = {} def _s1(): if not _S1: _S1.update(s1_exposure(*S1_BOX)) return _S1 def w4_leaves(w): """the seed with B7 at its best lift (RUN-010), and the four-body optimum (RUN-010), at box half-widths 1e-4 and 1e-3: the inner-point bound must stay below every sampled actual hull; whether the base cores alone reach 0.835 (base-pruned) and whether the lift does (lift-closed) are recorded.""" out = [] r7 = w["run010"] seed_q, seed_x = w["round07"]["repository"]["reuleaux"]["placement"], r7["w3"]["rows"]["7"]["placement"] four = r7["w4"]["placement"] cases = {"seed + best B7": (seed_q, seed_x), "four-body optimum": (four[:5], four[5:8])} rows = {} for name, (q, x) in cases.items(): for h in (1e-4, 1e-3): key = (name, h) if key not in _LEAVES: _LEAVES[key] = leaf(q, x, h, h, np.random.default_rng(int(h * 1e6))) r = _LEAVES[key] rows[f"{name} @ {h:g}"] = r if max(r["inner_lower"], r["base_inner_lower"]) > r["least_sampled_actual"] + 1e-12: out.append(f"{name} @ {h:g}: the core bound {r['inner_lower']:.9f} exceeds an actual hull " f"{r['least_sampled_actual']:.9f}") pruned = {k: v["base_inner_lower"] >= w["target"] for k, v in rows.items()} if pruned != w["base_pruned"]: out.append(f"base pruning {pruned} differs from the recorded {w['base_pruned']}") closes = {k: v["inner_lower"] >= w["target"] for k, v in rows.items()} if closes != w["leaf_closures"]: out.append(f"leaf closures {closes} differ from the recorded {w['leaf_closures']}") w["w4"] = {"rows": rows, "base_pruned_at_0.835": pruned, "closes_at_0.835": closes} return out def w5_trees(w): out, rng = [], np.random.default_rng(85) for _ in range(200): S = int(rng.integers(1, 6)) leaves, nodes = S, S # each seed starts as a leaf for _ in range(int(rng.integers(0, 60))): leaves += 1 # splitting a leaf: one leaf becomes two nodes += 2 if nodes != w["tree_identity"](leaves, S): out.append(f"a forest of {S} seeds with {leaves} leaves has {nodes} nodes") break return out def p1_package(w): out, v, spec, schema = [], w["validation"]["sanity"], w["spec"], w["schema"] R7 = 1 / (2 * math.sin(3 * math.pi / 7)) t7, t3, t5 = (t_text(n, d_star(0.835)) for n in (7, 3, 5)) if abs(v["B7_root"]["R7"] - R7) > 1e-15 or abs(v["B7_root"]["tmax_at_0_835"] - t7) > 1e-13 \ or abs(v["B7_root"]["rotation_period"] - 2 * math.pi / 7) > 1e-15: out.append("the recorded B7 root differs") hd = v["headroom"] if abs(hd["required_increment"] - (0.835 - 0.834781190917)) > 1e-15 \ or abs(hd["search_headroom_above_target"] - (0.836494901 - 0.835)) > 1e-15: out.append("the recorded headroom differs") g = v["generic_common_core"] if abs(g["core_curvature_min"] - (g["original_curvature_min"] - g["delta"])) > 1e-12 or g["violations"] != 0: out.append("the recorded generic core is inconsistent") if abs(motion_delta(*S1_BOX, S1_RK) - g["delta"]) > 1e-15: out.append("S1's box does not reproduce the recorded delta") pw = spec["primary_witness"] if (spec["target"] != w["target"] or abs(pw["rotation_radius"] - R7) > 1e-15 or abs(pw["translation_radius"] - t7) > 1e-13 or abs(pw["phi"][1] - 2 * math.pi / 7) > 1e-15 or abs(spec["base_root"]["translation_radius_R3"] - t3) > 1e-13 or abs(spec["base_root"]["translation_radius_R5"] - t5) > 1e-13 or pw["core_provider"] != "REULEAUX-EROSION"): out.append("the compute spec disagrees with the text") if spec["fallback_pool"][:3] != ["Reuleaux11", "Reuleaux13", "Reuleaux9"]: out.append("the fallback order differs from sec. 29") if schema["properties"]["magic"]["const"] != "LUCFC08": out.append("the schema's magic is not sec. 17's LUCFC08") providers = schema["properties"]["witness_catalog"]["items"]["properties"]["core_provider_type"]["enum"] if sorted(providers) != sorted(["REULEAUX-EROSION", "ANALYTIC-SUPPORT-CORE", "CERTIFIED-SUPPORT-CORE"]): out.append("the schema's core providers are not sec. 14's") # sec. 14 lists the fields a witness record must carry; the schema requires only some required = set(schema["properties"]["witness_catalog"]["items"]["required"]) missing = sorted(set(w["sec14_fields"]) - required - {"support_or_geometry_hash"}) if missing != sorted(w["schema_missing"]): out.append(f"the schema leaves out {missing}, recorded {sorted(w['schema_missing'])}") w["p1"] = {"schema_missing_sec14_fields": missing, "s1": _s1()} return out def p2_package(w): out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]} v = w["validation"] for rec, leaf_id, text in ((v["round08"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"])): _, size, digest = leaves[leaf_id] if rec["sha256"] != digest or rec["bytes"] != size: out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive") n = text.count("$$") if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0): out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}") if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)): out.append(f"{rec['file']}: unicode-escape flag differs") if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)): out.append(f"{rec['file']}: bracket-delimiter flag differs") for key, leaf_id in (("schema_sha256", SCHEMA), ("compute_spec_sha256", SPEC), ("verifier_skeleton_sha256", SKELETON)): if v[key] != leaves[leaf_id][2]: out.append(f"{key}: recorded digest differs from the archive") return out # ---------------------------------------------------------------- registry (Round 08) TOKEN = "a grammar token or label of sec. 10-17, 24 or 31, defined there; not a judgment" R08_DEFINITIONS = { "NOT YET CERTIFIED": ("contextual", "sec. 36: open, and the certificate that would settle it is specified"), "SPECIFIED": ("contextual", "sec. 36: written down as a grammar or a list of invariants; nothing is implemented"), "SPLIT": ("in-line", "sec. 10-11 token: an internal node of the base or lift tree"), "ANALYTIC-SUPPORT-CORE": ("in-line", "sec. 3 core provider: h_K - delta is itself a legal support function"), "B7-CELL-COUNTEREXAMPLE": ("in-line", "sec. 24: an explicit placement whose rigorous outer hull is below T"), "B7-NOT-YET-CERTIFIED": ("in-line", "sec. 24: no lower certificate yet, and no counterexample either"), "CERTIFIED-SUPPORT-CORE": ("in-line", "sec. 3, 25 core provider: any core with a finite certificate of h_C + delta <= h_K"), "FIXED": ("contextual", "sec. 36: a constant determined and written down (B7's root)"), "NOT PROOF PATH": ("in-line", "sec. 31: an implementation function whose proof obligation is unmet"), "PROVED AS CERTIFICATE INTERFACE": ("contextual", "sec. 36: the interface is shown sound for any core that meets it"), "PRUNED": ("in-line", "sec. 11 token: a lift leaf whose inner hull clears T"), "REULEAUX-EROSION": ("in-line", "sec. 3 core provider: the discs about the corners shrunk to 1 - delta"), "UNRESOLVED": ("in-line", "sec. 10, 21: a leaf with no certificate; forbidden in a final certificate"), } PBCT = "PASS by cited theorem" R08_REVIEWS = [ ("PROVED", "Generic convex motion bound", "analytic", "PASS", "sec. 1 = Mishra's Lemma 22; W2"), ("PROVED", "General common-core theorem", "analytic", "PASS", "Thm 2.1: support functions; W3"), ("PROVED", "Reuleaux erosion as specialization", "analytic", "PASS", "sec. 4 = Mishra's Lemma 21; W3"), ("PROVED", "Nested base/lift soundness", "analytic", "PASS", "Thm 12.1; needs the a-priori root bound for placements outside the roots (Round 07)"), ("PROVED AS CERTIFICATE INTERFACE", "Generic Fourier/asymmetric witness interface", "analytic", "PASS", "Thm 2.1 holds in each reflection branch; a chiral witness's root must carry both branches (see the invariants)"), ("PASS", "General common-core sanity", "computation", "PASS", "rebuilt (W3, P1)"), ("CLOSED", "CONDITIONAL-LIFT CERTIFICATE COMPILER", "reading", "PASS", "closed as a grammar; nothing is run"), ("CLOSED", "GENERIC CONVEX COMMON-CORE INTERFACE", "analytic", "PASS", "Thm 2.1"), ("COMPUTE-DEFERRED", "37. 最短交接結論", "n/a", "n/a", ""), ("FIXED", "B7 $0.8350$ root domain", "computation", "PASS", "W1"), ("SPECIFIED", "Certificate grammar", "reading", "PASS", "sec. 10-11, 17"), ("SPECIFIED", "Independent verifier invariants", "reading", "PARTIAL", "V1-V10 sound (V8 = Mishra's forest identity, W5), but V3 states the witness root for B7 only: for a chiral " "fallback witness the reflection branch must be in the root, and neither V3 nor the package's schema requires " "it (sec. 14's record lists reflection_symmetry; the schema leaves it and four other fields out, P1)"), ("NOT YET CERTIFIED", "$0.8350$ lower bound", "n/a", "n/a", "two live leaves close at box half-width 1e-4 (W4)"), ("LIFT-CLOSED", "", "n/a", "n/a", TOKEN), ("LIFT-CLOSED", "", "n/a", "n/a", TOKEN), ("LIFT-CLOSED", "11. Lift tree grammar", "n/a", "n/a", TOKEN), ("LIFT-CLOSED", "證明", "n/a", "n/a", TOKEN), ("BASE-PRUNED", "", "n/a", "n/a", TOKEN), ("BASE-PRUNED", "", "n/a", "n/a", TOKEN), ("SPLIT", "", "n/a", "n/a", TOKEN), ("SPLIT", "", "n/a", "n/a", TOKEN), ("PRUNED", "", "n/a", "n/a", TOKEN), ("UNRESOLVED", "`LIFT-CLOSED`", "n/a", "n/a", TOKEN), ("ANALYTIC-SUPPORT-CORE", "", "n/a", "n/a", TOKEN), ("CERTIFIED-SUPPORT-CORE", "", "n/a", "n/a", TOKEN), ("REULEAUX-EROSION", "", "n/a", "n/a", TOKEN), ("B7-CELL-COUNTEREXAMPLE", "24. Certified negative result for one witness", "n/a", "n/a", TOKEN), ("B7-NOT-YET-CERTIFIED", "24. Certified negative result for one witness", "n/a", "n/a", TOKEN), ("NOT PROOF PATH", "`root_domain(K,T)`", "n/a", "n/a", TOKEN), ] def r1_registry(w): return registry.completeness(w["registry"], "R08", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "A1": gate.citations_check(CITE_OPTS), "X1": x1_paper, "W1": w1_constants, "W2": w2_motion, "W3": w3_cores, "W4": w4_leaves, "W5": w5_trees, "P1": p1_package, "P2": p2_package, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "A1": {"text", "snapshot"}, "X1": {"snapshot", "paper_claims"}, "W1": {"R7", "t7", "headroom", "ratio", "core_thresholds"}, "W2": {"motion"}, "W3": {"motion", "core_radius"}, "W4": {"run010", "round07", "target", "base_pruned", "leaf_closures"}, "W5": {"tree_identity"}, "P1": {"validation", "spec", "schema", "target", "sec14_fields", "schema_missing"}, "P2": {"validation", "text", "crystal", "manifest"}, "R1": {"registry", "definitions", "reviews"}} SEC14 = ["witness_id", "representation_type", "diameter", "constant_width_status", "centering_gauge", "symmetry_period", "reflection_symmetry", "rotation_radius_bound", "translation_domain_rule", "core_provider_type", "support_or_geometry_hash"] CLAIMS = { "R7": 0.512858431636, "t7": 0.196935046771, "headroom": 0.000218809083, "ratio": 6.83, "core_thresholds": {3: 0.422649730810, 5: 0.474268887881, 7: 0.487141568364}, "motion": motion_delta, "core_radius": lambda delta: 1 - delta, "target": 0.835, "base_pruned": {"seed + best B7 @ 0.0001": False, "seed + best B7 @ 0.001": False, "four-body optimum @ 0.0001": False, "four-body optimum @ 0.001": False}, "leaf_closures": {"seed + best B7 @ 0.0001": True, "seed + best B7 @ 0.001": False, "four-body optimum @ 0.0001": True, "four-body optimum @ 0.001": False}, "tree_identity": lambda L, S: 2 * L - S, "paper_claims": {"core_thresholds": {3: 0.422649730810, 5: 0.474268887881}}, "sec14_fields": SEC14, "schema_missing": ["centering_gauge", "constant_width_status", "reflection_symmetry", "rotation_radius_bound", "translation_domain_rule"], } def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, VALIDATION, SPEC, SCHEMA} got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} return (got[DOC].decode("utf-8"), got[CRYSTAL].decode("utf-8"), json.loads(got[VALIDATION]), json.loads(got[SPEC]), json.loads(got[SCHEMA]), json.loads(MANIFEST.read_text(encoding="utf-8"))) def main(): ap = argparse.ArgumentParser() ap.add_argument("--refresh", action="store_true") ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() if args.refresh: recs = {str(n): (gate.fetch_arxiv(r["id"]) if r["kind"] == "arxiv" else gate.fetch_crossref(doi=r["doi"])) for n, r in REFS.items()} SNAPSHOT.write_text(json.dumps({"retrieved": datetime.date.today().isoformat(), "records": recs, "mishra_fulltext": gate.fetch_arxiv_facts(REFS[1]["id"], 2, MISHRA_FACTS, strip_invisible=True)}, ensure_ascii=False, indent=1) + "\n", encoding="utf-8") snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8")) round07 = json.loads(ROUND07.read_text(encoding="utf-8")) run010 = json.loads(RUN010.read_text(encoding="utf-8")) text, crystal, validation, spec, schema, manifest = load_inputs() def build(): return {"text": text, "crystal": crystal, "validation": json.loads(json.dumps(validation)), "spec": json.loads(json.dumps(spec)), "schema": json.loads(json.dumps(schema)), "manifest": manifest, "snapshot": json.loads(json.dumps(snapshot)), "round07": round07, "run010": run010, "registry": registry.load(), "definitions": dict(R08_DEFINITIONS), "reviews": list(R08_REVIEWS), **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", "p1"): print(key, w.get(key)) if not args.drill: return pc, lc, bp, spec_pw = CLAIMS["paper_claims"], CLAIMS["leaf_closures"], CLAIMS["base_pruned"], spec["primary_witness"] gc = validation["sanity"]["generic_common_core"] cases = [ ("K0-unmodified", "control", {}, set()), ("K1-motion-by-double-angle", "control", {"motion": lambda hx, hy, hp, RK: math.hypot(hx, hy) + 4 * RK * math.sin(hp / 4) * math.cos(hp / 4)}, set()), ("K2-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K3-tree-identity-rewritten", "control", {"tree_identity": lambda L, S: L + (L - S)}, set()), ("M1-doc-t7-digit", "mutation", {"text": text.replace("0.196935046771", "0.196935046772")}, {"A0"}), ("M2-ref-year", "mutation", {"snapshot": {**snapshot, "records": { **snapshot["records"], "3": {**snapshot["records"]["3"], "years": [2019]}}}}, {"A1"}), ("M3-threshold-misquoted", "mutation", {"paper_claims": {**pc, "core_thresholds": {**pc["core_thresholds"], 3: 0.422649730811}}}, {"X1"}), ("M4-R7-digit", "mutation", {"R7": 0.512858431637}, {"W1"}), ("M5-t7-digit", "mutation", {"t7": 0.196935046772}, {"W1"}), ("M6-ratio", "mutation", {"ratio": 6.93}, {"W1"}), ("M7-motion-without-rotation", "mutation", {"motion": lambda hx, hy, hp, RK: math.hypot(hx, hy)}, {"W2", "W3"}), ("M8-core-eroded-by-half", "mutation", {"core_radius": lambda delta: 1 - delta / 2}, {"W3"}), ("M9-coarse-leaf-claimed-closed", "mutation", {"leaf_closures": {**lc, "seed + best B7 @ 0.001": True}}, {"W4"}), ("M15-hard-cell-claimed-base-pruned", "mutation", {"base_pruned": {**bp, "four-body optimum @ 0.0001": True}}, {"W4"}), ("M10-tree-single-root", "mutation", {"tree_identity": lambda L, S: 2 * L - 1}, {"W5"}), ("M11-spec-t7", "mutation", {"spec": {**spec, "primary_witness": {**spec_pw, "translation_radius": 0.197}}}, {"P1"}), ("M12-reflection-field-assumed", "mutation", {"schema_missing": [f for f in CLAIMS["schema_missing"] if f != "reflection_symmetry"]}, {"P1"}), ("M13-schema-digest", "mutation", {"validation": {**validation, "schema_sha256": "0" * 64}}, {"P2"}), ("M16-sanity-delta-shifted", "mutation", {"validation": {**validation, "sanity": { **validation["sanity"], "generic_common_core": {**gc, "delta": gc["delta"] + 1e-6, "core_curvature_min": gc["core_curvature_min"] - 1e-6}}}}, {"P1"}), ("M14-review-dropped", "mutation", {"reviews": list(R08_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-011", "subject": "Round 08: the conditional-lift certificate compiler", "document": DOC, "snapshot_retrieved": snapshot["retrieved"], "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "p1")}, "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("R08", "RUN-011", R08_DEFINITIONS, R08_REVIEWS) print(f"registry: {len(R08_DEFINITIONS)} definitions, {len(R08_REVIEWS)} reviews recorded for R08") if __name__ == "__main__": main()