Census five-call two-relation BIT words: no three rank-two targets at one or two dirty auxiliaries, corroborating #5481 (no new κ)

research/bit-span4-five-call-two-relation/CERTIFICATE.json

@@ -0,0 +1,149 @@
+{
+ "rows": {
+  "W2_rank2": {
+   "W": 2,
+   "candidates": 0,
+   "diagonal_words_weighted": 178880,
+   "evaluated_words": 589440,
+   "high_hist": {
+    "0": 16528,
+    "1": 87352,
+    "2": 75000
+   },
+   "k": 5,
+   "lattices": 4060,
+   "weighted_words": 1048960
+  },
+  "W2_rank_le_1": {
+   "W": 2,
+   "candidates": 0,
+   "diagonal_words_weighted": 4384,
+   "evaluated_words": 7456,
+   "high_hist": {
+    "0": 146,
+    "1": 1942,
+    "2": 2296
+   },
+   "k": 5,
+   "lattices": 117,
+   "weighted_words": 11168
+  },
+  "W3_rank2": {
+   "W": 3,
+   "candidates": 0,
+   "diagonal_words_weighted": 1637212,
+   "evaluated_words": 4239480,
+   "high_hist": {
+    "0": 263455,
+    "1": 816003,
+    "2": 557754
+   },
+   "k": 5,
+   "lattices": 4060,
+   "weighted_words": 18097280
+  },
+  "W3_rank_le_1": {
+   "W": 3,
+   "candidates": 0,
+   "diagonal_words_weighted": 36757,
+   "evaluated_words": 40047,
+   "high_hist": {
+    "0": 2437,
+    "1": 17142,
+    "2": 17178
+   },
+   "k": 5,
+   "lattices": 117,
+   "weighted_words": 86731
+  },
+  "W4_rank2": {
+   "W": 4,
+   "candidates": 0,
+   "diagonal_words_weighted": 9388016,
+   "evaluated_words": 18827280,
+   "high_hist": {
+    "0": 2843284,
+    "1": 4763716,
+    "2": 1781016
+   },
+   "k": 5,
+   "lattices": 4060,
+   "weighted_words": 222008960
+  },
+  "W4_rank_le_1": {
+   "W": 4,
+   "candidates": 0,
+   "diagonal_words_weighted": 183432,
+   "evaluated_words": 154080,
+   "high_hist": {
+    "0": 26556,
+    "1": 101940,
+    "2": 54936
+   },
+   "k": 5,
+   "lattices": 117,
+   "weighted_words": 472384
+  },
+  "W5_rank2": {
+   "W": 5,
+   "candidates": 0,
+   "diagonal_words_weighted": 53463710,
+   "evaluated_words": 71355080,
+   "high_hist": {
+    "0": 28198385,
+    "1": 21187785,
+    "2": 4077540
+   },
+   "k": 5,
+   "lattices": 4060,
+   "weighted_words": 3043554480
+  },
+  "W5_rank_le_1": {
+   "W": 5,
+   "candidates": 0,
+   "diagonal_words_weighted": 785591,
+   "evaluated_words": 457941,
+   "high_hist": {
+    "0": 229511,
+    "1": 430220,
+    "2": 125860
+   },
+   "k": 5,
+   "lattices": 117,
+   "weighted_words": 2475781
+  },
+  "unpruned_W2_k4": {
+   "W": 2,
+   "derivative_violations": 0,
+   "diagonal": 9056,
+   "hist": {
+    "0": 3192,
+    "1": 4578,
+    "2": 1286
+   },
+   "k": 4
+  },
+  "unpruned_W2_k5": {
+   "W": 2,
+   "derivative_violations": 0,
+   "diagonal": 178880,
+   "hist": {
+    "0": 16528,
+    "1": 87352,
+    "2": 75000
+   },
+   "k": 5
+  },
+  "unpruned_W3_k3": {
+   "W": 3,
+   "derivative_violations": 0,
+   "diagonal": 1959,
+   "hist": {
+    "0": 1731,
+    "1": 228
+   },
+   "k": 3
+  }
+ },
+ "schema_version": 1
+}

research/bit-span4-five-call-two-relation/README.md

@@ -0,0 +1,167 @@
+# Five calls, two relations: an exhaustive census at one and two dirty auxiliaries
+
+**Independent finite corroboration; no new κ.** JoyboyBrian's merged
+[PR #5481](https://github.com/CrocSwap/integer-mult-bounds/pull/5481)
+([`research/bit-fivecall-dirty-block`](../bit-fivecall-dirty-block/README.md))
+proves in writing that three invertible rational 2×2 targets need six rank-one
+calls in the formal abelian BIT model, with any number of dirty auxiliary
+registers. That closes open question 1 of unpaidmoon's
+[`research/bit-span4-auxiliary-structure`](../bit-span4-auxiliary-structure/README.md)
+(five calls at frame span 3), and so the eight-call span-four case. Its README
+says that no five-call word enumeration was run and that the inherited
+low-span, one-relation and three-register lemmas were cited, not re-proved.
+
+This package runs that enumeration for **W = 4** scalar registers (three data
+registers and one dirty auxiliary) and **W = 5** (two auxiliaries), and for
+W = 2, 3. It covers every relation lattice of rank at most 2, that is, every
+five-call word with frame span at least 3. It does not use the conic argument,
+the one-relation theorem or the three-register theorem. The 120^5 search that
+the span-four note called blocked becomes small after one reduction (step 2
+below), which extends seed04's derivative step to two relations.
+
+**Result.** For W ≤ 5 and every relation lattice of rank ≤ 2, no diagonal
+five-call word has three registers whose endpoint class differs from `0` and
+from every `±A_j` modulo the relations. Two such registers do occur. An invertible 2×2
+target is not `0` or a rank-one frame, so no five-call word reaches three
+invertible targets at W ≤ 5. This agrees with PR #5481 for one and two dirty
+auxiliaries. The census does not cover three or more auxiliaries or frame span ≤ 2.
+Span ≤ 2 is Lemma 2 of
+[`research/bit-dirty-auxiliary-registers`](../bit-dirty-auxiliary-registers/README.md).
+
+Base: `721c03822c421b7f7fcbb2598993b947c4d88419` (priority revision 8). Card
+`bit-new-register-model`, drawn with seed `df1ea4ba466d07a5fa28dab974fcdd78`.
+
+## Model
+
+This is the model of `bit-span4-auxiliary-structure` and PR #5481, at five calls.
+Paid factors are `F_j = I + ([A_j] - 1) N_j` on `W` binary scalar registers. Here `A_j`
+is a nonzero rational 2×2 frame of rank one and `N_j = x y^T` is a binary rank-one
+idempotent. The product must equal `diag([C_1], ..., [C_W])` in `F2[(M_2(Q), +)]`.
+The data endpoints must be invertible; auxiliary endpoints are arbitrary. Let
+`L = {n in Z^5 : sum n_j A_j = 0}`, a saturated lattice. Then
+`H = Z^5 / L` embeds in `M_2(Q)`, and the product can be computed in `F2[H]`.
+
+## Reduction
+
+**Step 1 (only the cube part of L matters).** The product is multilinear in the
+`t_j`: `P = sum_S c_S t^S` over subsets `S` of the calls. Two subsets
+`S`, `T` have the same address exactly when `1_S - 1_T` lies in `L`, so in
+`D = L ∩ {-1,0,1}^5`. Let `L'` be the saturation of the span of `D`. Then
+`L' ⊆ L` and `L' ∩ {-1,0,1}^5 = D`. So diagonality is the same over `L` and `L'`.
+A class that is `0` or `±A_j` modulo `L'` is also so modulo `L`.
+Hence it suffices to enumerate the finitely many `L'`:
+
+- rank 2: the Q-spans of two independent cube vectors (4,250 lattices; 4,060 after
+  removing those that contain a unit vector, because frames are nonzero);
+- rank ≤ 1: the zero lattice and the 116 lines spanned by a cube vector
+  with at least two nonzero entries.
+
+**Step 2 (derivative condition).** Let `b_1, b_2` be a Z-basis of `L'` (rank 2).
+The kernel of `F2[Z^5] -> F2[Z^5 / L']` is generated by `t^{b_1} - 1` and
+`t^{b_2} - 1`, so every off-diagonal entry of `P` is `(t^{b_1} - 1) g_1 + (t^{b_2} - 1) g_2`.
+At `t = 1`, `d/dt_j P = N_j`, and so
+
+```
+offdiag(N_j) = (b_1)_j M_1 + (b_2)_j M_2   (mod 2)
+```
+
+for two fixed off-diagonal binary patterns `M_1`, `M_2`. A call whose basis
+column is `0 mod 2` is a coordinate projector. The other calls take at most
+three patterns, `M_1`, `M_2` and `M_1 + M_2`, each fixed by its column class. Over F2 this is
+seed04's step 1 with one more relation. It is the "pattern plane" of the
+[`two-relation-pattern-census-seed52`](../two-relation-pattern-census-seed52/README.md) census.
+Each pattern has at most two idempotent lifts, except the zero pattern, which has `W`.
+So the census enumerates, for each lattice, every admissible `(M_1, M_2)`
+and every lift. Rank 1 is the same with one pattern.
+
+**Step 3 (orbit reduction).** Register permutations act on `(M_1, M_2)`.
+The census evaluates one representative per orbit and weights it by the orbit
+size. The weighted counts equal the unreduced enumeration at W = 2.
+
+For each word the exact product is formed over all 32 subsets. Coefficients are
+merged by address class, and the word is accepted only if every class is diagonal
+and each register has exactly one class with coefficient 1. A register is
+**high** if its endpoint class is not `0` and not `±e_j` modulo the lattice.
+Lattice membership is exact rational rank arithmetic.
+
+## Evidence
+
+| Lattices | W | Evaluated orbit reps | Words (weighted) | Diagonal words | high = 0 / 1 / 2 | high ≥ 3 |
+|---|---:|---:|---:|---:|---|---:|
+| rank 2 (4,060) | 2 | 589,440 | 1,048,960 | 178,880 | 16,528 / 87,352 / 75,000 | 0 |
+| rank 2 | 3 | 4,239,480 | 18,097,280 | 1,637,212 | 263,455 / 816,003 / 557,754 | 0 |
+| rank 2 | 4 | 18,827,280 | 222,008,960 | 9,388,016 | 2,843,284 / 4,763,716 / 1,781,016 | 0 |
+| rank 2 | 5 | 71,355,080 | 3,043,554,480 | 53,463,710 | 28,198,385 / 21,187,785 / 4,077,540 | 0 |
+| rank ≤ 1 (117) | 2 | 7,456 | 11,168 | 4,384 | 146 / 1,942 / 2,296 | 0 |
+| rank ≤ 1 | 3 | 40,047 | 86,731 | 36,757 | 2,437 / 17,142 / 17,178 | 0 |
+| rank ≤ 1 | 4 | 154,080 | 472,384 | 183,432 | 26,556 / 101,940 / 54,936 | 0 |
+| rank ≤ 1 | 5 | 457,941 | 2,475,781 | 785,591 | 229,511 / 430,220 / 125,860 | 0 |
+
+"Words" counts the words that satisfy step 2. Words that fail it are never diagonal.
+The unpruned cross-check enumerates every word of idempotents for every rank-2 lattice. It finds
+the same diagonal words and histogram, and no diagonal word that violates step 2:
+
+| W | k | Words | Diagonal | Step-2 violations |
+|---:|---:|---:|---:|---:|
+| 2 | 4 | 6^4 × 316 lattices | 9,056 | 0 |
+| 3 | 3 | 28^3 × 16 lattices | 1,959 | 0 |
+| 2 | 5 | 6^5 × 4,060 lattices | 178,880 | 0 |
+
+Controls: six coordinate calls, two per data register, give three high
+registers, so the detector can fire. A cancelling pair `A_1 + A_2 = 0` makes its
+register low. A non-coordinate projector without a relation is rejected, and
+`D_N(B) D_N(-B)` is accepted. Every listed lattice basis is saturated and spans its cube part,
+and 190 of the 4,250 planes contain a unit vector (a zero frame) and are dropped.
+
+[CERTIFICATE.json](CERTIFICATE.json) records every row.
+
+## Reproduce
+
+```sh
+python3.12 scripts/research_package.py --package research/bit-span4-five-call-two-relation
+python3 -I -B research/bit-span4-five-call-two-relation/verify.py          # W <= 4, about 3 min
+python3 -I -B research/bit-span4-five-call-two-relation/verify.py --long   # adds W = 5 and the (2,5) unpruned check
+```
+
+Expected: `PASS_FIVE_CALL_TWO_RELATION_CENSUS ... max_high_registers=2 candidates=0 controls=5 ... no_new_kappa`.
+Without `--long`, the W = 5 rows and the (2, 5) unpruned row are in the certificate but not replayed
+(`not_replayed=3`), so the two-auxiliary conclusion rests on the `--long` run recorded below.
+
+`--long` was run once locally on CPython 3.14 (macOS, about 17 min) and wrote the W = 5 rows.
+
+## Scope
+
+This is a finite census in a formal model. It corroborates PR #5481 for at most two
+dirty auxiliaries. It is not a new proof for any number of auxiliaries, and it
+does not re-check the conic argument. It is independent of the one-relation and
+three-register theorems for these W. The only cited ingredient is Lemma 2 (frame span ≤ 2).
+The written steps 1 and 2 are short; the unpruned cross-checks test step 2 at small sizes,
+not at W = 4, 5. The "high" test is a necessary condition for an invertible target, so the
+census is stronger than needed, and it says nothing about rank realizability of the words
+it does find. No physical supplier, pricing, compiler or recursive-bill obligation is addressed.
+The selected bit profile and κ are unchanged.
+
+## Open next questions
+
+1. **Why at most two high registers?** At W ≤ 5 every diagonal five-call word with
+   relation rank ≤ 2 has at most two high registers, and two is attained. A written proof
+   for every W would give a second, conic-free proof of PR #5481. A first step: classify the
+   lattices and pattern planes that attain two.
+2. **Spans 5 and 6 at eight calls** (PR #5481's open question). Step 2 applies to any relation
+   rank: offdiag `N_j` is the `j`-th column of the relation basis mod 2 applied to fixed
+   patterns. At `k = 8` the cube-lattice count and the pattern space grow, so an enumeration
+   needs stronger pruning (for example a prefix test or second derivatives).
+
+## Attribution
+
+Model and the span-four reduction: unpaidmoon's `research/bit-span4-auxiliary-structure`,
+on waynenilsen's `research/bit-dirty-auxiliary-registers` (Lemma 2), Ali Romman's PR #468
+(`research/bit-three-register-lower-bound`), eumemic's PR #288 and huxint's PR #203.
+The written six-call theorem for any number of auxiliaries is JoyboyBrian's PR #5481; this package
+only corroborates it for W ≤ 5. Step 2 extends the derivative step of Hanson Sun's
+`research/bit-one-relation-seed04` (after PR #468 §4 and `research/bit-one-relation-any-registers`).
+The pattern-plane view follows `research/two-relation-pattern-census-seed52` and woklerx's
+`research/bit-four-role-two-patterns`. The census code and the step-1 reduction to cube lattices are new here.
+
+Prepared for Josie Elliston with substantial assistance from Claude (Anthropic) in the
+reduction, code and writing. No independent human review is claimed. Apache-2.0.

research/bit-span4-five-call-two-relation/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-span4-auxiliary-structure/README.md",
+      "usage": "provenance",
+      "git_blob": "b22887c72ff33e6c9b0d2f809a9f23c60a933581",
+      "sha256": "18209bc77ce7583947f117600fd84ced45f7777d94465155c3ac385eab22a26a"
+    },
+    {
+      "path": "research/bit-span4-auxiliary-structure/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "84833a7ef6711c2db9a7af8150e690fb03f9ac4c",
+      "sha256": "58f95c1fbe14cfec8b5d772fec7cc6a1ac6d603f3e1cec2d2ec6178b79444f7f"
+    },
+    {
+      "path": "research/bit-fivecall-dirty-block/README.md",
+      "usage": "provenance",
+      "git_blob": "c5d557d6b264ae982240484ff892c30d73bf5a36",
+      "sha256": "99678fb586c650733da61d95a307937cc55079d0ec1e08c0111fc5b9686e62c2"
+    },
+    {
+      "path": "research/bit-dirty-auxiliary-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "273bb963ee40869145cf8309db4f8dddebcfe43d",
+      "sha256": "da984fddaa09bfa7b1a3e11505e737283cee36e7972b2081f9de28ec420607cd"
+    },
+    {
+      "path": "research/bit-one-relation-seed04/README.md",
+      "usage": "provenance",
+      "git_blob": "98dd39621b58ffe909fa8846ecb814fe21813a27",
+      "sha256": "38c823584621d2cbd6cd1899dca04c53ca93bab1435056a28b1d5a2e001d4a0d"
+    },
+    {
+      "path": "research/two-relation-pattern-census-seed52/README.md",
+      "usage": "provenance",
+      "git_blob": "07a54e97d5d3afe83c2f77169c34b0b06c885634",
+      "sha256": "3b5917d407ac83dcdca36b74b190bf5b528b5b65cbf74b33d4f6af04f84dba79"
+    }
+  ]
+}