diff --git a/research/d8-rotation-pair-seedff568/CERTIFICATE.json b/research/d8-rotation-pair-seedff568/CERTIFICATE.json new file mode 100644 index 0000000000..f5029733c4 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/CERTIFICATE.json @@ -0,0 +1,55 @@ +{ + "status": "PASS_D8_ROTATION_PAIR_EXACT_MINIMUM", + "group_presentation": "D8=", + "target": "diag([st],[ts])", + "registers": 2, + "paid_labels": [ + "s", + "t" + ], + "rank_one_idempotents_per_label": 6, + "direct_upper_bound": 4, + "exact_minimum": 4, + "excluded_lengths": [ + { + "length": 0, + "factor_words_checked": 1, + "expected": 1, + "complete": true + }, + { + "length": 1, + "factor_words_checked": 12, + "expected": 12, + "complete": true + }, + { + "length": 2, + "factor_words_checked": 144, + "expected": 144, + "complete": true + }, + { + "length": 3, + "factor_words_checked": 1728, + "expected": 1728, + "complete": true + } + ], + "factorizations_at_or_below_3": [], + "direct_word": [ + "s:u01v01", + "t:u01v01", + "t:u10v10", + "s:u10v10" + ], + "regular_representation_ranks": { + "reflection_difference": 4, + "rotation_difference": 6, + "inverse_rotation_difference": 6, + "target_difference": 12, + "calls_required_by_rank_floor": 3 + }, + "free_GL2_normalization": "All interspersed free scalar matrices conjugate paid rank-one idempotents; augmentation of target and paid factors is I.", + "scope_limit": "Exactly two roles, this reflection alphabet, and this endpoint; no kappa or supplier claim." +} diff --git a/research/d8-rotation-pair-seedff568/CLAIM.md b/research/d8-rotation-pair-seedff568/CLAIM.md new file mode 100644 index 0000000000..67248c96ee --- /dev/null +++ b/research/d8-rotation-pair-seedff568/CLAIM.md @@ -0,0 +1,5 @@ +CLAIM — `bit-mechanisms` / `bit-new-register-model`; accepted OS seed `ff568c3e5cf8605fe719bcb7533b22f8`; priority revision 3, catalogue SHA-256 `6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075`. Exact base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. + +**Refined question:** In `F2[D8]`, with `D8=` and `r=st`, can `diag([r],[r^-1])` on exactly two arbitrary dirty scalar roles be factored in three paid calls `I+([g]+1)N`, `g in {s,t}`, `N` any rank-one idempotent over `F2`, allowing free `GL2(F2)` changes? The direct bill is four calls. Search every word of length 0–3 over the 12 factors with exact full-group-algebra multiplication. A regular-representation rank relaxation leaves three calls feasible: target rank 12, each call rank at most 4. + +The object is the noncentral rotation/inverse pair. Direct predecessor PR #1443 (merged, head `965ff75aabb16cdd0978f4bf9222bcdedf514021`) uses the same `F2[D8]` two-role reflection alphabet but targets the central pair `diag([r^2],[r^2])`; this work changes the target class and runs an exhaustive 0–3 word search rather than radius-four balls. Related work: open PR #1822 (Q8 central pairs); Discussion #1738 was released and linked PR #1792; Discussion #1759 concluded in PR #1761 (UT4); Discussion #1818 concluded in PR #1821 (D16); PRs #1705/#1716 and Discussion #1167. Full task refresh at 13:08 UTC covered 537 open PRs and 521 Discussions with full pagination. Refresh again before handoff. This alphabet is not the selected supplier and the complex side binds, so no selected moment or `kappa` change is claimed. Expected result: a three-call exact identity and controls, or a complete bounded negative result through length three. Expiry: 2026-10-14 14:52 UTC. Substantial OpenAI Codex assistance; predecessor attribution above. diff --git a/research/d8-rotation-pair-seedff568/CYCLE.md b/research/d8-rotation-pair-seedff568/CYCLE.md new file mode 100644 index 0000000000..f09637bcd5 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/CYCLE.md @@ -0,0 +1,27 @@ +# Cycle 12 scope and pivot record + +- Accepted OS seed: `ff568c3e5cf8605fe719bcb7533b22f8`. +- Track: `bit-mechanisms`. +- Priority revision: 3. +- Exact base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. +- Selected record SHA-256: `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. + +## First screen, released + +The first refined scope was the two-role S4 target `diag([w],[w^-1])` for a +4-cycle and adjacent-transposition alphabet. The natural permutation +representation immediately gave target rank six and rank-one effect per paid +call, forcing six calls and matching its direct bill. Exact meet-in-the-middle +also returned no word in lengths zero through five. No package or PR was +proposed. The scope was released at [Discussion #1166 comment 18924236](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18924236). + +## One evidence-driven pivot + +The second scope was claimed in [Discussion #1166 comment 18924259](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18924259), then clarified against merged PR #1443 in comment 18924309. It uses the D8 noncentral order-four pair `diag([r],[r^-1])` on +two dirty roles. Here the regular representation only forces three calls, +while the direct bill is four, so a genuine saving remained possible. Exact +search exhausted lengths zero through three and found no saving. The package +records this scoped negative result and its direct four-call control. + +The pivot followed the prescribed stop screen: the first scope had no +headroom, so it was released before packaging; no further pivot was made. diff --git a/research/d8-rotation-pair-seedff568/DETAILS.json b/research/d8-rotation-pair-seedff568/DETAILS.json new file mode 100644 index 0000000000..ab39e50645 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/DETAILS.json @@ -0,0 +1,12 @@ +{ + "title": "Exact four-call minimum for a noncentral D8 rotation/inverse pair", + "scope": "Formal F2[D8], two arbitrary dirty scalar roles, paid reflections s,t, free GL2(F2) mixing, target diag([st],[ts]).", + "scope_status": "refined", + "reason": "Target-class extension of merged PR #1443 central endpoint diag([r^2],[r^2]); this package proves the noncentral order-four inverse-pair minimum.", + "bottleneck": "Check whether a nonabelian inverse pair can share one paid call below the direct four-call bill.", + "stop": "Exhaust 12^n factor words for n=0..3; stop on complete coverage.", + "checks": "Generic exact group-algebra replay, direct four-call witness, three controls, and regular-representation rank screen.", + "result": "No word of length at most three; the direct four-call word is minimal in this exact model.", + "limits": "No larger register count, other alphabet, selected supplier substitution, physical invoice, or kappa conclusion.", + "credit": "PR #1443 and the prior free-scalar normalization are directly attributed; substantial OpenAI Codex assistance; no independent human review claimed." +} diff --git a/research/d8-rotation-pair-seedff568/OVERLAP.json b/research/d8-rotation-pair-seedff568/OVERLAP.json new file mode 100644 index 0000000000..fe24498447 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/OVERLAP.json @@ -0,0 +1,73 @@ +{ + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-14T13:08:54.048653+00:00", + "task_id": "bit-new-register-model", + "terms": [ + "bit-new-register-model", + "three-register", + "nonabelian", + "group algebra", + "bit-three-register-lower-bound" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T13:07:20.690768+00:00", + "complete_pagination": true, + "records": 537 + }, + "discussions": { + "fetched_at": "2026-10-14T13:08:53.892628+00:00", + "complete_pagination": true, + "records": 521 + } + }, + "local_records": 873, + "matches_total": 116, + "warnings": [], + "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.", + "exact_scope_assessment": "No active exact-scope D8 noncentral rotation/inverse pair claim found in the complete open PR and Discussion snapshots. The closest predecessor is merged PR #1443, manually inspected; it uses the same group, labels, role count, and free GL2 mixing but a different central endpoint.", + "related_records": [ + { + "kind": "merged-pr", + "number": 1443, + "head": "965ff75aabb16cdd0978f4bf9222bcdedf514021", + "scope": "F2[D8], two roles, reflections, free GL2; central target diag([r^2],[r^2]), exact minimum 8. Direct predecessor; changed endpoint here is diag([r],[r^-1])." + }, + { + "kind": "open-pr", + "number": 1822, + "head": "ee736b4b11bbd63b04d94c8edafb3790161ebdea", + "scope": "Q8 central commutator pairs; different group and endpoint." + }, + { + "kind": "discussion", + "number": 1738, + "status": "released / resolved via comment 18921339 and PR #1792", + "scope": "D8 central commutator with a third dirty role; different endpoint and width." + }, + { + "kind": "discussion", + "number": 1759, + "status": "completed in PR #1761", + "scope": "UT4(F2) noncentral root pair with three registers; different group and width." + }, + { + "kind": "discussion", + "number": 1818, + "status": "completed in PR #1821", + "scope": "D16 central pair; different group and endpoint." + }, + { + "kind": "open-pr", + "number": 1716, + "head": "fdbcd61eea435f9f8d497290a1db6513bb769d51", + "scope": "AGL2(F2) target triple; different alphabet and target." + }, + { + "kind": "discussion", + "number": 1167, + "scope": "S3 inverse pair; different group and address alphabet." + } + ], + "final_recheck": true +} diff --git a/research/d8-rotation-pair-seedff568/PR-BODY.md b/research/d8-rotation-pair-seedff568/PR-BODY.md new file mode 100644 index 0000000000..c17221112b --- /dev/null +++ b/research/d8-rotation-pair-seedff568/PR-BODY.md @@ -0,0 +1,21 @@ +## Result + +In the exact two-role formal `F2[D8]` model with paid reflection labels `s,t` only and arbitrary free `GL2(F2)` mixing, the noncentral rotation/inverse target `diag([r],[r^-1])`, `r=st`, has exact paid-call minimum **four**. The direct four-call word passes; exhaustive full-coefficient enumeration rules out every word of length zero through three. + +The regular representation gives only the lower bound three (target difference rank 12; each paid factor has rank 4). The exact word enumeration rules out that remaining three-call possibility. + +## Scope and relation to predecessors + +This is a target-class extension of merged [PR #1443](https://github.com/CrocSwap/integer-mult-bounds/pull/1443), which uses the same group, two reflection labels, two roles and free scalar mixing but proves an eight-call minimum for the central target `diag([r^2],[r^2])`. This PR concerns the noncentral order-four inverse pair and its four-call bill. It does not restate the central-target result. Other nearby work includes the open quaternion central-pair result in PR #1822 and the D8 third-role central-pair claim in Discussion #1738. + +## Reproduction + +```sh +python3 -I -B research/d8-rotation-pair-seedff568/search.py +python3 -I -B research/d8-rotation-pair-seedff568/verify.py +python3 scripts/research_package.py --package research/d8-rotation-pair-seedff568 --check-only +``` + +The search covers `1, 12, 144, 1728` words at lengths `0,1,2,3`. The independent verifier checks the direct word, complete group-algebra boundary, altered and truncated controls, and the rank screen. The registered package replay requests Python 3.12; direct checks in this environment use Python 3.14.7 because Python 3.12 is unavailable. + +This is a scoped abstract address-model result only. The selected supplier and selected moment are unchanged; there is no new `kappa` or physical/compiler admission. Substantial OpenAI Codex assistance; no independent human review is claimed. diff --git a/research/d8-rotation-pair-seedff568/PROOF.md b/research/d8-rotation-pair-seedff568/PROOF.md new file mode 100644 index 0000000000..1c88be65be --- /dev/null +++ b/research/d8-rotation-pair-seedff568/PROOF.md @@ -0,0 +1,54 @@ +# Exact finite argument + +Let `G=D8={r^i s^e : i in Z/4, e in F2}` with multiplication + +`(i,e)(j,f) = (i + (-1)^e j mod 4, e+f mod 2)`. + +Set `s=(0,1)` and `t=(3,1)`. Then `s^2=t^2=1`, `st=(1,0)=r`, and +`ts=(3,0)=r^-1`. + +## Paid factors and free scalar maps + +For a rank-one idempotent `N=u v^T` over `F2^2`, define +`F_g(N)=I+([g]+1)N`. The pairs `u,v` with `u!=0`, `v!=0`, and `v^T u=1` +are exactly the six rank-one idempotents. Therefore the complete paid alphabet +has 2*6=12 factors. + +Suppose free `GL2(F2)` matrices are interspersed with paid factors. Moving a +free matrix rightward across one paid factor conjugates its idempotent: +`M F_g(N) = F_g(M N M^-1) M`. Conjugation preserves the rank-one idempotent +class. After moving all free maps to the right, augmentation sends every paid +factor to `I` and sends the target `diag([r],[r^-1])` to `I`; hence the remaining +free product is `I`. The normalized twelve-factor word model is complete. + +## Exhaustive coefficient check + +Represent a group-algebra coefficient by an eight-bit mask, one bit for each +`r^i s^e`. Matrix multiplication uses the displayed multiplication rule and +XOR for coefficient addition. The search tests every length-n word in the +12-factor alphabet for n=0,1,2,3. The word counts are exactly + +`1, 12, 12^2=144, 12^3=1728`. + +The independent verifier recomputes every product by generic group-algebra +convolution and 2x2 matrix multiplication. It finds no target word through +length three. The four-factor word + +`F_s(E11) F_t(E11) F_t(E22) F_s(E22)` + +is checked coefficient-for-coefficient to equal `diag([r],[r^-1])`. Thus the +exact minimum in this finite model is four. + +## Rank relaxation + +In the left regular representation over `F2`, left multiplication by a +reflection has four 2-cycles, so `rank(L_s-I)=rank(L_t-I)=4`. Left +multiplication by `r` or `r^-1` has two 4-cycles, so each difference has rank +six. Since `rank(A tensor N)=rank(A)rank(N)`, a paid factor changes rank by +four. For invertible `A,B`, + +`rank(AB-I) = rank(A(B-I)+(A-I)) <= rank(B-I)+rank(A-I)`. + +The target difference has block-diagonal rank `6+6=12`, so at least three +calls are necessary. This relaxation leaves three calls feasible; the exact +coefficient enumeration proves that three do not suffice. diff --git a/research/d8-rotation-pair-seedff568/README.md b/research/d8-rotation-pair-seedff568/README.md new file mode 100644 index 0000000000..f5ddc68140 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/README.md @@ -0,0 +1,115 @@ +# A noncentral D8 rotation pair still costs four calls + +## Result + +For the exact two-role model over the formal group algebra `F2[D8]`, the target +`diag([r],[r^-1])`, where `r=st` has order four, needs exactly four paid calls +when the only paid labels are the reflections `s,t`. Free scalar `GL2(F2)` +changes do not reduce the minimum. The direct four-call word attains the bound; +complete exact enumeration rules out every word of length zero through three. + +This is a scoped target result, not a change to the selected bit supplier or a +new multiplication-exponent bound. The selected complex-side moment remains the +binding one, so no new `kappa` follows. + +## Model and complete price + +Write the eight elements as `r^i s^e`, with `i mod 4`, `e in {0,1}`, and +`s r = r^-1 s`. Set `t=r^-1 s`; then `s^2=t^2=1`, `st=r`, and `ts=r^-1`. +The paid alphabet is exactly + +```text +F_g(N) = I + ([g] + 1) N, g in {s,t}, +``` + +over `F2[D8]`. Here `N=u v^T` is a rank-one idempotent on the two scalar +roles, so `u,v` are nonzero binary two-vectors and `v^T u=1`. There are six +such projectors, hence twelve paid factors. Both role inputs are arbitrary; +the exact formal matrix boundary therefore includes restoration of all +cross-role information. No extra role, address map, copy, clean state, or +unpriced operation is available. + +The direct word is + +```text +F_s(E11) F_t(E11) F_t(E22) F_s(E22) + = diag([s][t], [t][s]) + = diag([r], [r^-1]). +``` + +Its complete paid bill is four calls. Every paid call is charged once. + +## Exact minimum + +Any interspersed free scalar matrices can be pushed to the right through the +paid factors by conjugating each projector: `M F_g(N) M^-1 = F_g(M N M^-1)`. +The conjugated matrix is still one of the six rank-one idempotents. Under the +augmentation `F2[D8] -> F2`, each paid factor maps to the identity and the +boundary also maps to the identity. Thus the total remaining free scalar map +must be `I`. The twelve-factor alphabet already covers every allowed sequence +with arbitrary free `GL2(F2)` changes. + +The exact verifier multiplies full 2x2 matrices of eight-bit group-algebra +coefficients. It enumerates all words at each length `n=0,1,2,3`, checking +`1, 12, 144, 1728` words respectively. No product equals the target. A second +implementation in `verify.py` uses generic group-algebra and matrix +multiplication, rather than the rank-one update used by the search. It repeats +the full enumeration, confirms the direct four-call word, and checks altered +and truncated words as negative controls. + +A separate rank screen shows why three calls were plausible. In the left +regular representation on eight group elements, each reflection difference +`L_g-I` has rank four, while `L_r-I` and `L_(r^-1)-I` each have rank six. The +target difference has rank twelve; one paid factor changes rank by at most +four. Subadditivity therefore forces at least three calls, but does not rule +out three. The exact coefficient search supplies that missing call: the +minimum is four. + +## Relation to prior work + +Merged [PR #1443](https://github.com/CrocSwap/integer-mult-bounds/pull/1443) +uses this same `F2[D8]` group, the same two reflection labels, exactly two +roles, and free `GL2(F2)` mixing. Identifying its `x,y` with `s,t` gives +`r=xy`, so its endpoint `diag([xyxy],[xyxy])` is the central target +`diag([r^2],[r^2])`. It proves an eight-call minimum for that different endpoint. This result changes the endpoint +to the noncentral order-four inverse pair and tests the shorter, four-call +bill. It does not re-run or alter PR #1443's central-target result. The related +open [PR #1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822) +uses a quaternion central-pair target; [Discussion #1738](https://github.com/CrocSwap/integer-mult-bounds/discussions/1738) +concerns a D8 central pair with a third dirty role. Scope and exact overlap +coverage are recorded in `OVERLAP.json`. + +The normalization of free scalar mixing follows the prior D8 and three-register +work. The exact group law, word domain, target and rank calculation here are +specified in this package. Substantial OpenAI Codex assistance; no independent +human review is claimed. + +## Reproduce + +```sh +python3 -I -B research/d8-rotation-pair-seedff568/search.py +python3 -I -B research/d8-rotation-pair-seedff568/verify.py +python3 scripts/research_package.py --package research/d8-rotation-pair-seedff568 --check-only +``` + +The search prints the exact length census and the direct four-call witness. The +independent verifier prints: + +```text +PASS_D8_ROTATION_PAIR minimum=4 lengths=[1,12,144,1728] regular_ranks=(4,6,6) positive_controls=2 negative_controls=2 no_new_kappa +``` + +The registered package replay requests Python 3.12. Direct verification in this +session was run with the installed Python 3.14.7; the full registered replay +could not be run because Python 3.12 is unavailable here. + +## Open next questions + +The result covers exactly two scalar roles, this reflection alphabet, and this +one target. It establishes no physical/compiler cost, selected supplier +admission, recursive profile change, or `kappa` improvement. It does not cover +three or more dirty roles or other group alphabets. + +A natural next construction question is whether a third arbitrary dirty scalar +role can realize `diag([r],[r^-1],1)` in three reflection calls. The regular +rank screen still permits three, while the two-role exact search rules it out. diff --git a/research/d8-rotation-pair-seedff568/RESULT.json b/research/d8-rotation-pair-seedff568/RESULT.json new file mode 100644 index 0000000000..570120ee65 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/RESULT.json @@ -0,0 +1,69 @@ +{ + "status": "PASS_D8_ROTATION_PAIR_SEARCH", + "group": "D8 = ", + "elements": [ + "r^0s^0", + "r^0s^1", + "r^1s^0", + "r^1s^1", + "r^2s^0", + "r^2s^1", + "r^3s^0", + "r^3s^1" + ], + "paid_factors": 12, + "factor_alphabet": [ + "s:u01v01", + "s:u01v11", + "s:u10v10", + "s:u10v11", + "s:u11v01", + "s:u11v10", + "t:u01v01", + "t:u01v11", + "t:u10v10", + "t:u10v11", + "t:u11v01", + "t:u11v10" + ], + "rank_one_idempotents": 6, + "target": "diag([r],[r^-1]) where r=st", + "direct_four_call": { + "status": "PASS", + "word": [ + "s:u01v01", + "t:u01v01", + "t:u10v10", + "s:u10v10" + ] + }, + "length_census": [ + { + "length": 0, + "factor_words_checked": 1, + "expected": 1, + "complete": true + }, + { + "length": 1, + "factor_words_checked": 12, + "expected": 12, + "complete": true + }, + { + "length": 2, + "factor_words_checked": 144, + "expected": 144, + "complete": true + }, + { + "length": 3, + "factor_words_checked": 1728, + "expected": 1728, + "complete": true + } + ], + "factorizations_at_or_below_3": [], + "claim_scope": "exactly r=2, F2[D8], labels {s,t}, target diag([st],[ts])", + "stopping_rule": "complete enumeration of all 12^n paid-factor words for n=0,1,2,3" +} diff --git a/research/d8-rotation-pair-seedff568/SOURCES.json b/research/d8-rotation-pair-seedff568/SOURCES.json new file mode 100644 index 0000000000..f9b72f411d --- /dev/null +++ b/research/d8-rotation-pair-seedff568/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/bit-dihedral-commutator/README.md", + "usage": "provenance", + "git_blob": "b7619a5d56f32daf7f48d6cc3a0e260c5a333510", + "sha256": "4f3f9df6d6d96a26ccb0fcd2ef947cce5d53b0d992da22e866f1e025be4c0492" + }, + { + "path": "research/bit-dihedral-commutator/verify.py", + "usage": "provenance", + "git_blob": "30c04afbc7f457f381143f57fc87a479dc9a36fa", + "sha256": "dff2985bc4ec27d0e527d017471f6e6d43bb7855e555385fc80027aad499735d" + } + ] +} diff --git a/research/d8-rotation-pair-seedff568/TASK.json b/research/d8-rotation-pair-seedff568/TASK.json new file mode 100644 index 0000000000..f40f21b5ef --- /dev/null +++ b/research/d8-rotation-pair-seedff568/TASK.json @@ -0,0 +1,60 @@ +{ + "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[D8] on exactly two arbitrary dirty scalar roles; paid labels s,t only, where s^2=t^2=1 and r=st has order four; arbitrary free GL2(F2) scalar mixing; target diag([r],[r^-1]); exact paid-call minimum four.", + "scope_change_reason": "Refine the catalogue nonabelian-model card to the noncentral order-four rotation/inverse endpoint. Merged PR #1443 has the same F2[D8] reflection alphabet and two-role interface but studies the different central endpoint diag([r^2],[r^2]); this package determines the exact cost for diag([r],[r^-1]) using complete short-word enumeration and a target-specific regular-representation rank screen.", + "bottleneck_link": "Tests whether two noncommuting inverse rotations can share a paid bit mechanism below their direct four-call bill. This is a local abstract primitive result only; the selected bit supplier is unchanged and the complex-side moment binds.", + "budget_minutes": 60, + "stop_rule": "Exhaust every word of length 0,1,2,3 in the 12-factor normalized alphabet. Stop at this finite boundary; no larger role count, other alphabet, selected-supplier substitution, or kappa claim is included.", + "outcome": "negative-result", + "evidence": "RESULT.json, PROOF.md, search.py, and independently implemented exact replay in verify.py.", + "author": "1337isnot1337", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review is claimed.", + "open_questions": [ + { + "question": "Can one extra arbitrary dirty scalar role reduce the same noncentral rotation/inverse target below four paid reflection calls?", + "why_it_matters": "This separates the two-role obstruction from a possible workspace-assisted sharing mechanism.", + "first_step": "Enumerate rank-one idempotents in GL3(F2), prove the regular-representation rank floor, then screen all exact three-call words for diag([r],[r^-1],1).", + "blocked_by": "The larger role alphabet increases the finite search, and this address model has no current selected-supplier or kappa admission." + } + ] +} diff --git a/research/d8-rotation-pair-seedff568/TASK.md b/research/d8-rotation-pair-seedff568/TASK.md new file mode 100644 index 0000000000..95c1d02f8e --- /dev/null +++ b/research/d8-rotation-pair-seedff568/TASK.md @@ -0,0 +1,19 @@ +# Cycle 12 research task (pivoted scope) + +- **Track / task / seed:** `bit-mechanisms` / `bit-new-register-model` / `ff568c3e5cf8605fe719bcb7533b22f8`. +- **Catalogue:** priority revision 3; SHA-256 `6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075`; scope key `7f5f4426ef796683c485` refined to `F2[D8]/r2/diag([r],[r^-1])/{s,t}/cost<=3`. +- **Exact base:** `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. +- **Selected record:** `certificates/selected-result.json`, SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +- **Pivot record:** The initially claimed `S4` 4-cycle/inverse pair has no saving headroom: rank in the natural permutation representation forces six calls, matching direct cost. Its complete 0–5 MITM returned no shorter identity; scope released at [Discussion #1166 comment 18924236](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18924236). + +## Current scope + +- **Object / question:** Let `D8=`, with `r=st` of order four. Over `F2[D8]`, can the exact boundary `diag([r],[r^-1])` on exactly two arbitrary dirty scalar roles be implemented with three paid calls `I+([g]+1)N`, where `g in {s,t}` and `N=uv^T` is any rank-one idempotent over `F2`? +- **Changed assumption:** The construction uses a specified nonabelian reflection alphabet and a noncentral order-four rotation/inverse pair on two roles. This is a target-class refinement of merged PR #1443, which uses the same F2[D8] group, two roles, reflection generators, and free GL2 mixing but targets the central involution pair diag([r^2],[r^2]); this scope instead targets the noncentral order-four pair diag([r],[r^-1]). It also differs from the Q8 central-pair PR #1822 and from the prior D8 third-role claim in Discussion #1738, which was subsequently released. +- **Alphabet and counted roles:** Exactly two scalar roles; 12 paid factors (2 labels times the 6 rank-one idempotents of `F2^2`); arbitrary free `GL2(F2)` changes may be normalized into the idempotent choices. Exact formal group-algebra equality is required, so the boundary holds for all input group-algebra coordinates. +- **Method / bounded domain:** Exact search over all paid words of length 0–3 in `F2[D8]` (at most `12^3=1,728` length-three words), with explicit multiplication table for the eight group elements. Check the full 2x2 matrix of eight-bit coefficients, not finite input columns. +- **Optimistic, fully charged cost:** The direct construction costs four calls (`st` on role 1, then `ts` on role 2). A 3-call factorization would save one call (25%) with all paid calls counted and no extra roles, copies, restoration, or input assumptions. The regular representation gives rank 4 for each reflection's `L_g-I` and rank 6 for each rotation's `L_r-I`; the target difference has rank 12 while each paid call changes rank by at most 4. Thus the best possible lower bound is three calls, leaving the proposed construction feasible and not screened out. This alphabet is not the selected bit supplier; the complex side binds, so no selected-moment or `kappa` gain is claimed. +- **Nearest predecessor:** merged PR #1443 (head `965ff75aabb16cdd0978f4bf9222bcdedf514021`) has the same `F2[D8]` group, exactly two roles, reflection alphabet, and free `GL2(F2)` normalization, but targets `diag([r^2],[r^2])`; its exact minimum is eight. This scope changes the target to noncentral `diag([r],[r^-1])`, with direct cost four. Other nearby work: open PR #1822 studies central pairs over `Q8`; the older D8 third-role claim in Discussion #1738 was released in comment #18921339 and linked to PR #1792; the UT4 root-pair claim in Discussion #1759 concluded in PR #1761; the D16 central-pair claim in Discussion #1818 concluded in PR #1821; PR #1705 studies four coordinate swaps at four roles; PR #1716 studies an `AGL2(F2)` triple; Discussion #1167 studies an `S3` inverse pair. The 12:52 exact-phrase overlap query had 0 matches, which did not surface merged #1443; manual predecessor inspection confirms that package is the direct model predecessor. Full task overlap was refreshed at 13:08 UTC; refresh again immediately before handoff/submission. +- **Expected result / stop rule:** An exact three-call identity plus controls, or a complete scoped negative result for lengths 0–3, together with the four-call upper bound. Stop after the finite word domain is exhausted; make no claim beyond this model. +- **Expiry:** 2026-10-14 14:52 UTC. +- **Credit:** Substantial OpenAI Codex assistance; predecessor attribution as listed above. diff --git a/research/d8-rotation-pair-seedff568/VALIDATION.json b/research/d8-rotation-pair-seedff568/VALIDATION.json new file mode 100644 index 0000000000..b2bc975a7f --- /dev/null +++ b/research/d8-rotation-pair-seedff568/VALIDATION.json @@ -0,0 +1,49 @@ +{ + "commands": [ + { + "command": [ + "python3", + "-I", + "-B", + "research/d8-rotation-pair-seedff568/search.py" + ], + "stdout": "PASS_D8_ROTATION_PAIR_SEARCH; direct four-call witness; complete word counts 1,12,144,1728; no length <=3 factorization", + "returncode": 0 + }, + { + "command": [ + "python3", + "-I", + "-B", + "research/d8-rotation-pair-seedff568/verify.py" + ], + "stdout": "PASS_D8_ROTATION_PAIR minimum=4 lengths=[1,12,144,1728] regular_ranks=(4,6,6) positive_controls=2 negative_controls=2 no_new_kappa", + "returncode": 0 + }, + { + "command": [ + "python3", + "scripts/research_package.py", + "--package", + "research/d8-rotation-pair-seedff568", + "--check-only" + ], + "stdout": "PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)", + "returncode": 0 + }, + { + "command": [ + "git", + "diff", + "--cached", + "--check" + ], + "stdout": "", + "returncode": 0 + } + ], + "python_direct": "Python 3.14.7", + "registered_replay": "Not run: VERIFY.json requests Python 3.12, which is unavailable in this environment.", + "selected_supplier": "Not replayed or altered; no selected-supplier or kappa claim.", + "notes": "The package checks validate metadata and source pins. Exact mathematical evidence is in RESULT.json and the independently implemented verify.py." +} diff --git a/research/d8-rotation-pair-seedff568/VERIFY.json b/research/d8-rotation-pair-seedff568/VERIFY.json new file mode 100644 index 0000000000..c0667e802c --- /dev/null +++ b/research/d8-rotation-pair-seedff568/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/agent-task-catalog.json", + "certificates/selected-result.json", + "research/bit-dihedral-commutator/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/search.py" + ], + "timeout_seconds": 60, + "checks": "Complete direct search over all 12^n factor words for n=0..3 and exact four-call upper-bound check; writes RESULT.json." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Independent generic F2[D8] convolution and 2x2 matrix multiplication over all lengths 0..3; positive and malformed-word controls; regular representation rank screen." + } + ] +} diff --git a/research/d8-rotation-pair-seedff568/search.py b/research/d8-rotation-pair-seedff568/search.py new file mode 100644 index 0000000000..a147af3598 --- /dev/null +++ b/research/d8-rotation-pair-seedff568/search.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python3 +"""Exact exhaustive search for the two-role D8 rotation/inverse target.""" +from __future__ import annotations + +import itertools +import json +from pathlib import Path + +# D8 elements are r^i s^e, i in Z/4, e in {0,1}; s r = r^-1 s. +ELEMENTS = tuple((i, e) for i in range(4) for e in range(2)) +INDEX = {x: i for i, x in enumerate(ELEMENTS)} +IDENTITY = INDEX[(0, 0)] + +def multiply(x: tuple[int, int], y: tuple[int, int]) -> tuple[int, int]: + i, e = x + j, f = y + return ((i + (-j if e else j)) % 4, e ^ f) + +S = INDEX[(0, 1)] +T = INDEX[(3, 1)] # t=s r = r^-1 s, so s*t=r. +R = INDEX[(1, 0)] +RINV = INDEX[(3, 0)] +assert multiply(ELEMENTS[S], ELEMENTS[S]) == (0, 0) +assert multiply(ELEMENTS[T], ELEMENTS[T]) == (0, 0) +assert multiply(ELEMENTS[S], ELEMENTS[T]) == ELEMENTS[R] +assert multiply(ELEMENTS[T], ELEMENTS[S]) == ELEMENTS[RINV] +RIGHT = [[INDEX[multiply(x, ELEMENTS[g])] for x in ELEMENTS] for g in (S, T)] +def translate(mask: int, table: list[int]) -> int: + out = 0 + while mask: + bit = mask & -mask + idx = bit.bit_length() - 1 + out ^= 1 << table[idx] + mask ^= bit + return out + +def right_x(mask: int, gi: int) -> int: + return mask ^ translate(mask, RIGHT[gi]) + +# Row-major 2x2 matrices over F2[D8], each coefficient stored as an 8-bit mask. +IMAT = (1 << IDENTITY, 0, 0, 1 << IDENTITY) +VECTORS = (1, 2, 3) +IDEMPOTENTS = tuple( + (u, v) for u in VECTORS for v in VECTORS + if ((u & v).bit_count() & 1) == 1 +) +assert len(IDEMPOTENTS) == 6 +FACTORS = tuple( + (gi, u, v) + for gi in range(2) for u, v in IDEMPOTENTS +) +assert len(FACTORS) == 12 + +def right_factor(mat: tuple[int, ...], gi: int, u: int, v: int) -> tuple[int, ...]: + """mat * (I + (1+[g]) u v^T), in characteristic two.""" + out = list(mat) + for i in range(2): + z = (mat[2 * i] if (u & 1) else 0) ^ (mat[2 * i + 1] if (u & 2) else 0) + zx = right_x(z, gi) + if v & 1: + out[2 * i] ^= zx + if v & 2: + out[2 * i + 1] ^= zx + return tuple(out) + +TARGET = (1 << R, 0, 0, 1 << RINV) + +def label(fi: int) -> str: + gi, u, v = FACTORS[fi] + return f"{'s' if gi == 0 else 't'}:u{u:02b}v{v:02b}" + +def direct_four_call_check() -> tuple[bool, list[int]]: + seq = [] + for gi in (0, 1): + seq.append(FACTORS.index((gi, 1, 1))) + for gi in (1, 0): + seq.append(FACTORS.index((gi, 2, 2))) + mat = IMAT + for fi in seq: + mat = right_factor(mat, *FACTORS[fi]) + return mat == TARGET, seq + +def exhaustive_search(max_length: int = 3): + counts = [] + found = [] + for n in range(max_length + 1): + checked = 0 + for word in itertools.product(range(len(FACTORS)), repeat=n): + checked += 1 + mat = IMAT + for fi in word: + mat = right_factor(mat, *FACTORS[fi]) + if mat == TARGET: + found.append({"length": n, "factor_indices": list(word), + "word": [label(fi) for fi in word]}) + counts.append({"length": n, "factor_words_checked": checked, + "expected": len(FACTORS) ** n, "complete": checked == len(FACTORS) ** n}) + return counts, found + +def main() -> None: + direct_ok, direct_word = direct_four_call_check() + if not direct_ok: + raise SystemExit("direct four-call construction failed") + counts, found = exhaustive_search(3) + result = { + "status": "PASS_D8_ROTATION_PAIR_SEARCH", + "group": "D8 = ", + "elements": [f"r^{i}s^{e}" for i, e in ELEMENTS], + "paid_factors": len(FACTORS), + "factor_alphabet": [label(i) for i in range(len(FACTORS))], + "rank_one_idempotents": len(IDEMPOTENTS), + "target": "diag([r],[r^-1]) where r=st", + "direct_four_call": {"status": "PASS", "word": [label(fi) for fi in direct_word]}, + "length_census": counts, + "factorizations_at_or_below_3": found, + "claim_scope": "exactly r=2, F2[D8], labels {s,t}, target diag([st],[ts])", + "stopping_rule": "complete enumeration of all 12^n paid-factor words for n=0,1,2,3", + } + Path(__file__).with_name("RESULT.json").write_text(json.dumps(result, indent=2) + "\n") + print(json.dumps(result, indent=2)) + +if __name__ == "__main__": + main() diff --git a/research/d8-rotation-pair-seedff568/verify.py b/research/d8-rotation-pair-seedff568/verify.py new file mode 100644 index 0000000000..d022baddfe --- /dev/null +++ b/research/d8-rotation-pair-seedff568/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +"""Independent exact replay using generic F2[D8] and matrix multiplication.""" +from __future__ import annotations + +import itertools +import json +from pathlib import Path + +ELEMENTS = tuple((i, e) for i in range(4) for e in range(2)) +INDEX = {x: i for i, x in enumerate(ELEMENTS)} +IDENTITY_PAIR = (0, 0) +ID = INDEX[IDENTITY_PAIR] + +def product_group(x: tuple[int, int], y: tuple[int, int]) -> tuple[int, int]: + i, e = x + j, f = y + return ((i + (j if e == 0 else -j)) % 4, e ^ f) + +GTABLE = [[INDEX[product_group(x, y)] for y in ELEMENTS] for x in ELEMENTS] +S = INDEX[(0, 1)] +T = INDEX[(3, 1)] +R = INDEX[(1, 0)] +RI = INDEX[(3, 0)] +assert len(ELEMENTS) == 8 +assert all(GTABLE[ID][i] == i and GTABLE[i][ID] == i for i in range(8)) +assert all(any(GTABLE[i][j] == ID and GTABLE[j][i] == ID for j in range(8)) for i in range(8)) +assert GTABLE[S][S] == ID and GTABLE[T][T] == ID +assert GTABLE[S][T] == R and GTABLE[T][S] == RI +assert GTABLE[R][R] == INDEX[(2, 0)] and GTABLE[R][INDEX[(2, 0)]] == RI +assert all(GTABLE[GTABLE[i][j]][k] == GTABLE[i][GTABLE[j][k]] + for i in range(8) for j in range(8) for k in range(8)) + +# A formal group-algebra element is an eight-bit vector of F2 coefficients. +def ring_product(a: int, b: int) -> int: + out = 0 + for i in range(8): + if (a >> i) & 1: + for j in range(8): + if (b >> j) & 1: + out ^= 1 << GTABLE[i][j] + return out + +# A 2x2 matrix is a row-major tuple of four such eight-bit vectors. +I = (1 << ID, 0, 0, 1 << ID) +def matrix_product(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + out = [] + for i in range(2): + for j in range(2): + z = 0 + for k in range(2): + z ^= ring_product(a[2 * i + k], b[2 * k + j]) + out.append(z) + return tuple(out) + +VECTORS = (1, 2, 3) +IDEMPOTENTS = tuple((u, v) for u in VECTORS for v in VECTORS + if ((u & v).bit_count() & 1) == 1) +assert len(IDEMPOTENTS) == 6 +LABELS = (S, T) +FACTORS = [] +for label_index, g in enumerate(LABELS): + for u, v in IDEMPOTENTS: + delta = (1 << ID) | (1 << g) + n = tuple(((u >> i) & 1) * ((v >> j) & 1) + for i in range(2) for j in range(2)) + f = tuple(((1 << ID) if i == j else 0) ^ (delta if n[2 * i + j] else 0) + for i in range(2) for j in range(2)) + FACTORS.append((label_index, u, v, f)) +assert len(FACTORS) == 12 +for _, _, _, f in FACTORS: + assert matrix_product(f, f) == I + augmentation = tuple(mask.bit_count() & 1 for mask in f) + assert augmentation == (1, 0, 0, 1) + +def word_product(word: tuple[int, ...]) -> tuple[int, ...]: + out = I + for fi in word: + out = matrix_product(out, FACTORS[fi][3]) + return out + +# Select the coordinate projections without relying on factor-list positions. +def factor_index(label_index: int, u: int, v: int) -> int: + for i, (li, ui, vi, _) in enumerate(FACTORS): + if (li, ui, vi) == (label_index, u, v): + return i + raise AssertionError((label_index, u, v)) + +TARGET = (1 << R, 0, 0, 1 << RI) +DIRECT = (factor_index(0, 1, 1), factor_index(1, 1, 1), + factor_index(1, 2, 2), factor_index(0, 2, 2)) +assert word_product(DIRECT) == TARGET + +# Positive control: two different reflections on two separate roles. +CONTROL = (1 << S, 0, 0, 1 << T) +assert word_product((factor_index(0, 1, 1), factor_index(1, 2, 2))) == CONTROL + +# Meaningful negative controls: one omitted paid operation and one altered label +# must fail the complete formal boundary, not only a selected group coordinate. +assert word_product(DIRECT[:-1]) != TARGET +mutated = (DIRECT[0], factor_index(0, 1, 1), DIRECT[2], DIRECT[3]) +assert word_product(mutated) != TARGET + +# Binary rank of a matrix encoded by row bitmasks. +def rank_f2(rows: list[int]) -> int: + rows = rows[:] + rank = 0 + width = max((r.bit_length() for r in rows), default=0) + for col in range(width): + pivot = next((i for i in range(rank, len(rows)) if (rows[i] >> col) & 1), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for i in range(len(rows)): + if i != rank and ((rows[i] >> col) & 1): + rows[i] ^= rows[rank] + rank += 1 + return rank + +def regular_difference(g: int) -> list[int]: + # Conventional rows of L_g + I, with basis vectors indexed by D8 elements. + rows = [] + for out_index in range(8): + row = 0 + for in_index in range(8): + if (out_index == in_index) ^ (out_index == GTABLE[g][in_index]): + row |= 1 << in_index + rows.append(row) + return rows + +def projection_rows(u: int, v: int) -> list[int]: + return [sum((((u >> i) & 1) * ((v >> j) & 1)) << j for j in range(2)) + for i in range(2)] + +def tensor_rows(a_rows: list[int], b_rows: list[int]) -> list[int]: + out = [] + for ai in range(len(a_rows)): + for bi in range(len(b_rows)): + row = 0 + for aj in range(len(a_rows)): + if (a_rows[ai] >> aj) & 1: + for bj in range(len(b_rows)): + if (b_rows[bi] >> bj) & 1: + row |= 1 << (2 * aj + bj) + out.append(row) + return out + +def target_difference_rows() -> list[int]: + rows = [] + for out_group in range(8): + for out_role in range(2): + row = 0 + for in_group in range(8): + for in_role in range(2): + if out_role == in_role: + g = R if out_role == 0 else RI + if (out_group == in_group) ^ (out_group == GTABLE[g][in_group]): + row |= 1 << (2 * in_group + in_role) + rows.append(row) + return rows + +reflection_rank = rank_f2(regular_difference(S)) +rotation_rank = rank_f2(regular_difference(R)) +rotation_inverse_rank = rank_f2(regular_difference(RI)) +assert (reflection_rank, rotation_rank, rotation_inverse_rank) == (4, 6, 6) +for g in LABELS: + for u, v in IDEMPOTENTS: + assert rank_f2(tensor_rows(regular_difference(g), projection_rows(u, v))) == 4 +assert rank_f2(target_difference_rows()) == 12 + +# Independent exhaustive full-coefficient replay for every word of lengths 0..3. +length_counts = [] +hits = [] +for n in range(4): + checked = 0 + for word in itertools.product(range(12), repeat=n): + checked += 1 + if word_product(word) == TARGET: + hits.append({"length": n, "factor_indices": list(word)}) + expected = 12 ** n + assert checked == expected + length_counts.append({"length": n, "factor_words_checked": checked, + "expected": expected, "complete": True}) +assert hits == [] + +result_path = Path(__file__).with_name("RESULT.json") +recorded = json.loads(result_path.read_text()) +assert recorded["status"] == "PASS_D8_ROTATION_PAIR_SEARCH" +assert recorded["length_census"] == length_counts +assert recorded["factorizations_at_or_below_3"] == hits +assert recorded["direct_four_call"]["status"] == "PASS" + +print("PASS_D8_ROTATION_PAIR minimum=4 lengths=[1,12,144,1728] " + "regular_ranks=(4,6,6) positive_controls=2 negative_controls=2 no_new_kappa")