Skip to content

Research: UT4 two-target unit count is independent of dirty workspace #1680

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 14, 2026
Merged

Research: UT4 two-target unit count is independent of dirty workspace #1680

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
146 changes: 146 additions & 0 deletions research/ut4-one-slack-workspace/CERTIFICATE.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,146 @@
{
"active_width": 2,
"dropped_factor_occurrences": 2268,
"equal_rank_wrong_target_plane_control": {
"active_basis": [
1,
2
],
"candidate_basis": [
1,
4
],
"candidate_rank": 2,
"union_rank": 3
},
"full_witness_basis_columns": 2560,
"independent": {
"address_bit_positions": [
[
0,
1
],
[
1,
2
],
[
2,
3
],
[
0,
2
],
[
1,
3
],
[
0,
3
]
],
"basis_order": "64*role+group_code",
"involution_controls": 3,
"method": "literal 4x4 binary matrices and full regular columns",
"mixed_active_feedback_sha256": "0a4012d66773923873a7f1ba87fe7e7de3af73db9708fdd5eb85aaaad22ba860",
"mixed_orientation_rejected": true,
"positive_compressions": [
{
"active_basis_columns": 128,
"active_corner_sha256": "8c7b90c68fe842a18ec061fe7e812468d23b99bdcf7eb9cf2a2f61c26d6d16b2",
"active_output_rows": 128,
"common_orientation": "both",
"dropped_zero_calls": 0,
"input_calls": 16,
"kept_calls": 16,
"r": 3,
"w": 2
},
{
"active_basis_columns": 128,
"active_corner_sha256": "8c7b90c68fe842a18ec061fe7e812468d23b99bdcf7eb9cf2a2f61c26d6d16b2",
"active_output_rows": 128,
"common_orientation": "both",
"dropped_zero_calls": 0,
"input_calls": 18,
"kept_calls": 18,
"r": 3,
"w": 2
},
{
"active_basis_columns": 128,
"active_corner_sha256": "b71831d42eda94bf1e3acb9691a1b898e506b6892e610084332839dc6333e070",
"active_output_rows": 128,
"common_orientation": "columns",
"dropped_zero_calls": 1,
"input_calls": 6,
"kept_calls": 5,
"r": 3,
"w": 2
},
{
"active_basis_columns": 128,
"active_corner_sha256": "681ab4802ba10d82016a5725c95de6820f4132687afa3193d69b1380b882eb76",
"active_output_rows": 128,
"common_orientation": "rows",
"dropped_zero_calls": 1,
"input_calls": 6,
"kept_calls": 5,
"r": 3,
"w": 2
}
],
"product_order_controls": 1,
"schema_version": 1,
"scope": "compression fixtures and known16-call endpoint; no14/15-call attainment claim"
},
"known_upper_witnesses": 10,
"mixed_feedback_rejected": true,
"new_14_or_15_word": false,
"ordered_triangular_pairs": 7938,
"pair_roles": 3,
"pair_transcript_sha256": "3bebc029cff84bf93dc2fb743aa5ec07daa011945bf85d1bd5af1ce73f393a78",
"quotient": {
"basis": [
"",
"a",
"b",
"c",
"ab",
"ac",
"ba",
"bc",
"cb",
"aba",
"abc",
"acb",
"bab",
"bac",
"bcb",
"cba",
"cbc"
],
"basis_associativity_products": 4913,
"central_image": [
"",
"abc",
"acb",
"bac",
"cba"
],
"common_kernel_zero": true,
"dimension": 17,
"distinct_group_images": 64,
"group_map_sha256": "9de6cc7ea95a1fd1f78782ba338371acbf0b667de289e787616582d262462443",
"group_products": 4096,
"schema_version": 1,
"scope": "Necessary cubic coefficients; full group-algebra endpoint admission remains separate."
},
"rank_profile_sha256": "7f1d23fa671360548bfe8fddc8590b3e47d44836ecc3de82d30414491117700d",
"rank_profiles": 105,
"schema_version": 1,
"two_target_minimum": "C_r=C_2 in {14,15,16}; exact value unresolved",
"uniform_scope": "w>=2,L<=7w+1,r>=w; written proof, not finite extrapolation"
}
111 changes: 111 additions & 0 deletions research/ut4-one-slack-workspace/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
# One-slack workspace compression in the UT4 model

**Uniform scoped theorem; no new construction or kappa.** The new result is
workspace compression near the retained call lower bound. It uses the span
and quotient lemmas of @ToikY's [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662),
pinned at `01cc02b164ecc4f9d84df3f56a1fe65b88daf390`.

## Model and normalization

All scalar coefficients and ranks are over F2. Let `G=UT4(F2)`, with
`a=I+E12`, `b=I+E23`, `c=I+E34`, and central `z=I+E14`.
Work in the full formal algebra `R=F2[G]`. For every finite `r>=w>=2`, a
paid factor is `D_N(g)=I_r+([g]+1)N`, where `g in {a,b,c}` and
`N=x y^T` for nonzero binary r-vectors x,y. Idempotent and nilpotent
rank-one couplings are both admitted. Count every paid occurrence at unit cost.
The required endpoint is `T=I_r+([z]+1)P`, `P=diag(I_w,0)`.
Every role has arbitrary input; the extra r-w roles must be restored exactly.

Scalar GL_r(F2) maps may be free. Move them to one end by conjugating paid
couplings, which preserves their nonzero rank one and their labels. Augmentation
`[g]->1` sends every paid factor and T to identity, so the remaining free map
is identity. We therefore analyze a normalized paid word without changing its
count or endpoint. There are no other free address operations, clean workspace,
higher-rank paid couplings, COPY or ERASE. All equalities below are formal
operator equalities, not agreement only on inputs with zero extra roles.

## Retained span premises

For label g, let X_g collect its column vectors and Y_g its row vectors:
X_g is r by n_g and Y_g is n_g by r. Write u_g=rank(X_g), v_g=rank(Y_g).
The first-order coefficient gives `X_g Y_g=0`, hence `n_g>=u_g+v_g`.
The fixed degree-three quotient used in PR1662 is

`Q=F2<a,b,c>/(a^2,b^2,c^2,ac-ca,all monomials of degree>=4)`.

Here a,b,c are augmentation variables: group generators map to 1+a,1+b,1+c,
and z maps to `1+abc+acb+bac+cba`. The unchanged pinned quotient implementation
replays all 4096 group products and 4913 basis associativity triples. This is
a fixed-group homomorphism certificate; it does not enumerate r,w or word lengths.
Each of these four target coefficients is P. Ordered scalar expansion gives:

| Coefficient | Target containment forced by its first/last scalar factor |
|---|---|
| abc | im(P) contained in im(X_a); row(P) contained in row(Y_c) |
| cba | im(P) contained in im(X_c); row(P) contained in row(Y_a) |
| bac, combining BAC and BCA | im(P) contained in im(X_b) |
| acb, combining ACB and CAB | row(P) contained in row(Y_b) |

No scalar matrices are commuted when the address monomials combine.
Consequently all six ranks are at least w. To recall the stronger middle bound,
number b factors and let A_j be the sum of preceding a couplings and C_j the
sum of following c couplings. Set X=X_b, Y=Y_b, `U=[A_j x_j]`, and let V
have rows `y_j^T C_j`. The B, AB, BC and ABC coefficients give
`XY=UY=XV=0`, `UV=P`. The last map factors through `ker(X)/im(Y)`, of dimension
`n_b-u_b-v_b`; therefore `n_b>=w+u_b+v_b`. These are inherited premises.

## New one-slack theorem

For every normalized legal word of length L with endpoint T, if `L<=7w+1`,
there is a legal word on exactly w roles with endpoint `[z]I_w` and length
at most L. More precisely, all normalized couplings share at least one orientation:

`N P=N for every factor`, or `P N=N for every factor`.

**Proof.** Summing the retained per-letter inequalities gives

`L=n_a+n_b+n_c >= w+sum_g(u_g+v_g) >= 7w`.

All ranks are integers. Thus their total excess over w is at most one.
At most one of the six spans can have dimension w+1; every other span has
dimension w and, by containment, equals the corresponding target span.
If the exceptional span is a column span, every row span equals row(P).
Thus each y satisfies `y^T P=y^T`, giving `N P=N` for every factor.
If it is a row span, every column span equals im(P), giving `P N=N`.
If no span is exceptional, both conclusions hold. The orientation is common
to the whole word, not chosen separately at each factor.

Split roles as the active w roles followed by the extra r-w roles. In the
first case each paid factor is block lower triangular; in the second it is
block upper triangular. On either common block-triangular algebra, projection
pi to the active corner is multiplicative, including over the noncommutative
ring R: the discarded cross-block product is zero. Therefore
`pi(product D_N(g))=product pi(D_N(g))=pi(T)=[z]I_w`.
Each projected coupling is the outer product of the active components of x,y,
so it has rank one or zero. Retain the former and discard zero identity factors.
This produces the claimed legal word. Each label count can only decrease;
no new preparation, inverse or restoration factor is introduced. This proves
the theorem for arbitrary extra-role inputs, using the full endpoint premise.

## Two-target optimum is independent of workspace

Let C_r be the minimum unit paid count for two targets and r>=2 roles.
Embedding a two-role word gives `C_r<=C_2`. The retained lower bound gives
`C_r>=14`, and `(abcb)^2=z` on each target gives `C_2<=16`.
If `C_r<C_2`, then `C_r<=15`; the new theorem compresses such an optimal
r-role word to two roles, implying `C_2<=C_r`, a contradiction. Hence

`C_r=C_2 in {14,15,16} for every finite r>=2`.

This does not decide which value occurs or provide a 14/15-call construction.
It does not claim that every 16-call word compresses. Optimal weighted tariffs
are outside this corollary: a cheaper weighted word may have more than 15 calls.
Physical/compiler/hosting, precision/tape, analytic transfer and proof-kernel
verification remain outside this formal-model theorem; the selected frontier is unchanged.

Credit @ToikY/PR1662 for the UT4 span and quotient machinery, steph4n-gh/PR1573
for the UT3 all-register rank method, Arham Tahir/PR1589 for nilpotent couplings,
and Hanson Sun (@bbMisk)/PR1607 for mixed-target coefficient spans. Their
retained source lineage remains credited. Prepared for @ToikY with substantial
OpenAI Codex assistance. Separate AI checks are not independent human review.
New work is Apache-2.0.
132 changes: 132 additions & 0 deletions research/ut4-one-slack-workspace/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,132 @@
# UT4 one-slack compression removes the two-target workspace search

**Uniform scoped reduction; no new word or kappa.** In the full formal
`F2[UT4(F2)]` alphabet of [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662),
every central-target word with `r>=w>=2` and unit paid length `L<=7w+1`
has an equivalent word on exactly `w` roles with no more calls. All extra
roles may begin arbitrary dirty and must be restored. Paid couplings may be
any nonzero binary rank-one matrix, including nilpotents; scalar mixing is
normalized first, and every paid call is counted.

Consequently the optimal **two-target unit count is identical for every finite
`r>=2`**, with its exact value still one of **14,15,16**. A 14/15-call witness
or complete exclusion on two roles therefore answers the same question for
arbitrary workspace. No such witness or exclusion is supplied here. This adds
the missing workspace implication to the predecessor's unchanged 14..16 interval.

The [written proof](PROOF.md) sums six scalar span inequalities. At length
`7w` all spans equal the active target plane; at `7w+1` at most one span has
one extra dimension. All paid factors therefore share one block orientation.
Projection to the active corner preserves their product over the **full
noncommutative group algebra**. Projected couplings have rank one or zero;
zero identity factors are discarded, so each label count can only decrease.

This does not claim that every 16-call word compresses, that weighted tariff
optima are workspace independent, or that larger-slack words admit the same
argument. There are no clean roles, free address operations, higher-rank paid
factors, COPY or ERASE. No physical supplier, rational-frame identity,
compiler/hosting contract, multiplication exponent or selected-frontier change
is claimed. Kernel formalization, precision/tape and analytic transfer remain open.

## Exact corroboration and scope controls

The theorem is a written uniform argument with a retained fixed-group lemma;
finite role fixtures corroborate its algebra and do not prove its quantifiers.

| Check | Coverage |
|---|---|
| Common-orientation formal/faithful operator comparison | 3,969 ordered pairs per upper/lower orientation on three roles, active width two |
| Distinct pair coverage | 7,209 distinct pairs; 729 belong to both orientation families, giving 7,938 recorded cases |
| Complete regular basis columns | 1,524,096 full input columns, including arbitrary dirty-role inputs |
| Zero projected factors actually discarded | 2,268 occurrences across the recorded pair cases |
| Integer span-slack profiles | 105 profiles, widths 2..16; all possible zero/one-excess positions |
| Known coordinate upper words | 10 fixtures through five roles, 2,560 complete basis columns |
| Retained quotient homomorphism/associativity | 4,096 group products and 4,913 basis triples |

[CERTIFICATE.json](CERTIFICATE.json) retains exact digests, the fixed quotient
receipt and the separately implemented faithful checker's receipt.
The primary engine multiplies six-coordinate formal group coefficients;
[independent.py](independent.py) uses literal four-by-four address matrices
and simultaneous updates of every regular-basis input. It imports no primary
or predecessor executable. Its four fixtures include both common orientations,
noncoordinate/nilpotent couplings and discarded zero projections. The 16/18-call
endpoint fixtures verify compression's algebraic conclusion; they are not
14/15-call witnesses or instances establishing the one-slack forcing premise.

A mixed upper/lower pair has two individually zero active projections, yet its
full product feeds the dirty role back into the active corner. The checker
rejects it. A rank-two plane missing one active direction demonstrates why
dimension counts alone do not replace the six target-span containments.
The fault suite covers the two-slack threshold, illegal alphabets/domains,
actual model/vendor/receipt corruption, occupied outputs and optimized read-only
relocation. No sampled bits or nonfaithful proof image admits a full endpoint.

## Reproduce

From the repository root, with Python3.12 and standard library only:

```sh
python3.12 -B scripts/research_package.py --package research/ut4-one-slack-workspace
```

Expect `PASS_UT4_ONE_SLACK_WORKSPACE`,
`PASS_UT4_ONE_SLACK_INDEPENDENT`, passing fault tests and
`PASS_REGISTERED_RESEARCH_PACKAGE research/ut4-one-slack-workspace outcome=completed`.
Normal verification writes nothing. Explicit `verify.py --write-receipt NEW_PATH`
and `independent.py --write NEW_PATH` refuse occupied outputs. The registered
manifest is [VERIFY.json](VERIFY.json); actual local commands, environment and
unrun obligations are recorded in [VALIDATION.json](VALIDATION.json).
Standalone optimized replay also works in a source export containing the
declared live model input. Generic provenance checking requires the pinned Git history.

## Scope, coordination and retained source credit

Base main: `a18b4b0136d647529971e9fcb99fa83f5b9a0b81`; revision3 task
`bit-new-register-model`, nonce `e5da093483cfe0c1dfea3262d0f0935b`, scope key
`7f5f4426ef796683c485`. Scope is explicitly **changed** from constructing a
shortest identity to a useful missing-workspace reduction for that construction
problem. [TASK.json](TASK.json) retains the original card, reason, bound and
overlap limitations. The required selected-baseline source-binding control passed;
it was not the selected full cold replay.

This is complementary to **Aaron Wang / navinor's active two-role exhaustive
search**, [claimed here](https://github.com/CrocSwap/integer-mult-bounds/discussions/1647#discussioncomment-18916137)
with Claude Code assistance. That claim leaves extra dirty roles open; this
package removes that gap at 14/15 calls without duplicating its search or
endorsing an unpublished result. [Our claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1647#discussioncomment-18916672)
states the complementary scope. Entry checks covered 537 open PR bodies including
drafts, local package metadata/ledger and bounded live Discussion reads.
Concurrent merges prevent an atomic PR snapshot; full Discussion pagination,
all diffs and unpublished work were not covered. No novelty guarantee is made.

Credit **@ToikY / PR1662**, head `01cc02b164ecc4f9d84df3f56a1fe65b88daf390`,
for the UT4 six span containments and middle quotient. Its `quotient.py` is copied
**byte-for-byte**, with exact Git blob and SHA256 in [VENDOR.json](VENDOR.json),
so replay does not require an unmerged dependency checkout. Its unchanged fixed
homomorphism certificate is inherited evidence, not a new independent implementation.
[SOURCES.json](SOURCES.json) binds the live model input and selected/catalog provenance.

Retain credit **steph4n-gh / [PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573)**
at `0b8c5a69297c794f2de22c04494c83e41300ae36` for all-register zero-sum ranks;
**Arham Tahir / [PR1589](https://github.com/CrocSwap/integer-mult-bounds/pull/1589)**
at `010ec8c01c0edbbb08b541be236ab78d096f2ca1` for nilpotent couplings;
**Hanson Sun (@bbMisk) / [PR1607](https://github.com/CrocSwap/integer-mult-bounds/pull/1607)**
at `9d6117918025cee6a0c5b7ef30ff8d936ca0621f` for coefficient spans, and the
juper997/PR1478, woklerx/PR1443, Gareth Davidson/bitplane/PR1333,
commdata2338/PR1414, eumemic/PR288 and Ali Romman/PR468 lineage retained by them.
No literature-priority claim is made. Prepared for @ToikY with substantial
OpenAI Codex assistance, including two bounded subagents; no independent human
or proof-kernel review claimed. Apache-2.0, with inherited notices preserved.

## Open next questions

Does the two-role 27-factor alphabet attain 14 calls? Coordinate with navinor's
active search and independently audit its eventual complete formal certificate.
The reduction makes a rigorous two-role exclusion decisive for all workspace
sizes; an incomplete census does not. No complete certificate is supplied here.

If 14 is excluded, does a 15-call two-role word exist? Define a complete exact
domain and full endpoint check; extra dirty-role sizes need not be searched.
This remains blocked by the unresolved 14-call question and any overlapping
active investigation. Weighted tariffs and larger-slack workspace use are
separate questions, not conclusions of this package.
Loading
Loading