From 862c3a844c55c134c43ba874a10c3c3e0b036e00 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 15:30:45 -0500 Subject: [PATCH] Research: bound D8 inverse pair with third role --- .../CERTIFICATE.json | 45 ++++ .../OVERLAP.json | 36 +++ .../PR-BODY.md | 35 +++ .../README.md | 117 ++++++++++ .../RESULT.json | 35 +++ .../SOURCES.json | 43 ++++ .../TASK.json | 84 +++++++ .../TASK.md | 23 ++ .../VERIFY.json | 19 ++ .../search.py | 148 ++++++++++++ .../verify.py | 217 ++++++++++++++++++ 11 files changed, 802 insertions(+) create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/CERTIFICATE.json create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/OVERLAP.json create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/PR-BODY.md create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/README.md create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/RESULT.json create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/SOURCES.json create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/TASK.json create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/TASK.md create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/VERIFY.json create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/search.py create mode 100644 research/d8-inverse-pair-third-role-seeddf1e67/verify.py diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/CERTIFICATE.json b/research/d8-inverse-pair-third-role-seeddf1e67/CERTIFICATE.json new file mode 100644 index 0000000000..00f8b1a252 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/CERTIFICATE.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "certificate_type": "complete finite exact word census plus displacement-rank lower bound", + "field": "F2", + "group_indexing": "index i+4e denotes r^i*s^e, i in Z/4 and e in Z/2", + "group_law": "(i,e)(j,f)=(i+(-1)^e*j mod 4,e+f mod 2)", + "elements": { + "identity": 0, + "r": 1, + "r_inverse": 3, + "s": 4, + "t=r_inverse*s": 7 + }, + "generator_family": { + "factor": "F_g(N)=I+([g]+1)N", + "labels": [4, 7], + "rank_one_idempotents": 28, + "paid_generators": 56 + }, + "endpoint": [ + {"role": 0, "group_element": 1}, + {"role": 1, "group_element": 3}, + {"role": 2, "group_element": 0} + ], + "lower_bound": { + "left_regular_dimension": 8, + "full_role_space_dimension": 24, + "rank_each_factor_minus_identity": 4, + "rank_endpoint_minus_identity": 12, + "excluded_lengths": [0, 1, 2] + }, + "finite_search": { + "word_length": 3, + "ordered_words": 175616, + "hits": 0, + "complete": true + }, + "direct_word": [ + {"label": "s", "projector": "E11"}, + {"label": "t", "projector": "E11"}, + {"label": "t", "projector": "E22"}, + {"label": "s", "projector": "E22"} + ], + "exact_conclusion_in_named_model": "minimum paid word length four" +} diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/OVERLAP.json b/research/d8-inverse-pair-third-role-seeddf1e67/OVERLAP.json new file mode 100644 index 0000000000..e8caf78944 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/OVERLAP.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "checked_at_utc": "2026-10-14T20:29:48Z", + "coverage": { + "open_prs": 391, + "discussions": 802, + "complete_pagination": true, + "warnings": [] + }, + "exact_all_term_query": { + "terms": ["D8", "inverse rotation", "third role", "rank-one"], + "matches": 0 + }, + "predecessors_and_neighbors": [ + { + "item": "PR #1881", + "commit": "5a51deaaab2746d42eddb454bbb968bda3af02cc", + "scope": "two roles, D8 reflection labels, noncentral diag([r],[r^-1]), exact minimum four", + "relation": "same group and endpoint, one fewer dirty role" + }, + { + "item": "Discussion #1738 / PR #1742", + "commit": "679f3624a0a41ed14942825dd7f413132412d1e3", + "scope": "three roles, D8/UT3 central endpoint diag([z],[z],[1]), exact minimum eight", + "relation": "same group and role count, different central endpoint and paid labels" + }, + { + "item": "PR #1443", + "scope": "two roles, D8 central endpoint diag([r^2],[r^2])", + "relation": "different role count and endpoint" + } + ], + "active_exact_scope_claim_found": false, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1738#discussioncomment-18933540", + "hub_pointer_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18933546" +} diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/PR-BODY.md b/research/d8-inverse-pair-third-role-seeddf1e67/PR-BODY.md new file mode 100644 index 0000000000..f04d6c127f --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/PR-BODY.md @@ -0,0 +1,35 @@ +## Result + +This package settles one exact three-role formal group-algebra question. For +`D8=`, `t=r^-1s`, and paid rank-one factors +`F_g(N)=I+([g]+1)N` with `g in {s,t}`, the endpoint +`diag([r],[r^-1],1)` has minimum paid length four on three arbitrary dirty +roles, even with interspersed free `GL3(F2)` scalar maps. It does not give a +supplier or `kappa` improvement. + +## Evidence + +- The regular-representation displacement rank is 12 for the endpoint and 4 + per paid factor, so lengths zero through two are impossible. +- The complete exact length-three census checks all 175,616 ordered words over + the 56 generators and finds zero hits. +- The explicit four-call word reaches the endpoint. A separate tuple-valued + verifier replays the whole census, positive control, omitted-call control, + and rank control. + +## Reproduction + +```sh +python3 -I -B research/d8-inverse-pair-third-role-seeddf1e67/search.py +python3 -I -B research/d8-inverse-pair-third-role-seeddf1e67/verify.py +python3 scripts/research_package.py --package research/d8-inverse-pair-third-role-seeddf1e67 --check-only +``` + +The scientific base is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +Predecessors are the two-role inverse-pair result (#1881, commit +`5a51deaaab2746d42eddb454bbb968bda3af02cc`) and the distinct three-role +central-pair result (#1742). The model excludes native third-role hosting, +recursive charges and supplier admission; no selected frontier changes. + +Substantial OpenAI Codex assistance in derivation, implementation, verification, +and packaging. No independent human review is claimed. diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/README.md b/research/d8-inverse-pair-third-role-seeddf1e67/README.md new file mode 100644 index 0000000000..93ba64e018 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/README.md @@ -0,0 +1,117 @@ +# A third dirty role does not reduce the D8 inverse-pair bill + +## Result + +In the formal group algebra `F2[D8]`, the three-role endpoint + +```text +diag([r], [r^-1], 1) +``` + +has exact paid-call minimum four when the paid labels are the two reflections +`s,t` and arbitrary free scalar `GL3(F2)` maps are allowed between calls. +The direct four-call word remains optimal after adding a third arbitrary dirty +role. An exact rank bound excludes lengths zero through two; a complete census +of the 56^3 ordered three-call words finds no endpoint hit. + +This is a scoped finite-algebra result. It does not improve the selected bit +supplier, price physical hosting of the third role, or change `kappa`. + +## Model and complete paid bill + +Index `D8=` by `r^i s^e`, with `i mod 4` and +`e in {0,1}`. Define `t=r^-1s`; then `s,t` are involutions and `st=r`, +`ts=r^-1`. Work in the full group algebra `F2[D8]`, not a finite address +quotient. A paid factor on three scalar roles is + +```text +F_g(N) = I + ([g] + 1)N, g in {s,t}, +``` + +where `N=u v^T` is any rank-one idempotent over `F2`, so +`u,v in F2^3 \ {0}` and `v^T u=1`. There are 28 such projectors and hence +56 distinct paid generators. All three input roles are arbitrary. The exact +diagonal endpoint restores the third role, and every paid factor is charged +once. No additional role, COPY, discarded output, or address operation is +available. Arbitrary interspersed scalar `GL3(F2)` maps are included: push them +to the right by conjugating each projector, then apply augmentation +`[g] -> 1`; because the target augments to `I`, the residual scalar output map +must be `I`. + +The direct word is + +```text +F_s(E11) F_t(E11) F_t(E22) F_s(E22) + = diag([s][t], [t][s], 1) + = diag([r], [r^-1], 1). +``` + +Its complete formal bill is four calls. A three-call word would save one +factor (25%) in this block, so the best-case budget justified searching exactly +three calls. + +## Lower bound for the first three lengths + +Use the left regular representation of `F2[D8]`; each role becomes an +eight-dimensional block, for a total dimension of 24. Write `L_g` for left +multiplication by `g`. Since each reflection is an involution, `L_s+I` and +`L_t+I` have rank four: each is a product of four disjoint transpositions over +`F2`. Thus the difference from identity of one paid factor is + +```text +(L_g + I) tensor N +``` + +and has rank four. Multiplication by `r` or `r^-1` consists of two cycles of +length four on `D8`, so each of `L_r+I` and `L_(r^-1)+I` has rank six. The +endpoint difference is block diagonal with ranks `6,6,0`, hence rank 12. +For any matrices `A,B`, `rank(AB-I) <= rank(A-I)+rank(B-I)`. Therefore at +least three paid factors are necessary. + +This makes length three the only unresolved length below the direct word. The +packed search checks every ordered triple from the 56 gates using exact +eight-coefficient group-algebra multiplication. A separate verifier repeats +the entire census with tuple-valued coefficients and direct group-law +convolution. Both report zero hits among 175,616 triples. Together with the +rank lower bound and direct word, this proves minimum four in the stated model. + +## Reproduction + +```sh +python3 -I -B research/d8-inverse-pair-third-role-seeddf1e67/search.py +# D8 inverse-pair W3 exact search: generators=56 triples=175616 matches=0 direct_calls=4 + +python3 -I -B research/d8-inverse-pair-third-role-seeddf1e67/verify.py +# PASS_D8_INVERSE_PAIR_W3 rank_floor=12/4 generators=56 triples=175616 matches=0 minimum=4 direct_control=pass omission_control=pass altered_rank_control=pass + +python3 scripts/research_package.py --package research/d8-inverse-pair-third-role-seeddf1e67 --check-only +``` + +The registered replay requests Python 3.12. Local direct runs used CPython +3.14.7; the registered 3.12 replay is not claimed unless available in the +submission environment. + +## Relation to prior work and limits + +- PR #1881 (`5a51deaaab2746d42eddb454bbb968bda3af02cc`) establishes the + two-role `diag([r],[r^-1])` minimum of four. This result adds a third + arbitrary restored role and keeps the same noncentral endpoint. +- Discussion #1738 / PR #1742 establish an eight-call minimum for the + three-role central endpoint `diag([z],[z],[1])` with `z=r^2`. The target, + paid labels and word-length question here differ. +- PR #1443 concerns a two-role central endpoint `diag([r^2],[r^2])`. + +The exact minimum concerns only the finite named formal alphabet. It does not +include native implementation/hosting of the third role or its recursive +charges, so it is not a bit-supplier construction or a new `kappa`. The task +record pins the selected frontier, current task catalogue and predecessors. +Prepared with substantial OpenAI Codex assistance; no independent human +review is claimed. + +## Open next questions + +Can a fourth arbitrary dirty role lower the four-call minimum for the same +inverse-pair endpoint and reflection alphabet? The dimension-five projector +count grows sharply; first apply the regular-representation rank floor and +estimate the complete length-three search. Any formal saving would still need +an added-role hosting and recursive-cost invoice. diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/RESULT.json b/research/d8-inverse-pair-third-role-seeddf1e67/RESULT.json new file mode 100644 index 0000000000..bff3ecb39b --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/RESULT.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "exact scoped negative result", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "seed": "df1e67db401c155561180b9d7f1a77f8", + "model": { + "field": "F2", + "group": "D8 = ", + "paid_labels": ["s", "t=r^-1*s"], + "roles": 3, + "paid_factor": "I + ([g]+1)N", + "projector_domain": "all 28 rank-one idempotents N=u*v^T in M3(F2), v^T*u=1", + "endpoint": "diag([r],[r^-1],1)", + "free_scalar_maps": "arbitrary interspersed GL3(F2), pushed into the complete projector alphabet; augmentation forces residual output map I" + }, + "rank_certificate": { + "regular_rep_dimension": 24, + "target_displacement_rank": 12, + "each_paid_factor_displacement_rank": 4, + "lower_bound_paid_calls": 3 + }, + "length_three_census": { + "distinct_paid_generators": 56, + "ordered_words_checked": 175616, + "target_hits": 0, + "independent_full_coefficient_replay": "PASS" + }, + "positive_control": { + "word": ["F_s(E11)", "F_t(E11)", "F_t(E22)", "F_s(E22)"], + "product": "diag([s][t],[t][s],1)=diag([r],[r^-1],1)", + "paid_calls": 4, + "exact_replay": "PASS" + }, + "conclusion": "The exact minimum is four paid factors in this formal D8, reflection-only, three-role model. No improvement over the direct four-call word; no native supplier realization or kappa claim." +} diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/SOURCES.json b/research/d8-inverse-pair-third-role-seeddf1e67/SOURCES.json new file mode 100644 index 0000000000..12b90f83a8 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/SOURCES.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor_commit": "5a51deaaab2746d42eddb454bbb968bda3af02cc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/d8-rotation-pair-seedff568/README.md", + "usage": "provenance", + "git_blob": "f5ddc6814071d97d783583bf5660ae4892da46b0", + "sha256": "5205ef41de0f06234ca915ee0d52baa4d70c16ffa7a00597859d97cf4482b758" + }, + { + "path": "research/d8-rotation-pair-seedff568/verify.py", + "usage": "provenance", + "git_blob": "d022baddfe4c2d669016ec8fb4d790c9941908c5", + "sha256": "baba451a88bc25a608b8f050626f38978526337087026c0e81e30d2b0e7872b5" + }, + { + "path": "research/d8-third-register-seed89de/README.md", + "usage": "provenance", + "git_blob": "554034517913dba181d96745ef78a111026f6d33", + "sha256": "cb25575c7fe61c2ad2f500f8dfbd2a24a4cd602ffdb21236285fce3358bffa98" + } + ] +} diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/TASK.json b/research/d8-inverse-pair-third-role-seeddf1e67/TASK.json new file mode 100644 index 0000000000..8aa266e700 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "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", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "For G=D8 and reflection labels {s,t}, determine whether the target diag([r],[r^-1],1), r=st of order four, can be realized on three arbitrary dirty scalar roles by at most three paid factors F_g(N)=I+([g]+1)N with all rank-one idempotents N in M3(F2).", + "scope_change_reason": "This fixes a nonabelian group-algebra operation family outside the abelian three-register model and narrows the question to one distinct noncentral inverse-pair endpoint. The neighboring three-role D8 result is for the central endpoint diag([z],[z],[1]); the two-role inverse-pair result has a different role count.", + "bottleneck_link": "A three-call word would save one of four paid rank-one calls in the formal block. The completed exact minimum is four, so this specific third-role mechanism does not reduce the direct paid bill. Physical hosting and recursive costs are outside the abstraction; no supplier admission or kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Use regular-representation displacement rank to exclude lengths zero through two. Enumerate every ordered length-three word over the 56-generator alphabet and stop after exact independent replay, direct length-four control, and endpoint/call negative controls.", + "outcome": "negative-result", + "evidence": "The exact full-coefficient census checks all 56^3=175616 length-three words and finds zero hits. The 24-dimensional regular representation gives target displacement rank 12 and each paid factor displacement rank 4, excluding lengths at most two. The explicit four-call word reaches the endpoint and is independently replayed; hence the minimum in the named formal model is exactly four.", + "author": "OpenAI Codex on behalf of Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical modeling, exact search, independent verification, packaging, and writing. No independent human review is claimed.", + "accepted_seed": "df1e67db401c155561180b9d7f1a77f8", + "track": "bit-mechanisms", + "scope_key": "D8-reflection-rank1-W3-inverse-rotation-length3", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "predecessor_commit": "5a51deaaab2746d42eddb454bbb968bda3af02cc", + "discussion_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1738#discussioncomment-18933540", + "pre_submission_overlap": { + "checked_at_utc": "2026-10-14T20:29:48Z", + "open_prs": 391, + "discussions": 802, + "complete_pagination": true, + "warnings": [], + "all_terms": [ + "D8", + "inverse rotation", + "third role", + "rank-one" + ], + "all_terms_exact_matches": 0 + }, + "open_questions": [ + { + "question": "Can adding a fourth arbitrary dirty role lower the four-call minimum for diag([r],[r^-1]) with the same D8 reflection alphabet?", + "why_it_matters": "This would test whether added restored storage, rather than the changed central/noncentral target alone, can enable sharing.", + "first_step": "Count all rank-one idempotents in M4(F2), apply the 24-dimensional address-rank floor on the 32-dimensional regular representation, and estimate the complete length-three search before implementation.", + "blocked_by": "No four-role result is established here; physical hosting and recursive charges would still need to be included for supplier adoption." + } + ] +} diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/TASK.md b/research/d8-inverse-pair-third-role-seeddf1e67/TASK.md new file mode 100644 index 0000000000..8f487e0ebd --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/TASK.md @@ -0,0 +1,23 @@ +Task ID / scope key: `bit-new-register-model` / `D8-reflection-rank1-W3-inverse-rotation-length3` +Track and accepted seed: `bit-mechanisms` / `df1e67db401c155561180b9d7f1a77f8` +Priority revision / catalogue SHA-256: 4 / `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7` +Exact research base / selected-record SHA-256: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` / `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32` +Scope status: refined. The catalogue question concerns escaping the abelian three-register obstruction. This fixes a nonabelian D8 group algebra, three arbitrary dirty roles, reflection labels `{s,t}`, and the exact noncentral endpoint `diag([r],[r^-1],1)` where `r=st` has order four. + +Question: can a fully restored three-role word of at most three paid factors reach this endpoint over the full formal algebra `F2[D8]`? + +Changed hypothesis/expense: use the nonabelian group-algebra operation alphabet and allow one arbitrary dirty role that must return exactly unchanged. Charge every rank-one factor once; allow no extra roles, COPY, discarded outputs, or unpriced address operations. Arbitrary free scalar `GL3(F2)` mixing is normalized into the complete idempotent alphabet, with the residual free map forced to identity by augmentation. + +Predecessors / nearest overlap: PR #1881, exact source commit `5a51deaaab2746d42eddb454bbb968bda3af02cc`, proves the two-role noncentral inverse-pair minimum is four; its README suggests testing a third dirty role. Discussion #1738 / PR #1742 cover a different D8 endpoint, the central pair `diag([z],[z],[1])`, and a seven-call search. The new endpoint has a four-call direct word and a three-call target. The refreshed overlap scan covered 388 open PRs and 796 Discussion records; exact-term cached intersection had no matches. + +Optimistic complete budget: one call is the entire new paid rank-one factor. The direct baseline is four calls, +`F_s(E11) F_t(E11) F_t(E22) F_s(E22) = diag([r],[r^-1],1)`. +The proposed three-call word would save one of four factors (25%) in this formal block. Physical hosting/recursive charges and native bit-supplier realization are outside the model and remain necessary for any supplier or kappa claim. + +Method/domain: over `D8=`, put `t=r^-1s`; enumerate all `56^3=175,616` ordered triples from the two labels and 28 rank-one idempotents in `M3(F2)`. First use the exact regular-representation rank floor (the target difference has rank 12 and each call difference rank 4), then compare the complete formal 3x3 group-algebra product with the target. Length 0--2 is excluded by rank; length 3 is fully enumerated. Stop after this exact domain and direct length-four replay. + +Success evidence: either one exact three-call word with all three arbitrary inputs restored, or zero matching words in the complete named domain and the resulting exact minimum-four statement. Require an independent full-coefficient replay, a direct four-call positive control, and endpoint / label / call-omission negative controls. + +Intended artifact and reproduction: package under this directory; `python3 -I -B research/d8-inverse-pair-third-role-seeddf1e67/verify.py` and `python3 scripts/research_package.py --package research/d8-inverse-pair-third-role-seeddf1e67 --check-only`. + +Claim location/expiry: Discussion #1738, 2026-10-14 22:20 UTC. Substantial OpenAI Codex assistance; no independent human review claimed. diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/VERIFY.json b/research/d8-inverse-pair-third-role-seeddf1e67/VERIFY.json new file mode 100644 index 0000000000..2c97b8b2d1 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/search.py"], + "timeout_seconds": 120, + "checks": "generators=56 triples=175616 matches=0 direct_calls=4" + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "PASS_D8_INVERSE_PAIR_W3 rank_floor=12/4 generators=56 triples=175616 matches=0 minimum=4" + } + ] +} diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/search.py b/research/d8-inverse-pair-third-role-seeddf1e67/search.py new file mode 100644 index 0000000000..48133ec3d0 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/search.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +"""Packed exact census for the three-call D8 inverse-pair target.""" + +from __future__ import annotations + +import itertools + +N = 3 +GROUP_ORDER = 8 +S = 4 # r^0 s +T = 7 # r^3 s = r^-1 s +R = 1 # r +R_INV = 3 # r^-1 +IDENTITY_GA = 1 # bit 0 represents the group identity + + +def group_product(a: int, b: int) -> int: + """D8 multiplication for indices i + 4e representing r^i s^e.""" + i, e = a & 3, a >> 2 + j, f = b & 3, b >> 2 + return ((i + (-j if e else j)) & 3) + (4 * (e ^ f)) + + +def make_ring_table() -> tuple[tuple[int, ...], ...]: + basis = tuple( + tuple(1 << group_product(i, j) for j in range(GROUP_ORDER)) + for i in range(GROUP_ORDER) + ) + table: list[tuple[int, ...]] = [] + for a in range(256): + row: list[int] = [] + for b in range(256): + out = 0 + aa = a + while aa: + bit_a = aa & -aa + i = bit_a.bit_length() - 1 + aa ^= bit_a + bb = b + while bb: + bit_b = bb & -bb + j = bit_b.bit_length() - 1 + bb ^= bit_b + out ^= basis[i][j] + row.append(out) + table.append(tuple(row)) + return tuple(table) + + +RING_MUL = make_ring_table() +IDENTITY = tuple(IDENTITY_GA if i == j else 0 for i in range(N) for j in range(N)) +TARGET = tuple( + (1 << R) if (i, j) == (0, 0) + else (1 << R_INV) if (i, j) == (1, 1) + else IDENTITY_GA if (i, j) == (2, 2) + else 0 + for i in range(N) for j in range(N) +) + + +def scalar_product(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + out = [0] * 9 + for i in range(N): + for j in range(N): + value = 0 + for k in range(N): + value ^= RING_MUL[a[3 * i + k]][b[3 * k + j]] + out[3 * i + j] = value + return tuple(out) + + +def rank_one_idempotents() -> tuple[tuple[int, ...], ...]: + result = [] + for u in range(1, 1 << N): + for v in range(1, 1 << N): + if (u & v).bit_count() % 2 != 1: + continue + result.append(tuple( + ((u >> i) & 1) & ((v >> j) & 1) + for i in range(N) for j in range(N) + )) + assert len(result) == 28 + return tuple(result) + + +def factor(g: int, projector: tuple[int, ...]) -> tuple[int, ...]: + delta = (1 << g) ^ IDENTITY_GA + return tuple( + (IDENTITY_GA if i == j else 0) ^ (delta if projector[3 * i + j] else 0) + for i in range(N) for j in range(N) + ) + + +def gates() -> tuple[tuple[str, tuple[int, ...]], ...]: + projectors = rank_one_idempotents() + return tuple( + (label, factor(group_element, projector)) + for label, group_element in (("s", S), ("t", T)) + for projector in projectors + ) + + +def direct_word() -> tuple[tuple[str, tuple[int, ...]], ...]: + e11 = (1, 0, 0, 0, 0, 0, 0, 0, 0) + e22 = (0, 0, 0, 0, 1, 0, 0, 0, 0) + return ( + ("s", factor(S, e11)), + ("t", factor(T, e11)), + ("t", factor(T, e22)), + ("s", factor(S, e22)), + ) + + +def census(target: tuple[int, ...], ops: tuple[tuple[str, tuple[int, ...]], ...]): + prefixes = [ + (a, b, scalar_product(a[1], b[1])) + for a, b in itertools.product(ops, repeat=2) + ] + matches = [] + checked = 0 + for a, b, prefix in prefixes: + for c in ops: + checked += 1 + if scalar_product(prefix, c[1]) == target: + matches.append((a[0], b[0], c[0])) + return checked, matches + + +def main() -> None: + ops = gates() + checked, matches = census(TARGET, ops) + direct = IDENTITY + for _, gate in direct_word(): + direct = scalar_product(direct, gate) + assert direct == TARGET + print( + "D8 inverse-pair W3 exact search: " + f"generators={len(ops)} triples={checked} matches={len(matches)} " + f"direct_calls={len(direct_word())}" + ) + if matches: + print("first match:", matches[0]) + else: + print("complete length-three census: no word reaches diag([r],[r^-1],1)") + + +if __name__ == "__main__": + main() diff --git a/research/d8-inverse-pair-third-role-seeddf1e67/verify.py b/research/d8-inverse-pair-third-role-seeddf1e67/verify.py new file mode 100644 index 0000000000..7568ccbdb0 --- /dev/null +++ b/research/d8-inverse-pair-third-role-seeddf1e67/verify.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Independent tuple-coefficient replay and exact rank certificate.""" + +from __future__ import annotations + +from functools import lru_cache +import itertools + +ORDER = 8 +ROLES = 3 +ZERO_GA = (0,) * ORDER +ONE_GA = (1,) + (0,) * (ORDER - 1) + + +def group_product(a: int, b: int) -> int: + i, e = a % 4, a // 4 + j, f = b % 4, b // 4 + return ((i + (4 - j if e else j)) % 4) + 4 * (e ^ f) + + +@lru_cache(maxsize=None) +def multiply_coefficients(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + out = [0] * ORDER + for i, x in enumerate(a): + if not x: + continue + for j, y in enumerate(b): + if x and y: + out[group_product(i, j)] ^= 1 + return tuple(out) + + +def add_coefficients(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple(x ^ y for x, y in zip(a, b)) + + +def matrix_identity(): + return tuple(ONE_GA if i == j else ZERO_GA for i in range(ROLES) for j in range(ROLES)) + + +def matrix_product(a, b): + out = [] + for i in range(ROLES): + for j in range(ROLES): + value = ZERO_GA + for k in range(ROLES): + value = add_coefficients(value, multiply_coefficients(a[3 * i + k], b[3 * k + j])) + out.append(value) + return tuple(out) + + +def idempotents(): + out = [] + for u in range(1, 8): + for v in range(1, 8): + if ((u & v).bit_count() & 1) == 0: + continue + out.append(tuple(((u >> i) & (v >> j) & 1) for i in range(3) for j in range(3))) + if len(out) != 28: + raise AssertionError(f"expected 28 idempotents, got {len(out)}") + return tuple(out) + + +def gate(label: int, n): + group_identity = 0 + diff = [0] * ORDER + diff[group_identity] = 1 + diff[label] ^= 1 + diff = tuple(diff) + matrix = [] + for i in range(3): + for j in range(3): + base = ONE_GA if i == j else ZERO_GA + matrix.append(add_coefficients(base, diff) if n[3 * i + j] else base) + return tuple(matrix) + + +def endpoint(r: int, rinv: int, third: int = 0): + result = [] + for i in range(3): + for j in range(3): + if i != j: + result.append(ZERO_GA) + elif i == 0: + result.append(tuple(int(k == r) for k in range(ORDER))) + elif i == 1: + result.append(tuple(int(k == rinv) for k in range(ORDER))) + else: + result.append(tuple(int(k == third) for k in range(ORDER))) + return tuple(result) + + +def rank_binary(rows: list[int], ncols: int) -> int: + rank = 0 + work = rows[:] + for col in range(ncols): + pivot = next((i for i in range(rank, len(work)) if (work[i] >> col) & 1), None) + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + for i in range(len(work)): + if i != rank and ((work[i] >> col) & 1): + work[i] ^= work[rank] + rank += 1 + return rank + + +def left_regular(g: int) -> list[int]: + rows = [0] * ORDER + for h in range(ORDER): + rows[group_product(g, h)] |= 1 << h + return rows + + +def add_binary(a: list[int], b: list[int]) -> list[int]: + return [x ^ y for x, y in zip(a, b)] + + +def target_difference_rank(r: int, rinv: int) -> int: + blocks = [] + for g in (r, rinv, 0): + block = left_regular(g) + if g == 0: + block = [0] * ORDER + else: + ident = [1 << i for i in range(ORDER)] + block = add_binary(block, ident) + blocks.append(block) + rows = [] + for role in range(3): + for i in range(ORDER): + row = 0 + for col_role in range(3): + if col_role == role: + row |= blocks[role][i] << (ORDER * col_role) + rows.append(row) + return rank_binary(rows, 3 * ORDER) + + +def gate_difference_rank(g: int, n) -> int: + # The represented 24x24 difference is (L_g + I_8) tensor N. + regular = add_binary(left_regular(g), [1 << i for i in range(ORDER)]) + rows = [] + for h in range(ORDER): + for i in range(3): + row = 0 + for k in range(ORDER): + if (regular[h] >> k) & 1: + for j in range(3): + if n[3 * i + j]: + row |= 1 << (3 * k + j) + rows.append(row) + return rank_binary(rows, ORDER * 3) + + +def main() -> None: + s, t, r, rinv = 4, 7, 1, 3 + ns = idempotents() + generators = tuple((g, gate(g, n)) for g in (s, t) for n in ns) + target = endpoint(r, rinv) + + # The elementary displacement-rank inequality excludes lengths 0, 1, 2. + trank = target_difference_rank(r, rinv) + gate_ranks = {gate_difference_rank(g, n) for g, n in ((s, ns[0]), (t, ns[-1]))} + if trank != 12 or gate_ranks != {4}: + raise AssertionError((trank, gate_ranks)) + if trank > 2 * max(gate_ranks): + pass + else: + raise AssertionError("rank floor failed to exclude length two") + + # Complete length-three census; matrices store all eight F2 coefficients + # independently rather than packed bitsets. + prefix_products = [] + for a, b in itertools.product(generators, repeat=2): + prefix_products.append((a[0], b[0], matrix_product(a[1], b[1]))) + checked = 0 + matches = [] + for ga, gb, prefix in prefix_products: + for gc, c in generators: + checked += 1 + if matrix_product(prefix, c) == target: + matches.append((ga, gb, gc)) + if checked != 56**3 or matches: + raise AssertionError((checked, matches[:3])) + + # Direct four-call positive control: st=r and ts=r^-1. + e11 = tuple(int((i, j) == (0, 0)) for i in range(3) for j in range(3)) + e22 = tuple(int((i, j) == (1, 1)) for i in range(3) for j in range(3)) + direct = matrix_identity() + for g, n in ((s, e11), (t, e11), (t, e22), (s, e22)): + direct = matrix_product(direct, gate(g, n)) + if direct != target: + raise AssertionError("four-call positive control failed") + + # Omission and a higher-rank altered endpoint are meaningful negatives. + truncated = matrix_identity() + for g, n in ((s, e11), (t, e11), (t, e22)): + truncated = matrix_product(truncated, gate(g, n)) + if truncated == target: + raise AssertionError("omission control unexpectedly hit target") + if target_difference_rank(1, 3) != 12: + raise AssertionError("target-rank control changed unexpectedly") + all_three_nontrivial_rank = 3 * 6 + if all_three_nontrivial_rank <= 3 * max(gate_ranks): + raise AssertionError("altered all-nontrivial endpoint should exceed three-call rank budget") + + print( + "PASS_D8_INVERSE_PAIR_W3 " + f"rank_floor={trank}/{max(gate_ranks)} generators=56 " + f"triples={checked} matches=0 minimum=4 " + "direct_control=pass omission_control=pass altered_rank_control=pass" + ) + + +if __name__ == "__main__": + main()