"""RUN-005 - Round 02: the finite shape compiler. Round 02 turns every centred unit constant-width body into a member of a finite legal dictionary: squared-Fejer (Jackson-type) smoothing J_N, a safety interiorization by delta, and coefficient quantization by q, with the error E_N + delta/2 + (N-1)q. Its theorems are read in the report; everything finite or symbolic in it is recomputed here, independently of the package's script. Checks A0 anchors the formulas below occur in Round 02 as written A1 citations its new references (Bari, Zygmund, Shah-Urschel-West, Schneider) exist K1 fejer F_N equals its stated Fourier series (2N+3 points, 40 digits, N = 1..16) K2 normalisation S_N = (2N^2+4N+3)/(3(N+1)) as a symbolic sum K3 moment-chain sec. 9: the two integrals, their sum over pi S_N, and E_N, symbolically K4 jordan F_N <= min(N+1, pi^2/((N+1)t^2)) on (0, pi] (grid evidence, N = 1..64) K5 validity exact mu_{2,N}/2 <= E_N for N = 1..64, 128, 256 K6 table sec. 22's table equals E_N rounded to 10 decimals K7 quantization A_N closed form; sec. 35's rule is qA_N <= delta/2; sec. 21 gives 5 eps/6 K8 dictionary coefficients of a legal h lie within 4/pi, so q <= 1/2 keeps the grid in [-2,2]; the lattice count is within (ceil(4/q)+1) K9 sanity sec. 32 and the package's VALIDATION.json, recomputed from exact multipliers K10 displays sec. 32's displayed digits against the recomputed values (known slips pinned) K11 package the package's self-description of the document matches the archive K12 reuleaux the actual J_N error on the Reuleaux triangle <= mu_{2,N}/2 <= E_N R1 registry Round 02's judgments reviewed, its first-used statuses defined Usage: python code/run005_round02_finite_compiler.py [--refresh] [--drill] [--blind CID] """ import argparse import json import math import re from fractions import Fraction as Fr import mpmath as mp import numpy as np import sympy as sp import gate import registry from corpus import SOURCES, TREE, source_bytes, walk_sources mp.mp.dps = 40 PKG = "main.zip!/AMRAL_LUC_FC_Round_02_Package_v0.1.zip!/" DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_02_Finite_Compiler_v0.1.md" CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_02_v0.1.md" VALIDATION = PKG + "AMRAL_LUC_FC_Round_02_VALIDATION.json" SNAPSHOT = TREE / "data" / "external" / "round02-citations.json" LOG = TREE / "data" / "gate-logs" / "run005-round02-finite-compiler.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" ANCHORS = { "K2": [r"S_N=\frac{2N^2+4N+3}{3(N+1)}."], "K3": [r"\int_0^{t_0}t^2(N+1)^2\,dt=\frac{\pi^3}{3(N+1)}.", r"\int_{t_0}^{\pi}\frac{\pi^4}{(N+1)^2t^2}\,dt=\frac{\pi^3N}{(N+1)^2}.", r"\mu_{2,N}\le\frac{\pi^2(4N+1)}{(2N^2+4N+3)(N+1)}.", r"E_N:=\frac{\pi^2(4N+1)}{2(2N^2+4N+3)(N+1)}."], "K4": [r"F_N(t)\leN+1", r"F_N(t)\le\frac{\pi^2}{(N+1)t^2}."], "K7": [r"A_N=\frac43(N-1)N(N+1).", r"qA_N\le\frac{\delta}{2},", r"q\le\frac{3\delta}{8(N-1)N(N+1)},", r"d_H(K,\widehatK)\le\frac56\varepsilon<\varepsilon."], "K8": [r"|\mathscrD_{N,\delta,q}|\le\left(\left\lceil\frac4q\right\rceil+1\right)^{2(N-1)}."], } REFS = {5: {"kind": "crossref", "doi": "10.1016/c2013-0-08001-2"}, 6: {"kind": "crossref", "doi": "10.1017/CBO9781316036587"}, 7: {"kind": "arxiv", "id": "2607.23375"}, 8: {"kind": "crossref", "doi": "10.1017/CBO9781139003858"}} # Bari: Crossref's record of the 1964 Pergamon edition lists no authors and gives the # publisher as Elsevier, which owns the Pergamon imprint; title and year are compared. # Zygmund: the record is the 2003 Cambridge edition, which also credits C. Fefferman # (its foreword); the cited author must be among the record's. CITE_OPTS = {5: {"check_authors": False, "check_venue": False}, 6: {"authors_subset": True}, 7: {}, 8: {}} KNOWN_DISPLAY_SLIPS = {"0.77710000": "quantized curvature maximum; the value is 0.7771000125..."} # ---------------------------------------------------------------- exact kernel data def jackson_coeffs(N, kernel="jackson"): """Exact Fourier coefficients c_k, k = 0..2N, of J_N = F_N^2/S_N (or of F_N).""" f = {m: Fr(N + 1 - abs(m), N + 1) for m in range(-N, N + 1)} if kernel == "fejer": return {k: (f[k] if k <= N else Fr(0)) for k in range(0, 2 * N + 1)} raw = {k: sum(f[m] * f[k - m] for m in range(-N, N + 1) if -N <= k - m <= N) for k in range(0, 2 * N + 1)} return {k: v / raw[0] for k, v in raw.items()} def mpf(x): return mp.mpf(x.numerator) / x.denominator def sym_mp(expr): """a sympy number at 45 digits, as an mpmath number""" return mp.mpf(str(sp.N(expr, 45))) def mu2(N): c = jackson_coeffs(N) rat = 4 * sum(c[k] * (-1) ** k / Fr(k * k) for k in range(1, 2 * N + 1)) return mp.pi ** 2 / 3 + mpf(rat) # ---------------------------------------------------------------- checks def k1_fejer(w): out = [] for N in range(1, 17): for i in range(2 * N + 3): t = (mp.mpf(i) + mp.mpf("0.37")) * 2 * mp.pi / (2 * N + 3) lhs = (mp.sin((N + 1) * t / 2) / mp.sin(t / 2)) ** 2 / (N + 1) rhs = 1 + 2 * sum(w["fejer_coeff"](N, k) * mp.cos(k * t) for k in range(1, N + 1)) if abs(lhs - rhs) > mp.mpf("1e-30"): out.append(f"N={N}: F_N differs from its series at t={mp.nstr(t, 8)}") break return out N_ = sp.Symbol("N", positive=True, integer=True) T_ = sp.Symbol("t", positive=True) def k2_normalisation(w): k = sp.Symbol("k", integer=True, positive=True) s = 1 + 2 * sp.summation((1 - k / (N_ + 1)) ** 2, (k, 1, N_)) return [] if sp.simplify(s - w["S_N"](N_)) == 0 else [f"S_N = {sp.factor(s)}"] def k3_moment_chain(w): out = [] t0 = sp.pi / (N_ + 1) i1 = sp.integrate(T_ ** 2 * (N_ + 1) ** 2, (T_, 0, t0)) i2 = sp.integrate(sp.pi ** 4 / ((N_ + 1) ** 2 * T_ ** 2), (T_, t0, sp.pi)) if sp.simplify(i1 - w["int1"](N_)) != 0: out.append(f"first integral is {sp.simplify(i1)}") if sp.simplify(i2 - w["int2"](N_)) != 0: out.append(f"second integral is {sp.simplify(i2)}") bound = (i1 + i2) / (sp.pi * w["S_N"](N_)) if sp.simplify(bound - w["mu_bound"](N_)) != 0: out.append(f"mu bound is {sp.factor(sp.simplify(bound))}") if sp.simplify(bound / 2 - w["E_N"](N_)) != 0: out.append("E_N is not half the mu bound") return out def k4_jordan(w): t = np.linspace(1e-6, np.pi, 4001) worst = 0.0 for N in range(1, 65): F = np.sin((N + 1) * t / 2) ** 2 / (np.sin(t / 2) ** 2 * (N + 1)) cap = np.minimum(N + 1, np.array([float(w["jordan"](N, x)) for x in t])) worst = max(worst, float(np.max(F / cap))) w["k4_worst_ratio"] = worst return [] if worst <= 1 + 1e-12 else [f"F_N exceeds its stated bound by a factor {worst:.4f}"] K5_NS = list(range(1, 65)) + [128, 256] def k5_validity(w): out, ratios = [], {} for N in K5_NS: half = mu2(N) / 2 EN = sym_mp(w["E_N"](sp.Integer(N))) ratios[N] = float(half / EN) if half > EN: out.append(f"N={N}: mu/2 = {mp.nstr(half, 10)} > E_N = {mp.nstr(EN, 10)}") w["k5_ratios"] = {n: ratios[n] for n in (1, 2, 8, 64, 256)} return out def k6_table(w): text = w["text"].replace("\r\n", "\n") sec = text[text.index("# 22."):text.index("# 23.")] rows = re.findall(r"\|\s*\$(\d+)\$\s*\|\s*\$([0-9.]+)\$\s*\|", sec) out = [] if rows else ["no table found"] for n, v in rows: exact = sym_mp(w["E_N"](sp.Integer(int(n)))) if f"{float(exact):.10f}" != v: out.append(f"N={n}: table {v}, E_N = {mp.nstr(exact, 14)}") return out def k7_quantization(w): out = [] j = sp.Symbol("j", integer=True, positive=True) s = sp.summation((2 * j + 1) ** 2 - 1, (j, 1, N_ - 1)) if sp.simplify(s - w["A_N"](N_)) != 0: out.append(f"A_N = {sp.factor(s)}") d = sp.Symbol("delta", positive=True) if sp.simplify(3 * d / (8 * (N_ - 1) * N_ * (N_ + 1)) - d / (2 * w["A_N"](N_))) != 0: out.append("sec. 35's q rule is not q A_N <= delta/2") e = sp.Symbol("eps", positive=True) total = e / 3 + (e / 3) / 2 + (N_ - 1) * (e / (3 * (N_ - 1))) if sp.simplify(total - w["five_sixths"] * e) != 0: out.append(f"sec. 21's choices give {sp.simplify(total)}") return out def k8_dictionary(w): out = [] # (1/pi) int |h cos| <= (1/pi) int |cos| = 4/pi for 0 <= h <= 1; rounding with q <= 1/2 moves <= 1/4 if not (4 / math.pi + 0.25 <= w["coef_box"]): out.append(f"coefficients can reach {4 / math.pi + 0.25:.4f} > box {w['coef_box']}") for q in (0.5, 0.3, 0.25, 0.1, 0.037, 0.01, 1 / 672, 3.7202380952380956e-05): lattice = 2 * math.floor(2 / q + 1e-12) + 1 if lattice > w["card_bound"](q): out.append(f"q={q}: {lattice} lattice values > bound {w['card_bound'](q)}") return out def sanity_values(kernel): """Round 02 sec. 32, recomputed: r = 1/2 + 0.25 cos 3t + 0.15 sin 5t, N = 8, delta = 0.1, q = 0.025/672 (the package's own q), from exact kernel multipliers.""" N, d = 8, mp.mpf("0.1") c = jackson_coeffs(N, kernel) j3, j5 = mpf(c[3]), mpf(c[5]) A3, B5 = mp.mpf("0.25"), mp.mpf("0.15") h3, h5 = A3 / (1 - 9), B5 / (1 - 25) q = mp.mpf("0.025") / 672 def ext(a, b): """min and max of a cos 3t + b sin 5t (a, b constants), by derivative roots.""" f = lambda x: a * mp.cos(3 * x) + b * mp.sin(5 * x) df = lambda x: -3 * a * mp.sin(3 * x) + 5 * b * mp.cos(5 * x) xs = [2 * mp.pi * i / 3000 for i in range(3001)] vals = [f(x) for x in xs] for i in range(3000): if (df(xs[i]) > 0) != (df(xs[i + 1]) > 0): vals.append(f(mp.findroot(df, (xs[i], xs[i + 1]), solver="anderson"))) return min(vals), max(vals) lo, hi = ext(A3, B5) elo, ehi = ext((j3 - 1) * h3, (j5 - 1) * h5) ilo, ihi = ext((1 - d) * j3 * A3, (1 - d) * j5 * B5) qa3 = q * mp.nint((1 - d) * j3 * h3 / q) qb5 = q * mp.nint((1 - d) * j5 * h5 / q) qlo, qhi = ext(-8 * qa3, -24 * qb5) tlo, thi = ext(qa3 - h3, qb5 - h5) EN = mp.pi ** 2 * (4 * N + 1) / (2 * (2 * N * N + 4 * N + 3) * (N + 1)) return {"original_r_min": 0.5 + lo, "original_r_max": 0.5 + hi, "smoothing_actual_support_error": max(-elo, ehi), "interiorized_r_min": 0.5 + ilo, "interiorized_r_max": 0.5 + ihi, "quantized_r_min": 0.5 + qlo, "quantized_r_max": 0.5 + qhi, "total_support_error": max(-tlo, thi), "smoothing_theoretical_bound_E_N": EN, "q": q, "A_N": 672, "theorem_total_bound": EN + d / 2 + 7 * q} SANITY_CACHE = {} def sanity(kernel): if kernel not in SANITY_CACHE: SANITY_CACHE[kernel] = sanity_values(kernel) return SANITY_CACHE[kernel] # grid-sampled extremes lie inside the true ones; errors at or below the true sup INSIDE = {"original_r_min": +1, "interiorized_r_min": +1, "quantized_r_min": +1, "original_r_max": -1, "interiorized_r_max": -1, "quantized_r_max": -1, "smoothing_actual_support_error": -1, "total_support_error": -1} def k9_sanity(w): out, mine, theirs = [], sanity(w["kernel"]), w["validation"]["sanity_check"] if theirs["A_N"] != int(sp.N(w["A_N"](sp.Integer(8)))): out.append(f"A_8 recorded {theirs['A_N']}, claimed formula gives {w['A_N'](sp.Integer(8))}") for key, val in mine.items(): t = mp.mpf(theirs[key]) if key == "smoothing_theoretical_bound_E_N": val = sym_mp(w["E_N"](sp.Integer(8))) if abs(t - val) > mp.mpf("1e-8"): out.append(f"{key}: recorded {theirs[key]}, recomputed {mp.nstr(val, 12)}") elif key in INSIDE and INSIDE[key] * (t - val) < -mp.mpf("1e-15"): out.append(f"{key}: recorded value lies outside the true extreme") return out def displays(text): t = gate.squash(text) grab = lambda pat: (re.search(pat, t) or [None, None])[1] return {"original_r_min": grab(r"(0\.\d+)\\ldots\\ler\\le0\.\d+\\ldots"), "original_r_max": grab(r"0\.\d+\\ldots\\ler\\le(0\.\d+)\\ldots"), "smoothing_actual_support_error": grab(r"actualsmoothingerror：\$\$(0\.\d+)\\ldots"), "smoothing_theoretical_bound_E_N": grab(r"E_8=(0\.\d+)\\ldots"), "quantized_r_min": grab(r"(0\.\d+)\\ldots\\le\\widehatr"), "quantized_r_max": grab(r"\\widehatr\\le(0\.\d+)\\ldots"), "total_support_error": grab(r"totalsupporterror：\$\$(0\.\d+)\\ldots")} def k10_displays(w): out, found_known = [], set() mine = sanity("jackson") for key, shown in displays(w["text"]).items(): if shown is None: out.append(f"{key}: display not found") continue places = len(shown.split(".")[1]) v = mine[key] trunc = f"{float(mp.floor(v * 10 ** places) / 10 ** places):.{places}f}" rnd = f"{float(v):.{places}f}" if shown in (trunc, rnd): continue if shown in w["known_slips"]: found_known.add(shown) else: out.append(f"{key}: shows {shown}, value {mp.nstr(v, places + 4)}") for s in w["known_slips"]: if s not in found_known: out.append(f"known slip {s} not reproduced - update the pin") return out def k11_package(w): out, v = [], w["validation"] leaves = {row[0]: row for row in w["manifest"]["leaves"]} for key, leaf, text in (("round02", DOC, w["text"]), ("state_crystal", CRYSTAL, w["crystal"])): rec = v[key] _, size, digest = leaves[leaf] if rec["sha256"] != digest or rec["bytes"] != size: out.append(f"{key}: recorded sha256/bytes differ from the archive") if rec["double_dollar_count"] != text.count("$$"): out.append(f"{key}: recorded {rec['double_dollar_count']} $$, document has {text.count('$$')}") if rec["contains_unicode_escape_literal"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)): out.append(f"{key}: recorded \\u flag wrong") return out def k12_reuleaux(w): th = np.linspace(0, 2 * np.pi / 3, 20001) out, rows = [], {} for N in (2, 4, 8, 16, 32, 64): c = jackson_coeffs(N, w["kernel"]) err = np.zeros_like(th) for m in range(1, 4002, 2): n = 3 * m mult = float(c[n]) if n <= 2 * N else 0.0 err += (mult - 1.0) * (2 / (np.pi * m)) / (1 - 9 * m * m) * np.sin(n * th) a = float(np.max(np.abs(err))) half = float(mu2(N) / 2) EN = float(sp.N(w["E_N"](sp.Integer(N)))) rows[N] = {"actual": a, "mu_half": half, "E_N": EN} if not (a <= half + 1e-9 and half <= EN): out.append(f"N={N}: actual {a:.3e}, mu/2 {half:.3e}, E_N {EN:.3e}") w["k12_rows"] = rows return out # ---------------------------------------------------------------- registry (Round 02) R02_DEFINITIONS = { "PROVED": ("contextual", "sec. 33 labels this round's theorems PROVED without defining the word; in use, a " "theorem proved in the round. It does not say whether the proof is analytic, a " "computation or a theorem application - the distinction Round 00's ten statuses keep"), "PROVED IN MEASURE FORM": ("contextual", "sec. 2: proved for the curvature measure h+h'' in the sense of " "distributions, so that non-smooth bodies are covered"), "PROVED CONSTRUCTIVELY": ("contextual", "sec. 19-20: the dictionary is exhibited and enumerable, not only shown to exist"), "STILL OPEN": ("contextual", "the gate stays open after this round (= OPEN)"), "ABSTRACT FINITE NET": ("in-line", "sec. 21: Round 01's existence-only net (Round 01's ABSTRACT-PASS), as a 'before' label"), "CONSTRUCTIVE LEGAL FINITE NET": ("in-line", "sec. 21: an explicit eps-net of legal bodies with explicit parameters"), "UNCONTROLLED INFINITE DOMAIN": ("in-line", "sec. 26: the target-shape domain before this round"), "CERTIFIED FINITE-RESOLUTION DOMAIN": ("in-line", "sec. 26: the target-shape domain after this round - a finite legal " "codebook at every resolution eps"), } PBCT = "PASS by cited theorem" R02_REVIEWS = [ ("PROVED", "Positive-kernel legality", "analytic", PBCT, "Thm 4.1 re-derived; convexity rests on the support-function criterion"), ("PROVED", "Explicit kernel error", "analytic", PBCT, "sec. 7-9 re-derived and recomputed (K2-K6, K12); 0<=h<=1 rests on the Steiner point lying in the body"), ("PROVED", "Legal coefficient quantization", "analytic", "PASS", "sec. 16-17; A_N recomputed (K7)"), ("PASS", "R-DOMAIN NONSMOOTH AUDIT", "analytic", PBCT, "sec. 2; h+h'' is a nonnegative measure for a convex body"), ("PASS", "UTF-8 canonical source", "computation", "PASS", "RUN-003 G1"), ("PASS", "Canonical math delimiters", "computation", "PASS", "RUN-003 G2-G4"), ("CLOSED", "CONSTRUCTIVE FINITE SHAPE COMPILER", "analytic", PBCT, "Thm 4.1, sec. 9, sec. 12-20"), ("COMPUTE-DEFERRED", "C02-3：Coefficient quantization branch compression", "n/a", "n/a", "C02-1..3 correctly deferred"), ("COMPUTE-DEFERRED", "Practical enumeration", "n/a", "n/a", ""), ("OPEN", "Global solution", "n/a", "n/a", ""), ("NONE", "New Lebesgue numerical bound", "reading", "PASS", "none claimed"), ("ABSTRACT FINITE NET", "21. 任意 $\\varepsilon$ 的顯式選參方式", "n/a", "n/a", "a label for Round 01's state"), ("CERTIFIED FINITE-RESOLUTION DOMAIN", "26. 本輪真正關閉了什麼", "analytic", PBCT, "= Thm 20.1"), ("CONSTRUCTIVE LEGAL FINITE NET", "21. 任意 $\\varepsilon$ 的顯式選參方式", "analytic", PBCT, "sec. 21 choices recomputed (K7)"), ("PROVED CONSTRUCTIVELY", "Finite dictionary existence", "analytic", PBCT, "Thm 20.1; box and count (K8)"), ("PROVED IN MEASURE FORM", "Nonsmooth constant-width inclusion", "analytic", PBCT, "sec. 2"), ("STILL OPEN", "GLOBAL FINITE CLOSURE", "n/a", "n/a", ""), ("UNCONTROLLED INFINITE DOMAIN", "26. 本輪真正關閉了什麼", "n/a", "n/a", "a label for Round 01's state"), ] def r1_registry(w): return registry.completeness(w["registry"], "R02", w["definitions"], w["reviews"]) # ---------------------------------------------------------------- world, checks, drill CHECKS = {"A0": gate.anchors_check(ANCHORS), "A1": gate.citations_check(CITE_OPTS), "K1": k1_fejer, "K2": k2_normalisation, "K3": k3_moment_chain, "K4": k4_jordan, "K5": k5_validity, "K6": k6_table, "K7": k7_quantization, "K8": k8_dictionary, "K9": k9_sanity, "K10": k10_displays, "K11": k11_package, "K12": k12_reuleaux, "R1": r1_registry} DEPENDS = {"A0": {"text"}, "A1": {"text", "snapshot"}, "K1": {"fejer_coeff"}, "K2": {"S_N"}, "K3": {"int1", "int2", "mu_bound", "E_N", "S_N"}, "K4": {"jordan"}, "K5": {"E_N"}, "K6": {"text", "E_N"}, "K7": {"A_N", "five_sixths"}, "K8": {"coef_box", "card_bound"}, "K9": {"validation", "kernel", "A_N", "E_N"}, "K10": {"text", "known_slips"}, "K11": {"validation", "text", "crystal", "manifest"}, "K12": {"kernel", "E_N"}, "R1": {"registry", "definitions", "reviews"}} def claims(): return { "fejer_coeff": lambda N, k: 1 - mp.mpf(k) / (N + 1), "S_N": lambda N: (2 * N ** 2 + 4 * N + 3) / (3 * (N + 1)), "int1": lambda N: sp.pi ** 3 / (3 * (N + 1)), "int2": lambda N: sp.pi ** 3 * N / (N + 1) ** 2, "mu_bound": lambda N: sp.pi ** 2 * (4 * N + 1) / ((2 * N ** 2 + 4 * N + 3) * (N + 1)), "E_N": lambda N: sp.pi ** 2 * (4 * N + 1) / (2 * (2 * N ** 2 + 4 * N + 3) * (N + 1)), "jordan": lambda N, t: math.pi ** 2 / ((N + 1) * t * t), "A_N": lambda N: sp.Rational(4, 3) * (N - 1) * N * (N + 1), "five_sixths": sp.Rational(5, 6), "coef_box": 2.0, "card_bound": lambda q: math.ceil(4 / q) + 1, "kernel": "jackson", "known_slips": dict(KNOWN_DISPLAY_SLIPS), } def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = {DOC, CRYSTAL, VALIDATION} 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(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()} import datetime SNAPSHOT.write_text(json.dumps({"retrieved": datetime.date.today().isoformat(), "records": recs}, ensure_ascii=False, indent=1) + "\n", encoding="utf-8") snapshot = json.loads(SNAPSHOT.read_text(encoding="utf-8")) text, crystal, validation, manifest = load_inputs() def build(): return {"text": text, "crystal": crystal, "validation": json.loads(json.dumps(validation)), "manifest": manifest, "snapshot": json.loads(json.dumps(snapshot)), "registry": registry.load(), "definitions": dict(R02_DEFINITIONS), "reviews": list(R02_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])) log = {"run": "RUN-005", "subject": "Round 02: the finite shape compiler", "document": DOC, "snapshot_retrieved": snapshot["retrieved"], "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, "k4_worst_ratio": w.get("k4_worst_ratio"), "k5_ratios": w.get("k5_ratios"), "k12_rows": w.get("k12_rows"), "sanity_recomputed": {k: mp.nstr(v, 17) for k, v in sanity("jackson").items()}, "known_display_slips": KNOWN_DISPLAY_SLIPS} if args.drill: rec = snapshot["records"] val = validation["sanity_check"] tweak = lambda key, delta: {"validation": {**validation, "sanity_check": {**val, key: val[key] + delta}}} pkg = lambda key, field, value: {"validation": {**validation, key: {**validation[key], field: value}}} cases = [ ("K0-unmodified", "control", {}, set()), ("K1-S_N-rewritten", "control", {"S_N": lambda N: 1 + N * (2 * N + 1) / (3 * (N + 1))}, set()), ("K2-E_N-rewritten", "control", {"E_N": lambda N: (sp.pi ** 2 / 2) * (4 * N + 1) / ((N + 1) * (2 * N ** 2 + 4 * N + 3))}, set()), ("K3-fejer-rewritten", "control", {"fejer_coeff": lambda N, k: mp.mpf(N + 1 - k) / (N + 1)}, set()), ("K4-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K5-record-float-noise", "control", tweak("smoothing_actual_support_error", -1e-13), set()), ("M1-fejer-coefficient", "mutation", {"fejer_coeff": lambda N, k: 1 - mp.mpf(k) / N}, {"K1"}), ("M2-S_N-denominator", "mutation", {"S_N": lambda N: (2 * N ** 2 + 4 * N + 3) / (3 * N)}, {"K2", "K3"}), ("M3-first-integral", "mutation", {"int1": lambda N: sp.pi ** 3 / (3 * N)}, {"K3"}), ("M4-E_N-slightly-small", "mutation", {"E_N": lambda N: sp.Rational(999, 1000) * sp.pi ** 2 * (4 * N + 1) / (2 * (2 * N ** 2 + 4 * N + 3) * (N + 1))}, {"K3", "K6", "K9"}), ("M5-E_N-tenfold-too-strong", "mutation", {"E_N": lambda N: sp.pi ** 2 * (4 * N + 1) / (20 * (2 * N ** 2 + 4 * N + 3) * (N + 1))}, {"K3", "K5", "K6", "K9", "K12"}), ("M6-jordan-too-strong", "mutation", {"jordan": lambda N, t: math.pi ** 2 / ((N + 1) ** 2 * t * t)}, {"K4"}), ("M7-A_N-halved", "mutation", {"A_N": lambda N: sp.Rational(2, 3) * (N - 1) * N * (N + 1)}, {"K7", "K9"}), ("M8-five-sixths-wrong", "mutation", {"five_sixths": sp.Rational(2, 3)}, {"K7"}), ("M9-coefficient-box-1", "mutation", {"coef_box": 1.0}, {"K8"}), ("M10-count-bound-too-small", "mutation", {"card_bound": lambda q: math.ceil(2 / q) + 1}, {"K8"}), ("M11-recorded-error-off", "mutation", tweak("smoothing_actual_support_error", 1e-6), {"K9"}), ("M12-recorded-min-outside", "mutation", tweak("quantized_r_min", -1e-9), {"K9"}), ("M13-kernel-fejer", "mutation", {"kernel": "fejer"}, {"K9", "K12"}), ("M14-table-entry", "mutation", {"text": text.replace("0.1110078205", "0.1110078206")}, {"K6"}), ("M15-display-digit", "mutation", {"text": text.replace("0.00946175", "0.00946185")}, {"K10"}), ("M16-known-slip-gone", "mutation", {"text": text.replace("0.77710000", "0.77710001")}, {"K10"}), ("M17-unpinned-slip", "mutation", {"known_slips": {}}, {"K10"}), ("M18-doc-A_N-edited", "mutation", {"text": text.replace(r"\frac43", r"\frac23")}, {"A0"}), ("M19-package-sha", "mutation", pkg("round02", "sha256", "0" * 64), {"K11"}), ("M20-package-dollars", "mutation", pkg("round02", "double_dollar_count", 420), {"K11"}), ("M21-ref-year", "mutation", {"snapshot": {**snapshot, "records": {**rec, "7": {**rec["7"], "years": [2027]}}}}, {"A1"}), ("M22-ref-title", "mutation", {"snapshot": {**snapshot, "records": {**rec, "5": { **rec["5"], "title": rec["5"]["title"].replace("Treatise", "Treatment")}}}}, {"A1"}), ("M23-review-dropped", "mutation", {"reviews": list(R02_REVIEWS[1:])}, {"R1"}), ("M24-definition-dropped", "mutation", {"definitions": {k: v for k, v in R02_DEFINITIONS.items() if k != "PROVED"}}, {"R1"}), ] d = gate.run_drill(build, CHECKS, DEPENDS, cases) log["drill"] = gate.summarize(d, CHECKS) print(gate.report_drill(log["drill"])) 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, default=str) + "\n", encoding="utf-8") if not results["R1"]: registry.record("R02", "RUN-005", R02_DEFINITIONS, R02_REVIEWS) print(f"registry: {len(R02_DEFINITIONS)} definitions, {len(R02_REVIEWS)} reviews recorded for R02") if __name__ == "__main__": main()