"""RUN-065 - BCODR LUC 03: the true common-point overlap time of LUC 02's nine parents. BCODR-LUC-03 (2026-09-21) defines T_true(B) = inf over z in B of max(d(z, S+), d(z, S-)), the first radius at which the critical ray's field and the prune boxes' field cover one same point of B, proves T_true >= T_box = max(T+, T-), and recomputes the nine parents: 131 and 127 are "balanced" (d+ = d- at the minimax point), the other seven "outward- limited" (the ray is the bottleneck) with a gap within 2e-9 of zero; 131's true time is 0.0473 (a midpoint), 127's is 0.126953667790942 against T_box = 0.125, its provenance 155 with a margin of 0.042 over 144, "so LUC 02's 144 -> 155 flip still holds"; and 127's minimax reduces to one dimension (r* = 0.0025452863775066, lambda* = 0.760555242947675, T = 0.126953667790925). Here every T_true is computed to 40 digits on the exact grid of RUN-064, by the dual of a convex problem, for every prune box separately. For a ray point p and a prune box Q, min over z in B of max(|z - p|, d(z, Q))^2 = max over mu in [0, 1] of min over z in B of mu |z - p|^2 + (1 - mu) d(z, Q)^2 (a convex-concave minimax), and the inner minimum is separable, with a closed form in each coordinate. mu = 1 at the optimum means the ray alone decides (outward-limited), mu = 0 the box alone, anything between both (balanced); z = p + lambda (q - p) has lambda = 1 - mu. T_true is then the least, over 0 <= rho <= 0.003 and over the five boxes, of these values. Checks A0 anchors the statements below occur in the document as written W1 times sec. 2-3, 5: T_box and T_true for the nine, the gaps, and where the ledger's negative gaps come from W2 modes sec. 4-6, 16: balanced or outward-limited, from the optimal mu W3 provenance sec. 5, 10, 17: the earliest box for each parent, with ties, the next one, and the margins W4 root131 sec. 8: half the distance from the ray to 155, at the midpoint W5 root127 sec. 9-14: the 5-D value, the one-dimensional reduction, its active set and its printed digits W6 records the ledger, CSV, state and plot against each other and the rebuild W7 verifier the verifier, read after this rebuild and never run P1 package the VALIDATION record against the bytes and the archive Usage: python code/run065_bcodr_luc03.py [--drill] [--blind CID] """ import argparse import copy import csv import hashlib import inspect import io import json import re import mpmath as mp import gate import run048_uesfcm_cycles_12_14 as r48 import run064_bcodr_luc02 as r64 from corpus import SOURCES, TREE, source_bytes, walk_sources PKG = "main.zip!/BCODR/BCODR_LUC_03_Package_v0.1.zip!/" DOC = PKG + "BCODR_LUC_03_True_Common_Point_Overlap_and_Provenance_Resolution_v0.1.md" LEDGER = PKG + "BCODR_LUC_03_True_Common_Point_Overlap_Ledger_v0.1.json" CSV = PKG + "BCODR_LUC_03_True_Overlap_Gaps_v0.1.csv" PLOT = PKG + "BCODR_LUC_03_True_Overlap_vs_Container_Contact.png" VERIFIER = PKG + "BCODR_LUC_03_Verify_True_Common_Point_Overlap.py" STATE = PKG + "BCODR_LUC_03_STATE_v0.1.json" VALIDATION = PKG + "BCODR_LUC_03_VALIDATION.json" LOG = TREE / "data" / "gate-logs" / "run065-bcodr-luc03.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" CACHE = TREE / "data" / "cache" / "run065-searches.json" # data/cache is not committed PRUNE, PARENTS = r64.PRUNE, r64.PARENTS HALF, KK = 2 ** 21, 2 ** 22 DPS = 40 TIE = "1e-30" # values: T is the maximum of a concave function in mu, so far more exact MU_TOL = "1e-18" # the optimal mu itself, and z, are located to about 1e-21 RHO_DOC, LAMBDA_DOC = "0.0025452863775066", "0.760555242947675" def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} want = (DOC, LEDGER, CSV, PLOT, VERIFIER, STATE, VALIDATION) got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None} rows = {r[0]: r for r in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"] if r[0] in want} c11 = r48.load_inputs() return {"text": got[DOC].decode("utf-8"), "ledger": json.loads(got[LEDGER]), "csv": got[CSV].decode("utf-8"), "verifier": got[VERIFIER].decode("utf-8"), "state": json.loads(got[STATE]), "validation": json.loads(got[VALIDATION]), "bytes": {k: got[k] for k in want}, "manifest_rows": rows, "subroots": c11["subroots"], "root": c11["root"]} # ---------------------------------------------------------------- the true overlap, rebuilt def nbox(g, i): return [mp.mpf(g["LO"][i][k] - HALF) / KK for k in range(5)], [mp.mpf(g["HI"][i][k] - HALF) / KK for k in range(5)] def ray_n(g, r): return [(x - HALF) / KK for x in r64.ray_units(r, g)] def phi(mu, p, lo, hi, ql, qh): """min over z in B of mu |z - p|^2 + (1 - mu) d(z, Q)^2, coordinate by coordinate: the free minimizer is the weighted mean of p and Q's near face (or p, inside Q's range), then clamped to B; works on floats and mpf alike""" v, z = 0, [] for k in range(5): xu = mu * p[k] + (1 - mu) * ql[k] if p[k] < ql[k] else mu * p[k] + (1 - mu) * qh[k] if p[k] > qh[k] else p[k] x = min(max(xu, lo[k]), hi[k]) gap = max(0, ql[k] - x, x - qh[k]) v += mu * (x - p[k]) ** 2 + (1 - mu) * gap * gap z.append(x) return v, z def golden_max(f, a, b, q, it): x1, x2 = b - q * (b - a), a + q * (b - a) f1, f2 = f(x1), f(x2) for _ in range(it): if f1 > f2: b, x2, f2 = x2, x1, f1 x1 = b - q * (b - a) f1 = f(x1) else: a, x1, f1 = x1, x2, f2 x2 = a + q * (b - a) f2 = f(x2) return max((f1, x1), (f2, x2)) def at_point(p, lo, hi, ql, qh, q, it, one): """for a fixed ray point: the minimax value over z in B, its mu and z (mu = 0 and mu = 1 tried as well)""" f = lambda m: phi(m, p, lo, hi, ql, qh)[0] v, m = max([(f(0 * one), 0 * one), (f(one), one), golden_max(f, 0 * one, one, q, it)]) return v, m def common_time(g, P, j): """the earliest common point of B = box P with the ray's field and box j's field: a 300-step float scan of rho, then golden sections in rho and in mu at 40 digits""" lo, hi = nbox(g, P) ql, qh = nbox(g, j) flo, fhi, fql, fqh = ([float(x) for x in v] for v in (lo, hi, ql, qh)) rays = [[float(x) for x in ray_n(g, mp.mpf(0.003) * i / 300)] for i in range(301)] qf = (5 ** 0.5 - 1) / 2 k = min(range(301), key=lambda i: at_point(rays[i], flo, fhi, fql, fqh, qf, 70, 1.0)[0]) qm, step = (mp.sqrt(5) - 1) / 2, mp.mpf(0.003) / 300 a, b = max(step * (k - 1), mp.mpf(0)), min(step * (k + 1), mp.mpf(0.003)) neg = lambda r: -at_point(ray_n(g, r), lo, hi, ql, qh, qm, 110, mp.mpf(1))[0] _, r = max([(neg(a), a), (neg(b), b), golden_max(neg, a, b, qm, 110)]) p = ray_n(g, r) v, m = at_point(p, lo, hi, ql, qh, qm, 110, mp.mpf(1)) z = phi(m, p, lo, hi, ql, qh)[1] dist = lambda Q: mp.sqrt(sum(max(0, Q[0][k] - z[k], z[k] - Q[1][k]) ** 2 for k in range(5))) return {"T": mp.sqrt(v), "rho": r, "mu": m, "z": z, "p": p, "dplus": mp.sqrt(sum((z[k] - p[k]) ** 2 for k in range(5))), "dminus": {str(jj): dist(nbox(g, jj)) for jj in PRUNE}} def true_overlap(sub, root): """every parent against every prune box; T_box (T+ to 50 digits, T- exact) from RUN-064; the distances from the ray to boxes 155 and 144 themselves""" s = lambda x: mp.nstr(x, 32) with mp.workdps(50): g = r64.grid_boxes(sub, root) box = {} for P in PARENTS: a = r64.arrive(g["LO"][P], g["HI"][P], g) box[str(P)] = {"tp": s(a["tp"]), "tm": s(a["tm"]), "near": a["near"]} ray_to = {str(j): s(r64.t_plus(g["LO"][j], g["HI"][j], g)[0]) for j in (144, 155)} out = {} with mp.workdps(DPS): for P in PARENTS: out[str(P)] = {} for j in PRUNE: c = common_time(g, P, j) out[str(P)][str(j)] = {"T": s(c["T"]), "rho": s(c["rho"]), "mu": s(c["mu"]), "z": [s(x) for x in c["z"]], "p": [s(x) for x in c["p"]], "dplus": s(c["dplus"]), "dminus": {k: s(v) for k, v in c["dminus"].items()}} boxes = {str(i): [[(g["LO"][i][k] - HALF) / KK for k in range(5)], [(g["HI"][i][k] - HALF) / KK for k in range(5)]] for i in PARENTS + PRUNE} return {"box": box, "ray_to": ray_to, "pairs": out, "boxes": boxes} def reduction(sub, root): """sec. 12-14 for 127 against 155: a(r) = r1 - p1(r), b = r1 - q1, D(r)^2 over (rho5, y5), lambda(r) and T(r) as printed, minimized over r; and the 5-D value at the printed r*""" with mp.workdps(DPS): g = r64.grid_boxes(sub, root) lo, hi = nbox(g, 127) ql, qh = nbox(g, 155) r1, q1, q3, q5 = lo[0], qh[0], qh[2], qh[4] b = r1 - q1 def parts(r): p = ray_n(g, r) a = r1 - p[0] D2 = (p[2] - q3) ** 2 + (p[4] - q5) ** 2 lam = (b ** 2 - a ** 2 + D2) / (2 * D2) return p, a, D2, lam, mp.sqrt(a ** 2 + lam ** 2 * D2) qm = (mp.sqrt(5) - 1) / 2 _, r = golden_max(lambda x: -parts(x)[4], mp.mpf(0.0025), mp.mpf(0.0026), qm, 140) p, a, D2, lam, T = parts(r) z = [r1, p[1], p[2] + lam * (q3 - p[2]), p[3], p[4] + lam * (q5 - p[4])] doc = at_point(ray_n(g, mp.mpf(RHO_DOC)), lo, hi, ql, qh, qm, 110, mp.mpf(1)) s = lambda x: mp.nstr(x, 32) return {"r": s(r), "lambda": s(lam), "T": s(T), "a": s(a), "b": s(b), "D2": s(D2), "z": [s(x) for x in z], "faces": {"r1": s(r1), "q1": s(q1), "q3": s(q3), "q5": s(q5)}, "inside_127": all(lo[k] <= z[k] <= hi[k] for k in range(5)), "y3_x5_inside_155": all(ql[k] <= p[k] <= qh[k] for k in (1, 3)), "T_at_doc_rho": s(mp.sqrt(doc[0])), "lambda_at_doc_rho": s(1 - doc[1])} def _key(fn, extra=""): digest = hashlib.sha256(inspect.getsource(fn).encode()) for helper in (nbox, ray_n, phi, golden_max, at_point, common_time, r64.grid_boxes, r64.ray_units, r64.t_plus, r64.t_minus, r64.arrive): digest.update(inspect.getsource(helper).encode()) digest.update(f"{DPS} {r64.X30} {r64.S} {r64.X5} {r64.U} {r64.V} {PRUNE} {PARENTS} {RHO_DOC}".encode()) digest.update(extra.encode()) return digest.hexdigest() def searches(inputs): cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {} out = {} tag = json.dumps([inputs["subroots"], inputs["root"]], sort_keys=True) jobs = (("true", true_overlap, lambda: true_overlap(inputs["subroots"], inputs["root"])), ("reduction", reduction, lambda: reduction(inputs["subroots"], inputs["root"]))) for name, fn, call in jobs: key = _key(fn, tag) if cached.get(name, {}).get("key") != key: cached[name] = {"key": key, "value": json.loads(json.dumps(call()))} 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 # ---------------------------------------------------------------- derived def summary(search): """per parent: T_true, the earliest boxes (ties), the next ones, the mode and the optimal mu of the earliest box""" tie = mp.mpf(TIE) out = {} with mp.workdps(DPS): for P in PARENTS: pr = search["true"]["pairs"][str(P)] T = {j: mp.mpf(pr[str(j)]["T"]) for j in PRUNE} order = sorted(PRUNE, key=lambda j: T[j]) first = sorted(j for j in PRUNE if T[j] - T[order[0]] < tie) rest = [j for j in order if j not in first] second = sorted(j for j in rest if T[j] - T[rest[0]] < tie) best = pr[str(first[0])] mu = mp.mpf(best["mu"]) mode = "OUTWARD_LIMITED" if abs(mu - 1) < tie else "INWARD_LIMITED" if abs(mu) < tie else "BALANCED_BOTH_ACTIVE" tb = max(mp.mpf(search["true"]["box"][str(P)]["tp"]), mp.mpf(search["true"]["box"][str(P)]["tm"])) out[P] = {"T": T[order[0]], "first": first, "second": second, "second_T": T[rest[0]], "margin": T[rest[0]] - T[order[0]], "mode": mode, "mu": mu, "T_box": tb, "gap": T[order[0]] - tb, "best": best} return out # ---------------------------------------------------------------- checks ANCHORS = {"A0": [r"T_\cap^{\rmtrue}(B)=\inf_{z\inB}\max\{d_+(z),d_-(z)\}.", r"T_\cap^{\rmtrue}(B)\geT_{\rmbox}(B).", r"\varepsilon_{\rmnum}=2\times10^{-9}", "|131|0.000000000|0.047333350|0.047333350|BALANCED_BOTH_ACTIVE|155|0.129443345|", "|166|0.374427483|0.374427483|0.000000000|OUTWARD_LIMITED|155|0.013910203|", "|127|0.125000000|0.126953668|0.001953668|BALANCED_BOTH_ACTIVE|155|0.042014904|", "|101|0.729883874|0.729883873|0.000000000|OUTWARD_LIMITED|28|0.000000000|", "|103|0.745259994|0.745259993|0.000000000|OUTWARD_LIMITED|28|0.000000000|", r"\boxed{127,\131.}", r"T_\cap^{\rmtrue}(131)=0.0473333498927312.", "2.786e-08.", r"T_\cap^{\rmtrue}(127)=0.126953667790942.", r"G_{\rmsep}(127)=0.00195366779094197.", "0.168968571407971.", r"\DeltaT_{\rmprov}=0.0420149036170295.", "provenanceflip在真正minimaxgeometry中仍成立。", r"\lambda(r)=\frac{b^2-a(r)^2+D(r)^2}{2D(r)^2}.", r"T_{127,155}(r)^2=a(r)^2+\lambda(r)^2D(r)^2.", r"r^\star=0.0025452863775066,", r"\lambda^\star=0.760555242947675,", r"T_{127,155}(r^\star)=0.126953667790925.", "1.707e-14.", "101、103、104就接近這一類。", "PROVENANCE_RESOLVED=155"]} OUTWARD = [166, 167, 164, 165, 101, 104, 103] CLAIMS = { # T_true to 8e-13 (the ledger's optimizers); every gap of the seven outward-limited parents is exactly zero, and the # ledger's negative raw gaps are, to 5e-13, its T_box's excess from LUC 01's ray grid "times_claim": {"T_box": 1e-09, "T_true": 8e-13, "theorem": True, "zero_gap": sorted(OUTWARD), "negative_raw": sorted(OUTWARD), "raw_is_grid": 5e-13, "gaps": {"131": "0.047333349891945", "127": "0.00195366779092488"}}, "modes_claim": {"modes": {str(P): "BALANCED_BOTH_ACTIVE" if P in (131, 127) else "OUTWARD_LIMITED" for P in PARENTS}, "ledger": True, "mu": {"131": "0.5", "127": "0.239445"}, "balanced": [127, 131], "ledger_balanced": [127, 131], "ledger_outward": True, "balanced_equal": True, "outward_inside": 0.026}, # four boxes tie exactly at 101, 103 and 104 (the ledger's 28 is the first, its margins noise); three tie for second at # 164, at sqrt(5/32) "provenance_claim": {"first": {str(P): [28, 68, 144, 155] if P in (101, 104, 103) else [155] for P in PARENTS}, "second": {str(P): [36] if P in (101, 104, 103) else [28, 68, 144] if P == 164 else [144] for P in PARENTS}, "ledger_first_in_ties": True, "ledger_second_in_ties": True, "margins": 2e-12, "degenerate_ledger_margins": [1.4e-13, 2e-13, 4.4e-16], "next_after_ties": {"101": "0.181738", "104": "0.239762", "103": "0.19536"}, "164_second": "0.3952847075210474165", "sqrt_5_32": "0.3952847075210474165"}, "root131_claim": {"mu_half": True, "half_ray_to_155": True, "inside_131": True, "T": "0.04733334989194496", "ledger": [8e-13, 2.7855833491842798e-08], "second_144": [[144], True, [0, 0, 0.125, 0, 0.125], True], "ledger_second_below_bound": 1.3e-12, "rho": "0.002540688875"}, # the reduction is the 5-D minimum; the printed reduced T is right, the 5-D one 1.7e-14 high; r* and lambda* only to # 4e-11 and 7e-12, where T changes by 2e-18 "root127_claim": {"reduction_is_5d": True, "T": "0.12695366779092487911", "lambda_is_1_minus_mu": True, "rho": "0.0025452863403046", "lambda": "0.76055524294058", "face": ["-0.125", "-0.25", "-0.4375", "0.375"], "active": [True, True, True], "printed": {"reduced_T": 1e-16, "slsqp_T": 1.7e-14, "rho": 3.7e-11, "lambda": 7.1e-12, "T_at_printed_rho_above": 2e-18}, "gap": "0.00195366779092488", "ledger": [155, 2e-14, 2e-16]}, "records_claim": {"csv": [9, True, True], "state": [[127, 131], OUTWARD], "state_matches": [True, True, True, True, True], "role": "BALANCED_NEAR_TRUE_OVERLAP_GERM", "next": "BCODR-LUC-04 — True Overlap Germ Tangent Decomposition", "rows_match_reduction": True, "heuristic": {"127": 144, "104": 144, "103": 144}}, "verifier_facts": {"lines": 46, "reads": 1, "fails": 11, "constants": ["0.04", "155", "1e-6", "1e-8", "[127, 131]"], "geometry": False}, "package_claim": {"digests": {"paper_sha256": True, "ledger_sha256": True, "csv_sha256": True, "plot_sha256": True, "verifier_sha256": True, "state_sha256": True}, "plot_present": True, "manifest": True, "utf8": True, "delimiters": ["PASS", []], "replay": ["PASS", "balanced true-overlap germs = [127, 131]", "outward-limited selected cells = [166, 167, 164, 165, 101, 104, 103]", "root131 T_true = 0.04733334989273121", "root127 T_true = 0.12695366779094175", "root127 provenance = 155"]}, } def sig(x, n=2): return float(f"{float(x):.{n - 1}e}") def w1_times(w): """T_box: the ledger's against the exact (its T+ carries LUC 01's ray grid); T_true: the ledger's against 40 digits; the gaps; T_true >= T_box everywhere; for the seven outward-limited parents the gap is exactly zero, and the ledger's negative raw gaps are its T_box's excess over the exact T+""" sm, rows = w["summary"], {r["parent"]: r for r in w["ledger"]["rows"]} with mp.workdps(DPS): tbox = max(abs(float(sm[P]["T_box"]) - rows[P]["T_box"]) for P in PARENTS) ttrue = max(abs(float(sm[P]["T"]) - rows[P]["T_true"]) for P in PARENTS) zero = sorted(P for P in PARENTS if abs(sm[P]["gap"]) < mp.mpf(TIE)) grid = max(abs(rows[P]["raw_numerical_gap"] + (rows[P]["T_box"] - float(sm[P]["T_box"]))) for P in zero) got = {"T_box": sig(tbox, 1), "T_true": sig(ttrue, 1), "theorem": all(sm[P]["gap"] > -mp.mpf(TIE) for P in PARENTS), "zero_gap": zero, "negative_raw": sorted(P for P in PARENTS if rows[P]["raw_numerical_gap"] < 0), "raw_is_grid": sig(grid, 1), "gaps": {str(P): mp.nstr(sm[P]["gap"], 15) for P in PARENTS if P not in zero}} w["w1"] = got return [] if got == w["times_claim"] else [f"the times: {got}"] def w2_modes(w): """the mode from the optimal mu: 1/2 exactly at 131 (a midpoint), 0.2394... at 127, 1 for the seven; d+ = d- at the balanced points; at the outward-limited ones the earliest box is strictly inside the radius""" sm, rows, L = w["summary"], {r["parent"]: r for r in w["ledger"]["rows"]}, w["ledger"] with mp.workdps(DPS): modes = {str(P): sm[P]["mode"] for P in PARENTS} equal = all(abs(mp.mpf(sm[P]["best"]["dplus"]) - mp.mpf(sm[P]["best"]["dminus"][str(sm[P]["first"][0])])) < mp.mpf(MU_TOL) for P in PARENTS if sm[P]["mode"] == "BALANCED_BOTH_ACTIVE") inside = min(sm[P]["T"] - min(mp.mpf(v) for v in sm[P]["best"]["dminus"].values()) for P in PARENTS if sm[P]["mode"] == "OUTWARD_LIMITED") got = {"modes": modes, "ledger": all(rows[P]["true_overlap_mode"] == sm[P]["mode"] for P in PARENTS), "mu": {"131": mp.nstr(sm[131]["mu"], 6), "127": mp.nstr(sm[127]["mu"], 6)}, "balanced": sorted(P for P in PARENTS if sm[P]["mode"] == "BALANCED_BOTH_ACTIVE"), "ledger_balanced": sorted(L["selected_balanced_germs"]), "ledger_outward": L["selected_outward_limited"] == [P for P in PARENTS if sm[P]["mode"] == "OUTWARD_LIMITED"], "balanced_equal": equal, "outward_inside": sig(inside)} w["w2"] = got return [] if got == w["modes_claim"] else [f"the modes: {got}"] def w3_provenance(w): """the earliest boxes and the next, with every exact tie; the resolved margins against the ledger's; at 101, 103 and 104 four boxes tie exactly, and the ledger's 28 and its margins of 1e-13 are noise""" sm, rows = w["summary"], {r["parent"]: r for r in w["ledger"]["rows"]} with mp.workdps(DPS): resolved = [P for P in PARENTS if len(sm[P]["first"]) == 1] got = {"first": {str(P): sm[P]["first"] for P in PARENTS}, "second": {str(P): sm[P]["second"] for P in PARENTS}, "ledger_first_in_ties": all(rows[P]["true_provenance"] in sm[P]["first"] for P in PARENTS), "ledger_second_in_ties": all(rows[P]["second_provenance"] in (sm[P]["second"] if len(sm[P]["first"]) == 1 else sm[P]["first"]) for P in PARENTS), "margins": sig(max(abs(float(sm[P]["margin"]) - rows[P]["provenance_margin"]) for P in resolved), 1), "degenerate_ledger_margins": [sig(rows[P]["provenance_margin"], 2) for P in PARENTS if len(sm[P]["first"]) > 1], "next_after_ties": {str(P): mp.nstr(sm[P]["margin"], 6) for P in PARENTS if len(sm[P]["first"]) > 1}, "164_second": mp.nstr(sm[164]["second_T"], 20), "sqrt_5_32": mp.nstr(mp.sqrt(mp.mpf(5) / 32), 20)} w["w3"] = got return [] if got == w["provenance_claim"] else [f"the provenance: {got}"] def w4_root131(w): """131: mu = 1/2, so the meeting point is the midpoint of the ray point and its nearest point of 155, and T_true is half the ray's distance to 155; the midpoint lies in 131. 144 comes next with mu = 0: at the distance from 131 to 144 itself, sqrt 2 / 8 (1/8 in rho5 and in y5) - which the ledger's second time undercuts by 1e-12, so its optimizer left the box""" sm, s = w["summary"], w["search"]["true"] r131, row = w["ledger"]["root131_correction"], next(r for r in w["ledger"]["rows"] if r["parent"] == 131) with mp.workdps(DPS): b = sm[131]["best"] lo, hi = s["boxes"]["131"] ql, qh = s["boxes"]["144"] gaps = [max(0, ql[k] - hi[k], lo[k] - qh[k]) for k in range(5)] got = {"mu_half": abs(sm[131]["mu"] - mp.mpf(1) / 2) < mp.mpf(MU_TOL), "half_ray_to_155": abs(sm[131]["T"] - mp.mpf(s["ray_to"]["155"]) / 2) < mp.mpf(TIE), "inside_131": all(lo[k] <= float(b["z"][k]) <= hi[k] for k in range(5)), "T": mp.nstr(sm[131]["T"], 16), "ledger": [sig(abs(r131["T_true"] - float(sm[131]["T"])), 1), r131["midpoint_error"]], "second_144": [sm[131]["second"], mp.mpf(s["pairs"]["131"]["144"]["mu"]) == 0, gaps, abs(sm[131]["second_T"] - mp.sqrt(2) / 8) < mp.mpf(TIE)], "ledger_second_below_bound": sig(mp.sqrt(2) / 8 - mp.mpf(row["second_T_true"]), 2), "rho": mp.nstr(mp.mpf(b["rho"]), 10)} w["w4"] = got return [] if got == w["root131_claim"] else [f"root 131: {got}"] def w5_root127(w): """the one-dimensional reduction gives the 5-D value; its active set holds; the printed reduced T is right to its 15 digits, the 5-D one (sec. 9) is 1.7e-14 high, and the printed r* and lambda* are right only to about 1e-11 - the minimum is flat in r""" sm, red, R = w["summary"], w["search"]["reduction"], w["ledger"]["root127_reduction"] with mp.workdps(DPS): T5, Tr = sm[127]["T"], mp.mpf(red["T"]) b5 = sm[127]["best"] got = {"reduction_is_5d": abs(T5 - Tr) < mp.mpf(TIE), "T": mp.nstr(T5, 20), "lambda_is_1_minus_mu": abs(mp.mpf(red["lambda"]) - (1 - sm[127]["mu"])) < mp.mpf("1e-15"), "rho": mp.nstr(mp.mpf(red["r"]), 14), "lambda": mp.nstr(mp.mpf(red["lambda"]), 14), "face": [red["faces"]["r1"][:6], red["faces"]["q1"][:5], red["faces"]["q3"][:7], red["faces"]["q5"][:5]], "active": [red["inside_127"], red["y3_x5_inside_155"], abs(mp.mpf(b5["z"][0]) - mp.mpf(red["faces"]["r1"])) < mp.mpf(TIE)], "printed": {"reduced_T": sig(abs(mp.mpf("0.126953667790925") - Tr), 1), "slsqp_T": sig(mp.mpf("0.126953667790942") - Tr, 2), "rho": sig(abs(mp.mpf(RHO_DOC) - mp.mpf(red["r"])), 2), "lambda": sig(abs(mp.mpf(LAMBDA_DOC) - mp.mpf(red["lambda"])), 2), "T_at_printed_rho_above": sig(mp.mpf(red["T_at_doc_rho"]) - T5, 1)}, "gap": mp.nstr(T5 - mp.mpf(1) / 8, 15), "ledger": [R["true_provenance"], sig(abs(R["T_true"] - float(T5)), 1), sig(abs(R["reduced_T"] - float(T5)), 1)]} w["w5"] = got return [] if got == w["root127_claim"] else [f"root 127: {got}"] def w6_records(w): L, st = w["ledger"], w["state"] text = w["csv"] rows = list(csv.DictReader(io.StringIO(text.lstrip("")))) num = lambda v: int(v) if re.fullmatch(r"-?\d+", v) else float(v) if re.fullmatch(r"-?[\d.]+(e-?\d+)?", v) else v same = len(rows) == len(L["rows"]) and all(num(r[k]) == x[k] for r, x in zip(rows, L["rows"]) for k in r) r127 = L["root127_reduction"] got = {"csv": [len(rows), same, text.startswith("")], "state": [sorted(st["balanced_selected_germs"]), st["outward_limited_selected"]], "state_matches": [sorted(st["balanced_selected_germs"]) == sorted(L["selected_balanced_germs"]), st["outward_limited_selected"] == L["selected_outward_limited"], st["root127"]["T_true"] == r127["T_true"], st["root127"]["T_box"] == r127["T_box"], st["root127"]["provenance_margin"] == r127["provenance_margin"]], "role": st["root127"]["role"], "next": st["next"], "rows_match_reduction": next(r for r in L["rows"] if r["parent"] == 127)["T_true"] == r127["T_true"], "heuristic": {str(r["parent"]): r["heuristic_nearest_prune"] for r in L["rows"] if r["heuristic_nearest_prune"] != r["true_provenance"]}} w["w6"] = got return [] if got == w["records_claim"] else [f"the records: {got}"] def w7_verifier(w): """read after the rebuild and never run: it reads the ledger alone and checks its numbers against each other - T_true against T_box, the distances against T_true - and three facts as constants; it computes no distance""" code = w["verifier"] got = {"lines": code.count("\n"), "reads": len(re.findall(r"json\.load\(", code)), "fails": len(re.findall(r"raise SystemExit\(f?\"FAIL", code)), "constants": sorted(set(re.findall(r"!= (\[127, 131\]|155)|> (0\.04|1e-6|1e-8)", code)), key=str), "geometry": bool(re.search(r"center|halfwidth|subroot|sqrt|cos\(", code))} got["constants"] = sorted({a or b for a, b in got["constants"]}) w["w7"] = 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() keys = {"paper_sha256": DOC, "ledger_sha256": LEDGER, "csv_sha256": CSV, "plot_sha256": PLOT, "verifier_sha256": VERIFIER, "state_sha256": STATE} body = B[DOC].decode("utf-8") got = {"digests": {k: v[k] == sha(B[f]) for k, f in keys.items()}, "plot_present": v["plot_present"], "manifest": all(w["manifest_rows"][k][2] == sha(b) for k, b in B.items()), "utf8": v["utf8"] is True, "delimiters": [v["math_delimiters"], sorted(set(re.findall(r"\\\(|\\\)|\\\[|\\\]", body)))], "replay": v["fresh_replay_stdout"].split("\n")} w["p1"] = got return [] if got == w["package_claim"] else [f"the package: {got}"] 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] CHECKS = {"A0": a0_anchors, "W1": w1_times, "W2": w2_modes, "W3": w3_provenance, "W4": w4_root131, "W5": w5_root127, "W6": w6_records, "W7": w7_verifier, "P1": p1_package} DEPENDS = {"A0": {"text"}, "W1": {"summary", "ledger", "times_claim"}, "W2": {"summary", "ledger", "modes_claim"}, "W3": {"summary", "ledger", "provenance_claim"}, "W4": {"summary", "search", "ledger", "root131_claim"}, "W5": {"summary", "search", "ledger", "root127_claim"}, "W6": {"ledger", "state", "csv", "records_claim"}, "W7": {"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, L, s = base["text"], base["ledger"], base["search"] row = base["csv"].split("\n") lrow = lambda x, P: next(r for r in x["rows"] if r["parent"] == P) def untie(x): with mp.workdps(DPS): t = x["true"]["pairs"]["101"]["68"] t["T"] = mp.nstr(mp.mpf(t["T"]) + mp.mpf("1e-20"), 32) return [ ("K0-unmodified", "control", {}, set()), ("K1-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()), ("K2-validation-keys-sorted", "control", {"validation": json.loads(json.dumps(base["validation"], sort_keys=True))}, set()), ("K3-ledger-keys-sorted", "control", {"ledger": json.loads(json.dumps(L, sort_keys=True))}, set()), ("M1-text-reduced-T", "mutation", {"text": text.replace("0.126953667790925.", "0.126953667790926.")}, {"A0"}), ("M2-T-true", "mutation", {"ledger": edit(L, lambda x: lrow(x, 165).update(T_true=0.3661670813))}, {"W1", "W6"}), ("M3-raw-gap", "mutation", {"ledger": edit(L, lambda x: lrow(x, 101).update(raw_numerical_gap=-2e-9))}, {"W1", "W6"}), ("M4-mode", "mutation", {"ledger": edit(L, lambda x: lrow(x, 164).update(true_overlap_mode="BALANCED_BOTH_ACTIVE"))}, {"W2", "W6"}), ("M5-mu", "mutation", {"summary": edit(base["summary"], lambda x: x[166].update(mode="BALANCED_BOTH_ACTIVE"))}, {"W2"}), ("M6-provenance", "mutation", {"ledger": edit(L, lambda x: lrow(x, 165).update(true_provenance=144))}, {"W3", "W6"}), ("M7-tie", "mutation", {"summary": summary(edit(s, untie))}, {"W3"}), ("M8-midpoint", "mutation", {"search": edit(s, lambda x: x["true"]["ray_to"].update({"155": "0.0946666997839"}))}, {"W4"}), ("M9-131-box", "mutation", {"search": edit(s, lambda x: x["true"]["boxes"]["131"][0].__setitem__(0, -0.2))}, {"W4"}), ("M10-reduction", "mutation", {"search": edit(s, lambda x: x["reduction"].update(T="0.1269536677909250"))}, {"W5"}), ("M11-active", "mutation", {"search": edit(s, lambda x: x["reduction"].update(y3_x5_inside_155=False))}, {"W5"}), ("M12-csv-value", "mutation", {"csv": "\n".join(row[:2] + [row[2].replace(",155,144,", ",155,68,", 1)] + row[3:])}, {"W6"}), ("M13-state", "mutation", {"state": edit(base["state"], lambda x: x["root127"].update(provenance_margin=0.042))}, {"W6"}), ("M14-verifier-geometry", "mutation", {"verifier": base["verifier"] + "\nimport math\nd = math.sqrt(2)\n"}, {"W7"}), ("M15-validation-digest", "mutation", {"validation": {**base["validation"], "ledger_sha256": "0" * 64}}, {"P1"}), ("M16-paper-bytes", "mutation", {"bytes": {**base["bytes"], DOC: base["bytes"][DOC] + b" "}}, {"P1"}), ] def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() inputs = load_inputs() search = searches(inputs) base = {**inputs, "search": search, "summary": summary(search)} 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", "w7", "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) summ = gate.summarize(d, CHECKS) print(gate.report_drill(summ)) 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-065", "subject": "BCODR LUC 03: the true common-point overlap time of the nine frontier parents", "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", "w7", "p1")}, "drill": summ} LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=float) + "\n", encoding="utf-8") if __name__ == "__main__": main()