Skip to content

Finite certificate: three coordinate swaps need nine paid calls on three registers (no new kappa) #1491

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

Finite certificate: three coordinate swaps need nine paid calls on three registers (no new kappa) #1491

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
120 changes: 120 additions & 0 deletions research/three-swap-cnot-census/EXPECTED.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
{
"active_swaps": 3,
"ball_radius_four": 1094640,
"ball_radius_three": 47203,
"exact_distance_layers": [
1,
56,
1750,
45396,
1047437
],
"extra_dirty_registers": 0,
"formal_group_order": [
[
0,
1,
2
],
[
0,
2,
1
],
[
1,
0,
2
],
[
1,
2,
0
],
[
2,
0,
1
],
[
2,
1,
0
]
],
"formal_layer_sha256_7byte_little_endian": [
"ecbddeeab2e0b6f4e4b9005377629d164dc6fd2416662299eb87a63d7206b81a",
"625fac19b641720950a656ef52b7542f38dc1cc979bd776c060e58301c705a47",
"35666ddd0745f0c315360a23fb1365ebbd73f68589b25757e1fcfc93a8a5836e",
"aff97ee994a75a5f6add28466ef05631ec1e5bb6ffa39d5eaa7cc4f09a66a0ca",
"64d641567b5ece05a3b8d7b5943005b4a331a07d9bf3d4da5cd9d0b13d6561f2"
],
"independent_dense_transition_checks": 101192,
"independent_full_state_sets_equal": true,
"independent_target_intersections": [
0,
0,
0,
0
],
"minimum_paid_calls": 9,
"paid_generators": 56,
"parity_homomorphism_products": 36,
"permitted_call_count_parity": "odd",
"positive_minimum_controls": [
0,
3,
6
],
"rank_one_idempotents": 28,
"registers": 3,
"regular_layer_sha256_41byte_little_endian": [
"e8d84774982c75464b6c23c4295e2fcb1a2b4f50fe5681fc04f83cadfc94e1f5",
"f95a4899103e83b66d129cf1f767d88b82a32881578b7d4382c40a069d306099",
"e80f59882043b2842ec04929d8290449b5acc21333ca82417226510419c45186",
"989487d6e30ad7003cd78745c085472f8f5977ca4ad3bd708b0e2faaf7f97b48",
"cd071d15c60df520eac37f4c0f0b73e8583a983f1a6c7034e4dbd1b40dc4e9c4"
],
"schema_version": 1,
"scope": "Finite certificate: exactly three registers in the stated formal alphabet; no new kappa.",
"semantic_controls": [
"omit_call_0",
"omit_call_1",
"omit_call_2",
"omit_call_3",
"omit_call_4",
"omit_call_5",
"omit_call_6",
"omit_call_7",
"omit_call_8",
"wrong_label_0",
"wrong_label_1",
"wrong_label_2",
"wrong_label_3",
"wrong_label_4",
"wrong_label_5",
"wrong_label_6",
"wrong_label_7",
"wrong_label_8",
"omit_third_target",
"scalar_residue",
"expanded_address_alphabet",
"nonidempotent_scalar",
"rank_three_underpricing",
"natural_representation_kernel",
"noncommuting_order"
],
"status": "PASS_THREE_SWAP_CNOT_CENSUS",
"target_intersections_by_left_distance": [
0,
0,
0,
0
],
"transition_attempts_by_depth": [
56,
3136,
98000,
2542176
]
}
95 changes: 95 additions & 0 deletions research/three-swap-cnot-census/OVERLAP.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
{
"schema_version": 1,
"base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc",
"queries": [
[
"--task",
"bit-helper-contract"
],
[
"--task",
"bit-new-register-model"
],
[
"three swaps",
"three-SWAP",
"coordinate-CNOT",
"coordinate-cnot-register-bound"
],
[
"three swaps",
"three-SWAP",
"three-swap-cnot-census",
"coordinate-CNOT"
]
],
"entry_coverage": {
"open_prs": {
"fetched_at": "2026-10-14T01:13:06.664495+00:00",
"records": 828,
"complete_pagination": true
},
"discussions": {
"fetched_at": "2026-10-14T01:13:30.574789+00:00",
"records": 162,
"complete_pagination": true
}
},
"latest_checked_coverage": {
"discussions": {
"fetched_at": "2026-10-14T01:24:02.227375+00:00",
"complete_pagination": true,
"records": 169
},
"open_prs": {
"fetched_at": "2026-10-14T01:23:37.439709+00:00",
"complete_pagination": true,
"records": 776
}
},
"coverage_limit": "Offline shared snapshot. Open PRs include drafts; complete remote pagination is reported. Closed work is covered only by local notes/ledger; code diffs and arbitrary nested source are not searched. No match proves no novelty claim.",
"claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912673",
"nearest_prs": [
{
"number": 1414,
"head": "9e1640094f649ba6db9742796825a8d6c238989b",
"difference": "Two swaps, arbitrary restored dirty-register count; leaves three swaps open. This result is three swaps at exactly r=3."
},
{
"number": 1333,
"head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2",
"difference": "All affine rank-one address maps are units; the swap itself is permitted there. Here only the two coordinate CNOTs are paid labels."
},
{
"number": 720,
"head": "a942c0ae1b463710ca535c1fba1b07b6431b5a86",
"difference": "Arbitrary invertible rational targets in an abelian three-register model, not the present binary nonabelian address algebra."
}
],
"concurrent_claims": [
{
"url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912406",
"object": "Two central-commutator targets over UT_3(F2), r=2,3.",
"difference": "Different group, target and eight-call baseline."
},
{
"url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912696",
"object": "Two coordinate swaps over GL_3(F2), r=2,3, all six address CNOTs.",
"difference": "Different address dimension/alphabet and two targets, rather than three GL2 targets."
},
{
"url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912727",
"object": "Two copies of the order-four GL_3(F2) target with rows (2,4,7), r=2.",
"difference": "Different group, target order, register count and eight-call baseline."
}
],
"other_account_work": "The earlier copy-floor, feedback, hosting, receipt-binding, tape-boundary, Clifford-binding and bit-ledger results have different mathematical objects and are not repeated.",
"source_inspection": "PR1414 and PR1333 inspected by anonymous git fetch; exact heads and text hashes are in SOURCES.json. No pending implementation imported.",
"final_reviewed_at": "2026-10-14T01:31:55.869752+00:00",
"anonymous_head_recheck": {
"main": "92da4d718f1d4cf8de4e6ee947ddc7b180ce1c31",
"1414": "9e1640094f649ba6db9742796825a8d6c238989b",
"1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2",
"note": "The two contextual heads are unchanged. Main advanced after the research base was selected; historical provenance remains at the recorded base."
}
}
166 changes: 166 additions & 0 deletions research/three-swap-cnot-census/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,166 @@
# Exact three-register, three-swap minimum

This is a computer-assisted finite theorem for one explicit register count,
alphabet and endpoint. The enumeration in Section 4 is an essential premise
of its lower bound. It is not an arbitrary-register theorem.

## 1. Formal model and normalization

Let `G=GL_2(F2)` and `R=F2[G]`. Group symbols are formal and multiplication
retains their order. With column-vector address convention, put

```text
a = [[1,1],[0,1]], b = [[1,0],[1,1]], s = aba = bab = [[0,1],[1,0]].
```

The action on the three nonzero binary vectors identifies G with S3.
Registers are three arbitrary R-module inputs. Allowed words are 3x3
matrices over R generated by free scalar `GL_3(F2)` changes and unit paid
factors

`D_N(g)=I+([g]+1)N`, with `g in {a,b}`, `N=uv^T`, and `v^Tu=1` over F2.

Every paid occurrence, including an undo, costs one. There are no other
operations or additional registers. The full formal endpoint is

`T=diag([s],[s],[s])`.

Free scalar changes can be moved to the right by conjugating the N matrices.
Conjugation preserves rank one and idempotence. The augmentation homomorphism
`R -> F2`, sending every group element to one, sends each paid factor and T
to I. It therefore forces the remaining scalar factor to be I. Thus it is
enough to enumerate products of paid factors alone. This argument is credited
to PR #1333 and its restricted-alphabet use in PR #1414.

Every binary rank-one idempotent has the displayed form. There are seven
nonzero choices of u, and exactly four v with `v^Tu=1`; over F2 there is no
nontrivial scaling ambiguity. All **28** projectors, hence all **56** paid
generators, are included. Independently enumerating all 512 binary 3x3
matrices gives exactly the same projectors. The focused tests check closure
under all 168 scalar invertible matrices (4,704 conjugations).

Since a and b are involutions, `([g]+1)^2=0` in characteristic two. Scalar
coefficients commute with the group symbols, so `D_N(g)^2=I`. Reversing any
generator word gives its inverse with the same paid length.

## 2. Parity rules out all even lengths

The sign homomorphism `G -> C2` sends a, b and s to the nonidentity element t.
Over F2 its group algebra is `F2[epsilon]/(epsilon^2)`, with `t=1+epsilon`.
The induced map sends a normalized product of k paid factors to

`product_j (I+epsilon N_j) = I+epsilon sum_j N_j`.

The target maps to `I+epsilon I_3`, so `sum_j N_j=I_3`. Taking traces over
F2 and using `trace(uv^T)=v^Tu=1` gives

`k mod 2 = trace(I_3) = 1`.

Consequently a word with fewer than nine calls would have length 1, 3, 5 or
7. The same proof works for any number of restored dirty extras, but the
enumeration below does not. The checker verifies all 36 products in the sign
homomorphism and the projector trace premise. The general sign-trace method
is credited to PR #1414; here its target trace is odd instead of even.

## 3. Why radius three against radius four is complete

Let `B_d` be the set of distinct formal matrices expressible using at most
d allowed paid factors, including I. A breadth-first traversal computes
exact-distance layers `L_0={I}` and

`L_(d+1) = {x f : x in L_d, f a paid generator} minus (L_0 union ... union L_d)`.

Induction on word length proves completeness. If a word's prefix is already
reachable at a shorter distance, appending its last generator gives a path
no longer than the original, so deduplication cannot remove a required
endpoint. The implementation retains every new state. It applies no
symmetry quotient, heuristic, floating-point pruning or randomized sampling.

Every word of length at most seven can be split as `p q`, with
`p in B_3` and `q in B_4`. It equals T precisely when `p^-1 T=q`.
The involutive alphabet gives `B_3^-1=B_3`, so

`a word of length <=7 reaches T` iff `{x T : x in B_3} intersects B_4`.

The right multiplication by T is an exact permutation of the six coefficients
in every matrix entry. It is not a natural-representation test. The second
implementation computes the corresponding product by generic 18x18 matrix
multiplication.

## 4. Complete enumeration and independent representation

The computed exact-distance layer counts at distances 0..4 are

`1, 56, 1750, 45396, 1047437`.

At depths 1..4 the numbers of directed transition attempts are

`56, 3136, 98000, 2542176`.

Thus `|B_3|=47203` and `|B_4|=1094640`. For each of the four left-distance
layers 0..3 the intersection count is **zero**. This establishes the needed
finite exclusion. Counts, full-layer hashes and independent comparisons are
bound in EXPECTED.json; replay recomputes rather than trusts them.

The first implementation represents a formal matrix by 54 bits: six formal
coefficients in each of nine entries. It generates G as permutations and
multiplies on the right. Its rank-one update is ordinary matrix multiplication:
for a row m, `m D_N(g) = m + (m u)([g]+1)v^T`. The test suite checks all 56
optimized maps on a full 54-vector binary basis against unoptimized formal
multiplication, so each optimized linear map agrees on every possible matrix.

The separate implementation generates G as actual binary 2x2 matrices and
uses its left regular action on the six group elements. A formal scalar
`f=sum_g c_g[g]` acts by `L_f e_h=sum_g c_g e_(gh)`. This representation is
**faithful**: applying L_f to e_1 recovers every c_g. Applying it entrywise
to 3x3 matrices remains faithful, giving binary 18x18 matrices. Hence equality
of these represented matrices is equivalent to formal equality, unlike the
natural two-dimensional address representation.

The second implementation enumerates all scalar matrices to find projectors,
uses left rather than right generator multiplication, and checks optimized
steps against dense 18x18 multiplication on all 101,192 transitions through
radius three. Left and right breadth-first traversals enumerate the same
word balls. Their complete exact-distance state sets agree through radius
four after conversion. Their target maps and zero intersection counts agree
separately. No shared search engine or predecessor implementation is used.

The natural representation is deliberately falsified as an equality oracle:
the nonzero formal sum of all six elements of G maps to the zero 2x2 matrix
and has zero augmentation. Adding it to an off-diagonal entry preserves the
natural image of I but changes both the formal and regular matrices.

## 5. Nine calls attain the complete boundary

For any idempotent N and any group elements g,h, direct expansion gives

`D_N(g) D_N(h) = D_N(gh)`.

Use `a,b,a` on each of `N=E_11,E_22,E_33`. Each triple gives the swap on
one register, with the other two untouched, and their product is T. This is
nine paid calls with no extra register, scalar basis change or restoration
omission. The formal verifier multiplies all nine factors, and rejects every
single omitted factor and every single a/b label swap.

Sections 2-4 exclude all shorter words; this explicit word supplies the upper
bound. Therefore the minimum is exactly **nine**, for **exactly three registers**
in the stated formal alphabet.

## 6. Limits and attribution

The result is exact finite algebra, not a probabilistic rank test or a claim
about arbitrary rational frames. Equality in the formal algebra holds on
every module of that algebra; the address group and register count remain
fixed. A fourth dirty register introduces projectors absent from this census
and is an open case. The result does not prove the same bound for arbitrary
workspace or an enlarged address alphabet.

The scoped model and research question follow PR #1414, with augmentation
normalization and the broader research direction from Gareth Davidson's
PR #1333. Eumemic, Ali Romman and David Govea receive credit for the rational
register-model lineage. No new general group-algebra or rank principle is
claimed. No Lean build, independent human proof review, physical/compiler
admission, hosting, precision/tape or analytic transfer was performed.

Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
New work is Apache-2.0.
Loading