1337isnot1337 · Oct 19, 2026
diff --git a/research/sl2z-four-call-native-target/OVERLAP.md b/research/sl2z-four-call-native-target/OVERLAP.md
@@ -0,0 +1,61 @@
+# Overlap checks for the scoped SL2(Z) shear target
+
+Assignment: bit-new-register-model, priority revision 6, selector scope key
+7084092dd726e7ba1f2f, base commit
+20ecf2891d80b5acf18d980b2164fb44ea7faa90.
+
+## Cached search
+
+Ran the assigned broad search:
+
+~~~sh
+python3 scripts/find_overlap.py --task bit-new-register-model --offline --cache /home/user/int-bounds-pass/20261018-luna-xhigh/overlap.json --limit 8
+~~~
+
+It returned POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE. The cache covered
+586 open PRs and 2,536 discussions, fetched 2026-10-19 UTC; the offline run
+warned that live changes could be missing. The first relevant matches included
+the [free-group commutator-pair claim #1997](https://github.com/CrocSwap/integer-mult-bounds/discussions/1997),
+the [four-role UT5(Z) claim #2094](https://github.com/CrocSwap/integer-mult-bounds/discussions/2094),
+and Q8/S3/S4 proposals. No conclusion of novelty follows.
+
+A second cached query for S5, five-cycle and adjacent-transposition terms
+found prior S_n work. The S5 route was dropped: [discussion #1740 comment
+18928637](https://github.com/CrocSwap/integer-mult-bounds/discussions/1740#discussioncomment-18928637)
+states the exact minimum for all diagonal targets in F2[S_n] using paid adjacent
+transpositions and arbitrary dirty registers. [Discussion #1167 comment
+18936078](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18936078)
+records an eight-call minimum for the S5 inverse-5-cycle pair.
+
+## Live handoffs and open PRs
+
+Read the top-level Start here #1163, Handoffs #1166, and Mechanism proposals
+#1167 through the GitHub API. The live handoff scan covered all 684 comments
+in #1166 and found no SL2(Z), SL_2(Z), or integer-shear proposal. The latest
+register-model handoff was [#1166 comment
+19021147](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19021147),
+the Q8 t<=2 sharpness result; its target, group and alphabet differ.
+
+The current open PR search found related but distinct register-model work:
+
+- [#3774](https://github.com/CrocSwap/integer-mult-bounds/pull/3774), head
+  713c28c1b0ebbdf3f30d7887fcb173e7a786f245, uses UT3(F4), four involution
+  labels, and the three-output central target.
+- [#3788](https://github.com/CrocSwap/integer-mult-bounds/pull/3788), head
+  595b9426cc2fac34d31a71b24b98ed080f54c99a, adjoins the two w^2 labels to
+  that UT3(F4) alphabet and retains the twelve-call minimum.
+- [#3800](https://github.com/CrocSwap/integer-mult-bounds/pull/3800), head
+  5e4d41cb0e99e4773abca244cdc8c376686421b8, independently reconstructs that
+  UT3(F4) model and performs a bounded shorter-word search.
+- [#3783](https://github.com/CrocSwap/integer-mult-bounds/pull/3783) records
+  the twelve- and fourteen-call UT3(F4) central words without a shorter-word
+  search.
+- Open PR searches for SL2(Z), SL_2(Z), and opposite elementary matrices
+  returned zero results. Search for integer shear returned #3678, which checks
+  a scatter inverse identity and invoices, not an address-group target.
+- Reviewed predecessors #1974 and #2027, captured in the revision-6 review, cover a GL3(F2)
+  census with a bounded third-role probe and a UT4(F2) mixed-root tariff.
+  Their alphabets and address groups differ from the integer-shear group here.
+
+These are overlap checks, not a novelty certificate. The exact minimum proved
+here applies only to the stated generators and endpoint.
diff --git a/research/sl2z-four-call-native-target/README.md b/research/sl2z-four-call-native-target/README.md
@@ -0,0 +1,159 @@
+# A four-call exact target in an integer shear alphabet
+
+**Status: scoped exact minimum. No new kappa or supplier claim.**
+
+## Question and model
+
+Use the nonabelian address group
+
+$$
+G=\langle X,Y\rangle\leq \operatorname{SL}_2(\mathbb Z),\qquad
+X=\begin{pmatrix}1&1\\0&1\end{pmatrix},\quad
+Y=\begin{pmatrix}1&0\\1&1\end{pmatrix}.
+$$
+
+The paid address alphabet is exactly
+$$
+\mathcal A=\{X,X^{-1},Y,Y^{-1}\}.
+$$
+These are native reversible integer coordinate shears on an address pair
+$(a,b)\in\mathbb Z^2$: $X$ adds $b$ to $a$, and $Y$ adds $a$ to $b$.
+Their inverses subtract. Each label is unimodular and each difference from
+the identity has rational rank one:
+
+$$
+X-I=E_{12},\quad X^{-1}-I=-E_{12},\quad
+Y-I=E_{21},\quad Y^{-1}-I=-E_{21}.
+$$
+
+The scalar data has two roles, both arbitrary elements of
+$R=\mathbb F_2[G]$. One paid factor is
+$$
+D_N([g])=I_2+([g]+[e])N,
+$$
+where $g\in\mathcal A$ and $N$ is any rank-one idempotent in
+$M_2(\mathbb F_2)$. Every factor costs one call. There are no free address
+updates between calls. The lower bound below also survives any intervening
+constant scalar matrices over $\mathbb F_2$, since they add no group labels.
+
+The target is
+$$
+B=X^2Y^2=\begin{pmatrix}5&2\\2&1\end{pmatrix},\qquad
+\operatorname{diag}([B],[e]).
+$$
+Here $\det B=1$ and $\det(B-I)=-4$, so $B-I$ has rank two. Thus $B$ is not
+one of the legal rank-one address labels.
+
+**Question.** What is the minimum paid-call count for this target, over all
+legal idempotent frames and all arbitrary dirty inputs?
+
+## Result
+
+The exact minimum is **four calls**. With
+$P=E_{11}$, which is a legal rank-one idempotent,
+
+$$
+D_P([g])=\begin{pmatrix}[g]&0\\0&[e]\end{pmatrix},
+\qquad
+D_P([X])^2D_P([Y])^2
+=\begin{pmatrix}[X^2Y^2]&0\\0&[e]\end{pmatrix}.
+$$
+
+This is a full formal group-algebra equality. On arbitrary dirty
+$(u,v)\in R^2$, the endpoint is $(Bu,v)$. The second role is unchanged.
+
+## Why fewer calls cannot work
+
+In a product of $k$ paid factors, each factor contributes either the
+identity group label or its one alphabet label in each expanded term.
+Therefore every group element in every matrix-entry support is represented
+by a word of at most $k$ letters from $\mathcal A$. This remains true for
+arbitrary rank-one idempotents and for interleaved constant scalar matrices.
+The coefficient $[B]$ in the target's first diagonal entry requires
+$B$ to occur in that radius-$k$ word ball.
+
+An exact enumeration of all $1+4+4^2+4^3=85$ words of length at most three
+in $\mathcal A$ contains no $B$. Thus no word of at most three paid calls
+can reach the target, regardless of the idempotent frames. The four-call
+word above attains the bound. The verifier reproduces the 85-word check and
+checks the complete $2\times2$ formal operator.
+
+## Complete bill
+
+| Item | Count | End state |
+| --- | ---: | --- |
+| Paid factors, with labels $X,X,Y,Y$ | 4 | First role receives $B$ |
+| Other dirty scalar roles | 1 | Second role is unchanged |
+| Scratch roles | 0 | None borrowed |
+| Copy, reset, inverse cleanup, or restore calls | 0 | No cleanup required |
+| Uncharged address updates | 0 | Every label use is a paid factor |
+
+The count is complete in this stated group-algebra model. It does not price a
+larger bit-supplier interface or show that these labels improve the selected
+recursive cost profile. The label operations themselves are the specified
+native integer shears; a separate low-level hardware or compiler invoice is
+outside this result.
+
+## Relation to prior work
+
+The three-register lower-bound package uses the additive group of
+$M_3(\mathbb Q)$ and explicitly excludes extra roles and arbitrary free
+address maps between calls. This result keeps exact formal coefficients and
+rank-one paid updates, but refines the card to a specified multiplicative
+nonabelian address family generated by opposite integer shears. It uses two
+scalar roles and makes no claim about the original abelian theorem.
+
+The model and factor notation follow the prior register-model line cited in
+the [three-register bound](../bit-three-register-lower-bound/README.md),
+which credits eumemic's PR #288 and huxint's PR #203. The [GL3 mixed-target
+review](../bit-gl3-mixed-targets-length10/README.md) records a distinct
+finite GL3 alphabet and a three-role probe through length seven. We do not
+rerun either historical computation.
+
+The overlap check rejected an S5 route because a prior result gives the
+exact adjacent-transposition tariff for all symmetric groups. Other nearby
+work includes the free-group commutator-pair claim and a four-role UT5(Z)
+claim. This package uses a concrete integer matrix group and the different
+target $X^2Y^2$; it does not claim novelty for the general factor formalism.
+The current UT3(F4) central-triple PRs also use a different field, alphabet,
+target and role count. See [OVERLAP.md](OVERLAP.md) for exact heads, URLs and
+the live searches made for this pass.
+
+## Reproduce
+
+From the repository root:
+
+~~~sh
+python3 -B research/sl2z-four-call-native-target/verify.py
+python3 scripts/research_package.py --package research/sl2z-four-call-native-target --check-only
+~~~
+
+The verifier uses only the Python standard library and exact integer and
+$\mathbb F_2$ arithmetic. Its finite enumeration is limited to the 85 words
+needed for the length-three lower bound; the operator identity itself is
+checked in the full formal group algebra.
+
+## Limits
+
+This proves a minimum for one endpoint in one declared abstract address
+model. It does not certify a physical bit implementation of the group-algebra
+registers, a supplier invoice, a favorable recursive moment, or a change to
+the selected result. No larger target search was run.
+
+## Open next questions
+
+Can $B=X^2Y^2$ and $B^{-1}$ share paid factors in the two-role endpoint
+$\operatorname{diag}([B],[B^{-1}])$, whose coordinate-projector word costs
+eight calls? This matters because a one-target word has no slack below its
+four-call minimum; only cross-role sharing could lower the combined count.
+The first step is a complete 4+3 meet-in-the-middle over the 24 legal
+$(N,g)$ factors, covering every word through length seven with exact
+group-algebra joins and an eight-call positive control. The blocker is proving
+a lower bound if the split finds no seven-call word; the one-target support
+argument alone does not settle cross-role cancellation.
+
+## Credit
+
+Prepared by OpenAI Codex (macbook-02), with substantial AI assistance, on
+priority revision 6. Retain the prior register-model attribution above.
+New work is under Apache-2.0.
diff --git a/research/sl2z-four-call-native-target/SOURCES.json b/research/sl2z-four-call-native-target/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "docs/research/community-efficient1000-review.md",
+      "usage": "provenance",
+      "git_blob": "fc9704487ccf5fbf0472950117741c219fe98151",
+      "sha256": "bac19ca28be781e7ac444e0666320ef77c0ac159467eafa3198e07b7c280442e"
+    },
+    {
+      "path": "docs/research/current-priorities.md",
+      "usage": "provenance",
+      "git_blob": "231a089623bf11a70a434f5a57b0bf0a2ad4c317",
+      "sha256": "c95e09baa997b48ba00a26ea29168e782b17392d28184ecb7a17eea5472dd77c"
+    },
+    {
+      "path": "docs/research/research-family-status.md",
+      "usage": "provenance",
+      "git_blob": "9b7d65650d8fcd6247a758936b24426b40e40efa",
+      "sha256": "9b98ab42364e90588e90410fd2773f9bc4bf5050f514101bed0a0246881b5b7e"
+    },
+    {
+      "path": "research/bit-gl3-mixed-targets-length10/README.md",
+      "usage": "provenance",
+      "git_blob": "59ac7008af69ffb41e10e6574308d68c33d44c48",
+      "sha256": "f1f88a618fa998baa2bb5e8bc69c225405b6106b4c0a5646d84c42166cd4aff5"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    }
+  ]
+}
diff --git a/research/sl2z-four-call-native-target/TASK.json b/research/sl2z-four-call-native-target/TASK.json
@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_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": "In the nonabelian address group G=<X,Y> <= SL2(Z), with paid labels X, X^-1, Y, Y^-1 and two arbitrary dirty scalar roles, determine the exact minimum paid-call count for diag([X^2 Y^2],[e]) over rank-one idempotent frames.",
+  "scope_change_reason": "The card explicitly allows a specified nonabelian operation family. This pass fixes the native integer-shear group, its four rank-one labels, and one rank-two target so the smallest completed instance and full restoration bill can be decided exactly.",
+  "bottleneck_link": "The result prices one exact changed-address-alphabet endpoint. It does not show a lower recursive moment or supplier improvement; any future gain would need a multi-role sharing identity or a priced consumer.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at a full formal identity and exact minimum, or at any counterexample with at most three calls. Do not search longer words or convert this endpoint into a supplier in this session.",
+  "outcome": "completed",
+  "evidence": "README.md gives the arbitrary-dirty operator identity, native shear alphabet, support lower bound, and complete bill. verify.py checks the full formal 2x2 group-algebra endpoint, all 85 words through length three, and controls.",
+  "author": "OpenAI Codex (macbook-02)",
+  "ai_assistance": "Substantial assistance by OpenAI Codex, GPT-6 Luna xhigh. The user assigned this bounded research session.",
+  "open_questions": [
+    {
+      "question": "Can X^2Y^2 and its inverse share paid factors in the two-role endpoint diag([X^2Y^2],[(X^2Y^2)^-1])?",
+      "why_it_matters": "The one-target endpoint has an exact four-call minimum, so only cross-role sharing can lower the direct eight-call bill in this model.",
+      "first_step": "Build an exact radius-four split over the 24 legal (N,g) factors, join formal group-algebra states, and include the direct eight-call word as a positive control.",
+      "blocked_by": "The present support-ball lower bound does not control cross-role cancellation; a negative search would need a separate lower-bound proof."
+    }
+  ]
+}
diff --git a/research/sl2z-four-call-native-target/VERIFY.json b/research/sl2z-four-call-native-target/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact full group-algebra witness; all 85 group words of length at most three excluded; native rank-one label checks; omitted-factor and wrong-label controls."
+    }
+  ]
+}