Skip to content

Prove shortest S3 single-target word rigidity - #4740

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
JoyboyBrian:brian/s3-shortest-word-rigidity
Oct 22, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
JoyboyBrian:brian/s3-shortest-word-rigidity

Conversation

@JoyboyBrian

Copy link
Copy Markdown
Contributor

In the formal binary S3 rank-one-idempotent alphabet, the known three-call implementation of one longest-transposition target is rigid: for every register count, a three-call word must have labels sts or tst, and all three projectors must equal the target projector. This answers the shortest-word equality part of PR #4647's first open question; its shorter-word lower bound remains prior work.

The scoped package proves the result by six independent group-ring coefficients and supplies an independent faithful 18×18 binary-matrix census of all 175,616 three-register words. Each of the 28 rank-one targets has exactly two hits. It includes controls for dirty-scratch leakage, changed labels/projectors, rank-two outer factors, and representation/order mistakes.

Validation:

  • Python 3.12 registered package replay and both direct scripts in normal and -O modes pass.
  • Separate Codex review checked the proof and code, plus independent 8,192 arbitrary-matrix and 1,728 rank-one two-register cases.
  • Committed-byte/source-history preflight and Git-free exported direct replay pass.

This is a scoped formal-algebra result. It does not supply native operation prices, a complete multiplier or a new κ; longer-word searches and Lean/Docker suites were not run. Only the new package directory changes.

Canonical claim: #4350 (comment)

Predecessor: #4647 at 734bb589d082ccd7c61b987d36a84b85c318e117; local provenance and retained contributor credit are recorded in the package. Prepared for JoyboyBrian with substantial OpenAI Codex assistance, including a separate AI reviewer; no human or proof-kernel acceptance is claimed.

Submission overlap refresh: canonical main remains b58ad9ef4d4e861b0eaa5dba41742bdc072dca51 / priority revision 7. Scoped offline searches used 499 open PRs fetched at 18:35:14 UTC and 3,648 Discussion records fetched at 18:36:07 UTC on 2026-10-22, with 5,862 local notes including this package. PR #4647 remains at its pinned head. The refreshed matches and changed records did not identify another single-target three-call equality classification; this is bounded search coverage, not a novelty guarantee. Closed PR diffs and arbitrary nested code remain outside the search.

@Mister-Meeseeks
Mister-Meeseeks merged commit f8de75f into CrocSwap:main Oct 22, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants