Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 65 additions & 0 deletions research/sl2f3-conjugate-triple-seed592f/CERTIFICATE.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
{
"direct_paid_bill": 5,
"direct_word": [
"D[i;100*100^T]",
"D[w;010*010^T]",
"D[w^-1;001*001^T]",
"D[i;001*001^T]",
"D[w;001*001^T]"
],
"free_scalar_mixing_covered": true,
"group_generated_by": [
"i",
"i^-1",
"w",
"w^-1"
],
"group_order": 24,
"i_matrix_mod3": [
[
0,
1
],
[
2,
0
]
],
"limitations": [
"finite nonabelian address algebra only",
"address-operation implementation cost not priced",
"no selected supplier or kappa change claimed"
],
"model": "M3(F2[SL2(F3)])",
"mutated_generator_control": true,
"omission_controls": 5,
"one_call_states": 112,
"paid_call_alphabet": 112,
"positive_control_minimum": 2,
"rank_one_idempotents": 28,
"result_minimum": 5,
"schema_version": 1,
"search_depth": 4,
"short_witness": null,
"short_witness_indices": null,
"target_c": "w^-1*i*w",
"target_diagonal": [
"i",
"w",
"c"
],
"two_call_distinct_states": 8905,
"two_call_full_convolution_cross_checks": 12544,
"two_call_state_sha256": "7313957379a9c51963604fae5f6a69edda1771006526c9c2ef4ab068e76bed95",
"two_call_words": 12544,
"w_matrix_mod3": [
[
0,
2
],
[
1,
2
]
]
}
67 changes: 67 additions & 0 deletions research/sl2f3-conjugate-triple-seed592f/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
# Exact five-call minimum for a binary tetrahedral register endpoint

**Scoped exact negative result; no new `kappa`.** In the finite nonabelian model below, the heterogeneous target `diag([i],[w],[w^-1 i w])` has exact paid-call minimum **five**. Its direct word costs five. An exhaustive exact search excludes every word with four or fewer factors, so this target gives no paid-call saving in this model.

## Model and complete bill

Let `G = SL2(F3)`, the 24 matrices of determinant one over `F3`, and work in the full formal group algebra `R = F2[G]`. Use

```text
i = [[0, 1], [-1, 0]], w = [[0, -1], [1, -1]] (entries modulo 3),
c = w^-1 i w.
```

The four paid address labels are `i`, `i^-1`, `w`, and `w^-1`; they generate all of `G`. A paid factor is

```text
D_N(g) = I + ([g] + [e]) N,
```

where `N = x y^T` is a rank-one idempotent in `M3(F2)`, so `x,y` are nonzero binary three-vectors with `y^T x = 1`. There are 28 such idempotents and therefore 112 paid factors. Each costs one. The three registers are all targets; there is no extra dirty workspace, clean state, COPY/ERASE, or uncharged paid call. Free scalar `GL3(F2)` mixing is allowed.

The target is

```text
diag([i], [w], [c]).
```

The direct word applies `i` to role 0 and `w` to role 1, then applies `w^-1, i, w` in that order to role 2. This is an exact five-call word. The element `c` has order four and shortest length three in the four-label address alphabet.

## Exact coverage

The verifier stores each of the nine entries as a 24-bit coefficient support, so equality means equality of every coefficient in `F2[G]`. All four-call words are covered by a meet-in-the-middle join of two-call prefix and suffix states. There are 12,544 ordered two-call words and 8,905 distinct exact states. For each distinct suffix state `B`, the verifier computes `target * B^-1` and checks exact membership in the complete two-call prefix table. This covers all `112^4 = 157,351,936` raw four-call words, including duplicates. The same suffix set checks every three-call word as a one-plus-two split; words of length zero, one and two are checked directly. In total, every word at each length zero through four is excluded.

Each factor satisfies `D_N(g)^-1 = D_N(g^-1)`, so the suffix inverse is exact. The fast rank-one transition is independently cross-checked against full coefficient convolution for all 12,544 two-call products. The complete rank-one idempotent set absorbs arbitrary free `GL3(F2)` changes of basis: augmentation `[g] -> 1` sends each paid factor and the target to identity, forcing the net free scalar map to be identity, and pushing each free map through a factor only conjugates `N` within the enumerated set.

The exact minimum is therefore five **only for this fixed group, generator alphabet, target, three roles, and one-call factor definition**. `CERTIFICATE.json` records the two-call state count and a digest of the canonically ordered states; exact tuple equality, not the digest, decides the joins.

## Reproduce

From the repository root with Python 3.12 and the standard library:

```sh
python3.12 -I -B research/sl2f3-conjugate-triple-seed592f/verify.py
python3.12 scripts/research_package.py --package research/sl2f3-conjugate-triple-seed592f
```

Expected verifier line:

```text
PASS_SL2F3_CONJUGATE_TRIPLE group=24 calls=112 target_minimum=5 pair_words=12544 distinct_pair_states=8905 short_witness=none
```

`verify.py --write` regenerates the deterministic coverage certificate after review. Normal replay checks the regenerated result against the committed `CERTIFICATE.json`. The package pins the exact three-register predecessor source and the selected record/catalogue provenance in [SOURCES.json](SOURCES.json).

## Predecessors, relevance, and limits

The source result remains the maintainer-reviewed conditional finite construction with `kappa = 836330098538459/500000000000000000`. Its review is [`community-batch1099-review.md`](../../docs/research/community-batch1099-review.md) (SHA-256 `7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb`); the selected source manifest is `research/community-frontier1094-audit/SELECTED-SOURCE.json` (SHA-256 `79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b`); the assembly certificate SHA-256 is `1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`; its recorded reproduction command is `make frontier1094-verify`. This experiment does not use those supplier files, change the selected construction, or alter `kappa`.

The model descends from the scoped three-register abelian bit result in PR [#468](https://github.com/CrocSwap/integer-mult-bounds/pull/468), which explicitly excludes other address groups. The closest nonabelian predecessors are PR [#1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822), a Q8 repeated central-commutator pair, and PR [#1925](https://github.com/CrocSwap/integer-mult-bounds/pull/1925), Q8 mixed targets on three and four roles. This package changes the address group to its order-three binary tetrahedral extension and tests a heterogeneous `i,w,w^-1iw` target. It imports no predecessor implementation.

An eight-call result in the opening claim was narrowed before search to this smallest decisive heterogeneous endpoint, reducing the direct bill to five and the exhaustive saving threshold to four. The updated scope and exact budget are recorded in [Discussion #1999](https://github.com/CrocSwap/integer-mult-bounds/discussions/1999); the mechanism index is [Discussion #1167 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18929640).

The group elements are treated as unit-cost address labels in this finite model. Their physical realization, source access, compiler, frame conversions, hosting, precision, restoration in a selected supplier, and recursive-moment effect are not priced. The result supplies neither a multiplication construction nor a universal impossibility theorem. It is an exact negative result for one new operation alphabet and endpoint, prepared with substantial OpenAI Codex assistance; no independent human review or proof-assistant formalization is claimed.

## Open next questions

Does one arbitrary restored dirty scalar role lower the five-call minimum for this same `SL2(F3)` endpoint? That tests whether workspace sharing helps while keeping the nonabelian target fixed. A first step is to enumerate the four-role rank-one idempotents and screen exact depth-four meet-in-the-middle coverage against the unchanged direct word. The larger `4 x 4` formal matrix states and the missing physical address-operation implementation are the blockers.
24 changes: 24 additions & 0 deletions research/sl2f3-conjugate-triple-seed592f/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
{
"schema_version": 1,
"base_commit": "1c47876ef742ba64bf9140b0527d63acf656a3b4",
"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": "input",
"git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
"sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
}
]
}
88 changes: 88 additions & 0 deletions research/sl2f3-conjugate-triple-seed592f/TASK.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
{
"schema_version": 1,
"task_id": "bit-new-register-model",
"priority_revision": 3,
"base_commit": "1c47876ef742ba64bf9140b0527d63acf656a3b4",
"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": "In M3(F2[SL2(F3)]), with i=[[0,1],[-1,0]] and w=[[0,-1],[1,-1]] over F3, use the four paid address labels i,i^-1,w,w^-1 and all 28 rank-one idempotents N in M3(F2). Determine the exact minimum paid-call count for diag([i],[w],[w^-1 i w]), with free scalar GL3(F2) interleavings allowed, by exhausting every word through depth four and comparing with the direct five-call word.",
"scope_change_reason": "The catalogue explicitly permits a specified nonabelian operation family. This refines that broad option to the order-24 binary tetrahedral group SL2(F3), its four-generator alphabet, and one heterogeneous three-role endpoint so the full search through one call below the direct bill is finite and exactly coverable.",
"bottleneck_link": "A four-call factorization would remove one paid call from this five-call finite bit-register endpoint. The exact minimum is five, so this particular nonabelian extension supplies no saving. The model does not price any selected-supplier source, hosting, or physical address-operation implementation, and no kappa change follows.",
"budget_minutes": 60,
"stop_rule": "Exhaust all words of lengths zero through four over the 112 paid factors in M3(F2[SL2(F3)]), with exact full-coefficient equality, and verify the direct five-call endpoint and controls. Do not expand to a different group, target, or register count in this cycle.",
"outcome": "negative-result",
"evidence": "SL2(F3) has 24 elements and is generated by i,w. There are 28 rank-one idempotents and 112 paid factors. Exact meet-in-the-middle coverage checks every word of lengths 0..4 (112^k raw words at length k): the 12,544 two-call words yield 8,905 distinct exact states, each checked as a suffix for both 1+2 and 2+2 splits. The two-call transition is cross-checked against full group-algebra convolution for all 12,544 pairs. No target hit occurs through four calls; the direct five-call word realizes diag([i],[w],[w^-1 i w]), so the exact minimum is five in this model. Five omitted-call controls, a generator mutation, a two-call positive control, all gate inverses, and all group-table associativity checks pass.",
"author": "Cinna Davis",
"ai_assistance": "Substantial OpenAI Codex assistance in scope refinement, exact algebra/search implementation, verification and writing. No independent human review or proof-assistant formalization is claimed.",
"open_questions": [
{
"question": "Does one arbitrary restored dirty scalar role lower the five-call minimum for this same SL2(F3) endpoint?",
"why_it_matters": "This tests whether workspace sharing can beat the exact three-role result while preserving the same nonabelian target and paid address alphabet.",
"first_step": "Extend the formal state to four roles, derive the 120 rank-one idempotents and 480 paid factors, then compute the exact two-call state set and screen complete depth-four meet-in-the-middle coverage against the unchanged five-call direct word.",
"blocked_by": "The four-role matrix state is larger, and the exact finite address model still has no priced translation into a selected integer-multiplication supplier."
}
],
"seed": "592f04c45f93ecfac35ea0ab971b12ba",
"track": "bit-mechanisms",
"scope_key": "d03e83a1b42a1002ba51",
"selector_scope_key": "7084092dd726e7ba1f2f",
"catalogue_revision": 3,
"catalogue_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075",
"selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
"predecessors": [
{
"pr": 468,
"scope": "abelian three-register bit model; lower bound at exact base pin in package"
},
{
"pr": 1822,
"head": "ee736b4b11bbd63b04d94c8edafb3790161ebdea",
"scope": "Q8 repeated central-commutator pair"
},
{
"pr": 1925,
"head": "009ed860f34ed5d7b0d626098ce93c4c2a7eb4df",
"scope": "Q8 mixed diagonal triples"
}
],
"claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1999",
"claim_update_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1999#discussioncomment-18929639",
"mechanism_index_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18929640",
"finished_utc": "2026-10-14T16:55:22Z",
"certificate_sha256": "92870cc9c4bb777d816453bcbdfbbae2b3f90e39b95e0358931f2da1d2582f43"
}
20 changes: 20 additions & 0 deletions research/sl2f3-conjugate-triple-seed592f/VERIFY.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
{
"schema_version": 1,
"status": "ready",
"python": "3.12",
"requirements": [],
"inputs": [
"research/bit-three-register-lower-bound/README.md"
],
"commands": [
{
"argv": [
"{python}",
"-B",
"{package}/verify.py"
],
"timeout_seconds": 180,
"checks": "Construct SL2(F3) and all 112 paid gates exactly; exhaust words through four calls by exact meet-in-the-middle in the full group algebra; cross-check all 12,544 two-call products by independent convolution; verify the five-call direct endpoint, a two-call positive control, inverse laws, omitted-call and mutated-generator failures, and the committed state digest."
}
]
}
Loading
Loading