"""RUN-004 - Round 01: the reduction chain and the placement compiler. Round 01 compresses the target family of the Lebesgue problem along A -> closed convex hull -> unit constant-width body W -> h_W -> r_W = h_W + h_W'' and sets up the placement compiler (support containment under O(2), directed Hausdorff slack, at most three active directions for a fixed orientation). Its theorems are read line by line in the report. What is finite or symbolic is recomputed here, each claim pinned to Round 01's own bytes by an anchor. Checks A0 anchors every formula checked below occurs in Round 01 as written A1 citations Round 01's external references exist and match (arXiv / Crossref snapshot) S1 fourier-parity (sec. 9) h(t)+h(t+pi)=1 <=> a0=1/2 and every even mode vanishes S2 steiner-point (sec. 9) (1/pi) int h u dt = (a1, b1) S3 translation (sec. 8, 12) t.u_t cancels antipodally and is killed by D^2+1 S4 moments (sec. 11) int (h+h'') cos = int (h+h'') sin = 0 S5 inversion (sec. 13) the stated h solves h + h'' = r, mode by mode S6 width-ode (sec. 12) w''+w=1: general solution 1+A cos+B sin; pi-periodic forces w = 1 S7 sanity-family (sec. 14) r_a = 1/2 - 8a cos 3t, and 0 <= r_a <= 1 <=> |a| <= 1/16 S8 truncation (sec. 30) odd truncation can break convexity - witness: the Reuleaux triangle cut at n = 3 has min r = 1/2 - 2/pi < 0 N1 reconstruction (sec. 12, numerical) the Reuleaux triangle rebuilt from r alone, through the sec. 13 inversion, matches its geometric support function once centred at its Steiner point Usage: python code/run004_round01_reduction_chain.py [--refresh] [--drill] [--blind CID] """ import argparse import copy import datetime import html import json import math import re import urllib.parse import urllib.request import numpy as np import sympy as sp import registry from corpus import SOURCES, TREE, source_bytes, walk_sources ROUND01 = "main.zip!/AMRAL_LUC_FC_Round_01_Package_v0.1.zip!/AMRAL_Lebesgue_Finite_Closure_Round_01_Support_ConstantWidth_v0.1.md" SNAPSHOT = TREE / "data" / "external" / "round01-citations.json" LOG = TREE / "data" / "gate-logs" / "run004-round01-reduction-chain.json" TH = sp.Symbol("theta", real=True) ANCHORS = { "S1": [r"h(\theta)+h(\theta+\pi)=1.", r"a_0=\frac12,", r"a_{2m}=b_{2m}=0\qquadm\ge1."], "S2": [r"s(W)=(a_1,b_1)."], "S3": [r"t\cdotu_{\theta+\pi}=-t\cdotu_\theta", r"(D^2+1)\cos\theta=0,"], "S4": [r"\int_0^{2\pi}r(\theta)\cos\theta\,d\theta=0,", r"\int_0^{2\pi}r(\theta)\sin\theta\,d\theta=0."], "S5": [r"\frac{\alpha_n}{1-n^2}\cosn\theta+\frac{\beta_n}{1-n^2}\sinn\theta"], "S6": [r"w(\theta)=1+A\cos\theta+B\sin\theta.", r"但$\pi$週期要求：$$A=B=0.$$"], "S7": [r"h_a(\theta)=\frac12+a\cos3\theta.", r"r_a(\theta)=h_a+h_a''=\frac12-8a\cos3\theta.", r"|a|\le\frac1{16}.", r"r_a(\theta)=\frac12-\frac12\cos3\theta\in[0,1]."], "S8": [r"\text{oddFouriertruncationpreserveswidthbutmayviolateconvexity}"], } # Round 01's external references, as it lists them (its section "參考文獻"); # internal drafts and Round 00 are not externally checkable and are left out. REFS = { 1: {"kind": "arxiv", "id": "1502.01251", "query": None}, 2: {"kind": "arxiv", "id": "1810.10089", "query": None}, 3: {"kind": "arxiv", "id": "2608.30538", "query": None}, 4: {"kind": "arxiv", "id": "2609.01284", "query": None}, 5: {"kind": "crossref", "query": "He Martini Wu Complete sets in normed linear spaces Banach Journal of Mathematical Analysis"}, 6: {"kind": "crossref", "query": "Hynd On Extreme Constant Width Bodies Discrete Computational Geometry"}, 7: {"kind": "crossref", "query": "Thale A note on a problem posed by Linderholm Journal of Geometry"}, 8: {"kind": "crossref", "query": "Martinez-Maure Noncircular algebraic curves of constant width an answer to Rabinowitz"}, } REF_LINE = re.compile(r"^(\d+)\.\s+(.+?),\s+\*(.+?)\*,\s+(.+?)\.\s*$", re.M) # ---------------------------------------------------------------- snapshot def _get(url, accept): req = urllib.request.Request(url, headers={"User-Agent": "amral-verification (research)", "Accept": accept}) return urllib.request.urlopen(req, timeout=60).read() def fetch_snapshot(): out = {"retrieved": datetime.date.today().isoformat(), "records": {}} for n, ref in REFS.items(): if ref["kind"] == "arxiv": page = _get(f"https://arxiv.org/abs/{ref['id']}", "text/html").decode("utf-8", "replace") meta = lambda k: [html.unescape(x) for x in re.findall(rf']+>", " ", re.search(r"Submission history(.*?)", page, re.S).group(1))) v1 = re.search(r"\[v1\]\s*\w{3}, (\d{1,2} \w{3} \d{4})", history).group(1) out["records"][str(n)] = { "source": "arxiv", "id": ref["id"], "title": meta("citation_title")[0], "families": [a.split(",")[0].strip() for a in meta("citation_author")], "years": [datetime.datetime.strptime(v1, "%d %b %Y").year], } else: q = urllib.parse.quote(ref["query"]) hit = json.loads(_get(f"https://api.crossref.org/works?query.bibliographic={q}&rows=1", "application/json")) doi = hit["message"]["items"][0]["DOI"] rec = json.loads(_get(f"https://api.crossref.org/works/{urllib.parse.quote(doi)}", "application/json"))["message"] years = sorted({rec[k]["date-parts"][0][0] for k in ("issued", "published-print", "published-online") if k in rec}) out["records"][str(n)] = { "source": "crossref", "query": ref["query"], "doi": doi, "title": (rec.get("title") or [""])[0], "families": [a.get("family", "") for a in rec.get("author", [])], "container": (rec.get("container-title") or [""])[0], "volume": rec.get("volume"), "issue": rec.get("issue"), "article_number": rec.get("article-number"), "page": rec.get("page"), "years": years, } return out # ---------------------------------------------------------------- A checks def squash(s): return re.sub(r"\s+", "", s) def a0_anchors(w): text = squash(w["text"]) return [f"{cid}: anchor not found: {a[:50]}" for cid, anchors in ANCHORS.items() for a in anchors if a not in text] def norm_title(s): s = html.unescape(s).lower().replace("\u2019", "'") s = re.sub(r"\\mathbb\s*\{?\s*([a-z])\s*\}?", r"\1", s) return re.sub(r"[^a-z0-9]", "", s) def parse_refs(text): out = {} for n, authors, title, rest in REF_LINE.findall(text.replace("\r\n", "\n")): fam = [re.sub(r"^(?:[A-Z]\.\s*)+", "", a.strip()).strip() for a in re.split(r",\s*|\s+and\s+", authors) if a.strip()] out[int(n)] = {"families": fam, "title": title, "rest": rest} return out def a1_citations(w): failures, refs, recs = [], parse_refs(w["text"]), w["snapshot"]["records"] for n in REFS: ref, rec = refs.get(n), recs.get(str(n)) if ref is None: failures.append(f"ref {n}: not found in Round 01") continue if rec is None: failures.append(f"ref {n}: no external record") continue if norm_title(ref["title"]) != norm_title(rec["title"]): failures.append(f"ref {n}: title differs") if [f.lower() for f in ref["families"]] != [f.lower() for f in rec["families"]]: failures.append(f"ref {n}: authors {ref['families']} vs {rec['families']}") year = int(re.findall(r"(\d{4})$", ref["rest"])[0]) if year not in rec["years"]: failures.append(f"ref {n}: year {year} not in {rec['years']}") if rec["source"] == "arxiv": if f"arXiv:{rec['id']}" not in ref["rest"]: failures.append(f"ref {n}: arXiv id differs") continue venue = ref["rest"].rsplit(",", 1)[0] if norm_title(rec["container"]) not in norm_title(venue): failures.append(f"ref {n}: venue {venue!r} vs {rec['container']!r}") vol = re.search(r"\s(\d+)(?:\((\d+)\))?(?:,|$)", venue) if vol: if vol.group(1) != str(rec["volume"]): failures.append(f"ref {n}: volume {vol.group(1)} vs {rec['volume']}") if vol.group(2) and vol.group(2) != str(rec["issue"]): failures.append(f"ref {n}: issue {vol.group(2)} vs {rec['issue']}") art = re.search(r",\s*(?:article\s+)?(\d+)\s*$", venue) if art and str(rec.get("article_number")) != art.group(1): failures.append(f"ref {n}: article {art.group(1)} vs {rec.get('article_number')}") return failures # ---------------------------------------------------------------- S checks def trig_coeffs(expr, N): """constant, {n: (cos coeff, sin coeff)} of a trig polynomial of degree <= N.""" C = sp.symbols(f"C0:{N + 1}") S = sp.symbols(f"S0:{N + 1}") e = sp.expand(expr) rep = {} for n in range(1, N + 1): rep[sp.cos(n * TH)] = C[n] rep[sp.sin(n * TH)] = S[n] e = sp.expand(e.xreplace(rep)) const = e.subs({**{C[n]: 0 for n in range(1, N + 1)}, **{S[n]: 0 for n in range(1, N + 1)}}) return sp.simplify(const), {n: (sp.simplify(e.coeff(C[n])), sp.simplify(e.coeff(S[n]))) for n in range(1, N + 1)} def s1_fourier_parity(w): N = 8 a = sp.symbols(f"a0:{N + 1}") b = sp.symbols(f"b0:{N + 1}") h = a[0] + sum(a[n] * sp.cos(n * TH) + b[n] * sp.sin(n * TH) for n in range(1, N + 1)) const, modes = trig_coeffs(h + h.subs(TH, TH + sp.pi) - 1, N) eqs = [const] + [c for n in modes for c in modes[n] if c != 0] sol = sp.solve(eqs, list(a) + list(b[1:]), dict=True) if len(sol) != 1: return [f"parity system has {len(sol)} solutions"] got = {k: v for k, v in sol[0].items()} claimed = w["parity_claim"](a, b, N) return [] if got == claimed else [f"solution {got} != claimed {claimed}"] def s2_steiner_point(w): N = 5 a = sp.symbols(f"a0:{N + 1}") b = sp.symbols(f"b0:{N + 1}") h = a[0] + sum(a[n] * sp.cos(n * TH) + b[n] * sp.sin(n * TH) for n in range(1, N + 1)) sx = sp.integrate(h * sp.cos(TH), (TH, 0, 2 * sp.pi)) / sp.pi sy = sp.integrate(h * sp.sin(TH), (TH, 0, 2 * sp.pi)) / sp.pi cx, cy = w["steiner_claim"](a, b) return [] if sp.simplify(sx - cx) == 0 and sp.simplify(sy - cy) == 0 else [f"Steiner point is ({sx}, {sy})"] def s3_translation(w): t1, t2 = sp.symbols("t1 t2", real=True) tu = t1 * sp.cos(TH) + t2 * sp.sin(TH) out = [] if sp.simplify(tu + w["antipodal_claim"](t1, t2)) != 0: out.append("t.u_{theta+pi} is not the claimed value") if sp.simplify(sp.diff(tu, TH, 2) + tu) != 0: out.append("(D^2+1) does not annihilate t.u_theta") return out def s4_moments(w): N = 6 a = sp.symbols(f"a0:{N + 1}") b = sp.symbols(f"b0:{N + 1}") h = a[0] + sum(a[n] * sp.cos(n * TH) + b[n] * sp.sin(n * TH) for n in range(1, N + 1)) r = h + sp.diff(h, TH, 2) out = [] for f in w["moment_weights"]: val = sp.simplify(sp.integrate(r * f, (TH, 0, 2 * sp.pi))) if val != 0: out.append(f"int r*{f} = {val}") return out def s5_inversion(w): odd = [3, 5, 7, 9, 11] al = {n: sp.Symbol(f"alpha{n}") for n in odd} be = {n: sp.Symbol(f"beta{n}") for n in odd} r = sp.Rational(1, 2) + sum(al[n] * sp.cos(n * TH) + be[n] * sp.sin(n * TH) for n in odd) h = sp.Rational(1, 2) + sum(w["inversion"](n) * (al[n] * sp.cos(n * TH) + be[n] * sp.sin(n * TH)) for n in odd) return [] if sp.simplify(h + sp.diff(h, TH, 2) - r) == 0 else ["h + h'' != r"] def s6_width_ode(w): out = [] W = sp.Function("w") general = sp.dsolve(sp.Derivative(W(TH), TH, 2) + W(TH) - 1).rhs A, B = sp.symbols("A B") claimed = w["width_general"](A, B) # the claimed family must solve the ODE for all A, B, and span the same solutions if sp.simplify(sp.diff(claimed, TH, 2) + claimed - 1) != 0: out.append("claimed general solution does not solve w''+w=1") consts = sorted(general.free_symbols - {TH}, key=str) if sp.simplify(general.subs(dict(zip(consts, [0] * len(consts)))) - claimed.subs({A: 0, B: 0})) != 0: out.append("particular solutions differ") per = sp.expand(sp.expand_trig(claimed.subs(TH, TH + sp.pi) - claimed)) forced = sp.solve([per.coeff(sp.cos(TH)), per.coeff(sp.sin(TH))], [A, B], dict=True) if forced != [{A: 0, B: 0}]: out.append(f"pi-periodicity forces {forced}, not A = B = 0") return out def s7_sanity_family(w): a = sp.Symbol("a", real=True) h = sp.Rational(1, 2) + a * sp.cos(3 * TH) r = sp.simplify(h + sp.diff(h, TH, 2)) out = [] if sp.simplify(r - w["sanity_r"](a)) != 0: out.append(f"r_a = {r}") # r = 1/2 + k cos 3t with k linear in a: its range is [1/2-|k|, 1/2+|k|] k = sp.simplify(r.coeff(sp.cos(3 * TH))) bound = sp.solve(sp.Eq(sp.Abs(k.subs(a, sp.Symbol("x", positive=True))), sp.Rational(1, 2)), sp.Symbol("x", positive=True)) if bound != [w["sanity_bound"]]: out.append(f"exact bound |a| <= {bound}, claimed {w['sanity_bound']}") end = sp.simplify(r.subs(a, w["sanity_bound"])) if sp.simplify(end - (sp.Rational(1, 2) - sp.Rational(1, 2) * sp.cos(3 * TH))) != 0: out.append(f"endpoint curvature {end}") return out def reuleaux_r_intervals(phase): return [(phase + 2 * k * sp.pi / 3, phase + 2 * k * sp.pi / 3 + sp.pi / 3) for k in range(3)] def s8_truncation(w): """Existential claim: some odd truncation of a legal r leaves [0, 1]. Witness body from the world (the Reuleaux triangle by default).""" body = w["truncation_body"] n = 3 if body == "disc": alpha = beta = sp.Integer(0) else: iv = reuleaux_r_intervals(body) alpha = sum(sp.integrate(sp.cos(n * TH), (TH, lo, hi)) for lo, hi in iv) / sp.pi beta = sum(sp.integrate(sp.sin(n * TH), (TH, lo, hi)) for lo, hi in iv) / sp.pi amp = sp.sqrt(sp.simplify(alpha ** 2 + beta ** 2)) low = sp.Rational(1, 2) - amp w["s8_witness"] = {"n3_amplitude": str(amp), "min_r3": str(low), "min_r3_float": float(low)} return [] if low.is_negative else [f"truncation at n=3 stays in [0,1] (min {low})"] # ---------------------------------------------------------------- N1 def reuleaux_support(thetas, geometry): V = np.array([[0.0, 0.0], [1.0, 0.0], [0.5, math.sqrt(3) / 2]]) c = V.mean(axis=0) U = np.stack([np.cos(thetas), np.sin(thetas)], axis=1) h = (V @ U.T).max(axis=0) # the vertices if geometry == "reuleaux": for k in range(3): # arc of radius 1 about V[k] i, j = [m for m in range(3) if m != k] lo, hi = sorted(np.arctan2(*(V[m] - V[k])[::-1]) % (2 * np.pi) for m in (i, j)) if hi - lo > np.pi: # the arc's normal range wraps through 0 lo, hi = hi, lo + 2 * np.pi tt = np.where(thetas < lo, thetas + 2 * np.pi, thetas) inside = (tt >= lo) & (tt <= hi) h = np.where(inside, np.maximum(h, U @ V[k] + 1.0), h) return h - U @ c # centred at the centroid def n1_reconstruction(w): thetas = np.linspace(0, 2 * np.pi, 3601) m = np.arange(1, 4002, 2) # odd m <= 4001; modes n = 3m; tail ~1e-9 coef = (2 / (np.pi * m)) * np.array([float(w["inversion"](3 * int(k))) for k in m]) h_f = 0.5 + np.sin(np.outer(thetas, 3 * m)) @ coef h_g = reuleaux_support(thetas, w["geometry"]) err = float(np.max(np.abs(h_f - h_g))) w["n1_max_error"] = err return [] if err < 1e-7 else [f"max |h_fourier - h_geometric| = {err:.3e}"] # ---------------------------------------------------------------- the registry, for Round 01 # phrases Round 01 is the first to use in a judgment position: what it says they mean R01_DEFINITIONS = { "PASS": ("contextual", "used for gates, audits and re-judged older items without a definition; in use: " "the item holds as argued in this round"), "NONE": ("contextual", "no claim of this kind is made"), "SEARCH-ONLY": ("in-line", "sec. 28: an accelerator, never a completeness proof (cf. Round 00 sec. 5.5)"), "NOT ESTABLISHED": ("in-line", "sec. 29: the reduction would need a further lemma, which it names"), "ABSTRACT-PASS": ("in-line", "sec. 18: existence by compactness; explicitly not a constructive certificate"), "REBUILD-PASS": ("inherited", "Round 00 sec. 2 REBUILD (idea kept, proof or scope rebuilt), now passing: " "sec. 4 adds d<1, d=0 and the exact quantifier equivalence"), "COMMON-PLACEMENT / EXTREME-SATURATION LEMMA": ("not-a-status", "the name of the lemma sec. 29 says would be " "needed; the census reads it because it stands alone in backticks"), "FINITE-FAMILY-PASS": ("in-line", "sec. 28 gives only its new role (candidate-cover surgery heuristic + finite " "certificate); the graded item is outside the corpus"), "NEXT GATE": ("contextual", "designated as the next gate"), "PASS / PRIMARY HANDOFF": ("in-line", "sec. 6: the support-function form, upgraded to the primary exact handoff"), "PASS-WITH-SCOPE": ("in-line", "sec. 28: certified sampling for fixed shape/configuration variables only"), "REUSE": ("inherited", "Round 00 sec. 2: reliable enough to serve directly as a shared interface"), "TEST": ("inherited", "Round 00 sec. 2: a high-value conjecture, usable only as a falsifiable hypothesis"), } PBCT = "PASS by cited theorem" R01_REVIEWS = [ # status, subject (as the census records it), known_by, verdict, note ("PASS", "HANDOFF-A", "analytic", "PASS", "Thm 3.1 + Cor 3.2; proof complete"), ("PASS", "TRANSLATION LOCAL FINITE-ACTIVE", "theorem-application", PBCT, "subdifferential of a max of affine maps + Caratheodory; the 'one-active' branch sec. 22 lists is empty"), ("PASS", "Definition audit", "reading", "PASS", ""), ("PASS", "Quantifier audit", "reading", "PASS", "forall A exists g kept throughout"), ("PASS", "Degenerate diameter audit", "reading", "PASS", "Thm 4.1 case 3"), ("PASS", "Diameter $<1$ audit", "analytic", "PASS", "Thm 4.1 case 2 re-derived"), ("PASS", "Reflection audit", "reading", "PASS", "O(2), two components, sigma explicit (sec. 5.2, 23)"), ("PASS", "Translation gauge audit", "analytic", "PASS", "S2, S3"), ("PASS", "Support containment audit", "theorem-application", PBCT, "halfspace representation"), ("PASS", "Shape compactness audit", "theorem-application", PBCT, "Arzela-Ascoli / Blaschke selection"), ("PASS", "Shape finite-net status", "theorem-application", PBCT, "existence only"), ("PASS", "Q1 continuity", "outside-corpus", "PASS", "the draft it grades is outside the corpus; the property as used (Psi 1-Lipschitz in the cover) re-derived here"), ("PASS", "Q2 support function", "theorem-application", PBCT, "= Q2 primary handoff"), ("CLOSED", "SUPPORT-HANDOFF", "theorem-application", PBCT, "Thm 5.1, Thm 5.2, sec. 6"), ("CLOSED", "CONSTANT-WIDTH REDUCTION", "theorem-application", PBCT, "completion theorem; complete <=> constant width in the plane; d<1, d=0 re-derived"), ("CLOSED", "Round 01 status", "reading", "PASS", "every gate listed is closed as argued or honestly open"), ("COMPUTE-DEFERRED", "C03：High-mode adversarial shapes", "n/a", "n/a", "C01-C03 correctly deferred"), ("OPEN", "SHAPE-FINITE-COMPILER", "n/a", "n/a", ""), ("OPEN", "Lebesgue global problem", "n/a", "n/a", ""), ("OPEN", "CONSTRUCTIVE SHAPE CERTIFICATE", "n/a", "n/a", ""), ("OPEN", "GLOBAL PLACEMENT FINITE-BRANCH", "n/a", "n/a", ""), ("OPEN", "Shape finite-net status", "n/a", "n/a", "constructive part"), ("NONE", "Numerical-bound claim", "reading", "PASS", "none claimed"), ("NO", "New numerical lower bound", "reading", "PASS", ""), ("NO", "New numerical upper bound", "reading", "PASS", ""), ("YES", "New exact reduction", "theorem-application", PBCT, "the chain A -> conv -> W -> h -> r"), ("YES", "New canonical shape domain", "analytic", PBCT, "Thm 12.1 re-derived; classical correspondence, new as this program's variable; 0<=r<=1 re-derived " "via W+(-W) = unit disc; rests on the support-function criterion"), ("SEARCH-ONLY", "Q5 predictive $SE(2)$", "outside-corpus", "n/a", "a demotion; no claim"), ("NOT ESTABLISHED", "EXTREME-ONLY REDUCTION", "analytic", "PASS", "the caution is right"), ("ABSTRACT-PASS", "SHAPE-EPSILON-NET", "theorem-application", PBCT, "compactness; sandwich via Thm 16.1"), ("ABSTRACT-PASS", "Q4 missing shape net", "theorem-application", PBCT, "= SHAPE-EPSILON-NET"), ("REBUILD-PASS", "Q3", "theorem-application", PBCT, "= CONSTANT-WIDTH REDUCTION"), ("REBUILD-PASS", "Q3 constant-width reduction", "theorem-application", PBCT, "= CONSTANT-WIDTH REDUCTION"), ("COMMON-PLACEMENT / EXTREME-SATURATION LEMMA", "29. 一個重要的禁止捷徑：不能直接只測 extreme constant-width bodies", "n/a", "n/a", "not a status"), ("FINITE-FAMILY-PASS", "Q6 removable region", "outside-corpus", "UNMEASURED", "not re-proved in Round 01"), ("NEXT GATE", "Constructive finite shape certificate", "n/a", "n/a", ""), ("PASS / PRIMARY HANDOFF", "Q2", "theorem-application", PBCT, "sec. 6 formula re-derived from Thm 5.1"), ("PASS-WITH-SCOPE", "Q4 angular/rotation sampling", "outside-corpus", "UNMEASURED", "not re-proved in Round 01"), ("REUSE", "一維距離核", "outside-corpus", "n/a", "role assignment"), ("TEST", "$H_2/C_{10}$", "outside-corpus", "n/a", "hypothesis only"), ] def r1_registry(w): return registry.completeness(w["registry"], "R01", w["definitions"], w["reviews"]) CHECKS = {"A0": a0_anchors, "A1": a1_citations, "S1": s1_fourier_parity, "S2": s2_steiner_point, "S3": s3_translation, "S4": s4_moments, "S5": s5_inversion, "S6": s6_width_ode, "S7": s7_sanity_family, "S8": s8_truncation, "N1": n1_reconstruction, "R1": r1_registry} # the world keys each check reads; the drill recomputes a check only when a case # changes one of them (checks are deterministic, so the rest are reused) DEPENDS = {"A0": {"text"}, "A1": {"text", "snapshot"}, "S1": {"parity_claim"}, "S2": {"steiner_claim"}, "S3": {"antipodal_claim"}, "S4": {"moment_weights"}, "S5": {"inversion"}, "S6": {"width_general"}, "S7": {"sanity_r", "sanity_bound"}, "S8": {"truncation_body"}, "N1": {"inversion", "geometry"}, "R1": {"registry", "definitions", "reviews"}} def round01_claims(): """Round 01's statements, transcribed once; A0 pins each to the document.""" def parity(a, b, N): d = {a[0]: sp.Rational(1, 2)} for n in range(2, N + 1, 2): d[a[n]] = 0 d[b[n]] = 0 return d return { "parity_claim": parity, "steiner_claim": lambda a, b: (a[1], b[1]), "antipodal_claim": lambda t1, t2: -(t1 * sp.cos(TH) + t2 * sp.sin(TH)), "moment_weights": [sp.cos(TH), sp.sin(TH)], "inversion": lambda n: sp.Rational(1, 1 - n * n), "width_general": lambda A, B: 1 + A * sp.cos(TH) + B * sp.sin(TH), "sanity_r": lambda a: sp.Rational(1, 2) - 8 * a * sp.cos(3 * TH), "sanity_bound": sp.Rational(1, 16), "truncation_body": sp.Integer(0), # Reuleaux triangle, r = 1 on (0, pi/3) + 2k pi/3 "geometry": "reuleaux", } def build_world(text, snapshot): return {"text": text, "snapshot": snapshot, "registry": registry.load(), "definitions": dict(R01_DEFINITIONS), "reviews": list(R01_REVIEWS), **round01_claims()} def run_checks(w): return {cid: fn(w) for cid, fn in CHECKS.items()} # ---------------------------------------------------------------- drill def drill(text, snapshot): def world(**changes): return changes def doc(fn): return {"text": fn(text)} def snap(n, **changes): s = copy.deepcopy(snapshot) s["records"][str(n)].update(changes) return {"snapshot": s} def odd_modes_vanish(a, b, N): d = {a[0]: sp.Rational(1, 2)} for n in range(1, N + 1, 2): d[a[n]] = 0 d[b[n]] = 0 return d rec = snapshot["records"] cases = [ ("K0-unmodified", "control", world(), set()), ("K1-inversion-rewritten", "control", world(inversion=lambda n: -sp.Rational(1, n * n - 1)), set()), ("K2-sanity-rewritten", "control", world(sanity_r=lambda a: (1 - 16 * a * sp.cos(3 * TH)) / 2), set()), ("K3-reuleaux-rotated", "control", world(truncation_body=sp.pi / 6), set()), # Crossref returns the venue HTML-escaped ("&"); the plain form must match too ("K4-venue-unescaped", "control", snap(6, container=html.unescape(rec["6"]["container"])), set()), ("K5-doc-crlf", "control", doc(lambda t: t.replace("\n", "\r\n")), set()), ("M1-odd-modes-claimed-zero", "mutation", world(parity_claim=odd_modes_vanish), {"S1"}), ("M2-steiner-doubled", "mutation", world(steiner_claim=lambda a, b: (2 * a[1], 2 * b[1])), {"S2"}), ("M3-antipodal-sign", "mutation", world(antipodal_claim=lambda t1, t2: t1 * sp.cos(TH) + t2 * sp.sin(TH)), {"S3"}), ("M4-moment-weight-cos2", "mutation", world(moment_weights=[sp.cos(2 * TH)]), {"S4"}), ("M5-inversion-plus", "mutation", world(inversion=lambda n: sp.Rational(1, 1 + n * n)), {"S5", "N1"}), ("M6-inversion-sign", "mutation", world(inversion=lambda n: sp.Rational(1, n * n - 1)), {"S5", "N1"}), ("M7-width-kernel-cos2", "mutation", world(width_general=lambda A, B: 1 + A * sp.cos(2 * TH) + B * sp.sin(2 * TH)), {"S6"}), ("M8-sanity-sign", "mutation", world(sanity_r=lambda a: sp.Rational(1, 2) + 8 * a * sp.cos(3 * TH)), {"S7"}), ("M9-sanity-bound-1/8", "mutation", world(sanity_bound=sp.Rational(1, 8)), {"S7"}), ("M10-truncation-disc", "mutation", world(truncation_body="disc"), {"S8"}), ("M11-geometry-plain-triangle", "mutation", world(geometry="triangle"), {"N1"}), ("M12-doc-bound-edited", "mutation", doc(lambda t: t.replace(r"\frac1{16}.", r"\frac1{8}.")), {"A0"}), ("M13-doc-inversion-edited", "mutation", doc(lambda t: t.replace(r"\frac{\alpha_n}{1-n^2}", r"\frac{\alpha_n}{1+n^2}")), {"A0"}), ("M14-ref-title", "mutation", snap(8, title=rec["8"]["title"].replace("Rabinowitz", "Rabinovitz")), {"A1"}), ("M15-ref-volume", "mutation", snap(7, volume="118"), {"A1"}), ("M16-ref-article", "mutation", snap(5, article_number="46"), {"A1"}), ("M17-ref-year", "mutation", snap(8, years=[2020]), {"A1"}), ("M18-ref-author", "mutation", snap(5, families=["He", "Martini", "Wang"]), {"A1"}), ("M19-arxiv-year", "mutation", snap(1, years=[2016]), {"A1"}), ("M20-review-dropped", "mutation", world(reviews=list(R01_REVIEWS[1:])), {"R1"}), ("M21-review-duplicated", "mutation", world(reviews=list(R01_REVIEWS) + [R01_REVIEWS[0]]), {"R1"}), ("M22-review-for-no-judgment", "mutation", world(reviews=list(R01_REVIEWS) + [("PASS", "no such subject", "reading", "PASS", "")]), {"R1"}), ("M23-definition-dropped", "mutation", world(definitions={k: v for k, v in R01_DEFINITIONS.items() if k != "ABSTRACT-PASS"}), {"R1"}), ("M24-verdict-outside-vocabulary", "mutation", world(reviews=[R01_REVIEWS[0][:3] + ("PROVED", "")] + list(R01_REVIEWS[1:])), {"R1"}), ] base = run_checks(build_world(text, copy.deepcopy(snapshot))) out = [] for cid, kind, changes, expected in cases: w = build_world(text, copy.deepcopy(snapshot)) w.update(changes) got = {c: (fn(w) if DEPENDS[c] & set(changes) else base[c]) for c, fn in CHECKS.items()} tripped = {c for c, f in got.items() if f} out.append({"case": cid, "kind": kind, "expected": sorted(expected), "tripped": sorted(tripped), "ok": tripped == expected}) return out # ---------------------------------------------------------------- main 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: SNAPSHOT.write_text(json.dumps(fetch_snapshot(), ensure_ascii=False, indent=1) + "\n", encoding="utf-8") snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8")) blobs = {n: source_bytes(n) for n in SOURCES} text = next(d for leaf, d in walk_sources(blobs, keep=lambda l: l.id == ROUND01) if leaf.id == ROUND01).decode("utf-8") if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build_world(text, snapshot) results = run_checks(w) for cid, f in results.items(): print(f"{cid} {'PASS' if not f else 'FAIL'}", *(f"\n {x}" for x in f[:6])) log = {"run": "RUN-004", "subject": "Round 01: reduction chain and placement compiler", "document": ROUND01, "snapshot_retrieved": snapshot["retrieved"], "checks": {cid: {"pass": not f, "failures": f} for cid, f in results.items()}, "s8_witness": w.get("s8_witness"), "n1_max_error": w.get("n1_max_error")} print("S8 witness:", w.get("s8_witness"), "| N1 max error:", w.get("n1_max_error")) if args.drill: d = drill(text, snapshot) plants = [x for x in d if x["kind"] == "mutation"] controls = [x for x in d if x["kind"] == "control"] held = sum(1 for x in d for c in CHECKS if c not in x["expected"] and c not in x["tripped"]) quiet = sum(1 for x in d for c in CHECKS if c not in x["expected"]) log["drill"] = {"plants": len(plants), "plants_caught_by_named_checks": sum(x["ok"] for x in plants), "controls": len(controls), "controls_undisturbed": sum(x["ok"] for x in controls), "must_stay_green_assertions": quiet, "must_stay_green_held": held, "cases": d} print(f"drill: {log['drill']['plants_caught_by_named_checks']}/{len(plants)} plants caught by exactly the " f"named checks; {log['drill']['controls_undisturbed']}/{len(controls)} controls undisturbed; " f"{held}/{quiet} must-stay-green assertions held") 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.write_text(json.dumps(log, ensure_ascii=False, indent=1) + "\n", encoding="utf-8") if not results["R1"]: registry.record("R01", "RUN-004", R01_DEFINITIONS, R01_REVIEWS) print(f"registry: {len(R01_DEFINITIONS)} definitions, {len(R01_REVIEWS)} reviews recorded for R01") if __name__ == "__main__": main()