From 07910c7bee862dadbb3b3d30ea5dfcdbbbe23fda Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 05:11:14 -0400 Subject: [PATCH 1/3] Research: even order-3 targets need 2t calls through t=4 (no new kappa) --- research/even-target-cnot-census/README.md | 199 +++++ research/even-target-cnot-census/RECEIPT.json | 68 ++ research/even-target-cnot-census/SOURCES.json | 24 + research/even-target-cnot-census/TASK.json | 66 ++ research/even-target-cnot-census/TASK.md | 82 ++ research/even-target-cnot-census/VERIFY.json | 22 + .../even-target-cnot-census/test_verify.py | 75 ++ research/even-target-cnot-census/verify.py | 731 ++++++++++++++++++ 8 files changed, 1267 insertions(+) create mode 100644 research/even-target-cnot-census/README.md create mode 100644 research/even-target-cnot-census/RECEIPT.json create mode 100644 research/even-target-cnot-census/SOURCES.json create mode 100644 research/even-target-cnot-census/TASK.json create mode 100644 research/even-target-cnot-census/TASK.md create mode 100644 research/even-target-cnot-census/VERIFY.json create mode 100644 research/even-target-cnot-census/test_verify.py create mode 100644 research/even-target-cnot-census/verify.py diff --git a/research/even-target-cnot-census/README.md b/research/even-target-cnot-census/README.md new file mode 100644 index 0000000000..6390a5e231 --- /dev/null +++ b/research/even-target-cnot-census/README.md @@ -0,0 +1,199 @@ +# Even (order-3) diagonal targets: the 2-calls-per-target tariff is exact through t = 4 + +**Scoped register-model result; no new kappa.** The selected result, the selected +bit supplier and `upstream/` are unchanged; the bit side does not bind. + +In the formal `F2[GL_2(F2)]` rank-one-idempotent register model with free +scalar mixing, this package asks for the exact paid-call minimum of `t` copies +of the **even** order-3 target + +``` +T_t = diag([c],...,[c]), c = ab = (ba)^2, order 3, +``` + +at exactly `r = t` registers, every register an arbitrary dirty input restored +exactly. This is the first even-target tuple class of the coordinate-CNOT +line: the predecessors study transposition (SWAP) targets, where the sign +quotient gives `sum_i N_i = D_t` with `t > 0`. For even targets the same +argument gives `t = 0`, so the inherited invariants change and no predecessor +conclusion transfers. + +**Result.** The direct word is two calls per target, +`(I + ([a]+1)N)(I + ([b]+1)N) = I + ([c]+1)N`, i.e. `q = 2t`. It is optimal +in all four cases studied: + +| instance | excluded calls | conclusion | +|---|---|---| +| `t=1, r=1` | `q=1` (direct check) | min 2 | +| `t=2, r=2` | `q=2` (meet) | min 4 | +| `t=3, r=3` | `q=2, 4` (meets) | min 6 | +| **`t=4, r=4`** | **`q=2, 4, 6` (meets)** | **min 8** | + +So cross-register sharing does not beat `2t` through `t = 4`, in contrast to +nothing known either way for SWAP targets (where the tariff is `3t` and the +`t = 4` residual is open). A side observation: at `t = 2` exactly seven pairs +of 2-call words reach `T_2` in the natural image, and the same count holds in +the full formal algebra. + +## 1. Model and complete operation alphabet + +`G = GL_2(F_2) = S_3 = `, with `c = ab` +(order 3) and `S = aba = bab` (the coordinate swap). Work in the group +algebra `F_2[G]`; `r` registers carry formal `F_2[G]` labels and a word acts +by left multiplication by its call matrices in `M_r(F_2[G])` (first call +leftmost). + +A **paid call** is `C(g,N) = I + ([g]+1) N` with `g in {a,b}` and `N` any +binary rank-one idempotent over `F_2^r` (`N = v phi`, `phi(v) = 1`; 120 of +them at `r = 4`). Calls are unit-priced; this is the price rule of the +PR1333/1414/1491/1541/1705 line and is a hypothesis of this result. Each +call is an involution, since `([g]+1)^2 = 0`. + +**Free scalar mixing**: arbitrary `GL_r(F_2)` basis changes cost zero and may +be interleaved anywhere. Invariant L2' below forces any word hitting `T_t` +to have mixing factor `U = I`. + +The endpoint `[c] I_r` is accepted only on exact equality in `M_r(F_2[G])`, +covering arbitrary dirty inputs on all registers and their exact +restoration. Natural-matrix equality is used only as a necessary condition +for exclusion and never as acceptance. + +## 2. Written invariants (L1', L2') + +Write `x = [a]+1`, `y = [b]+1` in `F_2[G]`. + +**L1' (det parity).** Reduce `F_2[G]` through the sign homomorphism +`sigma: G -> C_2 = `, `a,b |-> z`, onto `F_2[eps]/(eps^2)` with +`z = 1 + eps`. An odd `[g]+1` maps to `eps`, an even one to 0. Since `c` is +even, the target maps to `I_r` and `det = 1`. A call maps to `I + eps N_i` +with `det = 1 + eps`. Multiplicativity gives `q = 0 (mod 2)`: every word +hitting `T_t` has even length. (Odd lengths are therefore never searched.) + +**L2' (mixing forced out; idempotent sum zero).** Since `eps^2 = 0`, a +`q`-call word maps to `U (I + eps sum_i N_i)` for the total mixing +`U in GL_r(F_2)`. Equality with `I_r` forces `U = I` and `sum_i N_i = 0` +over `F_2`. (For SWAP targets the corresponding identity is +`sum_i N_i = D_t`; that premise is gone here.) + +## 3. Written free-layer system (degree 1-3) + +Expand `prod_i (I + E_i) = [c] I_r` with `E_i = ([g_i]+1) N_i` in the free +filtered algebra `F = F_2/(x^2, y^2)`; here `x = [a]+1`, `y = [b]+1` +and `[c]+1 = x + y + xy`. The kernel of `F -> F_2[G]` up to degree 3 is +spanned by + +``` +R = xyx + yxy + x + y (from [S]+1 = xyx+xy+yx+y = yxy+yx+xy+x) +Z = z + z^2 + z^3, z = x+y+xy (from [c]^3 = 1), +``` + +with `R` carrying degrees 3 and 1, and `Z` carrying degrees 1, 2, 4, 5, 6. +Matching degrees 1-3 of `sum_S E_S - (x+y+xy) I_r = mu R + nu Z` gives, with +`lam = mu + nu`: + +``` +sum_a N_i = sum_b N_i = I_r + lam +sum_{ab-pairs} N_i N_j = I_r + nu +sum_{ba-pairs} N_i N_j = 0 +sum_{aba-triples} N_i N_j N_k = lam + nu +sum_{bab-triples} N_i N_j N_k = lam + nu +``` + +These are necessary conditions for any hitting word; `lam, nu in M_r(F_2)` +are free a priori. `verify.py` checks the system on every attaining word +(`t = 1, 2, 3, 4`) and rejects it on a wrong-target control. The system +alone does not exclude `q < 2t`; the meets below do. + +## 4. Meets and their completeness + +Exclusion runs in the entrywise natural image (2-dimensional representation +of `S_3`), a homomorphic image of `M_r(F_2[G])`: an empty meet there excludes +the formal word too. For `q = 2k` the meet enumerates all values `u` of +`k`-call words and tests `u^{-1} T` for membership in the same set (calls are +involutions, so the inverse value is tracked by reversed updates). Every +accepted word is verified exactly in `M_r(F_2[G])` by engine B. + +**Completeness with cross-depth value recurrence.** The BFS keeps one value +per state, but values recur across depths (`C C = I`, `C C C = C`), so the +meet covers `u, v` in `N_k` (values first reached at depth `k`). Any omitted +pair has a factor of length `j < k`, putting `T` in `V_{j+k}` with `j + k < +2k`; those lengths are excluded by L1' (odd) or by the shorter meets +(`q = 2, 4`). The `q = 6` exclusion at `t = 4` is therefore complete given +the `q = 2, 4` exclusions and L1'. + +**Engine calibration.** At `r = 4` the exact counts of word *values* at +depths 1-3 are `240 / 32,651 / 3,639,920`, exactly the ball counts PR1705 +records for the same generator set. (The counts of values first reached at +each depth are `240 / 32,650 / 3,639,680`; the differences are the identity +value at depth 2 and the 240 one-call values at depth 3, both verified in +`RECEIPT.json`.) Two engines, packed natural rank-1 updates and an +independently written formal coefficient implementation, agree on every +small meet and on all minima. + +## 5. Boundary: what this is not + +No word shorter than `2t` is found or excluded beyond `t = 4`; `t = 5` and +`r > t` (restored dirty extras) are untouched. Nothing is claimed for other +even or odd target tuples in `F_2[GL_2(F_2)]`, for other alphabets (the +generator-priced `AGL_2` alphabets or `UT_3(F_2)` commutators are different +models), or for alphabets with non-rank-one couplings. No physical compiler, +hosting, precision/tape, supplier, paid-moment or analytic-transfer +obligation is touched. No kappa claim; the selected frontier and frozen +inputs are unchanged. + +## Open next questions + +- **Question.** Is `q*(t) = 2t` for even order-3 targets at `t = r = 5` and + beyond, or does cross-register sharing first pay there? + **Why it matters.** It decides whether the tariff pattern is a general law + of the even-target line. **First step.** Run the same engine at `t = r = 5` + (480 generators) and measure the depth-3 ball before any deeper search. + **Blocker.** Ball growth: the `r = 5` depth-3 ball should exceed the + `r = 4` count of 3.6e6 states by at least an order of magnitude. +- **Question.** Can the free-layer system of section 3 exclude `q < 2t` at + general `t = r` in writing, without a meet? + **Why it matters.** A written exclusion removes the exponential meet from + the even-target line. **First step.** Extract rank constraints on the + `(q_a, q_b)` idempotent multisets summing to `I_r + lam` and test them on + the `t = 4` attaining data first. **Blocker.** The kernel correction pair + `(lam, nu)` is free in `M_r(F_2)`; bounding it uniformly is the missing + step. + +## Reproduce + +Standard library only, Python 3.10+ (registered replay uses Python 3.12): + +```sh +python3 -I -B research/even-target-cnot-census/verify.py --check-receipt # ~50 s +python3 -I -B research/even-target-cnot-census/test_verify.py # rejection controls +python3 -B scripts/research_package.py --package research/even-target-cnot-census +``` + +Expected final line of the verifier: + +```text +PASS_EVEN_TARGET_CNOT_CENSUS t1r1_min=2 t2r2_min=4 t3r3_min=6 t4r4_upper=8 t4r4_excluded={2: 0, 4: 0, 6: 0} balls4=240,32651,3639920 pr1705_ball_match=True no_new_kappa +``` + +## Task, overlap and credit + +Task card: `bit-new-register-model` (chooser track `bit-mechanisms`, OS nonce +`96dd0470d4d1febfb9db9174583232e0`, priority revision 3), refined to +`F2[GL2(F2)]/even-order3-targets/exactly-r=t`; see `TASK.md` and `TASK.json`. +`find_overlap.py` refreshes for `order-3 target`, `3-cycle target`, `cyclic +target`, `even target`, `diag([ab]`, `order-three` and the four-swap terms +found no competing even-target claim; no matches is not a novelty proof. +The concurrent balanced ten-call four-SWAP residual +(https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18919080) +is a different object (transposition targets at `r = 4`). + +Credit Gareth Davidson (@bitplane, PR1333) for the model question and scalar +normalization; commdata2338 (PR1414, PR1491, PR1495, PR1496), Cinna Davis +(1337isnot1337, PR1541), Aaron Wang (PR1705, whose recorded `r = 4` ball +counts calibrate the engine here), Ross Richardson (PR1722, label +saturation), juper997 (PR1478) and steph4n-gh (PR1573) for the surrounding +register-model line; Ali Romman (PR468), eumemic (PR288) and David Govea +(PR720) for the lineage. No predecessor executable is imported; engines A +and B are written in this session. + +Contributed by **Aaron Wang** with help from opencode. Apache-2.0. diff --git a/research/even-target-cnot-census/RECEIPT.json b/research/even-target-cnot-census/RECEIPT.json new file mode 100644 index 0000000000..8db17728dd --- /dev/null +++ b/research/even-target-cnot-census/RECEIPT.json @@ -0,0 +1,68 @@ +{ + "controls": { + "fast_update_crosscheck": 200, + "formal_natural_crosscheck": 100, + "group_table": 1, + "parity_control": 50 + }, + "group": { + "c": 14, + "elements": [ + 6, + 7, + 9, + 11, + 13, + 14 + ], + "s": 6 + }, + "main_t4r4": { + "ball_depth1": 240, + "ball_depth2": 32651, + "ball_depth3": 3639920, + "layer_ok": true, + "novel_depth1": 240, + "novel_depth2": 32650, + "novel_depth3": 3639680, + "pr1705_ball_match": true, + "q": { + "2": 0, + "4": 0, + "6": 0 + }, + "upper": 8 + }, + "runtime_seconds": 48.3, + "small_minima": { + "t2r2": { + "engine_b_agrees": true, + "min": 4, + "nat_hits": { + "2": 0, + "4": 7 + } + }, + "t3r3": { + "engine_b_agrees": true, + "min": 6, + "nat_hits": { + "2": 0, + "4": 0 + } + } + }, + "swap_t2r2": { + "excluded_q": { + "2": 0, + "4": 0 + }, + "layer_ok": true, + "min": 6 + }, + "t1r1": { + "layer_ok": true, + "min": 2, + "q1_formal_hits": 0 + } +} \ No newline at end of file diff --git a/research/even-target-cnot-census/SOURCES.json b/research/even-target-cnot-census/SOURCES.json new file mode 100644 index 0000000000..647efae4c9 --- /dev/null +++ b/research/even-target-cnot-census/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "input", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/even-target-cnot-census/TASK.json b/research/even-target-cnot-census/TASK.json new file mode 100644 index 0000000000..7dc4bd5c48 --- /dev/null +++ b/research/even-target-cnot-census/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Formal F2[GL2(F2)] rank-one-idempotent register model with free scalar GL_r(F2) mixing, but with the even order-3 target class: T_t = diag([c],...,[c]), c = ab = (ba)^2, at exactly r = t registers (t = 1, 2, 3, 4), all registers arbitrary dirty inputs restored exactly. Exact paid-call minimum; complete exclusion of every shorter even length; written sign-quotient and free-layer invariants; two engines (natural image and formal coefficients).", + "scope_change_reason": "Refinement inside the card's allowed variation (fixed larger register count, specified nonabelian family F2[GL2(F2)]). The target element class is changed from the predecessor line's transposition (SWAP) targets to even order-3 targets: the sign quotient maps [c] to 1, so the inherited invariant flips from sum_i N_i = D_t to sum_i N_i = 0 and no predecessor conclusion transfers. This is not the excluded three-register abelian model.", + "bottleneck_link": "Side result on the nonbinding bit side: no paid profile, supplier or moment changes. It prices the even-target tariff of an explicit nonabelian register alphabet, one input to whether any small-width completed saving could change the bit primitive; a q < 2t word would have been such a mechanism, and its absence through t = 4 narrows where one could live.", + "budget_minutes": 60, + "stop_rule": "Stop after the complete t = 4 decision (all shorter even lengths excluded or a formal witness found), one calibration against the predecessor's recorded ball counts, and the written-invariant checks; do not extend to t = 5 in this session.", + "outcome": "completed", + "evidence": "RECEIPT.json: minima q*(t) = 2t for t = 1, 2, 3, 4 (2, 4, 6, 8); all meets nat_hits = 0 for every shorter even length; t = r = 4 exact-depth ball-value counts 240 / 32,651 / 3,639,920 match PR1705's recorded calibration; engine B agrees with engine A on every small meet; attaining words verified exactly in M_r(F2[G]) with drop-one-call mutations failing; free-layer system holds on all attaining words and is rejected on a wrong-target control. Final line: PASS_EVEN_TARGET_CNOT_CENSUS t1r1_min=2 t2r2_min=4 t3r3_min=6 t4r4_upper=8 t4r4_excluded={2: 0, 4: 0, 6: 0} balls4=240,32651,3639920 pr1705_ball_match=True no_new_kappa.", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode", + "open_questions": [ + { + "question": "Does the 2-calls-per-target tariff stay exact for even order-3 targets at t = r = 5 and beyond, or does cross-register sharing first pay there?", + "why_it_matters": "It decides whether the tariff pattern q* = 2t is a general law of the even-target line, as 3t is for SWAP targets through t = 3.", + "first_step": "Run the same engine at t = r = 5 (480 generators; measure the depth-3 ball first) and exclude q = 8 and q = 10 by 4+4 and 5+5 meets or a written argument.", + "blocked_by": "Ball growth: the r = 5 depth-3 ball is expected to exceed the r = 4 depth-3 count of 3.6e6 states by at least an order of magnitude." + }, + { + "question": "Can the written free-layer system (sum_a = sum_b, sum_ba = 0, sum_aba = sum_bab = lam + nu) exclude q < 2t at general t = r in writing, without a meet?", + "why_it_matters": "A written exclusion would remove the exponential meet from the even-target line entirely.", + "first_step": "Extract rank constraints from the layer system on (q_a, q_b) multisets of rank-one idempotents summing to I_r + lam, and test them against the t = 4 attaining data first.", + "blocked_by": "The kernel correction pair (lam, nu) is free in M_r(F2); bounding it uniformly is the missing step." + } + ] +} diff --git a/research/even-target-cnot-census/TASK.md b/research/even-target-cnot-census/TASK.md new file mode 100644 index 0000000000..5886913139 --- /dev/null +++ b/research/even-target-cnot-census/TASK.md @@ -0,0 +1,82 @@ +# Local task card (written before substantial computation) + +Task ID / proposed scope key: `bit-new-register-model` (scope key `7084092dd726e7ba1f2f`), +chooser track `bit-mechanisms`, OS nonce `96dd0470d4d1febfb9db9174583232e0`, +refined object: **even (order-3) diagonal targets** `T_t = diag([c],...,[c])`, +`c = ab = (ba)^2` in the formal `F2[GL_2(F2)]` rank-one-idempotent register model. + +Base commit; exact predecessor and dependency heads: +- base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea` +- predecessors (read-only, pinned): PR1333 `7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2` + (Gareth Davidson; model and alphabet), PR1414 `9e1640094f649ba6db9742796825a8d6c238989b` + and PR1491 (commdata2338; transposition-target line), PR1705 + `ad6b7d641b3e8576a95add7981fa75b6a8278fbc` (Aaron Wang; `t = r = 4` SWAP targets and + the recorded `r = 4` ball sizes), PR1722 `246cd6b3a795a346bc6a741661ddcdb2d6359103` + (label saturation, context), PR1478 `b30fdba48f3db70e3589ba740b0782b56ec0ba2e` / + PR1573 `0b8c5a69297c794f2de22c04494c83e41300ae36` (UT3 commutator line, context). + +Concrete object and question: +With `c = ab` the order-3 element of `GL_2(F_2)`, what is the exact paid-call +minimum `q*(t)` for `T_t = diag([c],...,[c])` (`t` copies) at exactly `r = t` +registers (all registers arbitrary dirty inputs restored exactly), paid calls +`I + ([g]+1)N`, `g in {a,b}`, `N = v phi` any binary rank-one idempotent with +`phi(v) = 1`, and free scalar `GL_r(F2)` mixing at zero cost anywhere? The +direct word is `(I+([a]+1)N)(I+([b]+1)N) = I + ([c]+1)N` per target, i.e. +`2t` calls. Can cross-register sharing beat `2t` at `t = 2, 3, 4`? + +Scope status: **refined** within the card's allowed variation +"Choose a fixed larger register count or a specified nonabelian operation +family"; the target element class is changed from the studied transposition +targets to even order-3 targets, which flips the sign-quotient invariant. + +Existing restriction being changed (or exact claim being audited): +the predecessor line (PR1333/1414/1491/1541/1705/1722) studies transposition +(SWAP) targets, where the sign quotient gives `sum_i N_i = D_t` with `t > 0`. +For even targets the same argument gives `t = 0`, i.e. `q` even and +`sum_i N_i = 0`; the known invariants' premise changes and none of the +predecessor conclusions transfers. + +Method; explicit parameter ranges/candidate alphabet: +exact complete meet-in-the-middle censuses in the entrywise natural image +(2-dimensional representation of `S_3`, used only for exclusion), every +accepted word re-verified exactly in `M_r(F2[G])`; written free-layer +(Magnus) invariants with the exact `F2[G]` kernel correction; two separately +written engines cross-check on all small balls. Ranges: `t = r in {1,2,3,4}`, +`g in {a,b}`, all 6 / 28 / 120 binary rank-one idempotents of `F2^r`, +free `GL_r(F2)` mixing anywhere. + +Nearest overlapping PRs and why this adds something: +- PR1705 / discussion 1715 / the live balanced ten-call four-SWAP residual: + transposition targets at `r = 4`; different target parity and invariant. +- PR1478 / PR1573: UT3 commutator targets (different group `UT_3(F2)`), now + closed at `4k` for all registers; no order-3 `GL_2(F2)` tuple is covered. +- PR1496 / PR1567: `GL_3(F2)` targets and mixed `GL_3` pairs (different group). +- 1337isnot1337's live claims (discussion 1317, 07:09Z-07:24Z): heterogeneous + `GL_2`/`AGL_2` tuples `diag([a],[b],[aba])`, `diag([h],[h])`, `diag([a],[b],[h])` + at `r = 2, 3`; different tuples (transposition-bearing), different alphabets. +- `find_overlap.py` refresh for `order-3 target`, `3-cycle target`, `cyclic + target`, `even target`, `diag([ab]`, `order-three`: no competing claim. + +Optimistic full cost budget; required observable improvement: +No kappa and no supplier claim (register-model local bill only). The +optimistic local saving would be `q < 2t`; if no such word exists, the exact +minimum `2t` itself is the deliverable (a scoped negative result closing the +two-calls-per-target tariff question for this tuple class through `t = 4`). + +Success evidence; falsification test; time/compute cap: +Success = complete empty meets at every shorter even length in the natural +image, an exactly verified attaining word in `M_r(F2[G])`, and written +invariants checked on the attaining word. Falsification = any shorter formal +word found by the meet (then verified coefficientwise). Positive controls: +PR1705's recorded `r = 4` ball sizes 240 / 32,651 / 3,639,920; minima 2 at +`t = 1` and 6 for two SWAP targets at `r = 2`; drop-one-call mutation fails. +Compute cap: about 40 minutes of engine time (depth-3 ball at `r = 4` is the +measured wall). + +Predecessor authors; intended artifact and reproduction command: +Gareth Davidson (@bitplane), commdata2338, Cinna Davis (1337isnot1337), +Aaron Wang (PR1705), Ross Richardson (PR1722), juper997 (PR1478), +steph4n-gh (PR1573). Artifact: `research/even-target-cnot-census/` with +`verify.py`, receipts and source pins; reproduce with +`python3 -I -B research/even-target-cnot-census/verify.py`. +Contributed by Aaron Wang with help from opencode. Apache-2.0. diff --git a/research/even-target-cnot-census/VERIFY.json b/research/even-target-cnot-census/VERIFY.json new file mode 100644 index 0000000000..01e52ea6c7 --- /dev/null +++ b/research/even-target-cnot-census/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/agent-task-catalog.json", + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--check-receipt" + ], + "timeout_seconds": 600, + "checks": "Group table and packing controls (200 dense fast-update cross-checks, 100 formal-natural projection cross-checks, 50 parity controls); formal verification of every attaining word with drop-one-call mutations; written free-layer system checked on all attaining words and rejected on a wrong-target control; complete natural-image meets excluding q = 2 at t = 1, 2, 3, 4 and q = 4 at t = 3 and t = 4, q = 6 at t = 4; SWAP control reproduces the predecessor minimum 6 at t = r = 2; engine B (formal coefficients) agrees with engine A on every small meet; exact-depth ball-value counts at r = 4 recomputed as 240 / 32,651 / 3,639,920, matching the recorded PR1705 calibration; RECEIPT.json fields compared." + } + ] +} diff --git a/research/even-target-cnot-census/test_verify.py b/research/even-target-cnot-census/test_verify.py new file mode 100644 index 0000000000..c03a9e6f24 --- /dev/null +++ b/research/even-target-cnot-census/test_verify.py @@ -0,0 +1,75 @@ +"""Rejection controls for research/even-target-cnot-census/verify.py.""" + +import json +import random +import unittest +from pathlib import Path + +import verify as v + + +class PackageTests(unittest.TestCase): + def test_attaining_words_are_exact(self): + for r in (1, 2, 3): + w = v.word_even(r) + self.assertTrue(v.formal_is_target(v.formal_word_value(w, r), r)) + self.assertTrue(v.layer_ok_even_target(w, r)) + + def test_drop_one_rejected(self): + r = 3 + w = v.word_even(r) + for drop in range(len(w)): + mut = w[:drop] + w[drop + 1:] + self.assertFalse(v.formal_is_target(v.formal_word_value(mut, r), r)) + + def test_wrong_label_rejected(self): + r = 2 + w = v.word_even(r) + bad = list(w) + gi, vv, pp = bad[0] + bad[0] = (v.B_IDX, vv, pp) + self.assertFalse(v.formal_is_target(v.formal_word_value(bad, r), r)) + + def test_layer_system_rejects_wrong_target_word(self): + # a word that hits [c] cannot satisfy the SWAP-target layer system + self.assertFalse(v.layer_ok_swap_target(v.word_even(2), 2)) + self.assertTrue(v.layer_ok_swap_target(v.word_swap(2), 2)) + + def test_parity_and_or_confusion_control(self): + # the natural target transform is F_2 addition: 1+1 = 0 (a row of + # two equal bits must cancel). Regression for a | / ^ confusion. + r = 2 + v.set_r(r) + s = (0b11 << 0) | (0b11 << (v.ROWSZ * 1)) # rows 0 and 1 = (1,1) + got = v.nat_right_target(s, v.MAT_C, r) + # rho(c) = [[0,1],[1,1]]; a row (1,1) maps to (1^1, 1^1) = (1,0) + row0 = (got >> 0) & 0b11 + row1 = (got >> v.ROWSZ) & 0b11 + self.assertEqual(row0, 0b01) + self.assertEqual(row1, 0b01) + + def test_receipt_rejects_mutation(self): + here = Path(__file__).resolve().parent + stored = json.loads((here / "RECEIPT.json").read_text(encoding="utf-8")) + fresh = json.loads(json.dumps(v.run(fast=True), default=str)) + for key in ("t1r1", "small_minima", "swap_t2r2"): + self.assertEqual(stored.get(key), fresh.get(key)) + tampered = json.loads(json.dumps(stored)) + tampered["main_t4r4"]["q"]["6"] = 99 + self.assertNotEqual(tampered["main_t4r4"]["q"], fresh["main_t4r4"].get("q", {})) + + def test_random_words_do_not_hit_target(self): + rng = random.Random(99) + r = 2 + v.set_r(r) + gens = v.make_gens(r) + for _ in range(30): + n = rng.randrange(1, 6) + s = v.nat_identity() + for _k in range(n): + s = v.nat_right_mul(s, gens[rng.randrange(len(gens))]) + self.assertNotEqual(s, v.nat_right_target(v.nat_identity(), v.MAT_C, r)) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/even-target-cnot-census/verify.py b/research/even-target-cnot-census/verify.py new file mode 100644 index 0000000000..60f620cad0 --- /dev/null +++ b/research/even-target-cnot-census/verify.py @@ -0,0 +1,731 @@ +#!/usr/bin/env python3 +"""Even (order-3) diagonal targets in the formal F2[GL_2(F2)] register model. + +Scoped check for research/even-target-cnot-census. Standard library only. + +Model (README.md section 1): G = GL_2(F_2) = , +c = ab (order 3). Registers r, target T = [c] I_r in M_r(F2[G]). +A paid call is C(g,N) = I + ([g]+1) N with g in {a,b} and N = v phi any +binary rank-one idempotent (phi(v) = 1). Free scalar GL_r(F2) mixing is +free; the sign-quotient invariant (L1'/L2') forces any word hitting T to +have even length with mixing U = I and sum_i N_i = 0. + +All exclusion meets run in the entrywise natural image (2-dimensional +representation of S_3), a homomorphic image of M_r(F2[G]): an empty meet +there excludes the formal word as well. Every accepted word is verified +exactly in M_r(F2[G]) by engine B (formal coefficients). + +Engines: + A packed natural image, rank-1 fast updates (exclusion meets). + B formal coefficients in M_r(F2[G]) (independent small-ball cross-check + and exact acceptance of every attaining word). + +The written free-layer system (README section 3) is checked on every +attaining word. Final line starts with PASS_EVEN_TARGET_CNOT_CENSUS. +""" + +from __future__ import annotations + +import argparse +import json +import random +import sys +import time +from array import array +from bisect import bisect_left +from pathlib import Path + +# --------------------------------------------------------------------------- +# G = GL_2(F_2): 2x2 binary matrices packed row-major in bits 0..3. +# bit0 = (0,0), bit1 = (0,1), bit2 = (1,0), bit3 = (1,1). +# --------------------------------------------------------------------------- + +def mmul(u: int, v: int) -> int: + a00, a01 = u & 1, (u >> 1) & 1 + a10, a11 = (u >> 2) & 1, (u >> 3) & 1 + b00, b01 = v & 1, (v >> 1) & 1 + b10, b11 = (v >> 2) & 1, (v >> 3) & 1 + return ( + (a00 & b00) ^ (a01 & b10) + | (((a00 & b01) ^ (a01 & b11)) << 1) + | (((a10 & b00) ^ (a11 & b10)) << 2) + | (((a10 & b01) ^ (a11 & b11)) << 3) + ) + + +MAT_A = 0b1011 # [[1,1],[0,1]] +MAT_B = 0b1101 # [[1,0],[1,1]] +MAT_C = mmul(MAT_A, MAT_B) # [[0,1],[1,1]], order 3 +MAT_S = mmul(MAT_C, MAT_A) # [[0,1],[1,0]] +MAT_I = 0b1001 # [[1,0],[0,1]] + +GROUP = sorted({MAT_I, MAT_A, MAT_B, MAT_S, MAT_C, mmul(MAT_B, MAT_A)}) +assert len(GROUP) == 6 +GIDX = {m: i for i, m in enumerate(GROUP)} +E_IDX, A_IDX, B_IDX, C_IDX = GIDX[MAT_I], GIDX[MAT_A], GIDX[MAT_B], GIDX[MAT_C] +S_IDX = GIDX[MAT_S] +GTAB = [[GIDX[mmul(GROUP[i], GROUP[j])] for j in range(6)] for i in range(6)] +GINV = [next(j for j in range(6) if GTAB[i][j] == E_IDX) for i in range(6)] + +NAT = [None] * 6 # NAT[i][p] = row p of the natural image of GROUP[i], 2 bits +for i, m in enumerate(GROUP): + NAT[i] = [ + ((m >> (2 * p)) & 1) | (((m >> (2 * p + 1)) & 1) << 1) for p in range(2) + ] + +PARITY = [0] * 256 +for _i in range(256): + PARITY[_i] = bin(_i).count("1") & 1 + + +# --------------------------------------------------------------------------- +# Rank-one idempotents N = v phi over F2^r with phi(v) = 1. +# --------------------------------------------------------------------------- + +def idempotents(r: int): + out = [] + for v in range(1, 1 << r): + for phi in range(1 << r): + if PARITY[v & phi]: + out.append((v, phi)) + return out + + +def mat_of(v: int, phi: int, r: int) -> int: + out = 0 + for i in range(r): + if (v >> i) & 1: + out |= phi << (r * i) + return out + + +def mat_mul(u: int, v: int, r: int) -> int: + out = 0 + mask = (1 << r) - 1 + for i in range(r): + row = (u >> (r * i)) & mask + acc = 0 + for k in range(r): + if (row >> k) & 1: + acc ^= (v >> (r * k)) & mask + out |= acc << (r * i) + return out + + +def mat_sum(mats, r=None) -> int: + out = 0 + for m in mats: + out ^= m + return out + + +def mat_ident(r: int) -> int: + out = 0 + for i in range(r): + out |= 1 << (r * i + i) + return out + + +# --------------------------------------------------------------------------- +# Engine A: natural image. State = 2r x 2r binary matrix, rows of 2r bits. +# A call is I + U W^T with U = v (x) beta, W = phi (x) gamma, where +# rho(g) + I = beta gamma^T (rank one) for g in {a,b}. +# --------------------------------------------------------------------------- + +def beta_gamma(gi: int): + bg = [[(NAT[gi][p] >> q) & 1 for q in range(2)] for p in range(2)] + for p in range(2): + for q in range(2): + bg[p][q] ^= 1 if p == q else 0 + flat = [(p, q) for p in range(2) for q in range(2) if bg[p][q]] + assert len(flat) == 1 + p, q = flat[0] + return 1 << p, 1 << q + + +def make_gens(r: int): + """Generators as (Umask, Wmask, Urows, Wrows, gi, v, phi) over 2r bits.""" + gens = [] + for (v, phi) in idempotents(r): + for gi in (A_IDX, B_IDX): + beta, gamma = beta_gamma(gi) + U = W = 0 + urows = [] + wrows = [] + for i in range(r): + if (v >> i) & 1: + U |= beta << (2 * i) + urows.append(2 * i + (beta.bit_length() - 1)) + if (phi >> i) & 1: + W |= gamma << (2 * i) + wrows.append(2 * i + (gamma.bit_length() - 1)) + gens.append((U, W, urows, wrows, gi, v, phi)) + return gens + + +ROWSZ = None # set per r +ROWMASK = 255 + + +def set_r(r: int): + global ROWSZ, ROWMASK + ROWSZ = 2 * r + ROWMASK = (1 << ROWSZ) - 1 + + +def nat_right_mul(s: int, gen) -> int: + """s' = s (I + U W^T) = s + (s U) W^T.""" + U, W = gen[0], gen[1] + out = s + for i in range(ROWSZ): + if PARITY[((s >> (ROWSZ * i)) & ROWMASK) & U]: + out ^= W << (ROWSZ * i) + return out + + +def nat_left_mul(s: int, gen) -> int: + """s' = (I + U W^T) s = s + U (W^T s).""" + U, W, urows, wrows = gen[0], gen[1], gen[2], gen[3] + r = 0 + for i in wrows: + r ^= (s >> (ROWSZ * i)) & ROWMASK + if r == 0: + return s + out = s + for i in urows: + out ^= r << (ROWSZ * i) + return out + + +def nat_identity() -> int: + out = 0 + for i in range(ROWSZ): + out |= 1 << (ROWSZ * i + i) + return out + + +def nat_right_target(s: int, mat: int, r: int) -> int: + """s' = s * (I_r (x) mat); mixes the two column bits of each register.""" + out = 0 + for i in range(2 * r): + row = (s >> (ROWSZ * i)) & ROWMASK + for k in range(r): + b0 = (row >> (2 * k)) & 1 + b1 = (row >> (2 * k + 1)) & 1 + n0 = ((mat & 1) & b0) ^ (((mat >> 2) & 1) & b1) + n1 = (((mat >> 1) & 1) & b0) ^ (((mat >> 3) & 1) & b1) + row = (row & ~(3 << (2 * k))) | (n0 << (2 * k)) | (n1 << (2 * k + 1)) + out |= row << (ROWSZ * i) + return out + + +# --------------------------------------------------------------------------- +# Engine B: formal coefficients in M_r(F2[G]); state = 6 planes of r x r +# binary matrices, rows of r bits. +# --------------------------------------------------------------------------- + +def formal_identity(r: int): + pl = [0] * 6 + pl[E_IDX] = mat_ident(r) + return tuple(pl) + + +def formal_left_call(pl, gi: int, v: int, phi: int, r: int): + """Multiply on the left by C = I + ([g]+1) N.""" + mask = (1 << r) - 1 + ginv = GINV[gi] + out = [0] * 6 + for h in range(6): + q = pl[h] + acc = q ^ pl[GTAB[ginv][h]] + comb = 0 + for i in range(r): + if (phi >> i) & 1: + comb ^= (acc >> (r * i)) & mask + nacc = 0 + for i in range(r): + if (v >> i) & 1: + nacc |= comb << (r * i) + out[h] = q ^ nacc + return tuple(out) + + +def formal_right_call(pl, gi: int, v: int, phi: int, r: int): + """Multiply on the right by C = I + ([g]+1) N: (P C)^h = P^h + (P^h + P^{h g^-1}) N.""" + mask = (1 << r) - 1 + ginv = GINV[gi] + out = [0] * 6 + for h in range(6): + q = pl[h] + acc = q ^ pl[GTAB[h][ginv]] + # acc * N = (acc v) phi + col = 0 + for i in range(r): + row = (acc >> (r * i)) & mask + if PARITY[row & v]: + col |= 1 << i + rn = 0 + for i in range(r): + if (col >> i) & 1: + rn |= phi << (r * i) + out[h] = q ^ rn + return tuple(out) + + +def formal_right_target(pl, gi: int): + out = [0] * 6 + for h in range(6): + out[GTAB[h][gi]] = pl[h] + return tuple(out) + + +def formal_is_target(pl, r: int, target_gi: int = None) -> bool: + if target_gi is None: + target_gi = C_IDX + return list(pl) == [mat_ident(r) if h == target_gi else 0 for h in range(6)] + + +# --------------------------------------------------------------------------- +# Balls and meets. +# --------------------------------------------------------------------------- + +def build_ball(gens, r: int, depth: int): + """Values of products of exactly `depth` generators (newest on the right). + + Returns (states_sorted_array, invs_list, sizes, sorted_index_helper). + invs[i] is the inverse value of states[i] (well defined per value). + """ + global ROWSZ + set_r(r) + ident = nat_identity() + states = array("Q", [ident]) + invs = array("Q", [ident]) + seen = {ident: 0} + sizes = [1] + frontier = [0] + for _ in range(depth): + nxt = [] + for idx in frontier: + s = states[idx] + inv = invs[idx] + for g in gens: + s2 = nat_right_mul(s, g) + if s2 in seen: + continue + seen[s2] = len(states) + states.append(s2) + invs.append(nat_left_mul(inv, g)) + nxt.append(len(states) - 1) + sizes.append(len(states) - sum(sizes)) + frontier = nxt + if not frontier: + break + return states, invs, sizes, seen + + +def meet_count(gens, r: int, k: int, target_mat: int): + """Pairs (u,v) of exact-length-k words with u v = T in the natural image. + + Returns (hits, sizes, seen). hits == 0 excludes length 2k in the formal + model, given the exclusions at shorter lengths (README section 4). + """ + global ROWSZ + set_r(r) + states, invs, sizes, seen = build_ball(gens, r, k) + hits = 0 + for idx in range(len(states)): + v = nat_right_target(invs[idx], target_mat, r) + if v in seen: + hits += 1 + return hits, sizes, seen + + +def exact_value_counts(gens, r: int): + """|V_k| = number of VALUES of words of exactly k calls. + + V_0 = {I}; V_k = {y*g : y in V_{k-1}, g in gens}. Values recur across + depths (C*C = I and C*C*C = C), so these differ from the counts of + values first reached at each BFS depth. + """ + set_r(r) + ident = nat_identity() + V1 = {nat_right_mul(ident, g) for g in gens} + V2 = set() + for x in V1: + for g in gens: + V2.add(nat_right_mul(x, g)) + V3 = set() + for x in V2: + for g in gens: + V3.add(nat_right_mul(x, g)) + return len(V1), len(V2), len(V3) + + +def formal_ball(gens, r: int, depth: int): + """Engine-B ball: values of products of exactly `depth` formal calls.""" + ident = formal_identity(r) + states = [ident] + invs = [ident] + seen = {ident: 0} + sizes = [1] + frontier = [0] + for _ in range(depth): + nxt = [] + for idx in frontier: + s = states[idx] + inv = invs[idx] + for g in gens: + s2 = formal_right_call(s, g[4], g[5], g[6], r) + if s2 in seen: + continue + seen[s2] = len(states) + states.append(s2) + invs.append(formal_left_call(inv, g[4], g[5], g[6], r)) + nxt.append(len(states) - 1) + sizes.append(len(states) - sum(sizes)) + frontier = nxt + if not frontier: + break + return states, invs, sizes, seen + + +def formal_meet_count(gens, r: int, k: int, target_gi: int): + states, invs, sizes, seen = formal_ball(gens, r, k) + hits = 0 + for idx in range(len(states)): + v = formal_right_target(invs[idx], target_gi) + if v in seen: + hits += 1 + return hits, sizes + + +# --------------------------------------------------------------------------- +# Written free-layer system (README section 3). For a word w with letters +# g_i in {a,b} and idempotents N_i, expand prod (I + E_i) = T in the free +# filtered algebra F_2/(x^2, y^2); the kernel of F -> F_2[G] up to the +# needed degree is spanned by R = xyx + yxy + x + y and Z = z + z^2 + z^3 +# with z = x + y + xy. Matching degrees 1..3 gives the system below. +# --------------------------------------------------------------------------- + +def layer_sums(word, r: int): + mats = [mat_of(v, phi, r) for (_g, v, phi) in word] + gis = [gi for (gi, _v, _p) in word] + n = len(word) + sum_a = mat_sum([mats[i] for i in range(n) if gis[i] == A_IDX], r) + sum_b = mat_sum([mats[i] for i in range(n) if gis[i] == B_IDX], r) + sum_ab = mat_sum( + [mat_mul(mats[i], mats[j], r) for i in range(n) for j in range(i + 1, n) + if gis[i] == A_IDX and gis[j] == B_IDX], r) + sum_ba = mat_sum( + [mat_mul(mats[i], mats[j], r) for i in range(n) for j in range(i + 1, n) + if gis[i] == B_IDX and gis[j] == A_IDX], r) + sum_aba = mat_sum( + [mat_mul(mat_mul(mats[i], mats[j], r), mats[k], r) + for i in range(n) for j in range(i + 1, n) for k in range(j + 1, n) + if (gis[i], gis[j], gis[k]) == (A_IDX, B_IDX, A_IDX)], r) + sum_bab = mat_sum( + [mat_mul(mat_mul(mats[i], mats[j], r), mats[k], r) + for i in range(n) for j in range(i + 1, n) for k in range(j + 1, n) + if (gis[i], gis[j], gis[k]) == (B_IDX, A_IDX, B_IDX)], r) + return {"sum_a": sum_a, "sum_b": sum_b, "sum_ab": sum_ab, + "sum_ba": sum_ba, "sum_aba": sum_aba, "sum_bab": sum_bab} + + +def layer_ok_even_target(word, r: int) -> bool: + """Necessary conditions for a word to hit T = [c] I_r.""" + s = layer_sums(word, r) + ident = mat_ident(r) + if s["sum_a"] != s["sum_b"]: + return False + if s["sum_ba"] != 0: + return False + lam = s["sum_a"] ^ ident + nu = s["sum_ab"] ^ ident + if s["sum_aba"] != (lam ^ nu): + return False + if s["sum_bab"] != (lam ^ nu): + return False + return True + + +def layer_ok_swap_target(word, r: int) -> bool: + """Necessary conditions for a word to hit T = [S] I_r.""" + s = layer_sums(word, r) + ident = mat_ident(r) + if (s["sum_a"] ^ s["sum_b"]) != ident: + return False + if s["sum_ba"] != ident: + return False + if (s["sum_aba"] ^ s["sum_bab"]) != ident: + return False + if s["sum_bab"] != (s["sum_a"] ^ s["sum_ab"] ^ ident): + return False + return True + + +# --------------------------------------------------------------------------- +# Words and controls. +# --------------------------------------------------------------------------- + +def word_even(r: int): + """2r calls: (a, N_k) then (b, N_k) on each diagonal idempotent.""" + w = [] + for k in range(r): + w.append((A_IDX, 1 << k, 1 << k)) + w.append((B_IDX, 1 << k, 1 << k)) + return w + + +def word_swap(r: int): + """3r calls: aba on each diagonal idempotent (predecessor upper bound).""" + w = [] + for k in range(r): + w.append((A_IDX, 1 << k, 1 << k)) + w.append((B_IDX, 1 << k, 1 << k)) + w.append((A_IDX, 1 << k, 1 << k)) + return w + + +def formal_word_value(word, r: int): + pl = formal_identity(r) + for (gi, v, phi) in word: + pl = formal_right_call(pl, gi, v, phi, r) + return pl + + +def gen_lookup(gi, v, phi, gens): + for g in gens: + if (g[4], g[5], g[6]) == (gi, v, phi): + return g + raise KeyError((gi, v, phi)) + + +def ctrl_group_table(): + assert all(GTAB[i][E_IDX] == i and GTAB[E_IDX][i] == i for i in range(6)) + assert all(GTAB[i][GINV[i]] == E_IDX for i in range(6)) + assert mmul(MAT_A, MAT_A) == MAT_I and mmul(MAT_B, MAT_B) == MAT_I + assert mmul(MAT_C, mmul(MAT_C, MAT_C)) == MAT_I + assert MAT_S == mmul(MAT_C, MAT_A) == mmul(MAT_B, MAT_C) + return 1 + + +def ctrl_fast_update(rng, trials=200): + """Packed rank-1 updates agree with dense multiplication (r = 4).""" + r = 4 + set_r(r) + gens = make_gens(r) + n = 2 * r + + def dense(g): + U, W = g[0], g[1] + c = [[0] * n for _ in range(n)] + for i in range(n): + for j in range(n): + c[i][j] = (1 if i == j else 0) ^ (((U >> i) & 1) & ((W >> j) & 1)) + return c + + def to_mat(s): + return [[(s >> (ROWSZ * i + j)) & 1 for j in range(n)] for i in range(n)] + + def to_int(m): + out = 0 + for i in range(n): + for j in range(n): + if m[i][j]: + out |= 1 << (ROWSZ * i + j) + return out + + def mm(a, b): + return [[sum(a[i][k] & b[k][j] for k in range(n)) & 1 for j in range(n)] + for i in range(n)] + + for _ in range(trials): + s = rng.getrandbits(ROWSZ * ROWSZ) + g = gens[rng.randrange(len(gens))] + c = dense(g) + sm = to_mat(s) + assert to_int(mm(c, sm)) == nat_left_mul(s, g) + assert to_int(mm(sm, c)) == nat_right_mul(s, g) + return trials + + +def ctrl_formal_natural(rng, trials=100): + """Engine B projected entrywise equals engine A on random short words.""" + r = 4 + set_r(r) + gens = make_gens(r) + for _ in range(trials): + n = rng.randrange(1, 5) + picks = [gens[rng.randrange(len(gens))] for _ in range(n)] + word = [(g[4], g[5], g[6]) for g in picks] + pl = formal_word_value(word, r) + s = nat_identity() + for g in picks: + s = nat_right_mul(s, g) + proj = 0 + for h in range(6): + m = pl[h] + for i in range(r): + for j in range(r): + if (m >> (r * i + j)) & 1: + for p in range(2): + for q in range(2): + if (NAT[h][p] >> q) & 1: + proj ^= 1 << (ROWSZ * (2 * i + p) + (2 * j + q)) + assert proj == s + return trials + + +def ctrl_parity(rng, trials=50): + """L1' sign-quotient parity: an odd-length product never equals T.""" + r = 2 + set_r(r) + gens = make_gens(r) + for _ in range(trials): + n = rng.randrange(1, 8) | 1 + s = nat_identity() + for _k in range(n): + s = nat_right_mul(s, gens[rng.randrange(len(gens))]) + assert s != nat_right_target(nat_identity(), MAT_C, r) + return trials + + +# --------------------------------------------------------------------------- +# Main run. +# --------------------------------------------------------------------------- + +def run(fast: bool = False): + t0 = time.time() + rng = random.Random(20261014) + rec = {"group": {"elements": GROUP, "c": MAT_C, "s": MAT_S}} + rec["controls"] = { + "group_table": ctrl_group_table(), + "fast_update_crosscheck": ctrl_fast_update(rng), + "formal_natural_crosscheck": ctrl_formal_natural(rng), + "parity_control": ctrl_parity(rng), + } + + # t = 1, r = 1: minimum 2 (control). + r = 1 + gens = make_gens(r) + w = word_even(1) + assert formal_is_target(formal_word_value(w, 1), 1) + # direct q = 1 check in the formal model + hit1 = 0 + for g in gens: + if formal_is_target(formal_left_call(formal_identity(1), g[4], g[5], g[6], 1), 1): + hit1 += 1 + assert hit1 == 0 + assert layer_ok_even_target(w, 1) + rec["t1r1"] = {"min": 2, "q1_formal_hits": hit1, "layer_ok": True} + + small = {} + for r in (2, 3): + gens = make_gens(r) + w = word_even(r) + assert formal_is_target(formal_word_value(w, r), r), f"attaining word r={r}" + for drop in range(len(w)): + mut = w[:drop] + w[drop + 1:] + assert not formal_is_target(formal_word_value(mut, r), r), "drop-one" + assert layer_ok_even_target(w, r) + cand = {} + for q in (2, 4): + hits, _sizes, _seen = meet_count(gens, r, q // 2, MAT_C) + cand[q] = hits + # independent engine B meet at the same lengths + bcand = {} + for q in (2, 4): + bcand[q] = formal_meet_count(gens, r, q // 2, C_IDX)[0] + assert bcand == cand, (r, cand, bcand) + assert cand[2] == 0, (r, cand) # two calls cover one register only + min_q = 4 if cand[4] else 2 * r + small[f"t{r}r{r}"] = {"min": min_q, "nat_hits": cand, + "engine_b_agrees": True} + assert small["t2r2"]["min"] == 4, small + rec["small_minima"] = small + + # SWAP control at t = r = 2: predecessor minimum 6 (PR1414/1491 line). + r = 2 + gens = make_gens(r) + wsw = word_swap(2) + assert formal_is_target(formal_word_value(wsw, 2), 2, S_IDX), "SWAP attaining word" + assert layer_ok_swap_target(wsw, 2) + sw = {} + for q in (2, 4): + sw[q] = meet_count(gens, r, q // 2, MAT_S)[0] + assert sw[q] == 0, (q, sw) + # a word that hits T=[c] but not [S] must fail the SWAP layer system + assert not layer_ok_swap_target(word_even(2), 2) + rec["swap_t2r2"] = {"min": 6, "excluded_q": sw, "layer_ok": True} + + # main case t = r = 4. + r = 4 + gens = make_gens(r) + w = word_even(4) + assert formal_is_target(formal_word_value(w, 4), 4), "t=4 attaining word" + for drop in range(len(w)): + mut = w[:drop] + w[drop + 1:] + assert not formal_is_target(formal_word_value(mut, 4), 4), "drop-one t=4" + assert layer_ok_even_target(w, 4) + main = {"upper": 8, "layer_ok": True, "q": {}} + if not fast: + for q in (2, 4): + hits, sizes_k, _seen_k = meet_count(gens, r, q // 2, MAT_C) + main["q"][q] = hits + main[f"novel_depth{q // 2}"] = sizes_k[q // 2] + hits6, sizes3, seen3 = meet_count(gens, r, 3, MAT_C) + main["q"][6] = hits6 + main["novel_depth3"] = sizes3[3] + del seen3 + e1, e2, e3 = exact_value_counts(gens, r) + main["ball_depth1"] = e1 + main["ball_depth2"] = e2 + main["ball_depth3"] = e3 + main["pr1705_ball_match"] = (e1 == 240 and e2 == 32651 and e3 == 3639920) + assert main["pr1705_ball_match"], (e1, e2, e3) + rec["main_t4r4"] = main + rec["runtime_seconds"] = round(time.time() - t0, 1) + return rec + + +def final_line(rec) -> str: + m = rec["main_t4r4"] + q = m.get("q", {}) + small = rec["small_minima"] + return ( + "PASS_EVEN_TARGET_CNOT_CENSUS " + f"t1r1_min=2 t2r2_min={small['t2r2']['min']} t3r3_min={small['t3r3']['min']} " + f"t4r4_upper={m['upper']} t4r4_excluded={q} " + f"balls4={m.get('ball_depth1')},{m.get('ball_depth2')},{m.get('ball_depth3')} " + f"pr1705_ball_match={m.get('pr1705_ball_match')} no_new_kappa" + ) + + +def main(argv): + ap = argparse.ArgumentParser() + ap.add_argument("--fast", action="store_true", help="skip the r=4 depth-3 meet") + ap.add_argument("--record", action="store_true", help="write RECEIPT.json") + ap.add_argument("--check-receipt", action="store_true") + args = ap.parse_args(argv) + rec = run(fast=args.fast) + print(json.dumps(rec, indent=1, default=str)) + here = Path(__file__).resolve().parent + if args.record: + (here / "RECEIPT.json").write_text( + json.dumps(rec, indent=1, default=str, sort_keys=True), encoding="utf-8") + print("RECEIPT.json written") + if args.check_receipt: + stored = json.loads((here / "RECEIPT.json").read_text(encoding="utf-8")) + fresh = json.loads(json.dumps(rec, default=str)) + for key in ("t1r1", "small_minima", "swap_t2r2", "main_t4r4", "controls"): + if stored.get(key) != fresh.get(key): + print("RECEIPT_MISMATCH", key) + print(" stored:", json.dumps(stored.get(key), default=str)[:400]) + print(" fresh :", json.dumps(fresh.get(key), default=str)[:400]) + return 2 + print(final_line(rec)) + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) From b3f68c908d5bbff8886c197ff0dd968acfc17e78 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 13:19:55 -0400 Subject: [PATCH 2/3] Research: correct section-3 free-layer necessity claim in even-target census Review follow-up on https://github.com/CrocSwap/integer-mult-bounds/pull/1763 (counterexample from https://github.com/CrocSwap/integer-mult-bounds/pull/1763#issuecomment-6172859400): at r=1 with every projector [1], the word b a b a is an exact target word ((ba)^2 = ab = c) but sum_ba = 1, so the degree 1-3 free-layer system is not necessary. README section 3 now demotes layer_ok_even_target to a screening filter (neither necessary nor sufficient) and states the corrected necessary condition restricted to words of length q <= 3, where the degree matching is valid (kernel of F -> F2[G] up to degree 3 is spanned by R alone; machine-checked). New regression controls in test_verify.py: counterexample acceptance, filter non-sufficiency, kernel rank/scope, and minima independence from the layer condition. The q*(t) = 2t minima 2/4/6/8 are unchanged: exclusion uses only L1' parity, the q=1 direct check and the meets. TASK.json/VERIFY.json wording aligned. Contributed by Aaron Wang with help from opencode. --- research/even-target-cnot-census/README.md | 85 +++++++++++---- research/even-target-cnot-census/TASK.json | 10 +- research/even-target-cnot-census/VERIFY.json | 2 +- .../even-target-cnot-census/test_verify.py | 100 ++++++++++++++++++ research/even-target-cnot-census/verify.py | 33 ++++-- 5 files changed, 192 insertions(+), 38 deletions(-) diff --git a/research/even-target-cnot-census/README.md b/research/even-target-cnot-census/README.md index 6390a5e231..2e7112f653 100644 --- a/research/even-target-cnot-census/README.md +++ b/research/even-target-cnot-census/README.md @@ -75,34 +75,69 @@ hitting `T_t` has even length. (Odd lengths are therefore never searched.) over `F_2`. (For SWAP targets the corresponding identity is `sum_i N_i = D_t`; that premise is gone here.) -## 3. Written free-layer system (degree 1-3) - -Expand `prod_i (I + E_i) = [c] I_r` with `E_i = ([g_i]+1) N_i` in the free -filtered algebra `F = F_2/(x^2, y^2)`; here `x = [a]+1`, `y = [b]+1` -and `[c]+1 = x + y + xy`. The kernel of `F -> F_2[G]` up to degree 3 is -spanned by +## 3. Free-layer system (degree 1-3): screening filter, not necessary + +**Correction** (review of +https://github.com/CrocSwap/integer-mult-bounds/pull/1763). An earlier +version of this section claimed the degree 1-3 system below as "necessary +conditions for any hitting word". That claim is false. Counterexample: at +`r = 1` set every projector to `[1]` and take the word `b a b a`. Each call +is then `I + ([g]+1)[1] = [g]`, so the word value is `[baba] = [(ba)^2] = +[ab] = [c]`, an exact target word; but the claimed condition `sum_ba = 0` +fails, because the word has three ordered b-before-a pairs and `sum_ba = +[1]`. The package's own engine confirms it: +`formal_is_target(formal_word_value(word,1),1)` is `True` while +`layer_ok_even_target(word,1)` is `False` (regression +`test_layer_counterexample_baba` in `test_verify.py`). + +Where the old derivation went wrong: it expanded `prod_i (I + E_i) = [c] I_r` +with `E_i = ([g_i]+1) N_i` in the free filtered algebra +`F = F_2/(x^2, y^2)`, `x = [a]+1`, `y = [b]+1`, `[c]+1 = x + y + xy`, and +matched degrees 1-3 against the kernel elements ``` R = xyx + yxy + x + y (from [S]+1 = xyx+xy+yx+y = yxy+yx+xy+x) Z = z + z^2 + z^3, z = x+y+xy (from [c]^3 = 1), ``` -with `R` carrying degrees 3 and 1, and `Z` carrying degrees 1, 2, 4, 5, 6. -Matching degrees 1-3 of `sum_S E_S - (x+y+xy) I_r = mu R + nu Z` gives, with -`lam = mu + nu`: +claiming the kernel of `F -> F_2[G]` up to degree 3 is spanned by `R` and `Z`. +But `Z` carries degrees up to 6, and its truncation to degree at most 3, +`x + y + yx`, maps to `[ba] + [e] != 0`: it is not in the kernel. Up to degree +3 the kernel is 1-dimensional, spanned by `R` alone (the seven monomial +images `1, x, y, xy, yx, xyx, yxy` have rank 6 over `F_2`; both facts are +machine-checked in `test_verify.py`). Matching degrees 1-3 is therefore +justified only when the word length is `q <= 3`, where the difference +`prod_i (I + E_i) - I - (x+y+xy) I_r` itself has degree at most 3. For +`q >= 4` kernel elements of degree 4 and higher absorb the low-degree +mismatch, which is exactly what happens for `b a b a`. + +**Corrected statement (class: words of length `q <= 3`).** For a hitting +word of length at most 3, the difference lies in ` tensor M_r(F_2)` and +comparing degrees 1-3 gives, for some `lam in M_r(F_2)`: ``` sum_a N_i = sum_b N_i = I_r + lam -sum_{ab-pairs} N_i N_j = I_r + nu +sum_{ab-pairs} N_i N_j = I_r sum_{ba-pairs} N_i N_j = 0 -sum_{aba-triples} N_i N_j N_k = lam + nu -sum_{bab-triples} N_i N_j N_k = lam + nu +sum_{aba-triples} N_i N_j N_k = lam +sum_{bab-triples} N_i N_j N_k = lam ``` -These are necessary conditions for any hitting word; `lam, nu in M_r(F_2)` -are free a priori. `verify.py` checks the system on every attaining word -(`t = 1, 2, 3, 4`) and rejects it on a wrong-target control. The system -alone does not exclude `q < 2t`; the meets below do. +The counterexample `b a b a` has length 4 and lies outside this class. An +exhaustive check over all 1898 words of length 1-3 at `r = 1, 2` finds +exactly one hitting word, and it satisfies this system (`test_verify.py`). +No claim is made for words of length 4 or more. + +**What remains of the old system.** `layer_ok_even_target` keeps the looser +old form (`sum_ab = I_r + nu`, `sum_ba = 0`, triples `lam + nu`) as a +screening filter only. It accepts every attaining word used here +(`word_even`, `t = 1, 2, 3, 4`) and rejects the wrong-target control, but it +rejects genuine target words (the counterexample above) and accepts +non-target words (at `r = 2`, `a b` on one projector passes the filter and +is not a target), so it is neither necessary nor sufficient and is never +used to exclude candidates. All exclusions below come from L1', the `q = 1` +direct check and the meets; the reported minima are unchanged if the filter +is made vacuous (`test_minima_do_not_rely_on_layer_condition`). ## 4. Meets and their completeness @@ -150,14 +185,18 @@ inputs are unchanged. (480 generators) and measure the depth-3 ball before any deeper search. **Blocker.** Ball growth: the `r = 5` depth-3 ball should exceed the `r = 4` count of 3.6e6 states by at least an order of magnitude. -- **Question.** Can the free-layer system of section 3 exclude `q < 2t` at - general `t = r` in writing, without a meet? +- **Question.** Can a written degree-complete kernel analysis exclude + `q < 2t` at general `t = r`, without a meet? (The degree 1-3 free-layer + system of section 3 cannot: it is necessary only for words of length + `q <= 3`.) **Why it matters.** A written exclusion removes the exponential meet from - the even-target line. **First step.** Extract rank constraints on the - `(q_a, q_b)` idempotent multisets summing to `I_r + lam` and test them on - the `t = 4` attaining data first. **Blocker.** The kernel correction pair - `(lam, nu)` is free in `M_r(F_2)`; bounding it uniformly is the missing - step. + the even-target line. **First step.** Compute the kernel of + `F -> F_2[G]` in degree 4 (the smallest case where the low-degree matching + breaks) and re-derive conditions on the degree 1-4 layer sums there. + **Blocker.** From `q = 4` on, kernel elements of degree 4 and higher + absorb the low-degree mismatch (the `b a b a` counterexample of section 3 + is the smallest instance); controlling those higher-degree kernel terms is + the missing step. ## Reproduce diff --git a/research/even-target-cnot-census/TASK.json b/research/even-target-cnot-census/TASK.json index 7dc4bd5c48..e63487dae0 100644 --- a/research/even-target-cnot-census/TASK.json +++ b/research/even-target-cnot-census/TASK.json @@ -40,13 +40,13 @@ ] }, "scope_status": "refined", - "actual_scope": "Formal F2[GL2(F2)] rank-one-idempotent register model with free scalar GL_r(F2) mixing, but with the even order-3 target class: T_t = diag([c],...,[c]), c = ab = (ba)^2, at exactly r = t registers (t = 1, 2, 3, 4), all registers arbitrary dirty inputs restored exactly. Exact paid-call minimum; complete exclusion of every shorter even length; written sign-quotient and free-layer invariants; two engines (natural image and formal coefficients).", + "actual_scope": "Formal F2[GL2(F2)] rank-one-idempotent register model with free scalar GL_r(F2) mixing, but with the even order-3 target class: T_t = diag([c],...,[c]), c = ab = (ba)^2, at exactly r = t registers (t = 1, 2, 3, 4), all registers arbitrary dirty inputs restored exactly. Exact paid-call minimum; complete exclusion of every shorter even length; written sign-quotient invariants plus a free-layer screening system that is necessary only for words of length at most 3 (see README section 3); two engines (natural image and formal coefficients).", "scope_change_reason": "Refinement inside the card's allowed variation (fixed larger register count, specified nonabelian family F2[GL2(F2)]). The target element class is changed from the predecessor line's transposition (SWAP) targets to even order-3 targets: the sign quotient maps [c] to 1, so the inherited invariant flips from sum_i N_i = D_t to sum_i N_i = 0 and no predecessor conclusion transfers. This is not the excluded three-register abelian model.", "bottleneck_link": "Side result on the nonbinding bit side: no paid profile, supplier or moment changes. It prices the even-target tariff of an explicit nonabelian register alphabet, one input to whether any small-width completed saving could change the bit primitive; a q < 2t word would have been such a mechanism, and its absence through t = 4 narrows where one could live.", "budget_minutes": 60, "stop_rule": "Stop after the complete t = 4 decision (all shorter even lengths excluded or a formal witness found), one calibration against the predecessor's recorded ball counts, and the written-invariant checks; do not extend to t = 5 in this session.", "outcome": "completed", - "evidence": "RECEIPT.json: minima q*(t) = 2t for t = 1, 2, 3, 4 (2, 4, 6, 8); all meets nat_hits = 0 for every shorter even length; t = r = 4 exact-depth ball-value counts 240 / 32,651 / 3,639,920 match PR1705's recorded calibration; engine B agrees with engine A on every small meet; attaining words verified exactly in M_r(F2[G]) with drop-one-call mutations failing; free-layer system holds on all attaining words and is rejected on a wrong-target control. Final line: PASS_EVEN_TARGET_CNOT_CENSUS t1r1_min=2 t2r2_min=4 t3r3_min=6 t4r4_upper=8 t4r4_excluded={2: 0, 4: 0, 6: 0} balls4=240,32651,3639920 pr1705_ball_match=True no_new_kappa.", + "evidence": "RECEIPT.json: minima q*(t) = 2t for t = 1, 2, 3, 4 (2, 4, 6, 8); all meets nat_hits = 0 for every shorter even length; t = r = 4 exact-depth ball-value counts 240 / 32,651 / 3,639,920 match PR1705's recorded calibration; engine B agrees with engine A on every small meet; attaining words verified exactly in M_r(F2[G]) with drop-one-call mutations failing; free-layer screening system holds on the checked attaining words and is rejected on a wrong-target control, but is not necessary for hitting words (r = 1 b a b a counterexample; README section 3). Final line: PASS_EVEN_TARGET_CNOT_CENSUS t1r1_min=2 t2r2_min=4 t3r3_min=6 t4r4_upper=8 t4r4_excluded={2: 0, 4: 0, 6: 0} balls4=240,32651,3639920 pr1705_ball_match=True no_new_kappa.", "author": "Aaron Wang", "ai_assistance": "with help from opencode", "open_questions": [ @@ -57,10 +57,10 @@ "blocked_by": "Ball growth: the r = 5 depth-3 ball is expected to exceed the r = 4 depth-3 count of 3.6e6 states by at least an order of magnitude." }, { - "question": "Can the written free-layer system (sum_a = sum_b, sum_ba = 0, sum_aba = sum_bab = lam + nu) exclude q < 2t at general t = r in writing, without a meet?", + "question": "Can a written degree-complete kernel analysis exclude q < 2t at general t = r, without a meet? (The degree 1-3 free-layer system cannot: it is necessary only for words of length at most 3.)", "why_it_matters": "A written exclusion would remove the exponential meet from the even-target line entirely.", - "first_step": "Extract rank constraints from the layer system on (q_a, q_b) multisets of rank-one idempotents summing to I_r + lam, and test them against the t = 4 attaining data first.", - "blocked_by": "The kernel correction pair (lam, nu) is free in M_r(F2); bounding it uniformly is the missing step." + "first_step": "Compute the kernel of F -> F2[G] in degree 4 (the smallest case where the low-degree matching breaks) and re-derive conditions on the degree 1-4 layer sums there.", + "blocked_by": "From q = 4 on, kernel elements of degree 4 and higher absorb the low-degree mismatch (the r = 1 b a b a counterexample is the smallest instance); controlling those higher-degree kernel terms is the missing step." } ] } diff --git a/research/even-target-cnot-census/VERIFY.json b/research/even-target-cnot-census/VERIFY.json index 01e52ea6c7..db2ba8a9cc 100644 --- a/research/even-target-cnot-census/VERIFY.json +++ b/research/even-target-cnot-census/VERIFY.json @@ -16,7 +16,7 @@ "--check-receipt" ], "timeout_seconds": 600, - "checks": "Group table and packing controls (200 dense fast-update cross-checks, 100 formal-natural projection cross-checks, 50 parity controls); formal verification of every attaining word with drop-one-call mutations; written free-layer system checked on all attaining words and rejected on a wrong-target control; complete natural-image meets excluding q = 2 at t = 1, 2, 3, 4 and q = 4 at t = 3 and t = 4, q = 6 at t = 4; SWAP control reproduces the predecessor minimum 6 at t = r = 2; engine B (formal coefficients) agrees with engine A on every small meet; exact-depth ball-value counts at r = 4 recomputed as 240 / 32,651 / 3,639,920, matching the recorded PR1705 calibration; RECEIPT.json fields compared." + "checks": "Group table and packing controls (200 dense fast-update cross-checks, 100 formal-natural projection cross-checks, 50 parity controls); formal verification of every attaining word with drop-one-call mutations; free-layer screening filter asserted on the attaining words and rejected on a wrong-target control (screening only, not necessary and not sufficient; README section 3); complete natural-image meets excluding q = 2 at t = 1, 2, 3, 4 and q = 4 at t = 3 and t = 4, q = 6 at t = 4; SWAP control reproduces the predecessor minimum 6 at t = r = 2; engine B (formal coefficients) agrees with engine A on every small meet; exact-depth ball-value counts at r = 4 recomputed as 240 / 32,651 / 3,639,920, matching the recorded PR1705 calibration; RECEIPT.json fields compared." } ] } diff --git a/research/even-target-cnot-census/test_verify.py b/research/even-target-cnot-census/test_verify.py index c03a9e6f24..a1390f6bdc 100644 --- a/research/even-target-cnot-census/test_verify.py +++ b/research/even-target-cnot-census/test_verify.py @@ -1,10 +1,13 @@ """Rejection controls for research/even-target-cnot-census/verify.py.""" +import itertools import json import random +import sys import unittest from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) # works under -I import verify as v @@ -35,6 +38,103 @@ def test_layer_system_rejects_wrong_target_word(self): self.assertFalse(v.layer_ok_swap_target(v.word_even(2), 2)) self.assertTrue(v.layer_ok_swap_target(v.word_swap(2), 2)) + def test_layer_counterexample_baba(self): + # Review regression for + # https://github.com/CrocSwap/integer-mult-bounds/pull/1763 : at r=1 + # with every projector [1], the word b a b a is an exact target word + # since (ba)^2 = ab = c, but the free-layer screening filter rejects + # it (sum_ba = 1). The filter is therefore NOT a necessary condition + # (README section 3). + r = 1 + w = [(v.B_IDX, 1, 1), (v.A_IDX, 1, 1), (v.B_IDX, 1, 1), (v.A_IDX, 1, 1)] + self.assertTrue(v.formal_is_target(v.formal_word_value(w, r), r)) + self.assertFalse(v.layer_ok_even_target(w, r)) + self.assertEqual(v.layer_sums(w, r)["sum_ba"], 1) + + def test_layer_filter_not_sufficient(self): + # r=2, word a b on one projector passes the filter but is not a target + w = [(v.A_IDX, 1, 1), (v.B_IDX, 1, 1)] + self.assertTrue(v.layer_ok_even_target(w, 2)) + self.assertFalse(v.formal_is_target(v.formal_word_value(w, 2), 2)) + + def test_minima_do_not_rely_on_layer_condition(self): + # Make the invalid layer filter vacuous and confirm the reported + # minima and exclusion counts are unchanged: exclusion uses only L1' + # parity, the q=1 direct check and the meets. + here = Path(__file__).resolve().parent + stored = json.loads((here / "RECEIPT.json").read_text(encoding="utf-8")) + orig = v.layer_ok_even_target + v.layer_ok_even_target = lambda word, r: True + try: + fresh = json.loads(json.dumps(v.run(fast=True), default=str)) + finally: + v.layer_ok_even_target = orig + self.assertEqual(stored["t1r1"], fresh["t1r1"]) + self.assertEqual(stored["small_minima"], fresh["small_minima"]) + self.assertEqual(stored["swap_t2r2"], fresh["swap_t2r2"]) + self.assertEqual(fresh["main_t4r4"]["upper"], 8) + self.assertEqual(stored["main_t4r4"]["q"], {"2": 0, "4": 0, "6": 0}) + + def test_free_layer_validity_scope(self): + # README section 3 corrected claim. (1) up to degree 3 the kernel of + # F -> F_2[G] is 1-dimensional, spanned by R = xyx+yxy+x+y alone: + # the seven monomial images have rank 6 and Z's degree<=3 truncation + # x+y+yx maps to [ba]+[e] != 0. (2) every hitting word of length + # q <= 3 satisfies the corrected system (class: q <= 3 only). + e = 1 << v.E_IDX + + def gmul(u, w): + out = 0 + for i in range(6): + for j in range(6): + if ((u >> i) & 1) and ((w >> j) & 1): + out ^= 1 << v.GTAB[i][j] + return out + + x = e | (1 << v.A_IDX) + y = e | (1 << v.B_IDX) + imgs = {"1": e, "x": x, "y": y, "xy": gmul(x, y), "yx": gmul(y, x), + "xyx": gmul(gmul(x, y), x), "yxy": gmul(gmul(y, x), y)} + basis = [] + for key in ("1", "x", "y", "xy", "yx", "xyx", "yxy"): + cur = imgs[key] + for b in basis: + cur = min(cur, cur ^ b) + if cur: + basis.append(cur) + basis.sort() + self.assertEqual(len(basis), 6) # rank 6 -> ker dim 1 + self.assertEqual(imgs["x"] ^ imgs["y"] ^ imgs["xyx"] ^ imgs["yxy"], 0) + z_low = imgs["x"] ^ imgs["y"] ^ imgs["yx"] # Z = z+z^2+z^3, degree <= 3 + expected = (1 << v.E_IDX) | (1 << v.GIDX[v.mmul(v.MAT_B, v.MAT_A)]) + self.assertEqual(z_low, expected) # [ba] + [e], not in the kernel + + def layer_ok_short(word, r): + # corrected system, claimed only for words of length q <= 3 + self.assertLessEqual(len(word), 3) + s = v.layer_sums(word, r) + ident = v.mat_ident(r) + if s["sum_a"] != s["sum_b"]: + return False + lam = s["sum_a"] ^ ident + return (s["sum_ab"] == ident and s["sum_ba"] == 0 + and s["sum_aba"] == lam and s["sum_bab"] == lam) + + checked, hits = 0, 0 + for r in (1, 2): + gens = [(g[4], g[5], g[6]) for g in v.make_gens(r)] + for q in (1, 2, 3): + for w in itertools.product(gens, repeat=q): + checked += 1 + if v.formal_is_target(v.formal_word_value(list(w), r), r): + hits += 1 + self.assertTrue(layer_ok_short(list(w), r), (r, q, w)) + self.assertEqual(checked, 1898) # 14 at r=1, 1884 at r=2 + self.assertEqual(hits, 1) + # the counterexample has length 4: outside the claimed class + w4 = [(v.B_IDX, 1, 1), (v.A_IDX, 1, 1), (v.B_IDX, 1, 1), (v.A_IDX, 1, 1)] + self.assertTrue(v.formal_is_target(v.formal_word_value(w4, 1), 1)) + def test_parity_and_or_confusion_control(self): # the natural target transform is F_2 addition: 1+1 = 0 (a row of # two equal bits must cancel). Regression for a | / ^ confusion. diff --git a/research/even-target-cnot-census/verify.py b/research/even-target-cnot-census/verify.py index 60f620cad0..e4835830b2 100644 --- a/research/even-target-cnot-census/verify.py +++ b/research/even-target-cnot-census/verify.py @@ -20,8 +20,11 @@ B formal coefficients in M_r(F2[G]) (independent small-ball cross-check and exact acceptance of every attaining word). -The written free-layer system (README section 3) is checked on every -attaining word. Final line starts with PASS_EVEN_TARGET_CNOT_CENSUS. +The written free-layer system (README section 3) is asserted as a screening +filter on the attaining words only; it is NOT a necessary condition (the +r=1 word b a b a is a target word it rejects) and NOT sufficient (r=2 word +a b on one projector passes and is not a target). README section 3 states +the corrected scope. Final line starts with PASS_EVEN_TARGET_CNOT_CENSUS. """ from __future__ import annotations @@ -400,11 +403,16 @@ def formal_meet_count(gens, r: int, k: int, target_gi: int): # --------------------------------------------------------------------------- -# Written free-layer system (README section 3). For a word w with letters -# g_i in {a,b} and idempotents N_i, expand prod (I + E_i) = T in the free -# filtered algebra F_2/(x^2, y^2); the kernel of F -> F_2[G] up to the -# needed degree is spanned by R = xyx + yxy + x + y and Z = z + z^2 + z^3 -# with z = x + y + xy. Matching degrees 1..3 gives the system below. +# Free-layer sums (README section 3). For a word w with letters g_i in +# {a,b} and idempotents N_i, expand prod (I + E_i) = T in the free filtered +# algebra F_2/(x^2, y^2). Matching degrees 1..3 against the kernel of +# F -> F_2[G] is valid only for words of length q <= 3: up to degree 3 that +# kernel is 1-dimensional, spanned by R = xyx + yxy + x + y alone, since +# Z = z + z^2 + z^3 (z = x + y + xy) carries degrees up to 6 and its +# degree <= 3 truncation is not in the kernel. The checks below are +# screening filters only -- not necessary (r=1 b a b a is a target word they +# reject) and not sufficient (r=2 a b on one projector passes and is not a +# target). See README section 3. # --------------------------------------------------------------------------- def layer_sums(word, r: int): @@ -432,7 +440,10 @@ def layer_sums(word, r: int): def layer_ok_even_target(word, r: int) -> bool: - """Necessary conditions for a word to hit T = [c] I_r.""" + """Screening filter for words hitting T = [c] I_r (README section 3). + + Not necessary and not sufficient; never use it to exclude candidates. + """ s = layer_sums(word, r) ident = mat_ident(r) if s["sum_a"] != s["sum_b"]: @@ -449,7 +460,11 @@ def layer_ok_even_target(word, r: int) -> bool: def layer_ok_swap_target(word, r: int) -> bool: - """Necessary conditions for a word to hit T = [S] I_r.""" + """Layer conditions for the SWAP target T = [S] I_r. + + Used here only as a rejection control; necessity is not established + (same degree-matching caveat as README section 3). + """ s = layer_sums(word, r) ident = mat_ident(r) if (s["sum_a"] ^ s["sum_b"]) != ident: From eee12d54ae194afd0c74689d13ef1804f8ca0ff7 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 14:54:13 -0400 Subject: [PATCH 3/3] Research: bind task-catalogue provenance to pinned Git snapshot in even-target census --- research/even-target-cnot-census/SOURCES.json | 2 +- research/even-target-cnot-census/VERIFY.json | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/research/even-target-cnot-census/SOURCES.json b/research/even-target-cnot-census/SOURCES.json index 647efae4c9..46cc5b762e 100644 --- a/research/even-target-cnot-census/SOURCES.json +++ b/research/even-target-cnot-census/SOURCES.json @@ -10,7 +10,7 @@ }, { "path": "docs/research/agent-task-catalog.json", - "usage": "input", + "usage": "provenance", "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" }, diff --git a/research/even-target-cnot-census/VERIFY.json b/research/even-target-cnot-census/VERIFY.json index db2ba8a9cc..2529b9e442 100644 --- a/research/even-target-cnot-census/VERIFY.json +++ b/research/even-target-cnot-census/VERIFY.json @@ -4,7 +4,6 @@ "python": "3.12", "requirements": [], "inputs": [ - "docs/research/agent-task-catalog.json", "research/bit-three-register-lower-bound/README.md" ], "commands": [