# -*- coding: utf-8 -*- """ PHASE 4 — INDEPENDENT re-verification of all claimed artifacts. Reads ONLY the emitted JSON artifacts (no shared state with the construction code), re-parses every expression from strings, and re-verifies every claim with fresh randomness. This is the second oracle of the dual-path discipline. Checks: A. degree3_counterexample.json: 1. dimension/variable consistency 2. every H_k = F_k - v_k has only terms of total degree in [2,3] 3. J(0) == I 4. det J == 1 at 40 NEW random rational points (exact arithmetic, fresh seed) 5. Schwartz-Zippel line probes: det restricted to 3 random rational lines, sampled at 60 points each (a degree-<=B univariate poly that is 1 at B+1 points is identically 1 on the line) 6. three collision points: pairwise distinct, images identical (dual eval paths) B. dixmier_certificate.json: 7. re-verify det J_F = -2, collision, G*J^T = I, all 27 commutation identities C. base map: re-verify from an INDEPENDENT encoding (raw expanded monomial form, typed separately from the factored form used everywhere else) """ import sympy as sp import json, random, time t0 = time.time() random.seed(987654321) # fresh, different from construction seed report = {"checks": [], "ALL_PASS": True} def check(label, ok): print(f"[{'PASS' if ok else 'FAIL'}] {label}") report["checks"].append({"check": label, "pass": bool(ok)}) if not ok: report["ALL_PASS"] = False return ok # ===== A. degree-3 counterexample ========================================= art = json.load(open('post-jc-program/degree3_counterexample.json', encoding='utf-8')) V = [sp.Symbol(s) for s in art["variables"]] N = len(V) F = [sp.sympify(s) for s in art["components"]] check(f"A1 dimension consistent: {N} variables, {len(F)} components", N == art["dimension"] == len(F)) ok2 = True maxdeg = 0 for k in range(N): h = sp.expand(F[k] - V[k]) if h == 0: continue p = sp.Poly(h, *V) ds = [sum(m) for m in p.monoms()] maxdeg = max(maxdeg, max(ds)) if min(ds) < 2 or max(ds) > 3: ok2 = False check(f"A2 every H_k has terms only of degree 2..3 (max found: {maxdeg})", ok2 and maxdeg == 3) Fm = sp.Matrix(F) Jbig = Fm.jacobian(V) zero = {v: 0 for v in V} check("A3 J(0) == Identity", Jbig.subs(zero) == sp.eye(N)) ok4 = True for _ in range(40): sub = {v: sp.Rational(random.randint(-9, 9), random.randint(1, 6)) for v in V} if Jbig.subs(sub).det() != 1: ok4 = False; break check("A4 det J == 1 at 40 fresh random rational points (exact)", ok4) # A5: line probes. det(J(p + t*q)) is a univariate polynomial in t of degree # <= sum over rows of max entry degree <= 2*N. Sample 60 >= 2N+1 = 45 points. ok5 = True t = sp.Symbol('t') for line in range(3): p0 = [sp.Rational(random.randint(-5, 5), random.randint(1, 4)) for _ in V] q0 = [sp.Rational(random.randint(-5, 5), random.randint(1, 4)) for _ in V] for tv in range(60): tq = sp.Rational(tv - 30, 7) sub = {V[i]: p0[i] + tq * q0[i] for i in range(N)} if Jbig.subs(sub).det() != 1: ok5 = False; break if not ok5: break check("A5 det J == 1 on 3 random lines x 60 exact samples (degree bound 2N=44 < 60)", ok5) pts = [[sp.sympify(c) for c in p] for p in art["collision_points"]] check("A6a collision points pairwise distinct", len({tuple(p) for p in pts}) == 3) imA = [tuple(sp.expand(c.subs(dict(zip(V, p)))) for c in F) for p in pts] imB = [tuple(sp.expand(c.xreplace(dict(zip(V, p)))) for c in F) for p in pts] check("A6b images identical across all 3 points (subs)", imA[0] == imA[1] == imA[2]) check("A6c images identical across all 3 points (xreplace)", imB[0] == imB[1] == imB[2]) check("A6d dual paths agree and match artifact's recorded image", imA == imB and [str(c) for c in imA[0]] == art["collision_image"]) # ===== B. Dixmier certificate ============================================= x, y, z = sp.symbols('x y z') X3 = [x, y, z] cert = json.load(open('post-jc-program/dixmier_certificate.json', encoding='utf-8')) Fb = [sp.sympify(s) for s in cert["base_map_F"]] Jb = sp.Matrix(Fb).jacobian(X3) check("B1 base map det J == -2 identically", sp.expand(Jb.det()) == -2) G = sp.Matrix([[sp.sympify(cert["witness_G_rows_are_phi_d_coeffs"][j][k]) for k in range(3)] for j in range(3)]) check("B2 (R1) G * J^T == I (full expansion)", all(e == 0 for e in (G * Jb.T - sp.eye(3)).applyfunc(sp.expand))) ok_r3 = True for i in range(3): for j in range(i + 1, 3): for l in range(3): s = sp.expand(sum(G[i, k]*sp.diff(G[j, l], X3[k]) - G[j, k]*sp.diff(G[i, l], X3[k]) for k in range(3))) if s != 0: ok_r3 = False check("B3 (R3) all 27 Weyl commutation identities == 0 (full expansion)", ok_r3) # ===== C. base map from an independent raw encoding ======================== raw1 = z + 3*x*y*z + 3*x**2*y**2*z + x**3*y**3*z + 4*y**2 + 7*x*y**3 + 3*x**2*y**4 raw2 = y + 3*x*z + 6*x**2*y*z + 3*x**3*y**2*z + 12*x*y**2 + 9*x**2*y**3 raw3 = 2*x - 3*x**2*y - x**3*z f1 = (1 + x*y)**3 * z + y**2 * (1 + x*y) * (4 + 3*x*y) f2 = y + 3*x*(1 + x*y)**2 * z + 3*x*y**2 * (4 + 3*x*y) check("C1 independent raw-monomial encoding == factored encoding", sp.expand(raw1 - f1) == 0 and sp.expand(raw2 - f2) == 0 and sp.expand(raw3 - f3) == 0 if (f3 := 2*x - 3*x**2*y - x**3*z) is not None else False) Jraw = sp.Matrix([raw1, raw2, raw3]).jacobian(X3) check("C2 raw encoding: det J == -2 identically", sp.expand(Jraw.det()) == -2) p1 = {x: 0, y: 0, z: sp.Rational(-1, 4)} p2 = {x: 1, y: sp.Rational(-3, 2), z: sp.Rational(13, 2)} p3 = {x: -1, y: sp.Rational(3, 2), z: sp.Rational(13, 2)} ims = [tuple(sp.expand(e.subs(p)) for e in (raw1, raw2, raw3)) for p in (p1, p2, p3)] check("C3 raw encoding: 3-point collision", ims[0] == ims[1] == ims[2]) report["elapsed_sec"] = round(time.time() - t0, 2) json.dump(report, open('post-jc-program/verification_report.json', 'w', encoding='utf-8'), indent=2) print() print("=" * 66) print(f"INDEPENDENT VERIFICATION: ALL_PASS = {report['ALL_PASS']} ({report['elapsed_sec']}s)") print("artifact: verification_report.json")