From 84ce36e0223357715b62d0a68ca3391868c1b6a0 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:22:12 -0400 Subject: [PATCH 1/2] Census five-call two-relation BIT words at one and two dirty auxiliaries (no new kappa) Independent exhaustive corroboration of PR5481 (research/bit-fivecall-dirty-block) for W<=5 registers and every relation lattice of rank <= 2, via a cube-lattice reduction and a two-relation derivative condition over F2. Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 110 ++++++ .../README.md | 167 ++++++++ .../SOURCES.json | 54 +++ .../TASK.json | 70 ++++ .../VERIFY.json | 19 + .../census.py | 364 ++++++++++++++++++ .../verify.py | 174 +++++++++ 7 files changed, 958 insertions(+) create mode 100644 research/bit-span4-five-call-two-relation/CERTIFICATE.json create mode 100644 research/bit-span4-five-call-two-relation/README.md create mode 100644 research/bit-span4-five-call-two-relation/SOURCES.json create mode 100644 research/bit-span4-five-call-two-relation/TASK.json create mode 100644 research/bit-span4-five-call-two-relation/VERIFY.json create mode 100644 research/bit-span4-five-call-two-relation/census.py create mode 100644 research/bit-span4-five-call-two-relation/verify.py diff --git a/research/bit-span4-five-call-two-relation/CERTIFICATE.json b/research/bit-span4-five-call-two-relation/CERTIFICATE.json new file mode 100644 index 0000000000..1676135a8f --- /dev/null +++ b/research/bit-span4-five-call-two-relation/CERTIFICATE.json @@ -0,0 +1,110 @@ +{ + "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 + }, + "unpruned_W2_k4": { + "W": 2, + "derivative_violations": 0, + "diagonal": 9056, + "hist": { + "0": 3192, + "1": 4578, + "2": 1286 + }, + "k": 4 + }, + "unpruned_W3_k3": { + "W": 3, + "derivative_violations": 0, + "diagonal": 1959, + "hist": { + "0": 1731, + "1": 228 + }, + "k": 3 + } + }, + "schema_version": 1 +} diff --git a/research/bit-span4-five-call-two-relation/README.md b/research/bit-span4-five-call-two-relation/README.md new file mode 100644 index 0000000000..04d3f7f497 --- /dev/null +++ b/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 | UN25_DIAG | 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 LONG_MIN 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. diff --git a/research/bit-span4-five-call-two-relation/SOURCES.json b/research/bit-span4-five-call-two-relation/SOURCES.json new file mode 100644 index 0000000000..abacdbe5f9 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/bit-span4-five-call-two-relation/TASK.json b/research/bit-span4-five-call-two-relation/TASK.json new file mode 100644 index 0000000000..4a03a72eaa --- /dev/null +++ b/research/bit-span4-five-call-two-relation/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Open question 1 of research/bit-span4-auxiliary-structure (five calls, three invertible 2x2 targets, frame span 3, dirty auxiliaries), which merged PR5481 (research/bit-fivecall-dirty-block) answered in writing for any number of auxiliaries without a word enumeration. Delivered: an exhaustive five-call census over F2 at W=2..5 registers for every relation lattice of rank <= 2, via a cube-lattice reduction and a two-relation derivative condition, independent of the conic argument and of the one-relation and three-register lemmas.", + "scope_change_reason": "The card's alphabet is the abelian rank-one model with extra dirty registers. The open question was chosen from the span-four handoff; the pre-submission overlap check found PR5481, so the result is reframed as independent corroboration at one and two auxiliaries plus a reusable two-relation reduction.", + "bottleneck_link": "Side result for the BIT track: an independent check that one or two dirty auxiliaries do not let five rank-one calls reach three rank-two targets, so the eight-call span-four route stays closed by two independent methods at those register counts.", + "budget_minutes": 60, + "stop_rule": "Stop at the first word with three high registers, or after the exhaustive census at W <= 5; do not search k = 8.", + "outcome": "negative-result", + "evidence": "README steps 1-3; verify.py replays the pruned census for W=2,3,4 (W=5 with --long), unpruned cross-checks and controls; CERTIFICATE.json.", + "author": "Josie Elliston", + "ai_assistance": "Claude (Anthropic) assisted with the reduction, code and writing.", + "open_questions": [ + { + "question": "Why do at most two registers have a high endpoint class in every diagonal five-call word with relation rank <= 2?", + "why_it_matters": "A written proof for every W would give a second, conic-free proof of PR5481.", + "first_step": "Classify the lattices and pattern planes that attain two high registers in CERTIFICATE.json's domain.", + "blocked_by": "No uniform argument yet; the census covers W <= 5 only." + }, + { + "question": "Can the derivative condition prune the eight-call span-five and span-six cases (PR5481's open question)?", + "why_it_matters": "They are the remaining eight-call routes for three invertible 3x3 targets with dirty auxiliaries.", + "first_step": "Apply step 2 with relation rank 3 or 2 at k=8 and count admissible pattern spaces before any word enumeration.", + "blocked_by": "Cube-lattice and pattern-space counts grow quickly at k=8; a prefix or second-derivative test is likely needed." + } + ] +} diff --git a/research/bit-span4-five-call-two-relation/VERIFY.json b/research/bit-span4-five-call-two-relation/VERIFY.json new file mode 100644 index 0000000000..e488c434ae --- /dev/null +++ b/research/bit-span4-five-call-two-relation/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exhaustive five-call census over F2 for W=2,3,4 and every relation lattice of rank <= 2 (derivative-pruned, orbit-weighted): no diagonal word has three high registers; unpruned cross-checks at (W,k)=(2,4),(3,3); orbit weighting equals unreduced enumeration at W=2; five controls; exact CERTIFICATE.json equality (W=5 rows replayed only with --long). Finite corroboration of PR5481 for at most two dirty auxiliaries, not a proof for every W." + } + ] +} diff --git a/research/bit-span4-five-call-two-relation/census.py b/research/bit-span4-five-call-two-relation/census.py new file mode 100644 index 0000000000..e026ff2fdb --- /dev/null +++ b/research/bit-span4-five-call-two-relation/census.py @@ -0,0 +1,364 @@ +"""Five-call, nullity-two census for three rank-two data registers over F2. + +Apache-2.0. Prepared for Josie Elliston with Claude (Anthropic) assistance. + +Model: research/bit-span4-auxiliary-structure, open question 1. Paid factors +F_j = I + ([A_j] - 1) N_j with N_j a binary rank-one idempotent on W scalar +registers; the product lives in F2[Z^k / L], L the saturated relation lattice +of the frames. Two subsets S, T of calls give the same address exactly when +1_S - 1_T lies in L, i.e. in D = L cap {-1,0,1}^k, so only D matters. + +``run`` enumerates, for every L, only the words allowed by the derivative +condition offdiag(N_j) = sum_i (b_i)_j M_i (mod 2) for a Z-basis b of L +(README, step 2), one representative per register-permutation orbit of the +pattern assignment, weighted by orbit size. ``run_unpruned`` enumerates +every word and checks that each diagonal word satisfies that condition. +No floating point, randomness or assertions; standard library only. +""" +import itertools +import sys +import time +from fractions import Fraction + + +def idempotents(W): + out = set() + for x in range(1, 1 << W): + for y in range(1, 1 << W): + if bin(x & y).count("1") % 2 == 1: + rows = tuple(y if (x >> a) & 1 else 0 for a in range(W)) + out.add(rows) + return sorted(out) + + +def offdiag(Mrows, W): + p = 0 + for a, r in enumerate(Mrows): + p |= (r & ~(1 << a)) << (W * a) + return p + + +def mul(A, B): + out = [] + for r in A: + acc = 0 + b = 0 + while r: + if r & 1: + acc ^= B[b] + r >>= 1 + b += 1 + out.append(acc) + return tuple(out) + + +def rank_q(vectors): + """Rank over Q (exact Fractions).""" + rows = [[Fraction(v) for v in vec] for vec in vectors] + rank = 0 + ncol = len(rows[0]) if rows else 0 + for c in range(ncol): + piv = None + for i in range(rank, len(rows)): + if rows[i][c] != 0: + piv = i + break + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i][c] != 0: + f = rows[i][c] / rows[rank][c] + rows[i] = [x - f * y for x, y in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def in_span2(a, b, v): + """v in Q-span(a, b) (a, b independent): all 3x3 minors of [a; b; v] vanish.""" + n = len(a) + for i, j, l in itertools.combinations(range(n), 3): + d = (a[i] * (b[j] * v[l] - b[l] * v[j]) - a[j] * (b[i] * v[l] - b[l] * v[i]) + + a[l] * (b[i] * v[j] - b[j] * v[i])) + if d: + return False + return True + + +def independent(a, b): + return any(a[i] * b[j] - a[j] * b[i] for i, j in itertools.combinations(range(len(a)), 2)) + + +def lattices(k): + """Every 2-dim Q-span V of two {-1,0,1}^k vectors, as (D, basis). + + D = V cap {-1,0,1}^k (a frozenset), basis = a Z-basis of the saturated lattice V cap Z^k. + """ + cube = [v for v in itertools.product((-1, 0, 1), repeat=k) if any(v)] + half = [v for v in cube if next(x for x in v if x) > 0] + seen = {} + covered = set() + for a, b in itertools.combinations(half, 2): + if (a, b) in covered or not independent(a, b): + continue + D = frozenset(v for v in cube if in_span2(a, b, v)) + Dh = sorted(v for v in D if v in set(half)) + for x, y in itertools.combinations(Dh, 2): + covered.add((x, y)) + if D not in seen: + seen[D] = saturate(a, b) + return list(seen.items()) + + +def minors_gcd(a, b): + from math import gcd + g = 0 + for i, j in itertools.combinations(range(len(a)), 2): + g = gcd(g, a[i] * b[j] - a[j] * b[i]) + return g + + +def saturate(a, b): + a, b = list(a), list(b) + while True: + g = minors_gcd(a, b) + if g == 1: + return (tuple(a), tuple(b)) + # find prime p | g and an integral (la + mb)/p + p = next(q for q in range(2, abs(g) + 1) if g % q == 0) + done = False + for lam in range(p): + for mu in range(p): + if (lam, mu) == (0, 0): + continue + c = [lam * x + mu * y for x, y in zip(a, b)] + if all(x % p == 0 for x in c): + c = [x // p for x in c] + if mu != 0: + b = c + else: + a = c + done = True + break + if done: + break + if not done: + raise RuntimeError("saturation failed") + + +def in_span(basis, v): + return in_span2(basis[0], basis[1], v) + + +def run(W, k=5, data=3, sym=True, log=sys.stderr, lowrank=False): + idem = idempotents(W) + enc = lambda rows: sum(r << (W * a) for a, r in enumerate(rows)) + lifts = {} + for N in idem: + lifts.setdefault(offdiag(N, W), []).append(N) + patterns = sorted(lifts) + perms = list(itertools.permutations(range(W))) if sym else [tuple(range(W))] + def perm_pat(p, s): + q = 0 + for a in range(W): + for b in range(W): + if (p >> (W * a + b)) & 1: + q |= 1 << (W * s[a] + s[b]) + return q + ptab = {p: [perm_pat(p, s) for s in perms] for p in patterns} + allp = set(patterns) + # canonical pairs (p1,p2) and singles, with orbit weights + def reps_pairs(need3): + out = [] + for p1 in patterns: + for p2 in patterns: + if need3 and (p1 ^ p2) not in allp: + continue + imgs = {(ptab[p1][i], ptab[p2][i]) for i in range(len(perms))} + if (p1, p2) == min(imgs): + out.append((p1, p2, len(imgs))) + return out + R2, R3 = reps_pairs(False), reps_pairs(True) + R1 = [] + for p in patterns: + imgs = set(ptab[p]) + if p == min(imgs): + R1.append((p, len(imgs))) + I = enc(tuple(1 << a for a in range(W))) + full = (1 << (W * W)) - 1 + diagmask = sum(1 << (W * a + a) for a in range(W)) + rowmask = (1 << W) - 1 + def mulint(X, B): + out = 0 + for a in range(W): + r = (X >> (W * a)) & rowmask + acc = 0 + b = 0 + while r: + if r & 1: + acc ^= (B >> (W * b)) & rowmask + r >>= 1; b += 1 + out |= acc << (W * a) + return out + fac = {} + for N in idem: + n = enc(N) + fac[N] = ((n ^ I, {}), (n, {})) + lats = [(D, B) for D, B in lattices(k) if not any(sum(1 for x in v if x) == 1 for v in D)] + if lowrank: + cube = [v for v in itertools.product((-1, 0, 1), repeat=k) if any(v)] + lats = [(frozenset(), ())] + for r in cube: + if next(x for x in r if x) > 0 and sum(1 for x in r if x) >= 2: + lats.append((frozenset((r, tuple(-x for x in r))), (r,))) + def inspan(Bs, v): + if not Bs: + return not any(v) + if len(Bs) == 2: + return in_span(Bs, v) + return rank_q([Bs[0], v]) == 1 + words = wsum = diag = 0 + hist = {} + cands = [] + t0 = time.time() + for li, (D, B) in enumerate(lats): + cid = [] + reps = [] + for S in range(1 << k): + v = tuple((S >> j) & 1 for j in range(k)) + f = None + for c, T in enumerate(reps): + w = tuple(x - y for x, y in zip(v, T)) + if w in D: + f = c; break + if f is None: + f = len(reps); reps.append(v) + cid.append(f) + low = [] + for T in reps: + lw = (not any(T)) or inspan(B, T) + for j in range(k): + for sg in (1, -1): + if lw: break + u = list(T); u[j] -= sg + lw = (not any(u)) or inspan(B, u) + low.append(lw) + kap = [tuple(b[j] % 2 for b in B) + (0,) * (2 - len(B)) for j in range(k)] + used = sorted(set(c for c in kap if c != (0, 0))) + if not used: + assigns = [({}, 1)] + elif len(used) == 1: + assigns = [({used[0]: p}, w) for p, w in R1] + else: + c1, c2 = used[0], used[1] + c3 = (c1[0] ^ c2[0], c1[1] ^ c2[1]) + if c3 in used: + assigns = [({c1: p1, c2: p2, c3: p1 ^ p2}, w) for p1, p2, w in R3] + else: + assigns = [({c1: p1, c2: p2}, w) for p1, p2, w in R2] + if not used and sym: + pass # all-coordinate words: no orbit reduction, weight 1 per word + ncls = len(reps) + for a, wt in assigns: + choice = [lifts[a[c]] if c != (0, 0) else lifts[0] for c in kap] + for Ns in itertools.product(*choice): + words += 1; wsum += wt + prods = [(0, I)] + for j, N in enumerate(Ns): + (m0, d0), (m1, d1) = fac[N] + nxt = [] + bit = 1 << j + for S, X in prods: + y = d0.get(X) + if y is None: + y = d0[X] = mulint(X, m0) + z = d1.get(X) + if z is None: + z = d1[X] = mulint(X, m1) + nxt.append((S, y)); nxt.append((S | bit, z)) + prods = nxt + acc = [0] * ncls + for S, X in prods: + acc[cid[S]] ^= X + ok = True + seen = 0 + dcls = [None] * W + for c, X in enumerate(acc): + if X & ~diagmask & full: + ok = False; break + if X & seen: + ok = False; break + seen |= X + if X: + for a_ in range(W): + if (X >> (W * a_ + a_)) & 1: + dcls[a_] = c + if not ok or seen != diagmask: + continue + diag += wt if used else 1 + high = sum(1 for c in dcls if not low[c]) + hist[high] = hist.get(high, 0) + (wt if used else 1) + if high >= data: + cands.append((sorted(D), B, Ns)) + if log and li % 500 == 0: + print(f"W={W} {li}/{len(lats)} words={words} diag={diag} t={time.time()-t0:.0f}s", file=log, flush=True) + return dict(W=W, k=k, lattices=len(lats), evaluated_words=words, weighted_words=wsum, + diagonal_words_weighted=diag, high_hist=dict(sorted(hist.items())), candidates=len(cands)), cands + + +def run_unpruned(W, k): + idem = idempotents(W) + I = tuple(1 << a for a in range(W)) + pairs = {N: (tuple(r ^ i for r, i in zip(N, I)), N) for N in idem} + lats = [(D, B) for D, B in lattices(k) if not any(sum(1 for x in v if x) == 1 for v in D)] + diag = 0; hist = {}; viol = 0 + for D, B in lats: + cid, reps = [], [] + for S in range(1 << k): + v = tuple((S >> j) & 1 for j in range(k)) + f = next((c for c, T in enumerate(reps) if tuple(x - y for x, y in zip(v, T)) in D), None) + if f is None: + f = len(reps); reps.append(v) + cid.append(f) + low = [] + for T in reps: + lw = (not any(T)) or in_span(B, T) + for j in range(k): + for sg in (1, -1): + if lw: break + u = list(T); u[j] -= sg + lw = (not any(u)) or in_span(B, u) + low.append(lw) + kap = [(B[0][j] % 2, B[1][j] % 2) for j in range(k)] + for Ns in itertools.product(idem, repeat=k): + prods = [(0, I)] + for j, N in enumerate(Ns): + m0, m1 = pairs[N] + prods = [q for S, X in prods for q in ((S, mul(X, m0)), (S | 1 << j, mul(X, m1)))] + acc = [[0] * W for _ in reps] + for S, X in prods: + for a in range(W): + acc[cid[S]][a] ^= X[a] + dcls = [None] * W; ok = True + for c, X in enumerate(acc): + for a in range(W): + if X[a] & ~(1 << a): ok = False + elif X[a]: + if dcls[a] is not None: ok = False + dcls[a] = c + if not ok or None in dcls: + continue + diag += 1 + h = sum(1 for c in dcls if not low[c]); hist[h] = hist.get(h, 0) + 1 + # derivative condition: offdiag N_j = kap_j1 M1 + kap_j2 M2 for some M1, M2 + pats = [offdiag(N, W) for N in Ns] + good = False + cand = set(pats) | {0} + for M1 in cand | {p ^ q for p in cand for q in cand}: + for M2 in cand | {p ^ q for p in cand for q in cand}: + if all(p == ((M1 if c[0] else 0) ^ (M2 if c[1] else 0)) for p, c in zip(pats, kap)): + good = True; break + if good: break + if not good: viol += 1 + return dict(W=W, k=k, diagonal=diag, hist=dict(sorted(hist.items())), derivative_violations=viol) + diff --git a/research/bit-span4-five-call-two-relation/verify.py b/research/bit-span4-five-call-two-relation/verify.py new file mode 100644 index 0000000000..8636ea7d83 --- /dev/null +++ b/research/bit-span4-five-call-two-relation/verify.py @@ -0,0 +1,174 @@ +"""Replay the five-call, nullity-two census and its controls. + +Apache-2.0. Prepared for Josie Elliston with Claude (Anthropic) assistance. + +Default (a few minutes on CPython 3.12): register counts W = 2, 3, 4 for every +relation lattice of rank 2 and every lattice of rank at most 1, the unpruned +cross-checks at (W, k) = (2, 4) and (3, 3), the orbit-weighting check at W = 2, +controls, and exact comparison with CERTIFICATE.json. ``--long`` adds W = 5 +(about ten minutes) and the unpruned cross-check at (W, k) = (2, 5) (about +seven minutes). ``--write`` rewrites CERTIFICATE.json from the rows it ran. +""" +import itertools +import json +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +import census as C # noqa: E402 + +CERT = os.path.join(HERE, "CERTIFICATE.json") + + +def fail(msg): + raise SystemExit("FAIL " + msg) + + +def evaluate(W, Ns, D, B): + """Exact product of one word in F2[Z^k/L]; return (diagonal?, high register count).""" + k = len(Ns) + I = tuple(1 << a for a in range(W)) + prods = [(0, I)] + for j, N in enumerate(Ns): + m0 = tuple(r ^ i for r, i in zip(N, I)) + prods = [q for S, X in prods for q in ((S, C.mul(X, m0)), (S | 1 << j, C.mul(X, N)))] + reps, cid = [], [] + for S in range(1 << k): + v = tuple((S >> j) & 1 for j in range(k)) + f = next((c for c, T in enumerate(reps) if tuple(x - y for x, y in zip(v, T)) in D), None) + if f is None: + f = len(reps) + reps.append(v) + cid.append(f) + acc = [[0] * W for _ in reps] + for S, X in prods: + for a in range(W): + acc[cid[S]][a] ^= X[a] + dcls = [None] * W + for c, X in enumerate(acc): + for a in range(W): + if X[a] & ~(1 << a): + return False, None + if X[a]: + if dcls[a] is not None: + return False, None + dcls[a] = c + + def inspan(v): + if not B: + return not any(v) + return C.rank_q(list(B) + [list(v)]) == len(B) + + if None in dcls: + return False, None + high = 0 + for c in set(dcls): + T = reps[c] + lw = (not any(T)) or inspan(T) + for j in range(k): + for sg in (1, -1): + if not lw: + u = list(T) + u[j] -= sg + lw = (not any(u)) or inspan(u) + if not lw: + high += dcls.count(c) + return True, high + + +def E(W, a): + return tuple((1 << a) if i == a else 0 for i in range(W)) + + +def controls(): + n = 0 + # 1. detector can fire: six coordinate calls, two per data register, no relation (k = 6). + W = 4 + word = (E(W, 0), E(W, 0), E(W, 1), E(W, 1), E(W, 2), E(W, 2)) + ok, high = evaluate(W, word, frozenset(), ()) + if not (ok and high == 3): + fail("control 1: six coordinate calls should give three high registers") + n += 1 + # 2. under the relation A_1 + A_2 = 0 (a cancelling pair) register 0 ends at 0: low. + r = (1, 1, 0, 0, 0, 0) + ok, high = evaluate(W, word, frozenset({r, tuple(-x for x in r)}), (r,)) + if not (ok and high == 2): + fail("control 2: cancelling pair should make register 0 low") + n += 1 + # 3. a non-coordinate projector under no relation is not diagonal. + N = (0b011, 0, 0) # x = e0, y = e0 + e1 on three registers + ok, _ = evaluate(3, (N,) + (E(3, 0),) * 4, frozenset(), ()) + if ok: + fail("control 3: non-coordinate projector without relation accepted") + n += 1 + # 4. the same projector twice under the cancelling relation is diagonal (D_N(B) D_N(-B) = I). + r = (1, 1, 0, 0, 0) + ok, _ = evaluate(3, (N, N, E(3, 0), E(3, 1), E(3, 2)), frozenset({r, tuple(-x for x in r)}), (r,)) + if not ok: + fail("control 4: cancelling pair rejected") + n += 1 + # 5. lattice enumeration at k = 5: every listed basis is saturated (2x2 minors coprime) and + # spans its D; 4,250 rank-2 planes, of which 190 contain a unit vector (a zero frame). + lats = C.lattices(5) + for D, B in lats: + if C.minors_gcd(*B) != 1 or not all(C.in_span(B, v) for v in D): + fail("control 5: unsaturated or wrong basis") + unit = sum(1 for D, B in lats if any(sum(1 for x in v if x) == 1 for v in D)) + if (len(lats), unit) != (4250, 190): + fail(f"control 5: lattice counts {len(lats)}, {unit}") + n += 1 + return n + + +def main(): + long_ = "--long" in sys.argv + write = "--write" in sys.argv + rows = {} + for W in (2, 3, 4) + ((5,) if long_ else ()): + for mode, low in (("rank2", False), ("rank_le_1", True)): + st, cands = C.run(W, 5, log=None, lowrank=low) + if cands or st["candidates"]: + fail(f"candidate word at W={W} {mode}: {cands[:1]}") + if max(st["high_hist"]) >= 3: + fail("high histogram reaches 3") + rows[f"W{W}_{mode}"] = st + print(f"row W={W} {mode}: diagonal={st['diagonal_words_weighted']} hist={st['high_hist']}", flush=True) + # orbit weighting equals the unreduced enumeration at W = 2 + a, _ = C.run(2, 5, log=None, sym=False) + b = rows["W2_rank2"] + for key in ("weighted_words", "diagonal_words_weighted", "high_hist"): + if a[key] != b[key]: + fail(f"orbit weighting mismatch on {key}") + # unpruned cross-checks: same diagonal counts, no derivative violation + for W, k in ((2, 4), (3, 3)) + (((2, 5),) if long_ else ()): + u = C.run_unpruned(W, k) + p, _ = C.run(W, k, log=None, sym=False) + if u["derivative_violations"] or u["diagonal"] != p["diagonal_words_weighted"] or u["hist"] != p["high_hist"]: + fail(f"unpruned cross-check W={W} k={k}: {u} vs {p}") + rows[f"unpruned_W{W}_k{k}"] = u + print(f"unpruned W={W} k={k}: diagonal={u['diagonal']} violations=0", flush=True) + nctl = controls() + norm = json.loads(json.dumps(rows)) + if write: + old = {} + if os.path.exists(CERT): + with open(CERT) as fh: + old = json.load(fh).get("rows", {}) + old.update(norm) + with open(CERT, "w") as fh: + json.dump({"schema_version": 1, "rows": dict(sorted(old.items()))}, fh, indent=1, sort_keys=True) + fh.write("\n") + with open(CERT) as fh: + cert = json.load(fh)["rows"] + for key, val in norm.items(): + if cert.get(key) != val: + fail(f"certificate mismatch on {key}") + missing = sorted(set(cert) - set(norm)) + total = sum(r["diagonal_words_weighted"] for k_, r in norm.items() if not k_.startswith("unpruned")) + print(f"PASS_FIVE_CALL_TWO_RELATION_CENSUS rows={len(norm)} diagonal_words={total} " + f"max_high_registers=2 candidates=0 controls={nctl} not_replayed={len(missing)} no_new_kappa") + + +if __name__ == "__main__": + main() From c87fdea71026a7d79f2fb35ee16d6f0351209989 Mon Sep 17 00:00:00 2001 From: josie Date: Tue, 27 Oct 2026 23:38:41 -0400 Subject: [PATCH 2/2] Record W=5 and unpruned (2,5) census rows from --long Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 39 +++++++++++++++++++ .../README.md | 4 +- 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/research/bit-span4-five-call-two-relation/CERTIFICATE.json b/research/bit-span4-five-call-two-relation/CERTIFICATE.json index 1676135a8f..196f678d41 100644 --- a/research/bit-span4-five-call-two-relation/CERTIFICATE.json +++ b/research/bit-span4-five-call-two-relation/CERTIFICATE.json @@ -84,6 +84,34 @@ "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, @@ -95,6 +123,17 @@ }, "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, diff --git a/research/bit-span4-five-call-two-relation/README.md b/research/bit-span4-five-call-two-relation/README.md index 04d3f7f497..a8cf0a663e 100644 --- a/research/bit-span4-five-call-two-relation/README.md +++ b/research/bit-span4-five-call-two-relation/README.md @@ -105,7 +105,7 @@ the same diagonal words and histogram, and no diagonal word that violates step 2 |---:|---:|---:|---:|---:| | 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 | UN25_DIAG | 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 @@ -127,7 +127,7 @@ Expected: `PASS_FIVE_CALL_TWO_RELATION_CENSUS ... max_high_registers=2 candidate 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 LONG_MIN min) and wrote the W = 5 rows. +`--long` was run once locally on CPython 3.14 (macOS, about 17 min) and wrote the W = 5 rows. ## Scope