From 378275c8e1228d7cdad4888d808a8b8c6395b32e Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Thu, 22 Oct 2026 23:16:40 -0500 Subject: [PATCH] Prove exact Boolean disjointness repair rank --- .../HISTORICAL-REVIEW.txt | 66 +++++++ .../boolean-disjointness-repair/ORIGINS.json | 44 +++++ .../boolean-disjointness-repair/PROOF.txt | 51 ++++++ .../boolean-disjointness-repair/README.md | 69 +++++++ .../SOURCE-HASHES.json | 12 ++ .../boolean-disjointness-repair/SOURCES.json | 13 ++ .../ZETA-CORRECTOR-CHECK.json | 68 +++++++ .../check_zeta_corrector.py | 36 ++++ .../independent/RESULT.json | 40 +++++ .../independent/verify.py | 73 ++++++++ .../review/CHECKED-FILES.json | 13 ++ .../review/CURRENT-MAIN-OVERLAP.txt | 22 +++ .../review/OVERLAP.json | 170 ++++++++++++++++++ .../review/PREDECESSOR-SOURCES.json | 70 ++++++++ .../review/RESULT.json | 110 ++++++++++++ .../review/REVIEW.md | 155 ++++++++++++++++ .../review/review_checks.py | 125 +++++++++++++ .../boolean-disjointness-repair/verify.py | 25 +++ 18 files changed, 1162 insertions(+) create mode 100644 research/boolean-disjointness-repair/HISTORICAL-REVIEW.txt create mode 100644 research/boolean-disjointness-repair/ORIGINS.json create mode 100644 research/boolean-disjointness-repair/PROOF.txt create mode 100644 research/boolean-disjointness-repair/README.md create mode 100644 research/boolean-disjointness-repair/SOURCE-HASHES.json create mode 100644 research/boolean-disjointness-repair/SOURCES.json create mode 100644 research/boolean-disjointness-repair/ZETA-CORRECTOR-CHECK.json create mode 100644 research/boolean-disjointness-repair/check_zeta_corrector.py create mode 100644 research/boolean-disjointness-repair/independent/RESULT.json create mode 100644 research/boolean-disjointness-repair/independent/verify.py create mode 100644 research/boolean-disjointness-repair/review/CHECKED-FILES.json create mode 100644 research/boolean-disjointness-repair/review/CURRENT-MAIN-OVERLAP.txt create mode 100644 research/boolean-disjointness-repair/review/OVERLAP.json create mode 100644 research/boolean-disjointness-repair/review/PREDECESSOR-SOURCES.json create mode 100644 research/boolean-disjointness-repair/review/RESULT.json create mode 100644 research/boolean-disjointness-repair/review/REVIEW.md create mode 100644 research/boolean-disjointness-repair/review/review_checks.py create mode 100644 research/boolean-disjointness-repair/verify.py diff --git a/research/boolean-disjointness-repair/HISTORICAL-REVIEW.txt b/research/boolean-disjointness-repair/HISTORICAL-REVIEW.txt new file mode 100644 index 0000000000..673fcf9c4f --- /dev/null +++ b/research/boolean-disjointness-repair/HISTORICAL-REVIEW.txt @@ -0,0 +1,66 @@ +INDEPENDENT REVIEW: PASS + +The rank formula and its stated scope are correct. The proof in +ZETA-CORRECTOR-PROOF.txt has no gap that this review found. + +An alternate proof of the deletion step +-------------------------------------- +Let B=I+A_h, n=2^h-2, u=(1,...,1)^T, and J=uu^T over F_2. +Each row of A_h has 2^(h-|S|)-1 entries equal to one. Thus B u=0. +The full matrix M=I+T_h has block form + + [0 u^T 1] + [u B 0]. + [1 0 1] + +Since T_h^3=I, we have M^3=M^2+M. The central block of this +identity, together with B u=0 and u^T u=0, gives + + B^3+B^2+B=J. + +If Bz=0, then Jz=0, so u^T z=0. For any unit column e, put +w=(I+B+B^2)e. Then B w=u and u^T w=1. Hence + + ker M = {(0,z,0): z in ker B} + span{(1,w,1)}, + +where the sum is direct. Thus nullity(M)=nullity(B)+1 and +rank(M)=rank(B)+1. + +The full matrix rank +-------------------- +The factor L=[[1,1],[1,0]] satisfies L^2+L+I=0. Over F_4 it +has distinct eigenvalues omega and omega^2, where omega^3=1. +The tensor power T_h=L tensor ... tensor L is diagonalizable. +Let a_h count its eigenvalues equal to one. In T_(h+1), each +eigenvalue omega or omega^2 contributes one eigenvalue equal to +one, while an eigenvalue equal to one contributes none. Hence + + a_0=1, a_(h+1)=2^h-a_h, + a_h=(2^h+2*(-1)^h)/3. + +It follows that rank(M)=2^h-a_h. A field extension does not +change matrix rank. The deletion step therefore gives + + rank_F2(B)=(2^(h+1)-2*(-1)^h-3)/3. + +Verification by a different method +----------------------------------- +verify.py counts every kernel input, without row reduction. +For h=2,3,4, it checks all 4, 64, and 16,384 inputs to B and all +16, 256, and 65,536 inputs to M. It gets B ranks 1, 5, and 9. +It also checks every kernel parity, every preimage of u, and the +matrix identity B^3+B^2+B=J. All checks pass. This finite check +supports the proof; it does not replace the proof for all h. + +Application and limits +---------------------- +If K=B is a sum of ell rank-one additive corrections, rank(K) +is at most ell. With v=2^h-2 and the assumed ledger D=2v-3ell, +the formula gives D <= 2*(-1)^h-1. This is 1 for even h and -3 +for odd h. A copied scalar centre must have the stated additive +rank-one effect for this argument to apply. A product of general +maps is not being treated as an additive sum without proof. + +This does not exclude a new source basis, a new port design, a +new compiler, or another method of correction. It is not a bound +on all Boolean-lattice constructions. diff --git a/research/boolean-disjointness-repair/ORIGINS.json b/research/boolean-disjointness-repair/ORIGINS.json new file mode 100644 index 0000000000..3615ba7772 --- /dev/null +++ b/research/boolean-disjointness-repair/ORIGINS.json @@ -0,0 +1,44 @@ +[ + { + "file": "PROOF.txt", + "original_workspace_path": "work/frontier-crosscheck/ZETA-CORRECTOR-PROOF.txt", + "original_sha256": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427", + "adaptations": [] + }, + { + "file": "check_zeta_corrector.py", + "original_workspace_path": "work/frontier-crosscheck/check_zeta_corrector.py", + "original_sha256": "333e2b5a15c4c20c7c2c784af2196a77a5dddae846a82fed3f2b13d3dc4d050d", + "adaptations": [ + "Set the proof reference to the packaged PROOF.txt." + ] + }, + { + "file": "ZETA-CORRECTOR-CHECK.json", + "original_workspace_path": "work/frontier-crosscheck/ZETA-CORRECTOR-CHECK.json", + "original_sha256": "6de6e4c40c00cc8c6e987b536caf1e33381fcb35752fdb561894d0b2f5126154", + "adaptations": [ + "Set the proof reference to the packaged PROOF.txt." + ] + }, + { + "file": "independent/verify.py", + "original_workspace_path": "work/frontier-crosscheck/independent-zeta/verify.py", + "original_sha256": "2554a3346e53fd028c57023e09fc7131cc642e9d02cdbc2d432391bf21fca8ca", + "adaptations": [] + }, + { + "file": "independent/RESULT.json", + "original_workspace_path": "work/frontier-crosscheck/independent-zeta/RESULT.json", + "original_sha256": "08861a7b95425e64033658da62bad97ba994ad3f59126b3333ffd478f519dc2f", + "adaptations": [] + }, + { + "file": "HISTORICAL-REVIEW.txt", + "original_workspace_path": "work/frontier-crosscheck/independent-zeta/REVIEW.txt", + "original_sha256": "15fb582c3af7830c9f7c649892fdf224d802ee52b27360fa5c3fe1b2f53aed1f", + "adaptations": [ + "Omit the unrelated routing-only split review. Retain the rank proof review verbatim." + ] + } +] diff --git a/research/boolean-disjointness-repair/PROOF.txt b/research/boolean-disjointness-repair/PROOF.txt new file mode 100644 index 0000000000..96b0e770da --- /dev/null +++ b/research/boolean-disjointness-repair/PROOF.txt @@ -0,0 +1,51 @@ +Scope: this is an obstruction to one repair of PR172. It is not a bound +on all Boolean-lattice constructions or on a new source-basis compiler. + +Let h >= 2. Index A_h by the nonempty proper subsets of [h]. Set +A_h[u,v] = 1 if u and v are disjoint, and 0 otherwise, over F_2. +The literal side map in PR172 is A_h. If an additive correction K is to +make its endpoint the identity, it must equal B_h = I + A_h. + +THEOREM +rank_F2(B_h) = (2^(h+1) - 2*(-1)^h - 3)/3. +Thus a sum of ell scalar rank-one corrections needs at least this many +terms. Under the stated ledger D = 2v - 3ell, v = 2^h - 2, + D <= 2*(-1)^h - 1. +The bound is 1 for even h and -3 for odd h. It is not the projected +centerless deficit 2v in PR172. + +PROOF +Include the empty and full subsets. The full disjointness matrix is +T_h = [[1,1],[1,0]] tensor ... tensor [[1,1],[1,0]]. It satisfies T_h^3=I. +Over F_4 the two eigenvalues of its 2-by-2 factor are omega and omega^2. +If a_h is the multiplicity of eigenvalue 1, then a_0=1 and + a_(h+1)=2^h-a_h, +so a_h=(2^h+2*(-1)^h)/3. The polynomial X^3-1 has distinct roots over +F_4. Hence M=I+T_h has rank (2^(h+1)-2*(-1)^h)/3. Extension from F_2 +to F_4 preserves matrix rank. + +It remains to prove rank(M)=rank(B_h)+1. Order the indices as empty, +proper nonempty, full. For a column (x0,z,xF), + M(x0,z,xF) = (1^T z+xF, x0*1+B_h z, x0+xF). +Put P=I+T_h+T_h^2. Then PM=0 and P e_empty is the nonzero column +that is 1 exactly on the proper nonempty subsets. + +If B_h z=0, M(0,z,0)=(1^T z)e_empty. Apply P to obtain 1^T z=0. +Because B_h is symmetric, its image is the orthogonal complement of +its kernel. Thus 1 is in its image. Choose w with B_h w=1. +Then M(1,w,1)=(1^T w+1)e_empty. Apply P to obtain 1^T w=1. +Every kernel column of M has x0=xF. The kernel columns with x0=0 +are exactly (0,z,0) for z in ker(B_h). The column (1,w,1) supplies +one extra independent kernel column. Therefore + nullity(M)=nullity(B_h)+1, +and rank(M)=rank(B_h)+1. This proves the rank formula. + +Each scalar rank-one additive correction raises matrix rank by at most +one. Substitution in D=2v-3ell gives the final inequality. + +LIMITS +This does not prove that all variants of PR172 fail. A different endpoint, +a new source basis, a new port label design, or a correction implemented +by another method can evade this stated model. It does show that the +missing scalar identity cannot be repaired by a small number of copied +scalar centres while retaining PR172's projected deficit. diff --git a/research/boolean-disjointness-repair/README.md b/research/boolean-disjointness-repair/README.md new file mode 100644 index 0000000000..5d659814e9 --- /dev/null +++ b/research/boolean-disjointness-repair/README.md @@ -0,0 +1,69 @@ +# Exact rank of an additive Boolean-disjointness repair + +For every integer `h>=2`, let `A_h` be the F2 disjointness matrix on the +nonempty proper subsets of `[h]`. This package proves + +```text +rank_F2(I+A_h) = (2^(h+1) - 2*(-1)^h - 3)/3. +``` + +Thus any F2 additive repair of `A_h` to the identity by `ell` scalar rank-one +terms requires at least this many terms. Under the assumed ledger +`D=2v-3ell`, `v=2^h-2`, its deficit is at most 1 for even h and -3 for odd h. +This rules out a cheap copied-scalar repair of the specific missing endpoint +in [PR #172](https://github.com/CrocSwap/integer-mult-bounds/pull/172). +It does not rule out a new source basis, port design, endpoint, nonadditive +repair, or compiler. There is no construction or complete kappa improvement. + +`PROOF.txt` gives the all-dimensional proof. It computes the spectrum of the +full tensor disjointness matrix, then proves the exact rank change when the +empty and full sets are removed. `HISTORICAL-REVIEW.txt` gives a separate +written proof of that deletion step. Its review was by an AI agent, not a +human reviewer or a proof assistant. + +## Reproduce + +From the repository root, with Python 3.10 or later and its standard library: + +```sh +python3 -B research/boolean-disjointness-repair/verify.py +``` + +Expected final line: + +```text +PASS_BOOLEAN_DISJOINTNESS_REPAIR h=2..11 independent_kernels=2..4 no_new_kappa +``` + +The first check uses exact binary elimination for h=2 through 11. The +separate check enumerates every kernel input for h=2,3,4 by Gray code, with +no elimination. It also checks kernel parity, the required preimages, and +the identity `B^3+B^2+B=J`. These finite checks support the written proof +for all h; they do not replace it. The wrapper checks source hashes and +compares complete mathematical receipts in a temporary directory. No +selected supplier replay, complete repository build, or Lean check is claimed. + +## Credit and scope + +Publication base: `cef4b52f2a59009865bf8eabde1be3f159063703`. +The consumed semantic interface is PR172 at +`427b23bc79489e7b2b7548bfd434dd9670fd5c47`. Its +[retained package](https://github.com/mikey1201/integer-mult-bounds/tree/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family) +supplies the disjointness endpoint and ledger. The pinned [NOTICE](https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/NOTICE) +credits icekylinx's [PR #144](https://github.com/CrocSwap/integer-mult-bounds/pull/144) +lineage for the compiler, orthogonality contract, and bookkeeping; +its own construction and checks used Cline assistance. This package does +not claim its graph, compiler, or projected exponent as new work. + +Ali Romman directed the rank proof and audit with substantial OpenAI Codex +assistance, including a separate AI proof review and kernel enumeration. +New work is Apache-2.0. `SOURCES.json` and `ORIGINS.json` record source pins +and original local hashes. The physical interpretation assumes F2 scalar corrections and the stated +additive rank-one ledger; a product of general operators is not such a sum. + +## Open next questions + +Can a different endpoint or a nonadditive physical repair avoid the rank-one +ledger? First write its exact all-input identity and charge every added +operation. The present rank formula alone supplies neither a construction +nor a lower bound for that changed model. diff --git a/research/boolean-disjointness-repair/SOURCE-HASHES.json b/research/boolean-disjointness-repair/SOURCE-HASHES.json new file mode 100644 index 0000000000..de5394eb2a --- /dev/null +++ b/research/boolean-disjointness-repair/SOURCE-HASHES.json @@ -0,0 +1,12 @@ +{ + "HISTORICAL-REVIEW.txt": "e0ada149d05f1ca5bb6432095cbb591aa11de29dd0970134e92de0902b745e09", + "ORIGINS.json": "39e8913cc7d69b870cd6a3750c0a76cc117d43af6570d5fe6353551bb0e7ca4d", + "PROOF.txt": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427", + "README.md": "b37e421642070fe7769189655c29e8fd68100000292938ffbd4d5f777a1edc11", + "SOURCES.json": "254336a35d49ad4f771dde8093677ef5dfc42409d6a8c35c6f59e2149a05f47e", + "ZETA-CORRECTOR-CHECK.json": "8b5324c3821cead8eac68253395ae8e54470b3a107c854f62cb6a63e0a640ee2", + "check_zeta_corrector.py": "eaeb78e8a73cac408ef6570fee9e334081d2fc9b728170a29007a2d646b5b925", + "independent/RESULT.json": "08861a7b95425e64033658da62bad97ba994ad3f59126b3333ffd478f519dc2f", + "independent/verify.py": "2554a3346e53fd028c57023e09fc7131cc642e9d02cdbc2d432391bf21fca8ca", + "verify.py": "8b9525da24b0a21b047b2ce6315f072b27d456e6aa22fe9f0b51bcad0bdd1271" +} diff --git a/research/boolean-disjointness-repair/SOURCES.json b/research/boolean-disjointness-repair/SOURCES.json new file mode 100644 index 0000000000..99d87026e4 --- /dev/null +++ b/research/boolean-disjointness-repair/SOURCES.json @@ -0,0 +1,13 @@ +{ + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "predecessor": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/172", + "commit": "427b23bc79489e7b2b7548bfd434dd9670fd5c47", + "source": "https://github.com/mikey1201/integer-mult-bounds/tree/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family", + "role": "Disjointness endpoint and D=2v-3ell ledger. Algebraic proof and finite replays are self-contained.", + "notice": "https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/NOTICE", + "notice_git_blob": "5d32242250b85a59268cd27a2e63cb615c4850d9", + "compiler_lineage": "https://github.com/CrocSwap/integer-mult-bounds/pull/144" + }, + "new_kappa": false +} diff --git a/research/boolean-disjointness-repair/ZETA-CORRECTOR-CHECK.json b/research/boolean-disjointness-repair/ZETA-CORRECTOR-CHECK.json new file mode 100644 index 0000000000..c457bd0334 --- /dev/null +++ b/research/boolean-disjointness-repair/ZETA-CORRECTOR-CHECK.json @@ -0,0 +1,68 @@ +{ + "status": "PASS_EXACT_F2_CORRECTOR_RANK", + "scope": "PR172 literal disjointness endpoint, repaired by an additive sum of scalar rank-one copied centres.", + "general_formula": "rank(I+A_h)=(2^(h+1)-2*(-1)^h-3)/3 for h>=2", + "proof": "PROOF.txt", + "rows": [ + { + "h": 2, + "ports": 2, + "correction_rank": 1, + "maximum_deficit_with_rank_one_centres": 1 + }, + { + "h": 3, + "ports": 6, + "correction_rank": 5, + "maximum_deficit_with_rank_one_centres": -3 + }, + { + "h": 4, + "ports": 14, + "correction_rank": 9, + "maximum_deficit_with_rank_one_centres": 1 + }, + { + "h": 5, + "ports": 30, + "correction_rank": 21, + "maximum_deficit_with_rank_one_centres": -3 + }, + { + "h": 6, + "ports": 62, + "correction_rank": 41, + "maximum_deficit_with_rank_one_centres": 1 + }, + { + "h": 7, + "ports": 126, + "correction_rank": 85, + "maximum_deficit_with_rank_one_centres": -3 + }, + { + "h": 8, + "ports": 254, + "correction_rank": 169, + "maximum_deficit_with_rank_one_centres": 1 + }, + { + "h": 9, + "ports": 510, + "correction_rank": 341, + "maximum_deficit_with_rank_one_centres": -3 + }, + { + "h": 10, + "ports": 1022, + "correction_rank": 681, + "maximum_deficit_with_rank_one_centres": 1 + }, + { + "h": 11, + "ports": 2046, + "correction_rank": 1365, + "maximum_deficit_with_rank_one_centres": -3 + } + ] +} diff --git a/research/boolean-disjointness-repair/check_zeta_corrector.py b/research/boolean-disjointness-repair/check_zeta_corrector.py new file mode 100644 index 0000000000..a7a8e067d6 --- /dev/null +++ b/research/boolean-disjointness-repair/check_zeta_corrector.py @@ -0,0 +1,36 @@ +"""Compute the exact rank of the additive correction to the disjointness map.""" +import json +from pathlib import Path + + +def rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length()-1 + if pivot in pivots: + row ^= pivots[pivot] + else: + pivots[pivot] = row + break + return len(pivots) + + +rows = [] +for h in range(2,12): + masks = list(range(1,2**h-1)) + matrix = [sum(1<=2.", + "rows": [ + { + "h": 2, + "proper_dimension": 2, + "inputs_checked_b": 4, + "inputs_checked_m": 16, + "kernel_size_b": 2, + "kernel_size_m": 4, + "rank_b": 1, + "rank_m": 2, + "maximal_deficit": 1 + }, + { + "h": 3, + "proper_dimension": 6, + "inputs_checked_b": 64, + "inputs_checked_m": 256, + "kernel_size_b": 2, + "kernel_size_m": 4, + "rank_b": 5, + "rank_m": 6, + "maximal_deficit": -3 + }, + { + "h": 4, + "proper_dimension": 14, + "inputs_checked_b": 16384, + "inputs_checked_m": 65536, + "kernel_size_b": 32, + "kernel_size_m": 64, + "rank_b": 9, + "rank_m": 10, + "maximal_deficit": 1 + } + ] +} diff --git a/research/boolean-disjointness-repair/independent/verify.py b/research/boolean-disjointness-repair/independent/verify.py new file mode 100644 index 0000000000..d0b04180ac --- /dev/null +++ b/research/boolean-disjointness-repair/independent/verify.py @@ -0,0 +1,73 @@ +"""Count each kernel without row reduction over F_2.""" + +import json +from pathlib import Path + + +def columns(h, proper): + masks = range(1, (1 << h) - 1) if proper else range(1 << h) + return [sum(((u == v) ^ (not (u & v))) << i + for i, u in enumerate(masks)) for v in masks] + + +def images(cols): + # Gray code changes one input bit at each step. + image = 0 + previous = 0 + for i in range(1 << len(cols)): + gray = i ^ (i >> 1) + if i: + changed = gray ^ previous + image ^= cols[changed.bit_length() - 1] + yield gray, image + previous = gray + + +def product(cols, value): + image = 0 + for i, col in enumerate(cols): + if (value >> i) & 1: + image ^= col + return image + + +rows = [] +for h in range(2, 5): + b = columns(h, proper=True) + m = columns(h, proper=False) + ones = (1 << len(b)) - 1 + b_kernel = [x for x, y in images(b) if y == 0] + m_kernel = [x for x, y in images(m) if y == 0] + preimages = [x for x, y in images(b) if y == ones] + assert all(x.bit_count() % 2 == 0 for x in b_kernel) + assert preimages and all(x.bit_count() % 2 == 1 for x in preimages) + assert len(m_kernel) == 2 * len(b_kernel) + assert product(b, ones) == 0 + for i in range(len(b)): + first = b[i] + second = product(b, first) + third = product(b, second) + assert first ^ second ^ third == ones + w = (1 << i) ^ first ^ second + assert product(b, w) == ones + assert w.bit_count() % 2 == 1 + for size in (len(b_kernel), len(m_kernel)): + assert size & (size - 1) == 0 + rank_b = len(b) - (len(b_kernel).bit_length() - 1) + rank_m = len(m) - (len(m_kernel).bit_length() - 1) + expected = ((1 << (h + 1)) - 2 * (-1) ** h - 3) // 3 + assert rank_b == expected + assert rank_m == rank_b + 1 + rows.append(dict(h=h, proper_dimension=len(b), + inputs_checked_b=1 << len(b), + inputs_checked_m=1 << len(m), + kernel_size_b=len(b_kernel), + kernel_size_m=len(m_kernel), rank_b=rank_b, + rank_m=rank_m, + maximal_deficit=2 * len(b) - 3 * rank_b)) + +result = dict(status="PASS", method="Exhaustive input enumeration by Gray code; no Gaussian elimination.", + scope="Exact checks for h=2,3,4 support the separate proof for all h>=2.", rows=rows) +path = Path(__file__).with_name("RESULT.json") +path.write_text(json.dumps(result, indent=2) + "\n") +print(json.dumps(result, indent=2)) diff --git a/research/boolean-disjointness-repair/review/CHECKED-FILES.json b/research/boolean-disjointness-repair/review/CHECKED-FILES.json new file mode 100644 index 0000000000..732a6818f7 --- /dev/null +++ b/research/boolean-disjointness-repair/review/CHECKED-FILES.json @@ -0,0 +1,13 @@ +{ + "HISTORICAL-REVIEW.txt": "e0ada149d05f1ca5bb6432095cbb591aa11de29dd0970134e92de0902b745e09", + "ORIGINS.json": "39e8913cc7d69b870cd6a3750c0a76cc117d43af6570d5fe6353551bb0e7ca4d", + "PROOF.txt": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427", + "README.md": "b37e421642070fe7769189655c29e8fd68100000292938ffbd4d5f777a1edc11", + "SOURCE-HASHES.json": "8348e10e56640cea3b5904d429d2993ddfff2344ceef98a36bf9ffa53b67c859", + "SOURCES.json": "254336a35d49ad4f771dde8093677ef5dfc42409d6a8c35c6f59e2149a05f47e", + "ZETA-CORRECTOR-CHECK.json": "8b5324c3821cead8eac68253395ae8e54470b3a107c854f62cb6a63e0a640ee2", + "check_zeta_corrector.py": "eaeb78e8a73cac408ef6570fee9e334081d2fc9b728170a29007a2d646b5b925", + "independent/RESULT.json": "08861a7b95425e64033658da62bad97ba994ad3f59126b3333ffd478f519dc2f", + "independent/verify.py": "2554a3346e53fd028c57023e09fc7131cc642e9d02cdbc2d432391bf21fca8ca", + "verify.py": "8b9525da24b0a21b047b2ce6315f072b27d456e6aa22fe9f0b51bcad0bdd1271" +} diff --git a/research/boolean-disjointness-repair/review/CURRENT-MAIN-OVERLAP.txt b/research/boolean-disjointness-repair/review/CURRENT-MAIN-OVERLAP.txt new file mode 100644 index 0000000000..f1f377392e --- /dev/null +++ b/research/boolean-disjointness-repair/review/CURRENT-MAIN-OVERLAP.txt @@ -0,0 +1,22 @@ +cef4b52f2a59009865bf8eabde1be3f159063703:docs/research/pr-ledger.md:161:| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. | +cef4b52f2a59009865bf8eabde1be3f159063703:research/coalescing-subset-audit/CLAIM.md:27: single omissions, not every Boolean-lattice edge with a code-disjoint +cef4b52f2a59009865bf8eabde1be3f159063703:research/coalescing-subset-audit/verify.py:150: 'nonconstant Boolean-lattice marginal') +cef4b52f2a59009865bf8eabde1be3f159063703:research/community-batch970-audit/pr943-context/docs/research/pr-ledger.md:155:| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. | +cef4b52f2a59009865bf8eabde1be3f159063703:research/community-batch970-audit/submitted/828/docs/research/pr-ledger.md:155:| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. | +cef4b52f2a59009865bf8eabde1be3f159063703:research/community-efficient1900-audit/originals/1007/docs/research/pr-ledger.md:161:| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. | +cef4b52f2a59009865bf8eabde1be3f159063703:research/complex-pooled-full-admission/frozen/pr4180/EVIDENCE.md:162:claim concerns CRT reservoir placement, and PR4172 concerns QQ16 comparison. +cef4b52f2a59009865bf8eabde1be3f159063703:research/cubic-scalar-caller-bounds/cubic/PROOF.md:99:contained in the span of the four u_i. Since `(zeta-1)I_3` has rank three, +cef4b52f2a59009865bf8eabde1be3f159063703:research/cubic-scalar-caller-bounds/cubic/frozen/cubic_gate.py:150: 'Specialize a putative full-ring identity to a primitive cubic root zeta. Target zeta I3 has rank(target-I)=3, so the query column directions span Q^3.', +cef4b52f2a59009865bf8eabde1be3f159063703:research/even-subset-dyadic-kernels/OVERLAP.md:10:prime-subset research; open PR172 (head +cef4b52f2a59009865bf8eabde1be3f159063703:research/even-subset-dyadic-kernels/OVERLAP.md:12:Boolean-lattice disjointness map and does not prove its missing identity fitting +cef4b52f2a59009865bf8eabde1be3f159063703:research/even-subset-dyadic-kernels/README.md:32:compiler contributors, is prior subset-based work. Open PR172's Boolean-lattice +cef4b52f2a59009865bf8eabde1be3f159063703:research/mixed-provider-admission/EVIDENCE.md:162:claim concerns CRT reservoir placement, and PR4172 concerns QQ16 comparison. +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-complete-cost/runtime.py:29: raw=(HERE/'inputs/PR4172-MANIFEST.json').read_bytes() +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-complete-cost/runtime.py:31: manifest=parse(raw);archive=(HERE/'inputs/PR4172.tar').read_bytes() +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-complete-cost/test_verify.py:144: ('inputs/PR4172-MANIFEST.json', 'retained manifest integrity'), +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-complete-cost/test_verify.py:145: ('inputs/PR4172.tar', 'retained archive integrity'), +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-complete-cost/test_verify.py:156: archive_path = self.package / 'inputs/PR4172.tar' +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-complete-cost/test_verify.py:157: manifest_path = self.package / 'inputs/PR4172-MANIFEST.json' +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-nonterminal-c8-tree/README.md:108:#4177's PR4172 archive. `RootLayer` first constructs the original `Machine`. +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-nonterminal-c8-tree/verify.py:120: with tarfile.open(ROOT / 'research/qq16-complete-cost/inputs/PR4172.tar') as archive: +cef4b52f2a59009865bf8eabde1be3f159063703:research/qq16-protected-return-caller/verify.py:67: with tarfile.open(ROOT/'research/qq16-complete-cost/inputs/PR4172.tar') as t: diff --git a/research/boolean-disjointness-repair/review/OVERLAP.json b/research/boolean-disjointness-repair/review/OVERLAP.json new file mode 100644 index 0000000000..3b0e429041 --- /dev/null +++ b/research/boolean-disjointness-repair/review/OVERLAP.json @@ -0,0 +1,170 @@ +{ + "base": "cef4b52f2a59009865bf8eabde1be3f159063703", + "git_pattern": "zeta.{0,35}(correct|rank|repair)|boolean.lattice|PR.?172([^0-9]|$)|#172([^0-9]|$)", + "matched_main_files": [ + "docs/research/pr-ledger.md", + "research/coalescing-subset-audit/CLAIM.md", + "research/coalescing-subset-audit/verify.py", + "research/community-batch970-audit/pr943-context/docs/research/pr-ledger.md", + "research/community-batch970-audit/submitted/828/docs/research/pr-ledger.md", + "research/community-efficient1900-audit/originals/1007/docs/research/pr-ledger.md", + "research/complex-pooled-full-admission/frozen/pr4180/EVIDENCE.md", + "research/cubic-scalar-caller-bounds/cubic/PROOF.md", + "research/cubic-scalar-caller-bounds/cubic/frozen/cubic_gate.py", + "research/even-subset-dyadic-kernels/OVERLAP.md", + "research/even-subset-dyadic-kernels/README.md", + "research/mixed-provider-admission/EVIDENCE.md", + "research/qq16-complete-cost/runtime.py", + "research/qq16-complete-cost/test_verify.py", + "research/qq16-nonterminal-c8-tree/README.md", + "research/qq16-nonterminal-c8-tree/verify.py", + "research/qq16-protected-return-caller/verify.py" + ], + "main_excerpts": [ + { + "path": "docs/research/pr-ledger.md", + "line": "161", + "excerpt": "| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. |" + }, + { + "path": "research/coalescing-subset-audit/CLAIM.md", + "line": "27", + "excerpt": " single omissions, not every Boolean-lattice edge with a code-disjoint" + }, + { + "path": "research/coalescing-subset-audit/verify.py", + "line": "150", + "excerpt": " 'nonconstant Boolean-lattice marginal')" + }, + { + "path": "research/community-batch970-audit/pr943-context/docs/research/pr-ledger.md", + "line": "155", + "excerpt": "| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. |" + }, + { + "path": "research/community-batch970-audit/submitted/828/docs/research/pr-ledger.md", + "line": "155", + "excerpt": "| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. |" + }, + { + "path": "research/community-efficient1900-audit/originals/1007/docs/research/pr-ledger.md", + "line": "161", + "excerpt": "| [#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) | mikey1201 | unreviewed | No exact-head review established; inspect contribution and dependencies. |" + }, + { + "path": "research/complex-pooled-full-admission/frozen/pr4180/EVIDENCE.md", + "line": "162", + "excerpt": "claim concerns CRT reservoir placement, and PR4172 concerns QQ16 comparison." + }, + { + "path": "research/cubic-scalar-caller-bounds/cubic/PROOF.md", + "line": "99", + "excerpt": "contained in the span of the four u_i. Since `(zeta-1)I_3` has rank three," + }, + { + "path": "research/cubic-scalar-caller-bounds/cubic/frozen/cubic_gate.py", + "line": "150", + "excerpt": " 'Specialize a putative full-ring identity to a primitive cubic root zeta. Target zeta I3 has rank(target-I)=3, so the query column directions span Q^3.'," + }, + { + "path": "research/even-subset-dyadic-kernels/OVERLAP.md", + "line": "10", + "excerpt": "prime-subset research; open PR172 (head" + }, + { + "path": "research/even-subset-dyadic-kernels/OVERLAP.md", + "line": "12", + "excerpt": "Boolean-lattice disjointness map and does not prove its missing identity fitting" + }, + { + "path": "research/even-subset-dyadic-kernels/README.md", + "line": "32", + "excerpt": "compiler contributors, is prior subset-based work. Open PR172's Boolean-lattice" + }, + { + "path": "research/mixed-provider-admission/EVIDENCE.md", + "line": "162", + "excerpt": "claim concerns CRT reservoir placement, and PR4172 concerns QQ16 comparison." + }, + { + "path": "research/qq16-complete-cost/runtime.py", + "line": "29", + "excerpt": " raw=(HERE/'inputs/PR4172-MANIFEST.json').read_bytes()" + }, + { + "path": "research/qq16-complete-cost/runtime.py", + "line": "31", + "excerpt": " manifest=parse(raw);archive=(HERE/'inputs/PR4172.tar').read_bytes()" + }, + { + "path": "research/qq16-complete-cost/test_verify.py", + "line": "144", + "excerpt": " ('inputs/PR4172-MANIFEST.json', 'retained manifest integrity')," + }, + { + "path": "research/qq16-complete-cost/test_verify.py", + "line": "145", + "excerpt": " ('inputs/PR4172.tar', 'retained archive integrity')," + }, + { + "path": "research/qq16-complete-cost/test_verify.py", + "line": "156", + "excerpt": " archive_path = self.package / 'inputs/PR4172.tar'" + }, + { + "path": "research/qq16-complete-cost/test_verify.py", + "line": "157", + "excerpt": " manifest_path = self.package / 'inputs/PR4172-MANIFEST.json'" + }, + { + "path": "research/qq16-nonterminal-c8-tree/README.md", + "line": "108", + "excerpt": "#4177's PR4172 archive. `RootLayer` first constructs the original `Machine`." + }, + { + "path": "research/qq16-nonterminal-c8-tree/verify.py", + "line": "120", + "excerpt": " with tarfile.open(ROOT / 'research/qq16-complete-cost/inputs/PR4172.tar') as archive:" + }, + { + "path": "research/qq16-protected-return-caller/verify.py", + "line": "67", + "excerpt": " with tarfile.open(ROOT/'research/qq16-complete-cost/inputs/PR4172.tar') as t:" + } + ], + "open_pr_count": 315, + "open_pr_matches": [ + { + "number": 172, + "head": "427b23bc79489e7b2b7548bfd434dd9670fd5c47", + "title": "Boolean-lattice (zeta) finite networks: compiler-level construction, in-tree assembly projection 15x-48x, obligations named (research record, draft)" + } + ], + "open_pr_snapshot_sha256": "e0413ab0c3f982d9f35949478226b6617131708fae1469d49e3eb08e82a098e5", + "git_returncode": 0, + "main_search_scope": [ + ":(glob)research/**/*.md", + ":(glob)research/**/*.txt", + ":(glob)research/**/*.py", + ":(glob)docs/**/*.md" + ], + "matched_main_lines": 22, + "earlier_searches": [ + { + "scope": "All research and docs", + "returncode": -9, + "partial_lines": 21 + }, + { + "scope": "research/ and docs/, excluding JSON and JSONL snapshots; one grep worker", + "returncode": -9 + } + ], + "semantic_reads": { + "research/even-subset-dyadic-kernels/README.md": "e5c3ce5bdfb673501198d108ff5c34297f72c034d9c3adbcca8eaa567a0c036e", + "research/even-subset-dyadic-kernels/PROOF.md": "ddc0d91dff486a4593c6f200191f12774406ea84f52bde8bf75d1a473b5e6d52", + "research/even-subset-dyadic-kernels/OVERLAP.md": "47bab638c180e79a022ae6a8bbfc0e4a72b777b388d0372f4f06f38d8bff5cfd", + "research/coalescing-subset-audit/CLAIM.md": "1b971dc525a86ca28e97c9ce979bdce2f8201b06b5940d2cc0bf553c5643de12" + }, + "conclusion": "No matching rank theorem found in the completed source and open-PR metadata screen. No global novelty claim." +} diff --git a/research/boolean-disjointness-repair/review/PREDECESSOR-SOURCES.json b/research/boolean-disjointness-repair/review/PREDECESSOR-SOURCES.json new file mode 100644 index 0000000000..20a573baf8 --- /dev/null +++ b/research/boolean-disjointness-repair/review/PREDECESSOR-SOURCES.json @@ -0,0 +1,70 @@ +{ + "pr": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/172", + "number": 172, + "state": "open", + "merged": false, + "mergeable": true, + "draft": true, + "body": "**Research record (draft).** Adds `research/zeta-family/` only; no existing files change.\n\n## Change and mathematical scope\n\nA new finite-network construction, the **zeta family**, on the Boolean lattice. Inputs are all nonzero, non-full bitmasks of `[h]`; the DAG is the **fast Yates zeta transform**; the side root for target `t` is `Z_{full^t}` = the sum of every input submasked into `complement(t)`, i.e. bit-disjoint from `t`. The in-tree side-root orthogonality contract (value span inside the orthogonal complement of the targets' addresses) holds **by construction**. No center roots, so `ell = 0` and the in-tree identity gives `deficit = 2v`. The binding quantity is the role density `R/v`.\n\nCompiled through the merged in-tree compiler (`scripts/paired_cube/frames.py::compile_graph`, the #144 path), priced through the in-tree assembly with both sides configured at the family saving (the two-sided projection):\n\n| h | v | R | R/v | saving | kappa | x PR #163 (reference) |\n|---|---|---|---|---|---|---|\n| 3 | 6 | 12 | 2.00 | 3.0519e-2 | 2.8764e-2 | 48.4x |\n| 4 | 14 | 38 | 2.71 | 1.7960e-2 | 1.7337e-2 | 29.2x |\n| 5 | 30 | 100 | 3.33 | 1.2279e-2 | 1.1985e-2 | 20.2x |\n| 6 | 62 | 242 | 3.90 | 9.0809e-3 | 8.9189e-3 | 15.0x |\n| 7 | 126 | 560 | 4.44 | 7.0573e-3 | 6.9591e-3 | 11.7x |\n| 8 | 254 | 1262 | 4.97 | 5.6780e-3 | 5.6142e-3 | 9.5x |\n\n**Changed hypotheses:** none to the retained interfaces. `upstream/` untouched; no certificates, patches or `scripts/` edited.\n\n**Open obligations (stated; this is not a reviewed headword claim).**\nA. Source histogram shape supplied explicitly for `h <= 6` (the in-tree default `Counter({2:v, h-4:v, 1:v})` is a dict literal whose duplicate keys collapse at `h in {5,6}` and is negative at `h=3`; the supplied `{2:v, 1:v(h-3)}` is the legal mass-`v(h-1)` form and is conservative). `h >= 7` uses the default unchanged.\nB. Centerless scope: `ell = 0` passes every in-tree assert; the role coordinate-star centers discharge in the retained notes is not re-derived.\nC. **Semantics:** the DAG computes `y_t = sum_{u&t=0} x_u` (checked literally below). Its service to the upstream reduction - the analogue of `H+K+B = I` - is not established here and is the main open obligation.\nD. The scalar word/replay **is included**: adjoint pre-reads on raw dirt, V-gates, compute, reads, full inverse; dirty scratch restored; four tamper controls rejected (mod 2^61-1 and integers; three seeds). Not built here: the physical placement/recycling layer. The graph verifies through the merged complex-side compiler path; the **bit-side path carries its own H0 = (I-J/9)/2 cap geometry and does not accept this graph as-is** (checked: rejects with 'root physical compatibility'), so the bit-side construction remains an obligation and every table number is a two-sided projection under A-C.\n\n## Validation\n\n`python3 research/zeta-family/verify.py` (stdlib only, run without `-O`, about 1 second):\n\n- **Finite identity check (not a proof):** a literal semantic evaluation of the DAG - every root equals `sum_{u: u&t=0} x_u` for random inputs, both seeds, `h = 3..8`.\n- The scalar word/replay: dirty scratch on every register, restored by the inverse pass; the map `y_t = sum_{u&t=0} x_u` recovered exactly; four tamper controls rejected, on two rings and three seeds, `h = 3..8`.\n- The in-tree compiler's full assert chain on each graph, including `mass == h*R + ell` and `deficit == 2v - 3*ell`.\n- The in-tree 47-constraint assembly with both sides at the family saving (`b < 1/32`, `b > a`, all 47 slacks, seven margins).\n- `make paired-cube-verify`: PASS (recorded; the change adds files only, so the selected incremental target is unaffected).\n- CI: `.github/workflows/zeta-family.yml` runs the package verifier on Python 3.11 and 3.13.\n\nThe frontier multiple is re-derived from PR #163's certified number and is a reference only.\n\n## Credits\n\nThe compiler (`scripts/paired_cube/frames.py`), the assembly, the side-root orthogonality contract and the identity bookkeeping are icekylinx's #144 lineage, used unchanged. Graph construction, semantic evaluation and the audit table by this contribution, prepared with AI assistance (Cline). Apache-2.0.\n", + "title": "Boolean-lattice (zeta) finite networks: compiler-level construction, in-tree assembly projection 15x-48x, obligations named (research record, draft)", + "base": "main", + "base_sha": "d1d6c070f5a8c684727ee7ec35d930f9ebfa9758", + "head": "research/zeta-family", + "head_sha": "427b23bc79489e7b2b7548bfd434dd9670fd5c47", + "head_repo_id": 1411561745, + "head_repo_full_name": "mikey1201/integer-mult-bounds", + "merge_commit_sha": "d7caee0cf109c5c51f36b0cf5e27a63978141683", + "user": { + "login": "mikey1201", + "name": "mikey1201", + "email": null, + "avatar_url": "https://avatars.githubusercontent.com/u/159095682?v=4", + "id": 159095682 + }, + "requested_reviewers": null, + "requested_team_reviewers": null, + "diff": null, + "comments": null, + "created_at": "2026-10-09T09:05:31Z", + "updated_at": "2026-10-09T09:29:09Z", + "closed_at": null, + "merged_at": null, + "commits": 3, + "changed_files": 6, + "additions": 322, + "deletions": 0, + "display_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/172", + "display_title": "Boolean-lattice (zeta) finite networks: compiler-level construction, in-tree assembly projection 15x-48x, obligations named (research record, draft)" + }, + "pinned_files": { + "NOTICE": { + "content": "This research package is Apache-2.0. It uses, unchanged, the compiler\n(scripts/paired_cube/frames.py), the assembly (scripts/structured_bulk_assembly.py)\nand the side-root orthogonality contract from icekylinx's PR #144 lineage; their\nretained copyright and assistance notices apply. Graph construction, semantic\nevaluation and the audit table are new here, prepared with AI assistance (Cline).\n", + "encoding": "utf-8", + "sha": "5d32242250b85a59268cd27a2e63cb615c4850d9", + "display_url": "https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/NOTICE", + "display_title": "NOTICE" + }, + "README.md": { + "content": "# The zeta family: Boolean-lattice finite networks\n\nUnder the retained fixed-alphabet interfaces, the construction below compiles\nthrough the merged in-tree compiler\n(`scripts/paired_cube/frames.py::compile_graph`, the #144 path) and its profile\nprices through the in-tree assembly (`scripts/structured_bulk_assembly.py`) with\nboth sides configured at the family saving (the two-sided projection; the\nbit-side realization is an open obligation, see D):\n\n| h | v | R | R/v | saving (both sides) | kappa | x PR #163 |\n|---|---|---|---|---|---|---|\n| 3 | 6 | 12 | 2.00 | 3.0519e-2 | 2.8764e-2 | 48.4x |\n| 4 | 14 | 38 | 2.71 | 1.7960e-2 | 1.7337e-2 | 29.2x |\n| 5 | 30 | 100 | 3.33 | 1.2279e-2 | 1.1985e-2 | 20.2x |\n| 6 | 62 | 242 | 3.90 | 9.0809e-3 | 8.9189e-3 | 15.0x |\n| 7 | 126 | 560 | 4.44 | 7.0573e-3 | 6.9591e-3 | 11.7x |\n| 8 | 254 | 1262 | 4.97 | 5.6780e-3 | 5.6142e-3 | 9.5x |\n\n**Construction.** Inputs are all nonzero, non-full bitmasks of [h]. The DAG is\nthe fast Yates zeta transform over the Boolean lattice: accumulators\n`A_j(W)`, h*2^(h-1) - (2^h - 1) additions. The side root for target `t` is\n`Z_{full^t}`: the sum of every input submasked into `complement(t)`, i.e. bit-\ndisjoint from `t`. The side-root orthogonality contract is met by construction:\nthe accumulated addresses are exactly the directions orthogonal to `t`\n(integer disjointness), so every value span lies in the required complement.\nThere are no center roots, so `ell = 0` and the in-tree identity gives\n`deficit = 2v` (maximal data freeness). `R/v = 2.0 .. 5.0` is the binding\nquantity: `kappa ~ 1/(3h (2 + R/v) E)`.\n\n**Verify.**\n\n python3 research/zeta-family/verify.py\n\nStdlib only, run without `-O`, about 2 seconds. It checks (1) a literal semantic\nevaluation of the DAG: every root equals `sum_{u: u&t=0} x_u` for random inputs,\nboth seeds; (1b) the scalar word and its transparency replay (`word.py`) on two\nrings (mod 2^61-1 and the integers), three seeds each, with four tamper controls\n(skipped adjoint pre-read, skipped post-read, skipped inverse gate, flipped\ncoefficient) required to fail; (2) their compiler's full assert chain on each graph (value spans\ninside frames, backward-intersection annotators, root legality, target chains,\n`mass == h*R + ell`, `deficit == 2v - 3*ell`); (3) their 47-constraint\nassembly with both sides at the family saving, all slacks and seven margins,\n`b < 1/32`. The frontier multiple is re-derived from PR #163's certified number\nand is used for reference only.\n\n**Scope and open obligations (explicit).**\n\nA. The source-data histogram shape is supplied explicitly for `h <= 6`. The\n in-tree default `Counter({2:v, h-4:v, 1:v})` is a dict literal whose\n duplicate keys collapse at `h in {5,6}` and whose key is negative at `h=3`;\n the supplied shape `{2:v, 1:v(h-3)}` is the legal mass-`v(h-1)` form and is\n conservative (more rank-1 children, hence larger E) relative to a\n big-stride shape. At `h >= 7` the in-tree default is used unchanged.\nB. Centerless scope: `ell = 0` passes every in-tree assert. Whatever role the\n coordinate-star centers discharge in the retained proof notes is not\n re-derived here and is an open written obligation.\nC. The DAG computes the orthogonal-broadcast map `y_t = sum_{u: u&t=0} x_u`\n (checked literally above). Its service to the upstream reduction - the\n analogue of the `H+K+B = I` scalar ledger - is not established here and is\n the main open obligation.\nD. The scalar word/replay IS included (`word.py`: adjoint pre-reads, V-gates,\n compute, reads, full inverse; dirty scratch; tamper controls; two rings).\n Not built here: the physical placement/recycling layer and the scalar-domain\n realizations. The graph is verified through the merged\n complex-side compiler path; the bit-side path carries its own H0 = (I-J/9)/2\n cap geometry and does not accept this graph as-is (checked: it rejects with\n 'root physical compatibility'). The bit-side construction is therefore an\n explicit obligation, and every table number is a two-sided projection under\n obligations A-C. This package is a compiled graph and its in-tree-verified\n profile, not a certificate of multiplication.\n\n**Credits.** The compiler (`frames.py`), the assembly, the side-root\northogonality contract and the identity bookkeeping are icekylinx's PR #144\nlineage (with the retained notices), used unchanged. Graph construction,\nsemantic evaluation and the audit table by this contribution; prepared with\nAI assistance (Cline). Apache-2.0.\n", + "encoding": "utf-8", + "sha": "f6bb2034a61f01e0dfe3d4eb38b16d1cde65f33a", + "display_url": "https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/README.md", + "display_title": "README.md" + }, + "zeta.py": { + "content": "#!/usr/bin/env python3\n\"\"\"The zeta family: a finite-network construction on the Boolean lattice.\n\nGraph: inputs = all nonzero, non-full bitmasks of [h] (v = 2^h - 2).\nDAG: the fast Yates zeta transform A_j(W) accumulators (h*2^(h-1) - (2^h-1) adds).\nRoots: one side root per input t (except the all-ones target), delivering\nZ_{full^t} = sum over inputs submasked into complement(t), i.e. bit-disjoint\nfrom t. Their side-root contract (span contained in the orthogonal complement\nof the targets' addresses) holds BY CONSTRUCTION: the zeta accumulates only\naddresses bit-disjoint from t.\nNo centers: ell = 0; the compiler derives deficit = 2v.\n\"\"\"\n\n\ndef zeta_graph(h):\n full = (1 << h) - 1\n masks = list(range(1, full))\n v = len(masks)\n idx = {u: i for i, u in enumerate(masks)}\n args = [None] * v\n prev = {u: idx[u] for u in masks}\n for j in range(h):\n cur = {}\n for W in masks:\n node = prev[W]\n lower = W ^ (1 << j)\n if (W >> j) & 1 and lower != 0 and lower in prev:\n args.append([node, prev[lower]])\n node = len(args) - 1\n cur[W] = node\n prev = cur\n roots = [dict(node=prev[full ^ t], kind='side', targets=[idx[t]]) for t in masks if full ^ t]\n src = {2: v}\n if h >= 4:\n src[1] = v * (h - 3) # legal w(h-1) mass; the in-tree default\n # collapses at h in {5,6} (duplicate keys)\n return dict(h=h, inputs=masks, args=args, roots=roots, matching_frames='coordinate',\n source_data_histogram={str(r): n for r, n in src.items()})\n", + "encoding": "utf-8", + "sha": "5d69f4b2cf1b32ab0f03b4399e1f2fea5be02904", + "display_url": "https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/zeta.py", + "display_title": "zeta.py" + }, + "verify.py": { + "content": "#!/usr/bin/env python3\n\"\"\"Verify the zeta family: semantic evaluation, THEIR compiler, THEIR assembly.\nStdlib only; run without -O. Prints PASS with the certified table.\"\"\"\nimport random\nimport sys\nfrom fractions import Fraction as Q\nfrom pathlib import Path\n\nROOT = Path(__file__).resolve().parents[2]\nsys.path.insert(0, str(ROOT / 'scripts'))\nsys.path.insert(0, str(ROOT / 'scripts/paired_cube'))\nsys.path.insert(0, str(ROOT / 'research/zeta-family'))\nfrom paired_cube.frames import compile_graph # THEIR compiler\nfrom structured_bulk_assembly import assembly # THEIR 47-constraint assembly\nfrom zeta import zeta_graph\nfrom word import run_controls, replay\n\nFRONTIER = Q(593970203079492, 10**18) # PR #163, for reference only\nEXPECTED = {3: '3.0519e-02', 4: '1.7960e-02', 5: '1.2279e-02',\n 6: '9.0809e-03', 7: '7.3150e-03', 8: '5.9618e-03'} # roots (k>=7: default source)\n\n\ndef dummy_bridge():\n E = 2**200\n return dict(semantic=dict(E=E, strict_literal_gap=E, B=2**80 + E, C0=32 * 66 * (2**80 + E)**2,\n C1=1, induction_gap=E, fixed_odd_divisor=3),\n rows=dict(degree=70000, coefficient=100, degree_gap=70000 - 204))\n\n\ndef semantics(g, seed):\n rng = random.Random(seed)\n x = [rng.randrange(1, 10**6) for _ in g['inputs']]\n val = list(x) + [0] * (len(g['args']) - len(g['inputs']))\n for i in range(len(g['inputs']), len(g['args'])):\n a, b = g['args'][i]\n val[i] = val[a] + val[b]\n for r in g['roots']:\n t = g['inputs'][r['targets'][0]]\n if val[r['node']] != sum(x[i] for i, u in enumerate(g['inputs']) if (u & t) == 0):\n return False\n return True\n\n\ndef main():\n assert not sys.flags.optimize, 'run without -O'\n print('h v R R/v root kappa x-frontier')\n for h in (3, 4, 5, 6, 7, 8):\n g = zeta_graph(h)\n for seed in (1, 7):\n assert semantics(g, seed), 'semantic evaluation failed at seed %d' % seed\n assert run_controls(g), 'scalar word/replay controls failed' # the word layer\n prof, _ = compile_graph(g, []) # THEIR compiler, all asserts\n root = prof['numerical_complex_root']\n assert root is not None\n a = Q(int(root * 10**12), 10**12)\n b = a * (1 + Q(1, 1000))\n res = assembly(a, b, dummy_bridge(), Q(1, 10**12), beta=Q(1, 10**6)) # THEIR assembly\n kap = res['minimum_margin']\n assert float(kap) / float(FRONTIER) > 9.0, 'frontier multiple'\n print('%d %4d %5d %6.2f %10.4e %10.4e %8.1fx' % (\n h, prof['v'], prof['R'], prof['R'] / prof['v'], root, float(kap), float(kap) / float(FRONTIER)))\n print('PASS: semantic evaluation, scalar word/replay with tamper controls, in-tree compiler identities, in-tree assembly')\n\n\nif __name__ == '__main__':\n main()\n", + "encoding": "utf-8", + "sha": "bfa2221de40fc82db52c3ed1e7e11f71d6a29b52", + "display_url": "https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/verify.py", + "display_title": "verify.py" + } + } +} diff --git a/research/boolean-disjointness-repair/review/RESULT.json b/research/boolean-disjointness-repair/review/RESULT.json new file mode 100644 index 0000000000..249920b754 --- /dev/null +++ b/research/boolean-disjointness-repair/review/RESULT.json @@ -0,0 +1,110 @@ +{ + "baseline": { + "returncode": 0, + "stdout": "PASS check_zeta_corrector.py\nPASS independent/verify.py\nPASS_BOOLEAN_DISJOINTNESS_REPAIR h=2..11 independent_kernels=2..4 no_new_kappa\n", + "stderr": "" + }, + "baseline_with_pythonoptimize_1": { + "returncode": 0, + "stdout": "PASS check_zeta_corrector.py\nPASS independent/verify.py\nPASS_BOOLEAN_DISJOINTNESS_REPAIR h=2..11 independent_kernels=2..4 no_new_kappa\n", + "stderr": "" + }, + "negative_controls": [ + { + "name": "proof_hash", + "repinned": false, + "pythonoptimize": "1", + "expected_error": "Source hash mismatch: PROOF.txt", + "returncode": 1, + "stdout": "", + "stderr": "Traceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-repair-review-tn0fx6_u/package/verify.py\", line 12, in \n raise ValueError('Source hash mismatch: '+name)\nValueError: Source hash mismatch: PROOF.txt\n" + }, + { + "name": "wrong_rank_formula", + "repinned": true, + "pythonoptimize": "1", + "expected_error": "AssertionError", + "returncode": 1, + "stdout": "", + "stderr": "Traceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-repair-review-whtnamyj/package/verify.py\", line 21, in \n raise ValueError(script+'\\n'+run.stderr)\nValueError: check_zeta_corrector.py\nTraceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-disjointness-repair-4wbqetpq/package/check_zeta_corrector.py\", line 26, in \n assert actual == formula\n ^^^^^^^^^^^^^^^^^\nAssertionError\n\n" + }, + { + "name": "wrong_full_kernel_factor", + "repinned": true, + "pythonoptimize": "1", + "expected_error": "AssertionError", + "returncode": 1, + "stdout": "PASS check_zeta_corrector.py\n", + "stderr": "Traceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-repair-review-hcw3zr7v/package/verify.py\", line 21, in \n raise ValueError(script+'\\n'+run.stderr)\nValueError: independent/verify.py\nTraceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-disjointness-repair-2imjrbh5/package/independent/verify.py\", line 44, in \n assert len(m_kernel) == 3 * len(b_kernel)\n ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\nAssertionError\n\n" + }, + { + "name": "wrong_preimage_parity", + "repinned": true, + "pythonoptimize": "1", + "expected_error": "AssertionError", + "returncode": 1, + "stdout": "PASS check_zeta_corrector.py\n", + "stderr": "Traceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-repair-review-i4hgrm4a/package/verify.py\", line 21, in \n raise ValueError(script+'\\n'+run.stderr)\nValueError: independent/verify.py\nTraceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-disjointness-repair-7264m68o/package/independent/verify.py\", line 43, in \n assert preimages and all(x.bit_count() % 2 == 0 for x in preimages)\n ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\nAssertionError\n\n" + }, + { + "name": "receipt_mismatch", + "repinned": true, + "pythonoptimize": "1", + "expected_error": "Receipt mismatch: ZETA-CORRECTOR-CHECK.json", + "returncode": 1, + "stdout": "", + "stderr": "Traceback (most recent call last):\n File \"/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/boolean-repair-review-u5qb7dqj/package/verify.py\", line 23, in \n raise ValueError('Receipt mismatch: '+result)\nValueError: Receipt mismatch: ZETA-CORRECTOR-CHECK.json\n" + } + ], + "independent_set_matrix_rows": [ + { + "h": 2, + "rank_b": 1, + "rank_m": 2 + }, + { + "h": 3, + "rank_b": 5, + "rank_m": 6 + }, + { + "h": 4, + "rank_b": 9, + "rank_m": 10 + }, + { + "h": 5, + "rank_b": 21, + "rank_m": 22 + }, + { + "h": 6, + "rank_b": 41, + "rank_m": 42 + }, + { + "h": 7, + "rank_b": 85, + "rank_m": 86 + } + ], + "excluded_boundary_h1": { + "rank_b": 0, + "invalid_formula_value": 1 + }, + "checked_file_sha256": { + "HISTORICAL-REVIEW.txt": "e0ada149d05f1ca5bb6432095cbb591aa11de29dd0970134e92de0902b745e09", + "ORIGINS.json": "39e8913cc7d69b870cd6a3750c0a76cc117d43af6570d5fe6353551bb0e7ca4d", + "PROOF.txt": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427", + "README.md": "b37e421642070fe7769189655c29e8fd68100000292938ffbd4d5f777a1edc11", + "SOURCE-HASHES.json": "8348e10e56640cea3b5904d429d2993ddfff2344ceef98a36bf9ffa53b67c859", + "SOURCES.json": "254336a35d49ad4f771dde8093677ef5dfc42409d6a8c35c6f59e2149a05f47e", + "ZETA-CORRECTOR-CHECK.json": "8b5324c3821cead8eac68253395ae8e54470b3a107c854f62cb6a63e0a640ee2", + "check_zeta_corrector.py": "eaeb78e8a73cac408ef6570fee9e334081d2fc9b728170a29007a2d646b5b925", + "independent/RESULT.json": "08861a7b95425e64033658da62bad97ba994ad3f59126b3333ffd478f519dc2f", + "independent/verify.py": "2554a3346e53fd028c57023e09fc7131cc642e9d02cdbc2d432391bf21fca8ca", + "verify.py": "8b9525da24b0a21b047b2ce6315f072b27d456e6aa22fe9f0b51bcad0bdd1271" + }, + "python": "3.14.7 (main, Aug 5 2026, 10:29:49) [Clang 21.0.0 (clang-2100.1.1.101)]", + "status": "PASS_INDEPENDENT_BOOLEAN_REPAIR_REVIEW_CHECKS" +} diff --git a/research/boolean-disjointness-repair/review/REVIEW.md b/research/boolean-disjointness-repair/review/REVIEW.md new file mode 100644 index 0000000000..d86fb8cf25 --- /dev/null +++ b/research/boolean-disjointness-repair/review/REVIEW.md @@ -0,0 +1,155 @@ +# Independent review: Boolean disjointness repair + +Verdict: PASS for the stated rank theorem over F2 and its conditional +additive rank-one cost consequence. No material proof or replay error was +found. This is an independent OpenAI Codex agent review. It is not human +review or formal proof verification. + +The checked package is `boolean-disjointness-repair`. `RESULT.json` gives +the SHA-256 hash of each checked file. The publication base is +`cef4b52f2a59009865bf8eabde1be3f159063703`. + +## Claims checked + +Let A_h be the disjointness matrix on the nonempty proper subsets of [h], +over F2, and put B_h = I + A_h. For every integer h >= 2, the proof gives + +```text +rank_F2(B_h) = (2^(h+1) - 2*(-1)^h - 3)/3. +``` + +If B_h is a sum of ell rank-one matrices over F2, then ell is at least +this rank. Under the assumed ledger D = 2v - 3ell with v = 2^h - 2, +this gives D <= 2*(-1)^h - 1. The bound is 1 for even h and -3 for odd h. + +The cost consequence requires that additive rank-one model and ledger. +The package does not prove that all physical corrections have that form. +It does not cover a product of general maps, a different source basis, +another endpoint, or a different compiler. No rational or complex-field +extension is submitted. No complete supplier or kappa improvement follows. + +## Proof review + +The 2-by-2 factor L = [[1,1],[1,0]] has two distinct eigenvalues omega +and omega^2 over F4. It satisfies L^3 = I. Thus its h-fold tensor power +T_h has order dividing 3 and is diagonalizable. If a_h counts its +eigenvalues equal to 1, tensoring once more gives a_(h+1) = 2^h - a_h. +The initial value a_0 = 1 gives the stated closed formula. Extension from +F2 to F4 preserves rank, since a nonzero minor remains nonzero. + +The deletion of the empty and full subsets is the main step. I checked +the displayed block matrix directly. If e_0 is the empty-set column, +T_h e_0 is the all-one column and T_h^2 e_0 is the full-set column. +Hence P e_0, for P = I + T_h + T_h^2, is exactly the column supported on +the proper nonempty subsets. It is nonzero when h >= 2. Also P(I+T_h)=0. + +For B_h z = 0, applying P to (I+T_h)(0,z,0) proves that z has even +parity. Since B_h is symmetric, the all-one column is in its image. +Choose B_h w = 1. Applying the same identity to (1,w,1) proves that w +has odd parity. The full kernel is then the direct sum of the embedded +kernel of B_h and the span of (1,w,1). Its nullity is one larger, so +rank(I+T_h) = rank(B_h) + 1. This proves the claimed formula. + +I also checked the alternate deletion proof in `HISTORICAL-REVIEW.txt`. +The central block identity gives B_h^3 + B_h^2 + B_h = J. The vector +(I+B_h+B_h^2)e has image 1 and odd parity. These claims agree with the +first proof. The hypothesis h >= 2 is necessary for this formula: at +h = 1, B_h is empty and has rank 0, while the proposed expression is 1. + +Finally, rank of a sum of ell rank-one matrices is at most ell. +Substituting the proved lower bound for ell into the assumed ledger gives +the stated deficit bound. No other implementation cost is inferred. + +## Fresh checks + +From the workspace root, I ran: + +```sh +python3 -B work/project-final-cleanup-20261022/early-remainder-audit/packages/boolean-disjointness-repair/verify.py +python3 -B work/project-final-cleanup-20261022/reviews/boolean-repair/review_checks.py +``` + +The first command passed exact binary rank elimination for h=2..11 and +the separate complete kernel enumeration for h=2,3,4. It reproduced both +committed mathematical receipts. The second command passed with this output: + +```text +PASS_INDEPENDENT_BOOLEAN_REPAIR_REVIEW_CHECKS +baseline=PASS pythonoptimize_1=PASS negative_controls=5 independent_set_matrices=h2..7 +h1_excluded=CONFIRMED all_h_claim=WRITTEN_PROOF_ONLY no_new_kappa +``` + +The review script also accepts the package path as its one argument. +It constructs the matrices from sets and checks their ranks independently +for h=2..7. The two full receipt replays pass both with no optimization +environment and with `PYTHONOPTIMIZE=1`. The final wrapper uses isolated +child interpreters, so that environment cannot disable their assertions. + +Five controls run on temporary copies, with `PYTHONOPTIMIZE=1` set: + +- A changed proof without a new hash is rejected by the source hash check. +- A wrong rank formula, with its source hash updated, fails the rank assertion. +- A wrong full-kernel factor, with its hash updated, fails the kernel assertion. +- A wrong preimage parity, with its hash updated, fails the parity assertion. +- A changed receipt, with its hash updated, fails the fresh receipt comparison. + +These controls test different failure paths. They do not prove the theorem +for arbitrary h. That claim rests on the reviewed written proof. No +selected-supplier replay, complete repository test suite, Lean check, or +physical circuit construction was run or is claimed. + +## Source and attribution check + +I read the PR description standard before this review. I fetched live +[PR #172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) and +verified its head `427b23bc79489e7b2b7548bfd434dd9670fd5c47`. It remains +an open draft. Its +[pinned README](https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/README.md), +[graph source](https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/zeta.py), +and verifier support the disjointness endpoint and the stated ledger. +They leave the required scalar identity as an open obligation. This rank +theorem addresses the specified F2 additive repair of that obligation. + +The pinned +[NOTICE](https://github.com/mikey1201/integer-mult-bounds/blob/427b23bc79489e7b2b7548bfd434dd9670fd5c47/research/zeta-family/NOTICE) +has Git blob `5d32242250b85a59268cd27a2e63cb615c4850d9`. It credits +@icekylinx for the +[PR #144](https://github.com/CrocSwap/integer-mult-bounds/pull/144) +compiler, orthogonality contract, and bookkeeping lineage, and discloses +Cline assistance for PR #172. I verified that contributor login against +PR #144. The package retains these credits without claiming that work as +new. No predecessor code is imported into the new mathematical checkers. + +`PREDECESSOR-SOURCES.json` records the fetched source bytes and metadata. +Every original-workspace hash in `ORIGINS.json` matches the existing +historical file. The changed proof-reference paths and the removal of +unrelated routing discussion match the listed adaptations. The submitted +proof itself is byte-identical to its original local version. + +## Overlap check and publication limits + +`OVERLAP.json` records the exact search terms, source scope, base pin, and +hash of the supplied 315-PR snapshot. The matching open contribution is +PR #172 itself; it does not contain this rank theorem. The overlap check +completed for Markdown, text, and Python sources under `research/`, plus +Markdown under `docs/`. Two earlier broad searches were killed; their +partial output is not treated as a completed check. The final search uses +one worker and exits successfully. + +I read the matching +[even-subset kernel proof](https://github.com/CrocSwap/integer-mult-bounds/blob/cef4b52f2a59009865bf8eabde1be3f159063703/research/even-subset-dyadic-kernels/PROOF.md) +and its README and overlap note. It constructs a different fitting kernel +on a fixed even-subset shell with complementary labels. It neither proves +this all-subset disjointness rank formula nor contradicts the stated +restriction to this endpoint. The coalescing-subset audit match concerns +finite frame edits, not this matrix. Other matches are old ledgers, +unrelated cubic scalar rank bounds, and PR-number substring matches. + +This is a bounded repository and open-PR check, not a novelty claim against +all mathematical literature or a proof that every archived JSON receipt +and compressed source has been semantically reviewed. + +The coordinating agent must check the final PR description, commit-pinned +links, and GitHub rendering. Those publication actions are outside this +review. Mathematical claims in the final description must retain the F2 +field, additive rank-one model, assumed ledger, and absence of a kappa gain. diff --git a/research/boolean-disjointness-repair/review/review_checks.py b/research/boolean-disjointness-repair/review/review_checks.py new file mode 100644 index 0000000000..c2c68ade3e --- /dev/null +++ b/research/boolean-disjointness-repair/review/review_checks.py @@ -0,0 +1,125 @@ +"""Run the submitted replay and isolated controls for the rank proof review.""" +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +PACKAGE = (Path(sys.argv[1]).resolve() if len(sys.argv) == 2 else + HERE.parents[1] / 'early-remainder-audit/packages/boolean-disjointness-repair') + + +def run(path, optimize=None): + env = dict(os.environ) + env.pop('PYTHONOPTIMIZE', None) + if optimize is not None: + env['PYTHONOPTIMIZE'] = str(optimize) + result = subprocess.run([sys.executable, '-B', str(path / 'verify.py')], + cwd=path, env=env, capture_output=True, text=True, + timeout=120) + return dict(returncode=result.returncode, stdout=result.stdout, + stderr=result.stderr) + + +def change(path, name, old, new, repin): + source = path / name + text = source.read_text() + if text.count(old) != 1: + raise ValueError('Control needs one matching source string: ' + name) + source.write_text(text.replace(old, new)) + if repin: + manifest = path / 'SOURCE-HASHES.json' + hashes = json.loads(manifest.read_text()) + hashes[name] = hashlib.sha256(source.read_bytes()).hexdigest() + manifest.write_text(json.dumps(hashes, indent=2) + '\n') + + +results = {'baseline': run(PACKAGE), + 'baseline_with_pythonoptimize_1': run(PACKAGE, optimize=1), + 'negative_controls': []} +if results['baseline']['returncode'] != 0: + raise ValueError('Submitted replay failed') +if results['baseline_with_pythonoptimize_1']['returncode'] != 0: + raise ValueError('Submitted replay failed with PYTHONOPTIMIZE=1') + +controls = [ + ('proof_hash', 'PROOF.txt', 'Let h >= 2.', 'Let h >= 1.', False, + 'Source hash mismatch: PROOF.txt'), + ('wrong_rank_formula', 'check_zeta_corrector.py', + 'formula = (2**(h+1)-2*(-1)**h-3)//3', + 'formula = (2**(h+1)-2*(-1)**h-6)//3', True, 'AssertionError'), + ('wrong_full_kernel_factor', 'independent/verify.py', + 'len(m_kernel) == 2 * len(b_kernel)', + 'len(m_kernel) == 3 * len(b_kernel)', True, 'AssertionError'), + ('wrong_preimage_parity', 'independent/verify.py', + 'preimages and all(x.bit_count() % 2 == 1 for x in preimages)', + 'preimages and all(x.bit_count() % 2 == 0 for x in preimages)', + True, 'AssertionError'), + ('receipt_mismatch', 'ZETA-CORRECTOR-CHECK.json', + '"correction_rank": 1,', '"correction_rank": 0,', True, + 'Receipt mismatch: ZETA-CORRECTOR-CHECK.json'), +] +for label, name, old, new, repin, expected in controls: + with tempfile.TemporaryDirectory(prefix='boolean-repair-review-') as temp: + copy = Path(temp) / 'package' + shutil.copytree(PACKAGE, copy) + change(copy, name, old, new, repin) + result = run(copy, optimize=1) + if result['returncode'] == 0 or expected not in result['stderr']: + raise ValueError('Control was not rejected at its intended check: ' + label) + results['negative_controls'].append(dict(name=label, repinned=repin, + pythonoptimize='1', + expected_error=expected, **result)) + +# Construct disjointness by set membership, rather than bit-mask intersection. +# The full matrix must be one rank larger than the proper matrix. For h=1, +# the proper matrix is empty and the stated formula would be false. +def matrix(h, proper): + masks = range(1, 2**h - 1) if proper else range(2**h) + subsets = [{j for j in range(h) if (u >> j) & 1} for u in masks] + return [[int(i == j) ^ int(s.isdisjoint(t)) + for j, t in enumerate(subsets)] for i, s in enumerate(subsets)] + + +def rank(a): + a = [row[:] for row in a] + r = 0 + for c in range(len(a)): + pivot = next((i for i in range(r, len(a)) if a[i][c]), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + for i in range(r + 1, len(a)): + if a[i][c]: + a[i] = [x ^ y for x, y in zip(a[i], a[r])] + r += 1 + return r + + +results['independent_set_matrix_rows'] = [] +for h in range(2, 8): + b_rank = rank(matrix(h, True)) + m_rank = rank(matrix(h, False)) + expected = (2**(h + 1) - 2 * (-1)**h - 3) // 3 + if b_rank != expected or m_rank != b_rank + 1: + raise ValueError('Independent set matrix check failed') + results['independent_set_matrix_rows'].append(dict(h=h, rank_b=b_rank, + rank_m=m_rank)) +results['excluded_boundary_h1'] = dict(rank_b=rank(matrix(1, True)), + invalid_formula_value=(2**2 + 2 - 3)//3) +if results['excluded_boundary_h1'] != {'rank_b': 0, 'invalid_formula_value': 1}: + raise ValueError('The h=1 scope check failed') +results['checked_file_sha256'] = { + str(p.relative_to(PACKAGE)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.rglob('*')) if p.is_file() +} +results['python'] = sys.version +results['status'] = 'PASS_INDEPENDENT_BOOLEAN_REPAIR_REVIEW_CHECKS' +(HERE / 'RESULT.json').write_text(json.dumps(results, indent=2) + '\n') +print(results['status']) +print('baseline=PASS pythonoptimize_1=PASS negative_controls=5 independent_set_matrices=h2..7') +print('h1_excluded=CONFIRMED all_h_claim=WRITTEN_PROOF_ONLY no_new_kappa') diff --git a/research/boolean-disjointness-repair/verify.py b/research/boolean-disjointness-repair/verify.py new file mode 100644 index 0000000000..ac66bffbb6 --- /dev/null +++ b/research/boolean-disjointness-repair/verify.py @@ -0,0 +1,25 @@ +"""Replay rank elimination and the separate exhaustive kernel checks.""" +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path +HERE = Path(__file__).resolve().parent +for name, expected in json.loads((HERE/'SOURCE-HASHES.json').read_text()).items(): + if hashlib.sha256((HERE/name).read_bytes()).hexdigest() != expected: + raise ValueError('Source hash mismatch: '+name) +with tempfile.TemporaryDirectory(prefix='boolean-disjointness-repair-') as temp: + work = Path(temp)/'package' + shutil.copytree(HERE, work, ignore=shutil.ignore_patterns('__pycache__')) + for script, result in [('check_zeta_corrector.py','ZETA-CORRECTOR-CHECK.json'), + ('independent/verify.py','independent/RESULT.json')]: + run = subprocess.run([sys.executable,'-I','-B',str(work/script)],cwd=work, + capture_output=True,text=True,timeout=120) + if run.returncode: + raise ValueError(script+'\n'+run.stderr) + if json.loads((work/result).read_text()) != json.loads((HERE/result).read_text()): + raise ValueError('Receipt mismatch: '+result) + print('PASS '+script) +print('PASS_BOOLEAN_DISJOINTNESS_REPAIR h=2..11 independent_kernels=2..4 no_new_kappa')