From 4e7599f6c67ca0a965ed8954b6cf380f660641c4 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:51:18 -0400 Subject: [PATCH 1/4] WIP: zero-exclusion proof audit checker --- research/zero-exclusion-proof-audit/README.md | 35 +++ .../zero-exclusion-proof-audit/SOURCES.json | 18 ++ research/zero-exclusion-proof-audit/TASK.json | 60 +++++ .../zero-exclusion-proof-audit/VERIFY.json | 18 ++ .../binding_crosscheck.py | 178 ++++++++++++++ research/zero-exclusion-proof-audit/verify.py | 220 ++++++++++++++++++ 6 files changed, 529 insertions(+) create mode 100644 research/zero-exclusion-proof-audit/README.md create mode 100644 research/zero-exclusion-proof-audit/SOURCES.json create mode 100644 research/zero-exclusion-proof-audit/TASK.json create mode 100644 research/zero-exclusion-proof-audit/VERIFY.json create mode 100644 research/zero-exclusion-proof-audit/binding_crosscheck.py create mode 100644 research/zero-exclusion-proof-audit/verify.py diff --git a/research/zero-exclusion-proof-audit/README.md b/research/zero-exclusion-proof-audit/README.md new file mode 100644 index 0000000000..ff0bf63080 --- /dev/null +++ b/research/zero-exclusion-proof-audit/README.md @@ -0,0 +1,35 @@ +# zero-exclusion-proof-audit + +**Draft; no new bound claimed.** + +## Scope and evidence + +Original card: `formal-interface-lemma`. Complete [TASK.json](TASK.json), including any scope +change and its connection to the bottleneck. Explain the result and limitations here. +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue are historical provenance, so later priority +updates do not invalidate this package. Explicit --source files are live inputs +and must match their pins. Full Git history is needed to resolve provenance. + +## Reproduce + +After completing the verifier and marking VERIFY.json ready, from repo root: + +```sh +python3 scripts/research_package.py --package research/zero-exclusion-proof-audit --check-only +python3.12 scripts/research_package.py --package research/zero-exclusion-proof-audit +``` + +Declare all external inputs and pinned dependencies in VERIFY.json. The generic +hook is bounded; native/Lean or long replays need an explicit dedicated workflow. + +## Open next questions + +Complete the structured `open_questions` list in TASK.json and explain it here: +the question, why it matters, a feasible first step and any blocker. If no next +question is justified, say so rather than inventing one. + +## Credit + +Prepared by Josie Elliston (with Claude Opus 5.5). Retain predecessor attribution and source-specific notices. +New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. diff --git a/research/zero-exclusion-proof-audit/SOURCES.json b/research/zero-exclusion-proof-audit/SOURCES.json new file mode 100644 index 0000000000..db104fb5bb --- /dev/null +++ b/research/zero-exclusion-proof-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/zero-exclusion-proof-audit/TASK.json b/research/zero-exclusion-proof-audit/TASK.json new file mode 100644 index 0000000000..0d77d21d54 --- /dev/null +++ b/research/zero-exclusion-proof-audit/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 3, + "base_commit": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "unchanged", + "actual_scope": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "scope_change_reason": null, + "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "budget_minutes": 60, + "stop_rule": "TODO", + "outcome": "in-progress", + "evidence": "TODO", + "author": "Josie Elliston (with Claude Opus 5.5)", + "ai_assistance": "TODO: disclose tools used", + "open_questions": [ + { + "question": "TODO", + "why_it_matters": "TODO", + "first_step": "TODO", + "blocked_by": "TODO" + } + ] +} diff --git a/research/zero-exclusion-proof-audit/VERIFY.json b/research/zero-exclusion-proof-audit/VERIFY.json new file mode 100644 index 0000000000..b10c894394 --- /dev/null +++ b/research/zero-exclusion-proof-audit/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "draft", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "TODO: identity, positive fixture and failure controls" + } + ] +} diff --git a/research/zero-exclusion-proof-audit/binding_crosscheck.py b/research/zero-exclusion-proof-audit/binding_crosscheck.py new file mode 100644 index 0000000000..335aba1fe6 --- /dev/null +++ b/research/zero-exclusion-proof-audit/binding_crosscheck.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""Binding cross-check: PR1650's criterion() against a second implementation of PR1560's hypotheses. + +The second implementation below is written from proof.md section 3's prose, with deliberately different methods: +classes are found by orthogonality (not by sign parity), (D) uses the exact rational rank of the integer Gram +matrix M^T M by fraction-free (Bareiss) elimination (not a modular rank of M), and (G) uses breadth-first search. +It is compared with PR1650's criterion (head d960f8a2, research/complex-rank8-rigidity-p105/verify.py), which this +script imports from a path given on the command line. PR1650 is not on main, so this script is not part of the +registered replay; its output is recorded in the README. + + python3 -I -B research/zero-exclusion-proof-audit/binding_crosscheck.py PATH/TO/PR1650/verify.py [--samples N] +""" + +import importlib.util +import itertools +import random +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as mine # noqa: E402 (this package's model: lines, G, frames) + +G, N = mine.G, mine.N + + +def bareiss_rank(A): + """Exact rank of an integer matrix by fraction-free elimination.""" + A = [row[:] for row in A] + rows, cols = len(A), len(A[0]) if A else 0 + r, prev = 0, 1 + for c in range(cols): + p = next((i for i in range(r, rows) if A[i][c]), None) + if p is None: + continue + A[r], A[p] = A[p], A[r] + for i in range(r + 1, rows): + for j in range(c + 1, cols): + A[i][j] = (A[i][j] * A[r][c] - A[i][c] * A[r][j]) // prev + A[i][c] = 0 + prev = A[r][c] + r += 1 + return r + + +def rank_q(M): + """rank over Q of a 0-1 (or integer) matrix M, as the rank of its Gram matrix M^T M.""" + if not M: + return 0 + n = len(M[0]) + gram = [[0] * n for _ in range(n)] + for row in M: + nz = [j for j in range(n) if row[j]] + for a in nz: + ga = gram[a] + for b in nz: + ga[b] += row[a] * row[b] + return bareiss_rank(gram) + + +def hypotheses(L, F, frames): + """Booleans (blocks_nonempty, W, G, D) for live set L (a set of line IDs), pivot frame F (tuple of IDs) and + the family of all live frames, straight from proof.md section 3.""" + Fs = set(F) + S_all = [S for S in frames if set(S) <= L] + non = sorted(L - Fs) + T = {i: tuple(k for k in F if G[i][k]) for i in non} + blocks = {} + for i in non: + blocks.setdefault(T[i], []).append(i) + nonempty = len(blocks) == 14 + # (W): a block is witnessed when one class is complete (all 4 lines live) and the other has a live line. + # Classes by orthogonality among ALL 8 lines of the block (live or not). + witnessed_pairs = set() + allblocks = {} + for i in range(N): + if i not in Fs: + allblocks.setdefault(tuple(k for k in F if G[i][k]), []).append(i) + for t, lines in allblocks.items(): + a = lines[0] + c1 = [i for i in lines if i == a or G[a][i] == 0] # a and the lines orthogonal to it + c2 = [i for i in lines if i not in c1] + for C, D in ((c1, c2), (c2, c1)): + if all(i in L for i in C) and any(j in L for j in D): + witnessed_pairs.update(itertools.combinations(t, 2)) + W = len(witnessed_pairs) == 28 + # (G) + Gok = True + for k, l in itertools.combinations(F, 2): + I = [i for i in non if G[i][k] and G[i][l]] + if not I: + Gok = False + break + Iset = set(I) + adj = {i: set() for i in I} + for S in S_all: + hit = [i for i in S if i in Iset] + if len(hit) == 2: + adj[hit[0]].add(hit[1]) + adj[hit[1]].add(hit[0]) + seen, todo = {I[0]}, [I[0]] + while todo: + for j in adj[todo.pop()] - seen: + seen.add(j) + todo.append(j) + if len(seen) != len(I): + Gok = False + break + # (D) + Dok = True + for k in F: + I = [i for i in non if G[i][k]] + h = [[G[i][k] * G[i][l] for i in I] for l in F if l != k] + if rank_q(h) != 7: + Dok = False + break + rows = {tuple(1 if i in S else 0 for i in I) for S in S_all} + if rank_q(sorted(rows)) != len(I) - 7: + Dok = False + break + return nonempty, W, Gok, Dok + + +def load_pr1650(path): + spec = importlib.util.spec_from_file_location('pr1650_verify', path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def main(): + path = sys.argv[1] + samples = int(sys.argv[sys.argv.index('--samples') + 1]) if '--samples' in sys.argv else 60 + pr = load_pr1650(path) + assert pr.LINES == mine.V and pr.G == mine.G, 'line IDs / G disagree' + frames = mine.all_frames() + assert sorted(frames) == sorted(pr.FRAMES) + F0 = set(pr.FRAME0) + P112 = [i for i in range(N) if i not in F0] + rng = random.Random(1560) + cases = [ + ('pr1560-fixture', (32, 45, 73, 78, 88), (2, 5, 8, 9, 30, 41, 108, 117)), + ('pr1560-bad-control', (3, 13, 14, 22, 23), (2, 5, 8, 9, 30, 41, 108, 117)), + ('s13-full-family-g-without-d', (3, 4, 8, 9, 107, 108, 117, 118), (19, 25, 37, 47, 67, 82, 94, 115)), + ] + for n in range(samples): + size = rng.choice([5, 6, 7, 8, 9, 10]) + X = tuple(sorted(rng.sample(P112, size))) + live = set(P112) - set(X) + cand = [S for S in frames if set(S) <= live] + if cand: + cases.append((f'random-{n}-P{112 - size}', X, rng.choice(cand))) + # Every live frame as pivot for a few deletion sets: early frames fail blocks / (W), as in PR1650's tally. + for n in range(max(1, samples // 200)): + X = tuple(sorted(rng.sample(P112, 7 + n % 4))) + live = set(P112) - set(X) + cases += [(f'allframes-{n}', X, S) for S in frames if set(S) <= live] + tally = {} + t0 = time.time() + for name, X, F in cases: + reason, _ = pr.criterion(X, F) + L = set(P112) - set(X) + ne, W, Gk, Dk = hypotheses(L, F, frames) + # PR1650 tests in the order support, nonempty-blocks, W, G, D and stops at the first failure. + expect = None if (ne and W and Gk and Dk) else \ + 'nonempty-blocks' if not ne else 'W' if not W else 'G' if not Gk else 'D' + ok = reason == expect + tally[(reason, ok)] = tally.get((reason, ok), 0) + 1 + if name[:6] != 'random' or not ok: + print(f"{'AGREE' if ok else 'DISAGREE'} {name}: PR1650 {reason}; prose (blocks, W, G, D) = {ne, W, Gk, Dk}") + if not ok: + sys.exit(1) + print('tally (PR1650 verdict, agree):', dict(sorted(tally.items(), key=str))) + print(f'ALL_AGREE {len(cases)} cases in {time.time() - t0:.0f} s') + + +if __name__ == '__main__': + main() diff --git a/research/zero-exclusion-proof-audit/verify.py b/research/zero-exclusion-proof-audit/verify.py new file mode 100644 index 0000000000..881b844f8c --- /dev/null +++ b/research/zero-exclusion-proof-audit/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Finite E8 facts used implicitly by PR1560's proof of Theorem 1 and Corollary 2, checked for EVERY pivot frame. + +PR1560 (an664) proves a structural zero-exclusion criterion for a pivot frame F of the 120 doubled E8 lines. +Its proof (proof.md sections 2, 4 and 6) silently uses several facts about the lines relative to F. PR1560's own +checker establishes them only for its fixed pivot; PR1616 and PR1650 apply the theorem at hundreds of other pivots. +This file was written from proof.md's prose alone (it does not import or read PR1560's, PR1616's or PR1650's +code) and checks, for all 2025 frames F: + + E1 expansion: 2 v_i = sum_{k in F} G_ik v_k for every line i (gives identity (6) and sum_k G_ik G_jk = 2 G_ij); + E2 pivot rows: G_fk = 2 delta_fk; every nonpivot row has G_ik in {0, +1, -1} and |T_i| = 4; + E3 blocks: exactly 14 supports occur, each carried by exactly 8 lines, and they form a Steiner system + S(3,4,8) on F (every triple of pivots in exactly one block); + E4 classes: in each block the sign product prod_{k in T} eps_ik splits the 8 lines 4 + 4; lines in one class + are mutually orthogonal, lines in opposite classes have G = +-1, and class + (F minus T) is a frame; + E5 Hadamard: for every class C and k in T, the rows (1, s_i), i in C, satisfy H H^T = 4 I; + E6 the 4+1 step (section 4.3): for every block, class C, distinguished k, exceptional row i0 in C and line j of + the opposite class, the three signs s_{i0,l} s_{j,l} have product -1 and the shared diagonal formula with + c_kl = s_{i0,l}/4 predicts w_j in {1/2, -1/2}, a value that is neither root 0 nor 1 of x^2 - x; + E7 the class-sum dichotomy: four values in {x, 1-x} summing to 1 are all 1/4 or a permutation of (1,0,0,0) + (exact over Q for the case analysis m = 0..4 used in section 4.3); + E8 the gauge corollary's last step: for nonpivot i, j, sum_{k in F} eps_ik eps_jk = 2 G_ij (E1 restated on rows). + +Standard library only, exact integer / Fraction arithmetic. Run from the repository root: + + python3 -I -B research/zero-exclusion-proof-audit/verify.py [--controls-only] +""" + +import itertools +import sys +from fractions import Fraction + +RESULTS = [] + + +def check(tag, cond, info=''): + RESULTS.append(tag) + print(f"{'PASS' if cond else 'FAIL'} {tag}" + (f': {info}' if info else ''), flush=True) + if not cond: + print(f'FAIL_ZERO_EXCLUSION_PROOF_AUDIT: {tag}') + sys.exit(1) + + +# ------------------------------------------------------------------ the model, from proof.md section 2's prose + +def doubled_lines(): + """Doubled E8 roots (squared length 8) with first nonzero coordinate positive, sorted lexicographically.""" + out = set() + for a, b in itertools.combinations(range(8), 2): + for sa in (2, -2): + for sb in (2, -2): + v = [0] * 8 + v[a], v[b] = sa, sb + out.add(tuple(v)) + for signs in itertools.product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + out.add(signs) + return sorted(v for v in out if next(x for x in v if x) > 0) + + +V = doubled_lines() +N = len(V) + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +GRAM = [[dot(V[i], V[j]) for j in range(N)] for i in range(N)] +G = [[g // 4 for g in row] for row in GRAM] + + +def all_frames(): + """Every 8-clique of the orthogonality graph, by increasing-ID recursion (each visited once).""" + out = [] + + def grow(cur, cand): + if len(cur) == 8: + out.append(tuple(cur)) + return + for n, j in enumerate(cand): + grow(cur + [j], [k for k in cand[n + 1:] if G[j][k] == 0]) + + grow([], list(range(N))) + return out + + +def facts_at(F, frameset): + """Check E1-E6 and E8 at pivot frame F. Returns a count tuple, or a string naming the first failure.""" + # E1 (and E8): the expansion of every line in the orthogonal basis F. + for i in range(N): + for c in range(8): + if 2 * V[i][c] != sum(G[i][k] * V[k][c] for k in F): + return f'E1 line {i}' + # E2: pivot rows and nonpivot supports. + supp = {} + for i in range(N): + row = [G[i][k] for k in F] + if i in F: + if row != [2 if k == i else 0 for k in F]: + return f'E2 pivot {i}' + continue + if any(g not in (0, 1, -1) for g in row): + return f'E2 values {i}' + T = tuple(n for n in range(8) if row[n]) + if len(T) != 4: + return f'E2 support {i}' + supp.setdefault(T, []).append(i) + # E3: 14 blocks of 8 lines, a Steiner system S(3,4,8). + if len(supp) != 14 or any(len(v) != 8 for v in supp.values()): + return 'E3 blocks' + for tri in itertools.combinations(range(8), 3): + if sum(set(tri) <= set(T) for T in supp) != 1: + return f'E3 triple {tri}' + n_e6 = 0 + for T, lines in supp.items(): + eps = {i: {k: G[i][F[k]] for k in T} for i in lines} + prod = {i: eps[i][T[0]] * eps[i][T[1]] * eps[i][T[2]] * eps[i][T[3]] for i in lines} + classes = [[i for i in lines if prod[i] == 1], [i for i in lines if prod[i] == -1]] + # E4: 4 + 4, orthogonal inside a class, G = +-1 across, class + (F minus T) is a frame. + if sorted(map(len, classes)) != [4, 4]: + return f'E4 sizes {T}' + for C in classes: + if any(G[a][b] for a, b in itertools.combinations(C, 2)): + return f'E4 orthogonal {T}' + if tuple(sorted(C + [F[n] for n in range(8) if n not in T])) not in frameset: + return f'E4 frame {T}' + if any(abs(G[a][b]) != 1 for a in classes[0] for b in classes[1]): + return f'E4 across {T}' + for C, D in (classes, classes[::-1]): + for k in T: + rest = [l for l in T if l != k] + s = {i: [eps[i][k] * eps[i][l] for l in rest] for i in lines} + # E5: Hadamard rows (1, s_i) for i in C. + H = [[1] + s[i] for i in C] + if any(dot(H[a], H[b]) != (4 if a == b else 0) for a in range(4) for b in range(4)): + return f'E5 {T} {k}' + # E6: exceptional row i0 and opposite-class line j. + for i0 in C: + c = [Fraction(x, 4) for x in s[i0]] + # the coefficients are the unique solution of the shared formula with w = e_{i0} on C + for i in C: + w = Fraction(1, 4) + sum(cl * x for cl, x in zip(c, s[i])) + if w != (1 if i == i0 else 0): + return f'E6 solve {T} {k} {i0}' + for j in D: + p = s[i0][0] * s[j][0] * s[i0][1] * s[j][1] * s[i0][2] * s[j][2] + w = Fraction(1, 4) + sum(cl * x for cl, x in zip(c, s[j])) + if p != -1 or w not in (Fraction(1, 2), Fraction(-1, 2)) or w * w - w == 0: + return f'E6 {T} {k} {i0} {j}' + n_e6 += 1 + # E8: the identity used for nonpivot pairs in Corollary 2. + non = [i for i in range(N) if i not in F] + for i, j in itertools.combinations(non, 2): + if sum(G[i][k] * G[j][k] for k in F) != 2 * G[i][j]: + return f'E8 {i} {j}' + return (len(supp), n_e6) + + +def dichotomy(): + """E7: solve m x + (4 - m)(1 - x) = 1 for m = 0..4, where m counts the values equal to x (a root of + x^2 - x + q) and the rest equal 1 - x. Returns the set of possible sorted 4-tuples of values.""" + out = set() + for m in range(5): + # (2m - 4) x = 1 - (4 - m) + a, b = 2 * m - 4, 1 - (4 - m) + if a == 0: + if b == 0: + return None # would leave x free: not the case + continue + x = Fraction(b, a) + out.add(tuple(sorted([x] * m + [1 - x] * (4 - m)))) + return out + + +def main(): + controls_only = '--controls-only' in sys.argv[1:] + check('model.lines', N == 120 and len(V) == len(set(V)) and all(dot(v, v) == 8 for v in V), + '120 doubled lines of squared length 8') + check('model.gram', all(GRAM[i][j] % 4 == 0 for i in range(N) for j in range(N)) + and {G[i][j] for i in range(N) for j in range(N) if i != j} == {-1, 0, 1}, 'G = /4 in {0, +-1} off the diagonal') + frames = all_frames() + frameset = set(frames) + F0 = (0, 1, 6, 11, 20, 29, 106, 119) + F1560 = (2, 5, 8, 9, 30, 41, 108, 117) + check('model.frames', len(frames) == 2025 and F0 in frameset and F1560 in frameset, + "2025 frames; PR1560's FRAME0 and pivot F are frames under these IDs") + sols = dichotomy() + check('E7.dichotomy', sols == {(Fraction(1, 4),) * 4, (0, 0, 0, 1)}, + 'four values in {x, 1-x} with sum 1: all 1/4, or {1, 0, 0, 0} up to order') + + # Negative controls: each fact must be falsifiable by the check that is meant to catch it. + bad = list(frames[0]) + bad[0] = next(i for i in range(N) if i not in bad and G[i][bad[1]] == 0) # not a frame any more + check('control.non-frame-pivot', isinstance(facts_at(tuple(bad), frameset), str), + 'replacing one pivot breaks the expansion / support facts') + r = facts_at(F1560, frameset - {tuple(sorted([22, 27, 34, 37] + [8, 9, 108, 117]))}) + check('control.missing-class-frame', isinstance(r, str) and r.startswith('E4 frame'), + 'removing a class-completion frame from the frame list is detected: ' + str(r)) + check('control.same-class-witness', all( + Fraction(1, 4) + sum(Fraction(a * b, 4) for a, b in zip(s0, s0)) == 1 + for s0 in itertools.product((1, -1), repeat=3)), + 'a same-class "witness" (j = i0) reproduces w = 1, so the opposite parity of j is what forces 1/2 or -1/2') + if controls_only: + print('PASS_ZERO_EXCLUSION_PROOF_AUDIT_CONTROLS_ONLY') + return + + total_e6 = 0 + for n, F in enumerate(frames): + res = facts_at(F, frameset) + if isinstance(res, str): + check('facts.all-frames', False, f'frame {n} {F}: {res}') + total_e6 += res[1] + check('facts.all-frames', True, + f'E1-E6 and E8 hold at all {len(frames)} pivot frames; {total_e6} exceptional 4+1 configurations checked') + print('PASS_ZERO_EXCLUSION_PROOF_AUDIT') + + +if __name__ == '__main__': + main() From 088ed74b1d9f624960702525863261476ca892a8 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:53:22 -0400 Subject: [PATCH 2/4] Zero-exclusion proof audit: README, metadata --- research/zero-exclusion-proof-audit/README.md | 109 +++++++++++++++--- .../zero-exclusion-proof-audit/SOURCES.json | 39 +++++++ research/zero-exclusion-proof-audit/TASK.json | 30 +++-- .../zero-exclusion-proof-audit/VERIFY.json | 6 +- .../binding_crosscheck.py | 2 +- 5 files changed, 151 insertions(+), 35 deletions(-) diff --git a/research/zero-exclusion-proof-audit/README.md b/research/zero-exclusion-proof-audit/README.md index ff0bf63080..1ce72d9e86 100644 --- a/research/zero-exclusion-proof-audit/README.md +++ b/research/zero-exclusion-proof-audit/README.md @@ -1,35 +1,106 @@ -# zero-exclusion-proof-audit +# Audit of PR1560's zero-exclusion theorem and its use in PR1616 / PR1650 -**Draft; no new bound claimed.** +**Corroborated; no gap found. No new bound, κ or rigidity claim.** -## Scope and evidence +[PR1560](https://github.com/CrocSwap/integer-mult-bounds/pull/1560) (Andrey Mas / @an664, with GPT-6 Pro), head +`eb9f6f15`, proves in `proof.md` that three frame-incidence conditions (D), (G), (W) at a pivot frame F force +`a_ik b_ik = 4` on every live support (Theorem 1), and with nonempty blocks the gauge form `K = D(2G_L)D^{-1}` +(Corollary 2). It claims no independent human review. [PR1616](https://github.com/CrocSwap/integer-mult-bounds/pull/1616) +(`7b3e4624`) and [PR1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650) (`d960f8a2`) apply the +theorem at hundreds of different pivots to get rigidity on every P107, P106 and P105 unit, and cite it without +re-deriving it. This package audits that step. Pins are in [SOURCES.json](SOURCES.json). -Original card: `formal-interface-lemma`. Complete [TASK.json](TASK.json), including any scope -change and its connection to the bottleneck. Explain the result and limitations here. -Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). -The selected record and catalogue are historical provenance, so later priority -updates do not invalidate this package. Explicit --source files are live inputs -and must match their pins. Full Git history is needed to resolve provenance. +## 1. Written audit of proof.md §2–§4 and §6 -## Reproduce +Every step was rederived over an arbitrary field E of characteristic zero. Nothing below needs order, symmetry or +nonzero entries. + +| Step | Claim | Audit | +|---|---|---| +| §2 | `K = K[:,F]K[F,:]/4`; `Π_i` idempotent, trace 1, `Π_f = E_ff`, support in `T_i × T_i` | Holds: rank K = 8 = rank `K[F,F]`; `a_i·b_i = 16`; support from the zero entries on orthogonal pairs. | +| (4), (5) | `Σ_{i∈S} Π_i = I` for every live frame; `Σ_{i∈C} Π_i = E_T` | Holds: `A_S B_S^T = 16I` gives `A_S^T B_S = 16I`; (5) by completing C to the live frame `C ∪ (F∖T)` (fact E4 below). | +| (6) | `Σ_{i∈S} G_ik G_il = 4δ_kl` | Holds for every frame S and pivot F (E1). | +| §4.1 | `(Π_i)_kl = t_kl G_ik G_il` on `I_kl` | Holds: off-diagonal entry of (4) is zero, pivots contribute zero, edge rule `p_i + p_j = 0 = h_i + h_j` with `h = ±1`. | +| §4.2 | `(Π_i)_kk = 1/4 + Σ c_kl G_ik G_il` on `I_k` | Holds: the difference from `Π^0` vanishes on pivots (both are `E_ff`) and off `I_k`; (D) is a rank statement over Q, so it holds over E; the c_kl are unique because the seven h_kl are independent. | +| §4.3 | Hadamard rows; common quadratic `x² − x + q`; class sum 1; dichotomy; `w_j = ±1/2` contradiction | Holds. (10) uses only (7) on rows with support T, all in `I_kl`. The dichotomy is E7. The sign-product step is E4 + E6: the product of the three signs `s_{i0,l}s_{j,l}` is the product over T of `ε_{i0}ε_j`, which is −1 exactly for opposite classes. | +| §4.4 | every ordered `(k,l)` gets `c_kl = 0` | Holds: a witnessed block containing `{k,l}` gives both orientations, since either point can be the distinguished coordinate. | +| §6 | `t_kl t_lk = 1/16`, `t_kl t_lm = t_km/4`, `u_kl = g_k/g_l`, gauge form | Holds. 2×2 minors of the rank-one `Π_i`; each triple of pivots lies in exactly one block (E3), which is nonempty by hypothesis. | + +**One expository omission, filled here.** §6 says "the pivot entries have the required form" without the +calculation. With `a_ik = δ_i ε_ik g_k`, `b_ik = 4ε_ik/(δ_i g_k)`, `a_f = b_f = 4e_f`, `d_i = δ_i/2`, +`d_f = 1/g_f`: `K_if = a_if = δ_i ε_if g_f = 2G_if d_i/d_f` and `K_fi = b_if = 4ε_if/(δ_i g_f) = 2G_fi d_f/d_i`; +pivot–pivot entries are `4δ_ff' = 2G_ff'`. So the corollary holds as stated. + +## 2. Finite facts the proof uses implicitly, at every pivot + +PR1560's checker establishes its premises only for its own pivot. The proof also uses E8 facts about lines +relative to F that it never states as hypotheses. [verify.py](verify.py) was written from the prose only (it does +not read PR1560's, PR1616's or PR1650's code) and checks them exactly at **all 2025 frames** as pivot: + +- **E1** `2v_i = Σ_{k∈F} G_ik v_k` for every line (gives (6) and `Σ_k G_ik G_jk = 2G_ij`); +- **E2** pivot rows are `2δ`; every nonpivot row has `G_ik ∈ {0, ±1}` and `|T_i| = 4`; +- **E3** exactly 14 supports, 8 lines each, forming a Steiner system S(3,4,8) on F; +- **E4** the sign product splits each block 4 + 4; classes are mutually orthogonal, opposite classes have + `G = ±1`, and each class plus `F ∖ T` is a frame (needed for (5)); +- **E5** the class rows `(1, s_i)` are Hadamard for every distinguished k; +- **E6** for every block, class, k, exceptional row `i0` and opposite-class line j (3,628,800 configurations), the + sign product is −1 and the predicted `w_j` is ±1/2, never a root of `x² − x`; +- **E7** four values in `{x, 1−x}` with sum 1 are all 1/4 or a permutation of `(1,0,0,0)`; +- **E8** the identity `Σ_k ε_ik ε_jk = 2G_ij` used for nonpivot pairs in §6. + +All hold at every pivot. Controls: a non-frame pivot fails; removing one class-completion frame is caught by E4; +a same-class "witness" gives `w = 1`, so opposite parity is what forces the contradiction. + +## 3. Binding to PR1616 / PR1650 -After completing the verifier and marking VERIFY.json ready, from repo root: +Reading both `criterion` functions against §3: the pivot must be a frame inside `L = P112 ∖ X`; ScripS is all +live frames; supports must have size 4; all 14 blocks must be nonempty (tested before (W), so the code demands the +Corollary 2 premise for Theorem 1 too, which is stronger, not weaker); (W) asks for one class with 4 live lines +and a live line of the other; (G) builds the graph on `I_kl` with an edge exactly when a live frame meets `I_kl` +in two points and requires one component; (D) requires the seven `h_kl` independent (rank 7 modulo a prime) and +the deduplicated incidence rows to reach rank `|I_k| − 7` modulo the prime, a lower bound over Q whose matching +upper bound is the seven kernel vectors. Their kernel membership is identity (6), which both verifiers check +for all 2025 frames as `Σ_{i∈S} v_i v_i^T = 8I`. Classes by sign-parity are the orthogonality classes (E4). I +found no mismatch. + +[binding_crosscheck.py](binding_crosscheck.py) compares PR1650's `criterion` with a second implementation from +§3's prose that uses different exact methods: classes by orthogonality, Q-rank of the integer Gram matrix `MᵀM` by +Bareiss elimination, and BFS. RESULT_PLACEHOLDER + +Part 3 is a same-account check: PR1616/PR1650 were earlier Claude sessions on this account. Parts 1 and 2 do not +depend on that code. + +## Not covered + +- PR1212 §8 (the copy floor from gauge rigidity) and §10 (stabiliser transport of units). The floors 59/58/57 + claimed by PR1616/PR1650 also need those. +- The finite premises at PR1616/PR1650's units, beyond the cross-check sample (their own verifiers replay them). +- Whether (G) implies (D) (session 13's claim in #1502). +- Proof-assistant formalization. + +## Reproduce ```sh +python3 -I -B research/zero-exclusion-proof-audit/verify.py # about 50 s python3 scripts/research_package.py --package research/zero-exclusion-proof-audit --check-only python3.12 scripts/research_package.py --package research/zero-exclusion-proof-audit +# Cross-check (needs PR1650's verify.py at d960f8a2, not on main): +git show d960f8a2:research/complex-rank8-rigidity-p105/verify.py > /tmp/pr1650_verify.py +python3 -I -B research/zero-exclusion-proof-audit/binding_crosscheck.py /tmp/pr1650_verify.py --samples 1000 ``` -Declare all external inputs and pinned dependencies in VERIFY.json. The generic -hook is bounded; native/Lean or long replays need an explicit dedicated workflow. - ## Open next questions -Complete the structured `open_questions` list in TASK.json and explain it here: -the question, why it matters, a feasible first step and any blocker. If no next -question is justified, say so rather than inventing one. +1. **PR1212 §8 binding.** Does the floor lemma consume exactly Corollary 2's conclusion on `L = P112 ∖ X`, + with PR1212 §10's transport? It matters because PR1616/PR1650's floors need it. First step: state §8's + hypothesis next to Corollary 2's conclusion. Not started here. +2. **Formalization.** The §4.3 local step (Hadamard class, common quadratic, dichotomy) is small enough for Lean + over a characteristic-zero field, with E1–E8 as finite lemmas. Blocked by the lack of a Lean E8 model with + these line IDs. ## Credit -Prepared by Josie Elliston (with Claude Opus 5.5). Retain predecessor attribution and source-specific notices. -New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. +Theorem, proof and fixture: Andrey Mas (@an664) with GPT-6 Pro (PR1560). Applications audited: PR1616 and PR1650 +(Josie Elliston with Claude). Predecessors credited by PR1560: Brett Halligan / @burntout76 / Ninefold (PR1212), +@DreamingOfClouds (PR717), @themilkman216 (PR968). This audit: Josie Elliston with Claude Opus 5.5 (Anthropic) via +Claude Code; substantial AI assistance. Apache-2.0. diff --git a/research/zero-exclusion-proof-audit/SOURCES.json b/research/zero-exclusion-proof-audit/SOURCES.json index db104fb5bb..ddab7d6da2 100644 --- a/research/zero-exclusion-proof-audit/SOURCES.json +++ b/research/zero-exclusion-proof-audit/SOURCES.json @@ -14,5 +14,44 @@ "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" } + ], + "external_predecessor_note": "Informational pins of the audited proof and the two criterion implementations, authenticated locally against exact Git objects. The generic SOURCES.files hook does not validate these entries. verify.py uses none of them; binding_crosscheck.py imports PR1650's verify.py from a path given on its command line.", + "external_predecessors": [ + { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1560", + "commit": "eb9f6f15f15704949cbd25ca8fbf58063084dd8e", + "attribution": "Andrey Mas (@an664), with GPT-6 Pro assistance", + "files": [ + { + "path": "research/frame-incidence-zero-exclusion/proof.md", + "git_blob": "bfea905d386ce28d13d10682cb45da2050493ced", + "sha256": "3b9d25559ef38c6fbcfcd70dcd100ab09db7f36a33e827aba48b7f8d81c0befe" + } + ] + }, + { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1616", + "commit": "7b3e4624e31647fc2a8b777a181823739b12b36e", + "attribution": "Josie Elliston, with Claude", + "files": [ + { + "path": "research/complex-rank8-rigidity-p106/verify.py", + "git_blob": "591a4f5914a01a6edbf9d7c7e000eba4ec2ab83c", + "sha256": "b500a82e5a780e5acde0c034306ec2a2cf9a9d0d9d6cce68378312c7ba643f70" + } + ] + }, + { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1650", + "commit": "d960f8a276f752934ff37617da99e489ad5e9d5e", + "attribution": "Josie Elliston, with Claude", + "files": [ + { + "path": "research/complex-rank8-rigidity-p105/verify.py", + "git_blob": "d60ada8e40a03efb4506c1cfadd589d16df0a281", + "sha256": "8bab6588f19f0280a98dfce90835746387ef9845cdfb5768f84ac75247af7b01" + } + ] + } ] } diff --git a/research/zero-exclusion-proof-audit/TASK.json b/research/zero-exclusion-proof-audit/TASK.json index 0d77d21d54..b0449a2266 100644 --- a/research/zero-exclusion-proof-audit/TASK.json +++ b/research/zero-exclusion-proof-audit/TASK.json @@ -39,22 +39,28 @@ "Lean binding" ] }, - "scope_status": "unchanged", - "actual_scope": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", - "scope_change_reason": null, - "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "scope_status": "refined", + "actual_scope": "Separately authored audit of PR1560's written Theorem 1 (structural zero exclusion) and Corollary 2 (gauge form) at head eb9f6f15, and of the theorem-to-certificate binding used by PR1616 (7b3e4624) and PR1650 (d960f8a2): (1) a step-by-step written audit over an arbitrary characteristic-zero field; (2) an exact stdlib check, written from the prose only, of the finite E8 facts the proof uses implicitly, at every one of the 2025 frames as pivot; (3) a reading of PR1616/PR1650's criterion code against the stated hypotheses, plus a cross-check of PR1650's verdicts against a second implementation with different exact methods.", + "scope_change_reason": "The card asks for one interface lemma or one theorem-to-certificate binding. PR1560's theorem is the single unreviewed written step behind the P107, P106 and P105 rigidity results of PR1616/PR1650, which apply it at hundreds of pivots other than the one PR1560's checker covers; PR1560 states no independent human review, and PR1650 cites rather than re-derives it. This is an audit, not a proof-assistant formalization.", + "bottleneck_link": "Side result for the complex-decoder lower-bound line (no kappa). It removes one unreviewed proof obligation under the PR968 copy floors claimed at P107-P105 through #1212 section 8.", "budget_minutes": 60, - "stop_rule": "TODO", - "outcome": "in-progress", - "evidence": "TODO", + "stop_rule": "Stop at a written audit plus exact checks of every finite fact the proof uses; any genuine gap is reported as a FINDING instead of being patched silently.", + "outcome": "completed", + "evidence": "Corroborated, no gap in Theorem 1 or Corollary 2 (one expository omission in Corollary 2 filled in the README). verify.py: implicit finite facts E1-E8 hold at all 2025 pivot frames (about 50 s). binding_crosscheck.py: PR1650's criterion agrees with a second implementation on every sampled case (see README).", "author": "Josie Elliston (with Claude Opus 5.5)", - "ai_assistance": "TODO: disclose tools used", + "ai_assistance": "Claude Opus 5.5 (Anthropic) via Claude Code wrote the audit, both scripts and the README under Josie Elliston's account; a Codex read-only review was requested.", "open_questions": [ { - "question": "TODO", - "why_it_matters": "TODO", - "first_step": "TODO", - "blocked_by": "TODO" + "question": "Does PR1212 section 8 (copy floor from gauge rigidity) consume exactly Corollary 2's conclusion K = D(2G_L)D^{-1} on L = P112 minus X, with the FRAME0 stabiliser transport of PR1212 section 10?", + "why_it_matters": "PR1616/PR1650's floors 59/58/57 need this binding as well as Corollary 2; this audit stops at Corollary 2.", + "first_step": "State the hypothesis of PR1212 section 8's floor lemma and compare it with Corollary 2's conclusion and live set.", + "blocked_by": "Reading PR1212 section 8 and section 10 in full; not started here." + }, + { + "question": "Can Theorem 1 and Corollary 2 be formalized in Lean with the finite facts E1-E8 as kernel-checked lemmas?", + "why_it_matters": "The universal implication is still a written proof checked by humans/AI, not a kernel theorem.", + "first_step": "Formalize the section 4.3 local step (Hadamard class, common quadratic, dichotomy) over a field of characteristic zero.", + "blocked_by": "No Lean E8 model in the repository for these line IDs." } ] } diff --git a/research/zero-exclusion-proof-audit/VERIFY.json b/research/zero-exclusion-proof-audit/VERIFY.json index b10c894394..98b7aea81e 100644 --- a/research/zero-exclusion-proof-audit/VERIFY.json +++ b/research/zero-exclusion-proof-audit/VERIFY.json @@ -1,6 +1,6 @@ { "schema_version": 1, - "status": "draft", + "status": "ready", "python": "3.12", "requirements": [], "inputs": [], @@ -11,8 +11,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 120, - "checks": "TODO: identity, positive fixture and failure controls" + "timeout_seconds": 300, + "checks": "Model (120 lines, 2025 frames, PR1560 IDs), the E7 dichotomy, three negative controls, and E1-E6, E8 at every one of the 2025 pivot frames (about 50 s)." } ] } diff --git a/research/zero-exclusion-proof-audit/binding_crosscheck.py b/research/zero-exclusion-proof-audit/binding_crosscheck.py index 335aba1fe6..50ee1b9eab 100644 --- a/research/zero-exclusion-proof-audit/binding_crosscheck.py +++ b/research/zero-exclusion-proof-audit/binding_crosscheck.py @@ -166,7 +166,7 @@ def main(): 'nonempty-blocks' if not ne else 'W' if not W else 'G' if not Gk else 'D' ok = reason == expect tally[(reason, ok)] = tally.get((reason, ok), 0) + 1 - if name[:6] != 'random' or not ok: + if not name.startswith(('random', 'allframes')) or not ok: print(f"{'AGREE' if ok else 'DISAGREE'} {name}: PR1650 {reason}; prose (blocks, W, G, D) = {ne, W, Gk, Dk}") if not ok: sys.exit(1) From 84ada61137a35e3e0a874fdeace92712e23a18d7 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 02:01:31 -0400 Subject: [PATCH 3/4] Zero-exclusion proof audit: cross-check results, --thin mode --- research/zero-exclusion-proof-audit/README.md | 14 +++++++++++++- .../binding_crosscheck.py | 8 +++++--- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/research/zero-exclusion-proof-audit/README.md b/research/zero-exclusion-proof-audit/README.md index 1ce72d9e86..cdd9781863 100644 --- a/research/zero-exclusion-proof-audit/README.md +++ b/research/zero-exclusion-proof-audit/README.md @@ -65,7 +65,19 @@ found no mismatch. [binding_crosscheck.py](binding_crosscheck.py) compares PR1650's `criterion` with a second implementation from §3's prose that uses different exact methods: classes by orthogonality, Q-rank of the integer Gram matrix `MᵀM` by -Bareiss elimination, and BFS. RESULT_PLACEHOLDER +Bareiss elimination, and BFS. PR1650 stops at its first failing test (support, blocks, (W), (G), (D)); the cross-check +requires the same first failure, or a pass when all four hold. Results (Python 3.12, 2026-10-14 02:00 EDT, +PR1650 at `d960f8a2`), all **agree**: + +| Run | Cases | Pass | (W) | (G) | blocks | (D) | +|---|---:|---:|---:|---:|---:|---:| +| `--samples 1000`: fixtures, 1000 random 5–10-line deletions with a random live pivot, every live frame of five random 7–10-line deletions | 4354 | 4019 | 334 | 0 | 0 | 1 | +| `--samples 1500 --thin`: fixtures, random 11–40-line deletions | 1503 | 246 | 1252 | 2 | 2 | 1 | + +The fixtures are PR1560's positive fixture (passes), its `X_bad` control (fails (W)), and session 13's +full-family (G)-without-(D) pivot from #1502 (fails (D) in both). Because PR1650 stops at its first failure, this +compares (G) and (D) verdicts only where every earlier test passed. That is thin for (G) and (D): two and one +cases. Part 3 is a same-account check: PR1616/PR1650 were earlier Claude sessions on this account. Parts 1 and 2 do not depend on that code. diff --git a/research/zero-exclusion-proof-audit/binding_crosscheck.py b/research/zero-exclusion-proof-audit/binding_crosscheck.py index 50ee1b9eab..37bae5fb88 100644 --- a/research/zero-exclusion-proof-audit/binding_crosscheck.py +++ b/research/zero-exclusion-proof-audit/binding_crosscheck.py @@ -8,7 +8,7 @@ script imports from a path given on the command line. PR1650 is not on main, so this script is not part of the registered replay; its output is recorded in the README. - python3 -I -B research/zero-exclusion-proof-audit/binding_crosscheck.py PATH/TO/PR1650/verify.py [--samples N] + python3 -I -B research/zero-exclusion-proof-audit/binding_crosscheck.py PATH/TO/PR1650/verify.py [--samples N] [--thin] """ import importlib.util @@ -131,6 +131,8 @@ def load_pr1650(path): def main(): path = sys.argv[1] samples = int(sys.argv[sys.argv.index('--samples') + 1]) if '--samples' in sys.argv else 60 + # --thin: delete 11-40 lines instead of 5-10, so blocks, (G) and (D) also fail (thin live families). + sizes = list(range(11, 41)) if '--thin' in sys.argv else [5, 6, 7, 8, 9, 10] pr = load_pr1650(path) assert pr.LINES == mine.V and pr.G == mine.G, 'line IDs / G disagree' frames = mine.all_frames() @@ -144,14 +146,14 @@ def main(): ('s13-full-family-g-without-d', (3, 4, 8, 9, 107, 108, 117, 118), (19, 25, 37, 47, 67, 82, 94, 115)), ] for n in range(samples): - size = rng.choice([5, 6, 7, 8, 9, 10]) + size = rng.choice(sizes) X = tuple(sorted(rng.sample(P112, size))) live = set(P112) - set(X) cand = [S for S in frames if set(S) <= live] if cand: cases.append((f'random-{n}-P{112 - size}', X, rng.choice(cand))) # Every live frame as pivot for a few deletion sets: early frames fail blocks / (W), as in PR1650's tally. - for n in range(max(1, samples // 200)): + for n in range(max(1, samples // 200) if '--thin' not in sys.argv else 0): X = tuple(sorted(rng.sample(P112, 7 + n % 4))) live = set(P112) - set(X) cases += [(f'allframes-{n}', X, S) for S in frames if set(S) <= live] From c29103afcc252aeff3c89e8164b335b25c40096d Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 02:04:50 -0400 Subject: [PATCH 4/4] Zero-exclusion proof audit: address Codex review (illustration label, Python version, wording) --- research/zero-exclusion-proof-audit/README.md | 13 +++++++------ research/zero-exclusion-proof-audit/TASK.json | 2 +- research/zero-exclusion-proof-audit/verify.py | 5 +++-- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/research/zero-exclusion-proof-audit/README.md b/research/zero-exclusion-proof-audit/README.md index cdd9781863..d3a69a02c2 100644 --- a/research/zero-exclusion-proof-audit/README.md +++ b/research/zero-exclusion-proof-audit/README.md @@ -48,8 +48,9 @@ not read PR1560's, PR1616's or PR1650's code) and checks them exactly at **all 2 - **E7** four values in `{x, 1−x}` with sum 1 are all 1/4 or a permutation of `(1,0,0,0)`; - **E8** the identity `Σ_k ε_ik ε_jk = 2G_ij` used for nonpivot pairs in §6. -All hold at every pivot. Controls: a non-frame pivot fails; removing one class-completion frame is caught by E4; -a same-class "witness" gives `w = 1`, so opposite parity is what forces the contradiction. +All hold at every pivot. Controls: a non-frame pivot fails; removing one class-completion frame is caught by E4. +An illustration (an identity, not a rejection control) shows that a same-class "witness" gives `w = 1`, so +opposite parity is what forces the contradiction. ## 3. Binding to PR1616 / PR1650 @@ -76,8 +77,8 @@ PR1650 at `d960f8a2`), all **agree**: The fixtures are PR1560's positive fixture (passes), its `X_bad` control (fails (W)), and session 13's full-family (G)-without-(D) pivot from #1502 (fails (D) in both). Because PR1650 stops at its first failure, this -compares (G) and (D) verdicts only where every earlier test passed. That is thin for (G) and (D): two and one -cases. +compares (G) and (D) verdicts only where every earlier test passed. That is thin for (G) and (D): two cases and one distinct case (the same fixture in both runs). + Part 3 is a same-account check: PR1616/PR1650 were earlier Claude sessions on this account. Parts 1 and 2 do not depend on that code. @@ -93,12 +94,12 @@ depend on that code. ## Reproduce ```sh -python3 -I -B research/zero-exclusion-proof-audit/verify.py # about 50 s +python3.12 -I -B research/zero-exclusion-proof-audit/verify.py # about 50 s; 3.10+ python3 scripts/research_package.py --package research/zero-exclusion-proof-audit --check-only python3.12 scripts/research_package.py --package research/zero-exclusion-proof-audit # Cross-check (needs PR1650's verify.py at d960f8a2, not on main): git show d960f8a2:research/complex-rank8-rigidity-p105/verify.py > /tmp/pr1650_verify.py -python3 -I -B research/zero-exclusion-proof-audit/binding_crosscheck.py /tmp/pr1650_verify.py --samples 1000 +python3.12 -I -B research/zero-exclusion-proof-audit/binding_crosscheck.py /tmp/pr1650_verify.py --samples 1000 # needs 3.10+ (int.bit_count) ``` ## Open next questions diff --git a/research/zero-exclusion-proof-audit/TASK.json b/research/zero-exclusion-proof-audit/TASK.json index b0449a2266..61f30374c7 100644 --- a/research/zero-exclusion-proof-audit/TASK.json +++ b/research/zero-exclusion-proof-audit/TASK.json @@ -42,7 +42,7 @@ "scope_status": "refined", "actual_scope": "Separately authored audit of PR1560's written Theorem 1 (structural zero exclusion) and Corollary 2 (gauge form) at head eb9f6f15, and of the theorem-to-certificate binding used by PR1616 (7b3e4624) and PR1650 (d960f8a2): (1) a step-by-step written audit over an arbitrary characteristic-zero field; (2) an exact stdlib check, written from the prose only, of the finite E8 facts the proof uses implicitly, at every one of the 2025 frames as pivot; (3) a reading of PR1616/PR1650's criterion code against the stated hypotheses, plus a cross-check of PR1650's verdicts against a second implementation with different exact methods.", "scope_change_reason": "The card asks for one interface lemma or one theorem-to-certificate binding. PR1560's theorem is the single unreviewed written step behind the P107, P106 and P105 rigidity results of PR1616/PR1650, which apply it at hundreds of pivots other than the one PR1560's checker covers; PR1560 states no independent human review, and PR1650 cites rather than re-derives it. This is an audit, not a proof-assistant formalization.", - "bottleneck_link": "Side result for the complex-decoder lower-bound line (no kappa). It removes one unreviewed proof obligation under the PR968 copy floors claimed at P107-P105 through #1212 section 8.", + "bottleneck_link": "Side result for the complex-decoder lower-bound line (no kappa). It provides a separately authored written audit (not a formal proof) of one unreviewed proof obligation under the PR968 copy floors claimed at P107-P105 through #1212 section 8.", "budget_minutes": 60, "stop_rule": "Stop at a written audit plus exact checks of every finite fact the proof uses; any genuine gap is reported as a FINDING instead of being patched silently.", "outcome": "completed", diff --git a/research/zero-exclusion-proof-audit/verify.py b/research/zero-exclusion-proof-audit/verify.py index 881b844f8c..bced173621 100644 --- a/research/zero-exclusion-proof-audit/verify.py +++ b/research/zero-exclusion-proof-audit/verify.py @@ -189,7 +189,8 @@ def main(): check('E7.dichotomy', sols == {(Fraction(1, 4),) * 4, (0, 0, 0, 1)}, 'four values in {x, 1-x} with sum 1: all 1/4, or {1, 0, 0, 0} up to order') - # Negative controls: each fact must be falsifiable by the check that is meant to catch it. + # Negative controls: each fact must be falsifiable by the check that is meant to catch it. The third entry is + # an illustration (an arithmetic identity), not a rejection control. bad = list(frames[0]) bad[0] = next(i for i in range(N) if i not in bad and G[i][bad[1]] == 0) # not a frame any more check('control.non-frame-pivot', isinstance(facts_at(tuple(bad), frameset), str), @@ -197,7 +198,7 @@ def main(): r = facts_at(F1560, frameset - {tuple(sorted([22, 27, 34, 37] + [8, 9, 108, 117]))}) check('control.missing-class-frame', isinstance(r, str) and r.startswith('E4 frame'), 'removing a class-completion frame from the frame list is detected: ' + str(r)) - check('control.same-class-witness', all( + check('illustration.same-class-witness', all( Fraction(1, 4) + sum(Fraction(a * b, 4) for a, b in zip(s0, s0)) == 1 for s0 in itertools.product((1, -1), repeat=3)), 'a same-class "witness" (j = i0) reproduces w = 1, so the opposite parity of j is what forces 1/2 or -1/2')