From b27bf4c72a822b21f483e08cb3241ad9d165b66f Mon Sep 17 00:00:00 2001 From: Cinna Davis Date: Sun, 18 Oct 2026 21:33:10 -0500 Subject: [PATCH] research: price a four-call integer shear target --- .../sl2z-four-call-native-target/OVERLAP.md | 61 +++++++ .../sl2z-four-call-native-target/README.md | 159 ++++++++++++++++++ .../sl2z-four-call-native-target/SOURCES.json | 48 ++++++ .../sl2z-four-call-native-target/TASK.json | 64 +++++++ .../sl2z-four-call-native-target/VERIFY.json | 18 ++ .../sl2z-four-call-native-target/verify.py | 159 ++++++++++++++++++ 6 files changed, 509 insertions(+) create mode 100644 research/sl2z-four-call-native-target/OVERLAP.md create mode 100644 research/sl2z-four-call-native-target/README.md create mode 100644 research/sl2z-four-call-native-target/SOURCES.json create mode 100644 research/sl2z-four-call-native-target/TASK.json create mode 100644 research/sl2z-four-call-native-target/VERIFY.json create mode 100644 research/sl2z-four-call-native-target/verify.py diff --git a/research/sl2z-four-call-native-target/OVERLAP.md b/research/sl2z-four-call-native-target/OVERLAP.md new file mode 100644 index 0000000000..f62599d49a --- /dev/null +++ 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 new file mode 100644 index 0000000000..f8c354eeb9 --- /dev/null +++ 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 new file mode 100644 index 0000000000..80280d8622 --- /dev/null +++ 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 new file mode 100644 index 0000000000..c2cfcaa85d --- /dev/null +++ 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= <= 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 new file mode 100644 index 0000000000..c9e19142ad --- /dev/null +++ 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." + } + ] +} diff --git a/research/sl2z-four-call-native-target/verify.py b/research/sl2z-four-call-native-target/verify.py new file mode 100644 index 0000000000..db16b86750 --- /dev/null +++ b/research/sl2z-four-call-native-target/verify.py @@ -0,0 +1,159 @@ +#!/usr/bin/env python3 +"""Verify the exact four-call SL2(Z) shear target and its scoped minimum.""" + +from itertools import product + + +IDENTITY = (1, 0, 0, 1) +X = (1, 1, 0, 1) +XI = (1, -1, 0, 1) +Y = (1, 0, 1, 1) +YI = (1, 0, -1, 1) +ALPHABET = (X, XI, Y, YI) +EXPECTED = (5, 2, 2, 1) +P = ((1, 0), (0, 0)) + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +def mul(a, b): + a00, a01, a10, a11 = a + b00, b01, b10, b11 = b + return ( + a00 * b00 + a01 * b10, + a00 * b01 + a01 * b11, + a10 * b00 + a11 * b10, + a10 * b01 + a11 * b11, + ) + + +def det(a): + return a[0] * a[3] - a[1] * a[2] + + +def scalar_product(a, b): + return tuple( + tuple(sum(a[i][k] * b[k][j] for k in range(2)) % 2 for j in range(2)) + for i in range(2) + ) + + +def word_product(word): + out = IDENTITY + for label in word: + out = mul(out, label) + return out + + +def xor_term(dst, key, bit): + value = dst.get(key, 0) ^ bit + if value: + dst[key] = value + else: + dst.pop(key, None) + + +def matrix_product(a, b): + out = [[{}, {}], [{}, {}]] + for i in range(2): + for k in range(2): + for j in range(2): + for g, coefficient_a in a[i][k].items(): + for h, coefficient_b in b[k][j].items(): + key = mul(g, h) + xor_term(out[i][j], key, coefficient_a & coefficient_b) + return out + + +def paid_factor(g, n): + """Build I + ([g] + [e]) N over F2[G].""" + out = [[{IDENTITY: 1}, {}], [{}, {IDENTITY: 1}]] + for i in range(2): + for j in range(2): + if n[i][j]: + xor_term(out[i][j], IDENTITY, 1) + xor_term(out[i][j], g, 1) + return out + + +def target_matrix(g): + return [ + [{g: 1}, {}], + [{}, {IDENTITY: 1}], + ] + + +def all_short_words(): + words = [] + for length in range(4): + words.extend(product(ALPHABET, repeat=length)) + return words + + +def main(): + need(mul(X, XI) == IDENTITY and mul(XI, X) == IDENTITY, "X inverse mismatch") + need(mul(Y, YI) == IDENTITY and mul(YI, Y) == IDENTITY, "Y inverse mismatch") + need(det(X) == det(XI) == det(Y) == det(YI) == 1, "a label is not unimodular") + for label in ALPHABET: + difference = ( + label[0] - IDENTITY[0], + label[1] - IDENTITY[1], + label[2] - IDENTITY[2], + label[3] - IDENTITY[3], + ) + need(difference != (0, 0, 0, 0), "zero label difference") + need(det(difference) == 0, "label difference is not rank one") + need(mul(X, Y) != mul(Y, X), "the address group did not test noncommutativity") + need(scalar_product(P, P) == P, "chosen register frame is not idempotent") + need(sum(sum(row) for row in P) == 1 and det((P[0][0], P[0][1], P[1][0], P[1][1])) == 0, + "chosen register frame is not rank one") + + b = mul(mul(X, X), mul(Y, Y)) + need(b == EXPECTED, "target matrix mismatch") + difference = tuple(b[i] - IDENTITY[i] for i in range(4)) + need(det(b) == 1 and det(difference) == -4, "target rank/determinant mismatch") + + shorter = all_short_words() + need(len(shorter) == 85, "wrong bounded word count") + need(all(word_product(word) != b for word in shorter), "target occurs at length at most three") + radius3 = {word_product(word) for word in shorter} + need(b not in radius3, "target entered the radius-three word ball") + + factors = [paid_factor(g, P) for g in (X, X, Y, Y)] + result = factors[0] + for factor in factors[1:]: + result = matrix_product(result, factor) + expected = target_matrix(b) + need(result == expected, "full group-algebra endpoint mismatch") + + for omitted in range(4): + damaged = [factor for index, factor in enumerate(factors) if index != omitted] + value = damaged[0] + for factor in damaged[1:]: + value = matrix_product(value, factor) + need(value != expected, "omitted-call control was accepted") + wrong_middle = [paid_factor(g, P) for g in (X, X, YI, Y)] + value = wrong_middle[0] + for factor in wrong_middle[1:]: + value = matrix_product(value, factor) + need(value != expected, "wrong-label control was accepted") + wrong_role = [paid_factor(g, P) for g in (Y, Y, X, X)] + value = wrong_role[0] + for factor in wrong_role[1:]: + value = matrix_product(value, factor) + need(value != expected, "reversed target control was accepted") + + print( + "PASS_SL2Z_FOUR_CALL_TARGET " + "alphabet=4 roles=2 calls=4 shorter_words=85 " + f"distinct_radius3={len(radius3)} rank1_labels=4 " + "restoration_calls=0 omitted_controls=4 wrong_label=1 wrong_order=1 " + "no_new_kappa" + ) + + +if __name__ == "__main__": + main()