Prove the exact rank of additive Boolean disjointness repair

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.

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."
+    ]
+  }
+]

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.

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.

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"
+}

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
+}

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
+    }
+  ]
+}

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<<j for j,v in enumerate(masks)
+                  if (u==v) ^ (u&v==0)) for u in masks]
+    actual = rank(matrix)
+    formula = (2**(h+1)-2*(-1)**h-3)//3
+    assert actual == formula
+    deficit = 2*len(masks)-3*actual
+    assert deficit == 2*(-1)**h-1
+    rows.append(dict(h=h,ports=len(masks),correction_rank=actual,
+                     maximum_deficit_with_rank_one_centres=deficit))
+result = dict(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=rows)
+Path(__file__).with_name('ZETA-CORRECTOR-CHECK.json').write_text(json.dumps(result,indent=2)+'\n')
+print(json.dumps(result,indent=2))