From ff68746efa11b491734362d82ac7ff359aa1b48b Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 14 Oct 2026 20:12:35 +1100 Subject: [PATCH] Prove twelve-call minimum for four fully occupied swaps --- research/four-swap-full-occupancy/PINS.json | 13 + research/four-swap-full-occupancy/README.md | 183 ++ research/four-swap-full-occupancy/RESULT.json | 1763 +++++++++++++++++ .../four-swap-full-occupancy/SOURCES.json | 24 + research/four-swap-full-occupancy/TASK.json | 195 ++ research/four-swap-full-occupancy/VERIFY.json | 42 + .../four-swap-full-occupancy/independent.py | 219 ++ .../inputs/PR1722-PROOF.md | 166 ++ .../four-swap-full-occupancy/test_package.py | 136 ++ research/four-swap-full-occupancy/verify.py | 282 +++ 10 files changed, 3023 insertions(+) create mode 100644 research/four-swap-full-occupancy/PINS.json create mode 100644 research/four-swap-full-occupancy/README.md create mode 100644 research/four-swap-full-occupancy/RESULT.json create mode 100644 research/four-swap-full-occupancy/SOURCES.json create mode 100644 research/four-swap-full-occupancy/TASK.json create mode 100644 research/four-swap-full-occupancy/VERIFY.json create mode 100644 research/four-swap-full-occupancy/independent.py create mode 100644 research/four-swap-full-occupancy/inputs/PR1722-PROOF.md create mode 100644 research/four-swap-full-occupancy/test_package.py create mode 100644 research/four-swap-full-occupancy/verify.py diff --git a/research/four-swap-full-occupancy/PINS.json b/research/four-swap-full-occupancy/PINS.json new file mode 100644 index 0000000000..e5694ea9c4 --- /dev/null +++ b/research/four-swap-full-occupancy/PINS.json @@ -0,0 +1,13 @@ +{ + "files": [ + { + "local_path": "inputs/PR1722-PROOF.md", + "source_repo": "https://github.com/CrocSwap/integer-mult-bounds", + "source_head": "246cd6b3a795a346bc6a741661ddcdb2d6359103", + "source_path": "research/coordinate-cnot-label-saturation/PROOF.md", + "sha256": "b50ea6499ed5e7f142122ee56dfa07ea9a404e049e1a1c13d881299c69009893", + "author": "Ross Richardson with substantial OpenAI Codex assistance", + "license": "Apache-2.0" + } + ] +} diff --git a/research/four-swap-full-occupancy/README.md b/research/four-swap-full-occupancy/README.md new file mode 100644 index 0000000000..9d07ef4e83 --- /dev/null +++ b/research/four-swap-full-occupancy/README.md @@ -0,0 +1,183 @@ +# Four fully occupied coordinate-SWAP roles require twelve calls + +**Scoped written theorem; no new kappa.** In the formal +`F2[GL_2(F2)]` register model, four SWAP targets on exactly four roles +require **twelve** paid coordinate-CNOT calls. All four inputs are arbitrary; +there is no extra workspace role. Free scalar `GL_4(F2)` mixing is allowed. + +This closes the balanced ten-call case **at four roles** left by Ross +Richardson's [PR1722](https://github.com/CrocSwap/integer-mult-bounds/pull/1722) +and investigated by Aaron Wang's +[PR1755](https://github.com/CrocSwap/integer-mult-bounds/pull/1755). +It does **not** exclude ten calls with active/dirty coupling on five or six +roles. The arbitrary-workspace question remains open. + +The new step is an elementary twisted cyclic rotation, combined with the +credited label-saturation theorem. The proof is below and is self-contained; +finite checks corroborate its algebra and boundaries. No SAT solver, long +search trace or proof-assistant kernel is needed for the submitted result. + +## Exact model and bill + +Let `a=[[1,1],[0,1]]`, `b=[[1,0],[1,1]]`, and +`s=aba=bab=[[0,1],[1,0]]` in `G=GL_2(F2)`. A paid call is + +`D_N(g)=I+([g]+1)N`, with `g in {a,b}`, `N=uv^T` binary, `v^T u=1`. + +Every call, including an undo, costs one. Free scalar basis changes can be +moved to the right by conjugating the projectors; augmentation `[g] -> 1` +forces the remaining scalar factor to be identity. This normalization is +credited to Gareth Davidson/PR1333 and the coordinate-CNOT predecessors. +There are no free address maps, erasures, clean allocations or overwrites. +Equality is in the **full formal group algebra**, not just a small address +representation. + +For `t` fully occupied roles, the target is `T=[s] I_t`. The direct word +uses `aba` on each coordinate projector and costs `3t`, including every paid +operation. This is an optimistic abstract tariff: scalar work and workspace +costs are free in this model. It supplies no physical compiler, hosting, +precision/tape or analytic bound and no new recursive profile or exponent. + +## Proof + +**Credited saturation lemma (PR1722).** For `t` SWAP targets and any number +of restored dirty extras, both label counts are at least `t`. If one count +is exactly `t`, the other is at least `2t`. + +Here is the argument, restated with credit so this note has no unchecked +numerical dependency. Normalize the free scalar maps. The sign quotient +`G -> C2`, over `F2[epsilon]/(epsilon^2)`, gives `sum N_i=P`, where +`P=diag(I_t,0)`, and taking trace gives `q=t mod 2`. In the natural address +representation, the two paid maps are + +`a: [[I,N],[0,I]]`, `b: [[I,0],[N,I]]`, + +and the target is `[[I+P,P],[P,I+P]]`. Hence each label's image vectors span +`im P`, proving the count floor `t`. + +If exactly `t` a-calls occur, their image vectors form a basis of `im P`. +Conjugate that basis to the active coordinate basis, keeping the dirty +complement fixed. Each active top row changes exactly once from `[e_i,0]` +to `[0,e_i]`, so the sum of the two top blocks is always `I`. The two bottom +blocks therefore have sum `I + sum_(preceding b) N_j`; their final sum is +`I`, so `sum_b N_j=0`. The full sign equation then gives `sum_a N_i=P`. +Since the a images are distinct coordinate vectors, their covectors are +also the corresponding coordinate covectors. At a's unique update of row +`i`, bottom row `i` must be `[e_i,e_i]`; its block sum is zero. Thus +`e_i^T=sum_(b before a_i) e_i^T N_j`, so all active covectors lie in the +span of the b covectors. If `U` contains the b images and `V` the b +covectors, `UV=0`, `rank U>=t`, `rank V>=t`. Rank-nullity gives +`n_b>=rank U+rank V>=2t`. Interchanging address coordinates proves the +symmetric case. The original frozen proof is retained unchanged in +[inputs/PR1722-PROOF.md](inputs/PR1722-PROOF.md). + +**New rotation step.** Write a word in chronological order +`D_1,...,D_q`, so `D_q ... D_1=T`. At full occupancy, conjugation by +`T=[s]I_t` exchanges a and b and keeps every scalar projector `N` fixed: + +`T D_N(a) T^-1=D_N(b)`, and conversely. + +Consequently the chronological word + +`D_2,...,D_q, T D_1 T^-1` + +has the same target: its product is +`(T D_1 T^-1)(T D_1^-1)=T`. It has exactly the same number of legal paid +calls and flips just the moved call's label. + +For four roles, a sub-twelve word has even length by the sign trace and at +least four calls of each label. Saturation excludes length eight and the +`(4,6)`/`(6,4)` length-ten counts. Only `(5,5)` remains. Rotate its first +call: the result has counts `(4,6)` or `(6,4)`, which saturation excludes. +Four direct `aba` words attain twelve. This proves the stated minimum. + +**Uniform cut consequence.** The same observation is useful beyond four +roles. If a fully occupied `t`-target word saves over `3t`, then every +rotated cut must have both counts at least `t+1`, by saturation. Let the +original counts be `A,B`, and let `s_k` be a-prefix-count minus +b-prefix-count among the first `k` calls. Rotating that prefix flips all +its labels, so its new counts are `A-s_k, B+s_k`. Thus every cut obeys + +`t+1-B <= s_k <= A-t-1`. + +This integer interval has width `q-2t-2`. Since consecutive `s_k` differ +by one, `q>=2t+3`. If equality holds, the walk is confined to two adjacent +integers, so the labels strictly alternate. The retained trace parity +`q=t mod 2` still applies. For example, a possible thirteen-call saving +for five fully occupied targets must be strictly alternating. This note +neither constructs nor excludes that case. + +**Workspace boundary.** For a partial target `I+([s]+1)P`, conjugation can +mix group coefficients with active/dirty blocks, and need not preserve the +paid alphabet. The verifier gives an explicit legal coupled projector +whose conjugate is not *any* allowed paid factor. Thus the rotation proof +must not be extended to arbitrary restored dirty workspace. If every +normalized projector commutes with `P`, each rank-one projector acts wholly +inside either the active or dirty subspace; restricting to the active +subspace gives the four-role word. Therefore any ten-call escape with +extras must use active/dirty coupling. + +## Reproduce and checked scope + +From the repository root, Python 3.12 and the standard library only: + +```sh +python3.12 -I -B scripts/research_package.py --package research/four-swap-full-occupancy +``` + +The registered replay runs the primary exact checker, a separately written +faithful-operator checker, and the package failure controls. Expected markers +are `PASS_FOUR_SWAP_FULL_OCCUPANCY` and +`PASS_INDEPENDENT_FULL_OCCUPANCY`, with `minimum=12 no_new_kappa`. +Normal verification is read-only; `verify.py --write` explicitly regenerates +the deterministic receipt. Exact counts and source hashes are in RESULT.json. + +The primary engine multiplies formal six-coefficient algebra entries. The +second constructs the regular action on the six binary address matrices and +compares complete binary operators. They share the declared model and receipt, +not executable mathematics. Both were written by one assisted author; this is +not independent human review or a Lean formalization. + +The finite checks cover full-occupancy conjugation for every binary rank-one +idempotent through six roles, all cuts of diverse attaining words, the complete +binary-label cut screen through length sixteen, and a concrete partial-target +failure. They corroborate the written all-`t` argument; no finite search is +used to justify its universal quantifier. The selected-record check is separate +from a full selected cold replay, which was not needed or run. + +## Provenance, overlap and credit + +Base main: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Selected-record +SHA256: `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Chooser nonce: `31f0c7f2788860364077aac4b428311c`, priority revision 3, +card `bit-new-register-model`. TASK.json records the exact scope, initial +encoding experiment, final proof refinement, overlap coverage and pins. +The [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18919990) +coordinates this contribution with the existing register-model thread. + +Credit commdata2338/PR1414 and PR1491 for the formal model, sign invariant +and earlier swap results; Gareth Davidson/PR1333 for normalization; Cinna +Davis/PR1541 for arbitrary-workspace reasoning and role compression; +Ross Richardson/PR1722 for saturation; and Aaron Wang/PR1705 and PR1755 for +the four-target boundary, residual search and collapsed augmentation-layer +finding. The generic conjugation/cyclic-product identity is elementary; +no literature-priority claim for that identity is intended. The new +application excludes this exact residual and gives the cut constraint. + +Prepared for **Ross Richardson** with substantial **OpenAI Codex assistance** +in reasoning, implementation, checks and writing. New work is Apache-2.0; +predecessor attribution and the selected frontier are unchanged. + +## Open next questions + +1. **Can active/dirty coupling realize four swaps in ten calls?** This is + the remaining potential saving in the same alphabet. PR1722/PR1541 reduce + arbitrary finite workspace to at most six roles. First test the balanced + five-plus-five formal endpoint at five or six roles with a proof-producing + solver; full target conjugation cannot be used as a symmetry there. A + preliminary six-role conflict-budget run was inconclusive. +2. **Can five fully occupied targets use thirteen alternating calls?** The + new cut constraint isolates this next candidate below fifteen. Start with + either alternating label word and rank-one idempotent unknowns, retaining + the full formal endpoint and sign equation. Noncommuting scalar-projector + interactions remain the blocker. No success is predicted. diff --git a/research/four-swap-full-occupancy/RESULT.json b/research/four-swap-full-occupancy/RESULT.json new file mode 100644 index 0000000000..ad6c5892fd --- /dev/null +++ b/research/four-swap-full-occupancy/RESULT.json @@ -0,0 +1,1763 @@ +{ + "schema_version": 1, + "claim": { + "targets": 4, + "roles": 4, + "minimum": 12, + "extra_dirty_roles": 0, + "no_new_kappa": true + }, + "conjugations": [ + { + "roles": 1, + "projectors": 1, + "checks": 2, + "sha256": "8f2e433821d0945a67eb4f33d590301572eec9b9eeb6861770d531d922585dff" + }, + { + "roles": 2, + "projectors": 6, + "checks": 12, + "sha256": "a6b314987f7cffd66a545a9a0852daef6b1a1a4736fc6637c500f722fd4b87ff" + }, + { + "roles": 3, + "projectors": 28, + "checks": 56, + "sha256": "f5e8028fb24ff0641179dc60cae286b2c164397aac8b775738c49eabb20e1c2c" + }, + { + "roles": 4, + "projectors": 120, + "checks": 240, + "sha256": "90dc4cacbcb91c503b9bf925d48af529a2a83664b6b74aac5f547121980b57bd" + }, + { + "roles": 5, + "projectors": 496, + "checks": 992, + "sha256": "651363cd642801b0ce68705fc49efa8ec30798cede423980607e38ae006fa6b9" + }, + { + "roles": 6, + "projectors": 2016, + "checks": 4032, + "sha256": "5c936ce4fa055f7d59598600ed7dfe89d713301fce191ff51d9431f477c96882" + } + ], + "fixtures": [ + { + "roles": 1, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ] + ] + }, + { + "roles": 1, + "word": [ + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 1, + "word": [ + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 1, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 2, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ] + ] + }, + { + "roles": 2, + "word": [ + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 2, + "word": [ + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ] + ] + }, + { + "roles": 2, + "word": [ + [ + "a", + 3, + 1 + ], + [ + "a", + 3, + 1 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ] + ] + }, + { + "roles": 3, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ] + ] + }, + { + "roles": 3, + "word": [ + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 3, + "word": [ + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ] + ] + }, + { + "roles": 3, + "word": [ + [ + "a", + 7, + 1 + ], + [ + "a", + 7, + 1 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ] + ] + }, + { + "roles": 4, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 8, + 8 + ], + [ + "a", + 8, + 8 + ] + ] + }, + { + "roles": 4, + "word": [ + [ + "a", + 8, + 8 + ], + [ + "b", + 8, + 8 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 4, + "word": [ + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ] + ] + }, + { + "roles": 4, + "word": [ + [ + "a", + 15, + 1 + ], + [ + "a", + 15, + 1 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ] + ] + }, + { + "roles": 5, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 8, + 8 + ], + [ + "a", + 8, + 8 + ], + [ + "a", + 16, + 16 + ], + [ + "b", + 16, + 16 + ], + [ + "a", + 16, + 16 + ] + ] + }, + { + "roles": 5, + "word": [ + [ + "b", + 16, + 16 + ], + [ + "a", + 16, + 16 + ], + [ + "b", + 16, + 16 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 8, + 8 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 5, + "word": [ + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ] + ] + }, + { + "roles": 5, + "word": [ + [ + "a", + 31, + 1 + ], + [ + "a", + 31, + 1 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ] + ] + }, + { + "roles": 6, + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 8, + 8 + ], + [ + "a", + 8, + 8 + ], + [ + "a", + 16, + 16 + ], + [ + "b", + 16, + 16 + ], + [ + "a", + 16, + 16 + ], + [ + "a", + 32, + 32 + ], + [ + "b", + 32, + 32 + ], + [ + "a", + 32, + 32 + ] + ] + }, + { + "roles": 6, + "word": [ + [ + "a", + 32, + 32 + ], + [ + "b", + 32, + 32 + ], + [ + "a", + 32, + 32 + ], + [ + "b", + 16, + 16 + ], + [ + "a", + 16, + 16 + ], + [ + "b", + 16, + 16 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 8, + 8 + ], + [ + "a", + 8, + 8 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 4, + 4 + ], + [ + "b", + 4, + 4 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 2, + 2 + ], + [ + "a", + 2, + 2 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ] + }, + { + "roles": 6, + "word": [ + [ + "a", + 48, + 32 + ], + [ + "b", + 48, + 32 + ], + [ + "a", + 48, + 32 + ], + [ + "b", + 24, + 48 + ], + [ + "a", + 24, + 48 + ], + [ + "b", + 24, + 48 + ], + [ + "a", + 12, + 56 + ], + [ + "b", + 12, + 56 + ], + [ + "a", + 12, + 56 + ], + [ + "b", + 6, + 60 + ], + [ + "a", + 6, + 60 + ], + [ + "b", + 6, + 60 + ], + [ + "a", + 3, + 62 + ], + [ + "b", + 3, + 62 + ], + [ + "a", + 3, + 62 + ], + [ + "b", + 1, + 63 + ], + [ + "a", + 1, + 63 + ], + [ + "b", + 1, + 63 + ] + ] + }, + { + "roles": 6, + "word": [ + [ + "a", + 63, + 1 + ], + [ + "a", + 63, + 1 + ], + [ + "a", + 48, + 32 + ], + [ + "b", + 48, + 32 + ], + [ + "a", + 48, + 32 + ], + [ + "b", + 24, + 48 + ], + [ + "a", + 24, + 48 + ], + [ + "b", + 24, + 48 + ], + [ + "a", + 12, + 56 + ], + [ + "b", + 12, + 56 + ], + [ + "a", + 12, + 56 + ], + [ + "b", + 6, + 60 + ], + [ + "a", + 6, + 60 + ], + [ + "b", + 6, + 60 + ], + [ + "a", + 3, + 62 + ], + [ + "b", + 3, + 62 + ], + [ + "a", + 3, + 62 + ], + [ + "b", + 1, + 63 + ], + [ + "a", + 1, + 63 + ], + [ + "b", + 1, + 63 + ] + ] + } + ], + "cut_checks": 288, + "rotations_sha256": "8bb8ece200e1c5522b5bdc3356edfabfdb623483f259695be7ef2532ece2bcc5", + "omission_controls": 264, + "label_screen": { + "patterns": 99861, + "rows": [ + { + "targets": 1, + "calls": 1, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 2, + "calls": 0, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 2, + "calls": 2, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 2, + "calls": 4, + "floor": 6, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 3, + "calls": 1, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 3, + "calls": 3, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 3, + "calls": 5, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 3, + "calls": 7, + "floor": 70, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 4, + "calls": 0, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 4, + "calls": 2, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 4, + "calls": 4, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 4, + "calls": 6, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 4, + "calls": 8, + "floor": 70, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 4, + "calls": 10, + "floor": 672, + "after_saturation": 252, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 1, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 3, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 5, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 7, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 9, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 11, + "floor": 924, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 5, + "calls": 13, + "floor": 6006, + "after_saturation": 3432, + "after_cuts": 2 + }, + { + "targets": 6, + "calls": 0, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 2, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 4, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 6, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 8, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 10, + "floor": 0, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 12, + "floor": 924, + "after_saturation": 0, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 14, + "floor": 9438, + "after_saturation": 3432, + "after_cuts": 0 + }, + { + "targets": 6, + "calls": 16, + "floor": 51766, + "after_saturation": 35750, + "after_cuts": 512 + } + ] + }, + "workspace_boundary": { + "roles": 5, + "targets": 4, + "call": [ + "a", + 17, + 1 + ], + "conjugate": [ + [ + 16, + 0, + 0, + 0, + 0 + ], + [ + 0, + 4, + 0, + 0, + 0 + ], + [ + 0, + 0, + 4, + 0, + 0 + ], + [ + 0, + 0, + 0, + 4, + 0 + ], + [ + 3, + 0, + 0, + 0, + 4 + ] + ], + "alphabet_size": 992 + }, + "controls": [ + "expanded-label", + "nilpotent", + "boolean-vector", + "float-vector", + "unflipped-rotation", + "partial-target-not-in-alphabet" + ] +} diff --git a/research/four-swap-full-occupancy/SOURCES.json b/research/four-swap-full-occupancy/SOURCES.json new file mode 100644 index 0000000000..020b348e4b --- /dev/null +++ b/research/four-swap-full-occupancy/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": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/coordinate-cnot-register-bound/README.md", + "usage": "input", + "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211", + "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe" + } + ] +} diff --git a/research/four-swap-full-occupancy/TASK.json b/research/four-swap-full-occupancy/TASK.json new file mode 100644 index 0000000000..1fe311200f --- /dev/null +++ b/research/four-swap-full-occupancy/TASK.json @@ -0,0 +1,195 @@ +{ + "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": "Prove that four coordinate-SWAP targets on exactly four roles require twelve calls in formal F2[GL2(F2)], and derive the uniform full-occupancy twisted-cut constraint. No extra-workspace exclusion.", + "scope_change_reason": "The allowed nonabelian-family variation is narrowed to full occupancy. The initial faithful SAT encoding found the r=4 obstruction; twisting a boundary call gives a short analytic proof using credited saturation. A concrete partial-target conjugation counterexample prevents extension to r=5,6. The extra-workspace experiment remains explicitly inconclusive.", + "bottleneck_link": "Closes the exact four-role ten-call residual with a proof, so this fixed alphabet cannot improve the direct twelve-call abstract tariff at full occupancy. The selected bit primitive is nonbinding; no physical supplier, changed paid profile or kappa gain follows.", + "budget_minutes": 60, + "stop_rule": "Stop construction search when the four-role residual is excluded; verify the written argument, finite algebra and boundary counterexample, then refresh overlap and hand off the coupled-workspace case. Reserve the final session portion for replay and publication.", + "outcome": "completed", + "evidence": "Self-contained credited saturation proof plus new twisted-rotation argument in README. Primary formal coefficient replay, separate faithful regular operators, exact complete label-cut screen, source/receipt/domain/relocation controls. RESULT.json is deterministic; no SAT trace is a proof dependency.", + "author": "Ross Richardson with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in reasoning, implementation, verification and writing. Single agent; no independent human or proof-assistant review.", + "open_questions": [ + { + "question": "Can four active swaps be realized by ten balanced calls using one or two restored dirty extras?", + "why_it_matters": "This is the remaining possible saving in the same fixed alphabet; full-occupancy conjugation does not preserve coupled paid factors.", + "first_step": "Encode the full formal endpoint and balanced counts at five or six roles with proof-producing SAT; do not impose the full-occupancy conjugation symmetry.", + "blocked_by": "Noncommuting active/dirty projector interaction; the preliminary six-role budget was inconclusive." + }, + { + "question": "Can five fully occupied swap targets use thirteen strictly alternating calls?", + "why_it_matters": "The new cut bound isolates this next possible saving below the direct fifteen-call tariff.", + "first_step": "Fix either alternating thirteen-label pattern and search legal scalar projectors with the full formal endpoint and sign invariant.", + "blocked_by": "No construction or exclusion for the remaining noncommuting projector equations." + } + ], + "chooser_nonce": "31f0c7f2788860364077aac4b428311c", + "scope_key": "7084092dd726e7ba1f2f:full-occupancy-four-swap:twisted-cyclic-cut", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18919990", + "initial_task": "Balanced ten-call four-SWAP formal F2[GL2(F2)] word, with four active roles and zero to two arbitrary restored dirty roles; exact natural-plus-sign formulation and bounded SAT experiment.", + "predecessors": [ + { + "pr": 1722, + "head": "246cd6b3a795a346bc6a741661ddcdb2d6359103", + "author": "Ross Richardson", + "role": "Label-saturation theorem; exact original proof retained byte-for-byte." + }, + { + "pr": 1755, + "head": "bf73c0845196229b8050364ea7e26edd81f381ab", + "author": "Aaron Wang / navinor", + "role": "Direct residual predecessor: collapsed J^2 layer and bounded sampled search." + }, + { + "pr": 1705, + "head": "ad6b7d641b3e8576a95add7981fa75b6a8278fbc", + "author": "Aaron Wang / navinor", + "role": "Four-role finite lower boundary and search measurement." + }, + { + "pr": 1541, + "head": "194724d87505ec2517fdca1c1884da12398f4c33", + "author": "Cinna Davis / 1337isnot1337", + "role": "Arbitrary-workspace three-swap reasoning and role compression." + }, + { + "pr": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "author": "commdata2338", + "role": "Formal model and sign quotient." + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "author": "Gareth Davidson / bitplane", + "role": "Free scalar normalization and paid alphabet question." + } + ], + "overlap": { + "entry": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T08:48:38.838899+00:00", + "complete_pagination": true, + "records": 431 + }, + "discussions": { + "fetched_at": "2026-10-14T08:50:14.551323+00:00", + "complete_pagination": true, + "records": 387 + } + }, + "warnings": [] + }, + "proof_checkpoint": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T09:01:33.709629+00:00", + "complete_pagination": true, + "records": 434 + }, + "discussions": { + "fetched_at": "2026-10-14T09:03:11.699448+00:00", + "complete_pagination": true, + "records": 391 + } + }, + "warnings": [], + "matches_total": 15 + }, + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "distinction": "PR1722 leaves 5+5 open. PR1755 excludes one quotient method and reports a finite sampled search failure. This new proof excludes the entire r=4 residual by target conjugation, while preserving their broader workspace boundary and credit.", + "final": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T09:10:30.464597+00:00", + "complete_pagination": true, + "records": 435 + }, + "discussions": { + "fetched_at": "2026-10-14T09:12:05.095313+00:00", + "complete_pagination": true, + "records": 396 + } + }, + "warnings": [], + "matches_total": 15, + "assessed_matches": "All 15 records inspected: direct predecessors and their claims, own claim/package, one unrelated compact-control audit and one signed connector package. No matching full-occupancy twisted-cut proof found; this is not a novelty guarantee." + } + }, + "initial_experiments": { + "status": "Discovery only; not submitted proof dependencies or a package acceptance gate. The reproducible submitted argument is analytic.", + "tools": "z3-solver 5.1.0.0; python-sat 1.9.dev15 with Glucose4/CaDiCaL; drat-trim 2e3b2dc0ecf938addbd779d42877b6ed69d9a985; scratch files retained outside checkout.", + "four_roles_balanced": "Glucose4 UNSAT (278128 conflicts); separate drat-trim and C LRAT check passed; a separately written positive-hint checker accepted 153700 additions / 26331085 hints. This led to the short rotation proof, so the large search trace is not distributed or needed.", + "six_roles_balanced": "One 1000000-conflict-budget Glucose4 run returned unknown after 1000136 conflicts. No exclusion or construction at five/six roles.", + "four_roles_unrestricted_labels": "One 500000-conflict-budget Glucose4 run returned unknown; it does not weaken the separate analytic result." + }, + "validation": { + "python": "3.12.12", + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "mathematical_scope_frozen_at": "2026-10-14T09:03:39Z", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE research/four-swap-full-occupancy outcome=completed", + "commands": [ + "python3.12 -I -B scripts/research_package.py --package research/four-swap-full-occupancy", + "make selected-record-check", + "git diff --check" + ], + "finite_counts": { + "formal_and_regular_conjugations": 5334, + "positive_words": 24, + "chronological_cuts": 288, + "single_call_omissions": 264, + "label_patterns": 99861, + "partial_target_alphabet": 992, + "test_groups": 5 + }, + "unrun": [ + "selected supplier complete cold replay", + "physical/compiler/hosting admission", + "precision/tape and analytic transfer", + "Lean or independent human proof review", + "hosted CI" + ], + "sources_unchanged_on_refetch": "0b1cccf86e2f5132ed286a26ef0a681a495740ea" + } +} diff --git a/research/four-swap-full-occupancy/VERIFY.json b/research/four-swap-full-occupancy/VERIFY.json new file mode 100644 index 0000000000..cd41c6a77f --- /dev/null +++ b/research/four-swap-full-occupancy/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coordinate-cnot-register-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Formal coefficients: complete legal projectors through six roles, all positive-word cuts, omitted calls, label-cut screen and partial-target alphabet counterexample." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Code-disjoint faithful regular operators, full endpoints and separate literal cut enumeration." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Five failure-sensitive groups covering scope, chronology, nonfaithful aliases, corrupt receipts/source pins, JSON, optimized read-only relocation and deterministic replay." + } + ] +} diff --git a/research/four-swap-full-occupancy/independent.py b/research/four-swap-full-occupancy/independent.py new file mode 100644 index 0000000000..70275d4a30 --- /dev/null +++ b/research/four-swap-full-occupancy/independent.py @@ -0,0 +1,219 @@ +#!/usr/bin/env python3 +"""Faithful regular-operator check, with no import of primary mathematics. +Apache-2.0. Ross Richardson with substantial OpenAI Codex assistance. +""" +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +class Failure(ValueError): + pass + + +def require(condition, why): + if not condition: + raise Failure(why) + + +def load(path): + def pairs(items): + out = {} + for key, value in items: + require(key not in out, 'duplicate key') + out[key] = value + return out + def invalid(value): + raise Failure('nonfinite value') + return json.loads(path.read_text(), object_pairs_hook=pairs, parse_constant=invalid) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), ensure_ascii=True) + + +def hash_value(value): + return hashlib.sha256(canonical(value).encode()).hexdigest() + + +def action(m, x): + return ((m[0]*x[0]+m[1]*x[1]) % 2, (m[2]*x[0]+m[3]*x[1]) % 2) + + +def composition(m, n): + col0, col1 = action(m, (n[0], n[2])), action(m, (n[1], n[3])) + return col0[0], col1[0], col0[1], col1[1] + + +VECTORS = tuple(itertools.product((0, 1), repeat=2)) +GROUP = sorted((m for m in itertools.product((0, 1), repeat=4) + if len({action(m, x) for x in VECTORS}) == 4), + key=lambda m: sum(x << i for i, x in enumerate(m))) +IDENTITY = (1, 0, 0, 1) +LABELS = {'a': (1, 1, 0, 1), 'b': (1, 0, 1, 1)} +SWAP = (0, 1, 1, 0) +ID_COLUMN = GROUP.index(IDENTITY) + + +def bm(x, y): + result = [] + for row in x: + value = 0 + while row: + bit = row & -row + value ^= y[bit.bit_length()-1] + row -= bit + result.append(value) + return result + + +def eye(n): + return [1 << i for i in range(n)] + + +def regular(g): + result = [0] * 6 + for j, h in enumerate(GROUP): + result[GROUP.index(composition(g, h))] |= 1 << j + return result + + +def target(r, t): + rows = [0] * (6*r) + for i in range(r): + block = regular(SWAP if i < t else IDENTITY) + for j in range(6): + rows[6*i+j] = block[j] << (6*i) + return rows + + +def scalar_projectors(r): + out = [] + for image in range(1, 2**r): + for coimage in range(1, 2**r): + matrix = [coimage if (image >> i) & 1 else 0 for i in range(r)] + # Rank one follows because all nonzero rows equal one nonzero row. + if bm(matrix, matrix) == matrix: + out.append((image, coimage)) + return out + + +def operator(call, r): + require(type(r) is int and 1 <= r <= 6, 'roles') + require(type(call) is list and len(call) == 3, 'call shape') + label, image, coimage = call + require(type(label) is str and label in LABELS, 'label domain') + require(type(image) is int and type(coimage) is int and 0 < image < 2**r and 0 < coimage < 2**r, 'vectors') + scalar = [coimage if image & (1 << i) else 0 for i in range(r)] + require(bm(scalar, scalar) == scalar, 'idempotent') + delta = [x ^ y for x, y in zip(regular(LABELS[label]), eye(6))] + result = eye(6*r) + for i in range(r): + if image & (1 << i): + for j in range(r): + if coimage & (1 << j): + for k in range(6): + result[6*i+k] ^= delta[k] << (6*j) + return result + + +def replay(word, r): + require(type(word) is list, 'word type') + result = eye(6*r) + for call in word: + result = bm(operator(call, r), result) + return result + + +def coefficients(operator_rows, r): + # Faithfulness: applying a group-algebra block to [identity] reads its coefficients. + return [[sum(((operator_rows[6*i+k] >> (6*j+ID_COLUMN)) & 1) << k for k in range(6)) + for j in range(r)] for i in range(r)] + + +def screen(): + rows = [] + patterns = 0 + for t in range(1, 7): + for q in range(min(3*t, 17)): + if q % 2 != t % 2: + continue + f = s = c = 0 + for labels in itertools.product('ab', repeat=q): + patterns += 1 + a, b = labels.count('a'), labels.count('b') + if a < t or b < t: + continue + f += 1 + if a == t or b == t: + continue + s += 1 + # Rebuild every transformed word, instead of using the walk formula. + allowed = True + for k in range(q+1): + moved = labels[k:] + tuple('b' if g == 'a' else 'a' for g in labels[:k]) + if moved.count('a') <= t or moved.count('b') <= t: + allowed = False + break + c += allowed + rows.append({'targets':t,'calls':q,'floor':f,'after_saturation':s,'after_cuts':c}) + return {'patterns':patterns,'rows':rows} + + +def verify(): + receipt = load(HERE / 'RESULT.json') + require(canonical(receipt['claim']) == canonical({'targets':4,'roles':4,'minimum':12,'extra_dirty_roles':0,'no_new_kappa':True}), 'claim boundary') + for source in load(HERE / 'PINS.json')['files']: + require(hashlib.sha256((HERE / source['local_path']).read_bytes()).hexdigest() == source['sha256'], 'source pin') + classes = [] + for r in range(1, 7): + transform = target(r, r) + projectors = scalar_projectors(r) + values = [] + for u, v in projectors: + for label in ('a', 'b'): + op = operator([label, u, v], r) + conjugated = bm(bm(transform, op), transform) + require(conjugated == operator(['b' if label == 'a' else 'a', u, v], r), 'conjugation') + require(bm(op, op) == eye(6*r), 'involution') + values.append(coefficients(conjugated, r)) + classes.append({'roles':r,'projectors':len(projectors),'checks':len(values),'sha256':hash_value(values)}) + require(canonical(classes) == canonical(receipt['conjugations']), 'conjugation receipt') + require(len(receipt['fixtures']) == 24, 'positive fixture coverage') + cuts = omissions = 0 + all_rotated = [] + for fixture in receipt['fixtures']: + r, word = fixture['roles'], fixture['word'] + require(replay(word,r) == target(r,r), 'full positive operator') + for k in range(len(word)+1): + rotated = [x[:] for x in word[k:]] + [['b' if x[0]=='a' else 'a',x[1],x[2]] for x in word[:k]] + require(replay(rotated,r) == target(r,r), 'full rotated operator') + all_rotated.append(rotated) + cuts += 1 + for k in range(len(word)): + require(replay(word[:k]+word[k+1:],r) != target(r,r), 'omission') + omissions += 1 + require(type(receipt['cut_checks']) is int and cuts == receipt['cut_checks'], 'cut count') + require(type(receipt['omission_controls']) is int and omissions == receipt['omission_controls'], 'omission count') + require(hash_value(all_rotated) == receipt['rotations_sha256'], 'rotation hash') + require(canonical(screen()) == canonical(receipt['label_screen']), 'label screen') + r,t,call = 5,4,['a',17,1] + conjugated = bm(bm(target(r,t),operator(call,r)),target(r,t)) + alphabet = [operator([g,u,v],r) for u,v in scalar_projectors(r) for g in ('a','b')] + require(conjugated not in alphabet, 'workspace boundary') + expect = {'roles':r,'targets':t,'call':call,'conjugate':coefficients(conjugated,r),'alphabet_size':len(alphabet)} + require(canonical(expect) == canonical(receipt['workspace_boundary']), 'boundary receipt') + # Direct operator corruption: one changed output bit must not be hidden by coefficient projection. + bad = target(4,4) + bad[0] ^= 1 + require(bad != replay([['a',1,1],['b',1,1],['a',1,1]] + [[g,1<=t>=1`, work in the **formal** +algebra `M_r(F2[G])`. One paid unit is + +`D_N(g)=I+([g]+1)N`, where `g` is only `a` or `b`, `N=uv^T`, and `v^T u=1`. + +Free scalar `GL_r(F2)` basis changes are allowed. Every address call, +including an undo, costs one. No other address maps, copies, erasures, +overwrites or clean allocation are available. The complete target is + +`T=I+([s]+1)P`, with `P=diag(I_t,0)`. + +All inputs are arbitrary. Every extra register is restored and may not leak +into active outputs. Equality is in the group algebra, not merely its +natural two-dimensional address representation. The direct bill is `3t`: +use `bab` or `aba` on each active coordinate projector. + +**Label-saturation theorem.** Write `n_a,n_b` for the paid label counts. +Every such word has `n_a,n_b>=t`. If `n_a=t`, then `n_b>=2t`; symmetrically, +if `n_b=t`, then `n_a>=2t`. At equality `(t,2t)` or `(2t,t)`, every normalized +paid projector satisfies `PN=N=NP`: the paid factors do not couple the +restored dirty complement. This last claim concerns normalized paid factors, +not the original placement of free scalar operations. + +## 1. Credited reductions + +Move all scalar basis changes to the right, conjugating each projector. +Augmentation `[g]->1` sends each paid factor and the target to `I`, so the +remaining scalar factor is `I`. Rank-one idempotence is preserved. This is +the normalization used by Gareth Davidson's PR1333 and the later CNOT work. + +The sign quotient `G=S3 -> C2`, over +`F2[C2]=F2[epsilon]/(epsilon^2)`, sends each `a,b,s` to `1+epsilon`. +The normalized formal identity therefore gives + +`sum_all N_i=P`, and hence `n_a+n_b = t (mod 2)`. + +The matrix-sum identity is stronger than its trace consequence and is needed +below. This is the sign argument of PR1414, reused with credit. + +Order coordinates by the two address components in the natural +representation. Chronological **left** multiplication gives + +`a: [[I,N],[0,I]]`, `b: [[I,0],[N,I]]`, + +and the target is `[[I+P,P],[P,I+P]]`. Only an `a` call changes the top block +row, with image in its vector `u`; only a `b` call changes the bottom block +row. The two final off-diagonal blocks `P` imply + +`im P <= span(u_a)` and `im P <= span(u_b)`. + +Thus each label occurs at least `t` times. This is the image-span step of +PR1541. A formal identity implies the represented identity; the converse is +not assumed. + +## 2. Exactly t a calls make the top block row rigid + +Suppose `n_a=t`. The `t` vectors `u_a` are a basis of `im P`. Conjugate by a +scalar basis change on `im P`, extended by the identity on `ker P`, so that +the image vectors, in occurrence order, are `e_1,...,e_t`. This conjugation +commutes with `P` and does not change the target or either count. + +Write the running natural matrix as `[[A,B],[C,D]]`. Each active top row +is changed by exactly one call; all other top rows are unchanged. Top row +`i` is initially `[e_i^T,0]` and finally `[0,e_i^T]`. Before its unique call +it equals its initial row, and after that call it equals its final row. +Both have the same row sum. Consequently + +`A+B=I` at **every** chronological cut. + +A `b` call with projector `N_j` changes `C+D` by +`N_j(A+B)=N_j`. Initially and finally `C+D=I`, so + +`sum_b N_j=0`. + +Combine this with the full sign identity to obtain `sum_a N_i=P`. But +`N_i=e_i v_i^T`, so comparison of its distinct rows gives `v_i=e_i`. +Every `a` projector is therefore precisely `E_ii` in this basis. + +At the unique `a` call on row `i`, the needed top-row change is +`[e_i^T,e_i^T]`. Since its covector is `e_i`, bottom row `i` at that instant +is exactly this row. Its two block halves sum to zero. On the other hand, + +`C+D=I+sum_(b before a_i) N_j`. + +Taking row `i` gives + +`e_i^T = sum_(b before a_i) e_i^T N_j`. + +Each summand is a scalar multiple of `v_j^T`. Thus **every active coordinate +covector belongs to the span of the b covectors**. This chronological step, +together with the zero sum, is the additional ingredient. + +## 3. A zero rank-one sum must pay for both spans + +Let `m=n_b`, let `U` be the `r by m` matrix with columns `u_j`, and let `V` +be the `m by r` matrix with rows `v_j^T`, over the `b` calls. We have + +`UV=sum_b N_j=0`, `rank U>=t`, and `rank V>=t`. + +Since `im V` is contained in `ker U`, rank-nullity gives + +`m >= rank U + rank V >= 2t`. + +This proves saturation. Exchanging the two address coordinates exchanges +`a` and `b` while fixing `s`, giving the symmetric statement. + +If `m=2t`, both ranks are exactly `t`. Their column and row spans contain, +respectively, the active coordinate space and its covector space, so those +spans equal the active spaces. Each `b` image and covector has no dirty +component. The `a` projectors are already `E_ii`. Undoing the scalar change +that commutes with `P` gives `PN=N=NP` for every normalized paid factor. + +The proof uses no upper bound on `r` or `t`, no finite search, and no +assumption that different projectors commute. + +## 4. Consequences and the unresolved case + +* **Three swaps cost nine with arbitrary finite dirty workspace.** A word + below nine has odd length and at least three of each label, so only seven + remains, with counts `(3,4)` or `(4,3)`. Saturation rules both out. Three + direct `bab` words attain nine in the full formal algebra. This is an + analytic alternative proof of PR1541's theorem; that predecessor retains + priority for the arbitrary-workspace result and its checked SAT proof. +* **Four swaps need at least ten.** Below twelve, parity and the label floor + leave totals eight or ten. Saturation excludes `(4,4)`, `(4,6)` and + `(6,4)`. Only `(5,5)` at total ten remains. The direct twelve-call word + attains the upper bound. This covers arbitrary finite dirty workspace and + strengthens the `r=4`, `{8,10,12}` boundary reported in PR1705. It does + **not** prove the four-swap minimum is twelve or supply a ten-call word. + +For completeness, PR1541's compression step reduces that remaining ten-call +case to at most six roles: put `L=span(u_a)+span(u_b)`. Both spans contain +`im P`, so `dim L<=n_a+n_b-t=6`. Every paid projector preserves `L`, and its +restriction remains rank-one idempotent because its image vector lies in +`L` and its covector evaluates to one on that vector. Restrict the full +formal identity to `L` and choose a basis of `im P` plus `L intersect ker P`. +This gives four active swaps and at most two dirty roles, with the same ten +paid calls. Compression is credited to PR1541, not claimed as new here. + +More generally, every potential saving below `3t` must have both counts at +least `t+1`, as well as the retained sign parity. The theorem only screens +this fixed two-label formal model; it does not exclude other alphabets. + +## Credit and limits + +Credit commdata2338 (PR1414/1491), Gareth Davidson (PR1333), Cinna Davis +(PR1541), and Aaron Wang (PR1705), with exact heads in TASK.json. Eumemic +(PR288), Ali Romman (PR468), and David Govea (PR720) supply surrounding +rational/register-model lineage. This proof does not import the rational +three-register obstruction into the nonabelian model. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. The written proof has not been checked by a proof assistant or +independently reviewed by a human. Physical compiler/common-label realization, +hosting, precision/tape, full selected cold replay and analytic transfer +remain outside this contribution. No new kappa. diff --git a/research/four-swap-full-occupancy/test_package.py b/research/four-swap-full-occupancy/test_package.py new file mode 100644 index 0000000000..4a917e5ed7 --- /dev/null +++ b/research/four-swap-full-occupancy/test_package.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +"""Failure-sensitive checks for the mathematical scope and replay boundary.""" +import hashlib +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +def module(name, filename): + spec = importlib.util.spec_from_file_location(name, HERE / filename) + value = importlib.util.module_from_spec(spec) + spec.loader.exec_module(value) + return value + + +primary = module('primary_full_occupancy', 'verify.py') +oracle = module('regular_full_occupancy', 'independent.py') + + +class PackageTests(unittest.TestCase): + def copied(self, directory): + out = Path(directory) / 'renamed-package' + shutil.copytree(HERE, out, ignore=shutil.ignore_patterns('__pycache__')) + return out + + def run_check(self, package, script): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(package / script)], + cwd=package.parent, capture_output=True, text=True, + timeout=30, env={**os.environ, 'PYTHONOPTIMIZE':'2'}) + + def test_scope_and_chronology(self): + direct = [[g, 1 << i, 1 << i] for i in range(4) for g in 'aba'] + self.assertEqual(primary.replay(direct,4), primary.target(4,4)) + self.assertEqual(oracle.replay(direct,4), oracle.target(4,4)) + ordinary_rotation = direct[1:] + direct[:1] + self.assertNotEqual(primary.replay(ordinary_rotation,4), primary.target(4,4)) + self.assertNotEqual(oracle.replay(ordinary_rotation,4), oracle.target(4,4)) + self.assertEqual(primary.replay(primary.rotate(direct,1),4), primary.target(4,4)) + # Partial-target conjugation is outside the alphabet, not just a different N. + r,t,call = 5,4,['a',17,1] + transformed = oracle.bm(oracle.bm(oracle.target(r,t),oracle.operator(call,r)),oracle.target(r,t)) + self.assertTrue(all(transformed != oracle.operator([g,u,v],r) + for u,v in oracle.scalar_projectors(r) for g in 'ab')) + + def test_domains_and_natural_alias(self): + for word in ([['a',True,1]],[['b',1.0,1]],[['s',1,1]],[['a',3,3]],[['a',0,1]]): + with self.assertRaises((primary.Invalid, TypeError, ValueError)): + primary.replay(word,2) + with self.assertRaises((oracle.Failure, TypeError, ValueError)): + oracle.replay(word,2) + # Sum of all six group elements is invisible naturally but not regularly. + natural = [0]*4 + regular = [0]*6 + for g in oracle.GROUP: + natural = [x ^ y for x,y in zip(natural,g)] + regular = [x ^ y for x,y in zip(regular,oracle.regular(g))] + self.assertEqual(natural,[0]*4) + self.assertNotEqual(regular,[0]*6) + self.assertEqual(regular,[63]*6) + + def test_corrupt_receipts_rejected_by_both(self): + changes = [ + lambda d: d['claim'].__setitem__('minimum',10), + lambda d: d['claim'].__setitem__('extra_dirty_roles',True), + lambda d: d.__setitem__('cut_checks',288.0), + lambda d: d['fixtures'][12]['word'][0].__setitem__(1,3), + lambda d: d['label_screen']['rows'][-1].__setitem__('after_cuts',-1), + lambda d: d['workspace_boundary'].__setitem__('alphabet_size',991), + lambda d: d.__setitem__('fixtures',[]), + ] + original = json.loads((HERE/'RESULT.json').read_text()) + with tempfile.TemporaryDirectory() as temp: + package = self.copied(temp) + for change in changes: + data = json.loads(json.dumps(original)) + change(data) + (package/'RESULT.json').write_text(json.dumps(data)) + for script in ('verify.py','independent.py'): + with self.subTest(change=changes.index(change), script=script): + self.assertNotEqual(self.run_check(package,script).returncode,0) + + def test_source_and_json_fail_closed(self): + with tempfile.TemporaryDirectory() as temp: + package = self.copied(temp) + source = package/'inputs/PR1722-PROOF.md' + old = source.read_bytes() + source.write_bytes(old+b'\nchanged\n') + for script in ('verify.py','independent.py'): + self.assertNotEqual(self.run_check(package,script).returncode,0) + source.unlink() + for script in ('verify.py','independent.py'): + self.assertNotEqual(self.run_check(package,script).returncode,0) + source.write_bytes(old) + result = package/'RESULT.json' + for text in ('{"claim": {}, "claim": {}}', '{"claim": NaN}'): + result.write_text(text) + for script in ('verify.py','independent.py'): + self.assertNotEqual(self.run_check(package,script).returncode,0) + result.unlink() + self.assertNotEqual(self.run_check(package,'verify.py').returncode,0) + self.assertFalse(result.exists()) + + def test_read_only_relocation_and_determinism(self): + with tempfile.TemporaryDirectory() as temp: + package = self.copied(temp) + paths = [p for p in package.rglob('*') if p.is_file()] + before = {p.relative_to(package).as_posix():hashlib.sha256(p.read_bytes()).hexdigest() for p in paths} + for p in paths: + p.chmod(0o444) + dirs = [p for p in package.rglob('*') if p.is_dir()]+[package] + for p in dirs: + p.chmod(0o555) + try: + for script in ('verify.py','independent.py'): + completed = self.run_check(package,script) + self.assertEqual(completed.returncode,0,completed.stderr) + after = {p.relative_to(package).as_posix():hashlib.sha256(p.read_bytes()).hexdigest() for p in package.rglob('*') if p.is_file()} + self.assertEqual(before,after) + finally: + for p in dirs: + p.chmod(0o755) + for p in paths: + p.chmod(0o644) + self.assertEqual(primary.canonical(primary.compute()), primary.canonical(primary.read_json(HERE/'RESULT.json'))) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/four-swap-full-occupancy/verify.py b/research/four-swap-full-occupancy/verify.py new file mode 100644 index 0000000000..986d53e9b1 --- /dev/null +++ b/research/four-swap-full-occupancy/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written full-occupancy theorem. +Apache-2.0. Ross Richardson with substantial OpenAI Codex assistance. +""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +class Invalid(ValueError): + pass + + +def need(ok, message): + if not ok: + raise Invalid(message) + + +def read_json(path): + def unique(items): + out = {} + for k, v in items: + need(k not in out, 'duplicate JSON key') + out[k] = v + return out + def invalid(x): + raise Invalid('nonfinite JSON') + return json.loads(Path(path).read_text(), object_pairs_hook=unique, parse_constant=invalid) + + +def canonical(x): + return json.dumps(x, sort_keys=True, separators=(',', ':'), ensure_ascii=True) + + +def digest(x): + return hashlib.sha256(canonical(x).encode()).hexdigest() + + +def mat2(a, b): + return sum((((a >> (2*i)) & 1)*((b >> j) & 1) ^ + ((a >> (2*i+1)) & 1)*((b >> (2+j)) & 1)) << (2*i+j) + for i in range(2) for j in range(2)) + + +G = tuple(x for x in range(16) if (((x & 1)*((x >> 3) & 1)) ^ (((x >> 1) & 1)*((x >> 2) & 1)))) +INDEX = {x: i for i, x in enumerate(G)} +E, A, B, S = 9, 11, 13, 6 +ONE = 1 << INDEX[E] + + +def rmul(a, b): + out = 0 + for i, x in enumerate(G): + if (a >> i) & 1: + for j, y in enumerate(G): + if (b >> j) & 1: + out ^= 1 << INDEX[mat2(x, y)] + return out + + +RMUL = tuple(tuple(rmul(a, b) for b in range(64)) for a in range(64)) + + +def mul(x, y): + r = len(x) + out = [[0] * r for _ in range(r)] + for i in range(r): + for k in range(r): + if x[i][k]: + table = RMUL[x[i][k]] + for j in range(r): + out[i][j] ^= table[y[k][j]] + return out + + +def target(r, t): + return [[((1 << INDEX[S]) if i < t else ONE) if i == j else 0 for j in range(r)] for i in range(r)] + + +def projectors(r): + return [(u, v) for u in range(1, 1 << r) for v in range(1, 1 << r) + if (u & v).bit_count() % 2] + + +def validate(word, r): + need(type(r) is int and 1 <= r <= 6, 'roles') + need(type(word) is list, 'word type') + for call in word: + need(type(call) is list and len(call) == 3, 'call shape') + g, u, v = call + need(type(g) is str and g in ('a', 'b'), 'paid label') + need(type(u) is int and type(v) is int and 0 < u < 1 << r and 0 < v < 1 << r, 'vector domain') + need((u & v).bit_count() % 2 == 1, 'idempotence') + + +def factor(call, r): + validate([call], r) + g, u, v = call + coeff = ONE ^ (1 << INDEX[A if g == 'a' else B]) + return [[(ONE if i == j else 0) ^ (coeff if ((u >> i) & (v >> j) & 1) else 0) + for j in range(r)] for i in range(r)] + + +def replay(word, r): + validate(word, r) + value = target(r, 0) + for call in word: + value = mul(factor(call, r), value) + return value + + +def rotate(word, k): + need(type(k) is int and 0 <= k <= len(word), 'cut') + return [x[:] for x in word[k:]] + [['b' if g == 'a' else 'a', u, v] for g, u, v in word[:k]] + + +def binary_inverse(rows): + n = len(rows) + a = [rows[i] | (1 << (n+i)) for i in range(n)] + for col in range(n): + pivot = next((i for i in range(col, n) if (a[i] >> col) & 1), None) + need(pivot is not None, 'singular basis') + a[col], a[pivot] = a[pivot], a[col] + for i in range(n): + if i != col and (a[i] >> col) & 1: + a[i] ^= a[col] + return [row >> n for row in a] + + +def conjugate(word, rows): + inverse = binary_inverse(rows) + out = [] + for g, u, v in word: + new_u = sum(((row & u).bit_count() % 2) << i for i, row in enumerate(rows)) + new_v = 0 + for i, row in enumerate(inverse): + if (v >> i) & 1: + new_v ^= row + out.append([g, new_u, new_v]) + return out + + +def fixtures(): + result = [] + for r in range(1, 7): + direct = [[g, 1 << i, 1 << i] for i in range(r) for g in 'aba'] + mixed = [[g, 1 << i, 1 << i] for i in reversed(range(r)) for g in ('aba' if i % 2 else 'bab')] + rows = [(1 << i) | (1 << (i+1) if i+1 < r else 0) for i in range(r)] + basis = conjugate(mixed, rows) + pair = ['a', (1 << r)-1, 1] + coupled = [pair[:], pair[:]] + basis + result.extend({'roles': r, 'word': w} for w in (direct, mixed, basis, coupled)) + return result + + +def label_screen(): + rows = [] + checked = 0 + for t in range(1, 7): + for q in range(min(3*t, 17)): + if (q-t) % 2: + continue + floor = saturated = survivors = 0 + for bits in range(1 << q): + checked += 1 + a = bits.bit_count() + b = q-a + if min(a, b) < t: + continue + floor += 1 + if min(a, b) == t: + continue + saturated += 1 + walk = 0 + low, high = t+1-b, a-t-1 + good = low <= 0 <= high + for k in range(q): + walk += 1 if (bits >> k) & 1 else -1 + good &= low <= walk <= high + if good: + survivors += 1 + need(q >= 2*t+3, 'cut width bound') + if q == 2*t+3: + need(all(((bits >> k) ^ (bits >> (k+1))) & 1 for k in range(q-1)), 'alternating boundary') + rows.append({'targets': t, 'calls': q, 'floor': floor, + 'after_saturation': saturated, 'after_cuts': survivors}) + need(next(x['after_cuts'] for x in rows if x['targets'] == 4 and x['calls'] == 10) == 0, 'four-target residual') + need(next(x['after_cuts'] for x in rows if x['targets'] == 5 and x['calls'] == 13) == 2, 'five-target boundary') + return {'patterns': checked, 'rows': rows} + + +def source_check(): + pins = read_json(HERE / 'PINS.json') + for record in pins['files']: + path = HERE / record['local_path'] + need(path.is_file(), 'missing source input') + need(hashlib.sha256(path.read_bytes()).hexdigest() == record['sha256'], 'source bytes changed') + return pins + + +def reject(action, label): + try: + action() + except (Invalid, ValueError, TypeError): + return label + raise Invalid('control accepted: '+label) + + +def compute(): + source_check() + conjugations = [] + for r in range(1, 7): + ts = target(r, r) + count = 0 + values = [] + for u, v in projectors(r): + for g in ('a', 'b'): + f = factor([g, u, v], r) + value = mul(mul(ts, f), ts) + need(value == factor(['b' if g == 'a' else 'a', u, v], r), 'full conjugation') + need(mul(f, f) == target(r, 0), 'paid involution') + values.append(value) + count += 1 + conjugations.append({'roles': r, 'projectors': len(projectors(r)), 'checks': count, 'sha256': digest(values)}) + words = fixtures() + cuts = omitted = 0 + rotations = [] + for fixture in words: + r, word = fixture['roles'], fixture['word'] + need(replay(word, r) == target(r, r), 'positive word') + for k in range(len(word)+1): + rotated = rotate(word, k) + need(replay(rotated, r) == target(r, r), 'chronological rotation') + rotations.append(rotated) + cuts += 1 + for k in range(len(word)): + need(replay(word[:k]+word[k+1:], r) != target(r, r), 'omission accepted') + omitted += 1 + # One active/dirty-coupled projector, embedded at the actual four-target boundary. + r, t = 5, 4 + boundary = target(r, t) + coupled = ['a', 17, 1] + conjugated = mul(mul(boundary, factor(coupled, r)), boundary) + alphabet = [factor([g, u, v], r) for u, v in projectors(r) for g in ('a', 'b')] + need(conjugated not in alphabet, 'partial-target conjugation escaped control') + need(conjugated != factor(['b', 17, 1], r), 'false workspace flip') + controls = [] + for word, label in [([['s',1,1]],'expanded-label'),([['a',3,3]],'nilpotent'), + ([['a',True,1]],'boolean-vector'),([['a',1.0,1]],'float-vector')]: + controls.append(reject(lambda word=word: validate(word, 2), label)) + actual = [[g,1<