Prove all-field rigidity of shortest permutation circuits (no κ)

research/all-field-permutation-rigidity/PROOF.md

@@ -0,0 +1,171 @@
+# Every shortest single-permutation word has one scalar projector
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let K be any field, n>=2, and R>=1. Let w be a nonidentity element of S_n
+and let E in M_R(K) satisfy E^2=E and rank E=1. Work in the full formal
+group algebra M_R(K[S_n]), with products acting on columns, rightmost first.
+The endpoint is
+
+    T = I + ([w]-[e]) E.
+
+A normalized paid factor is
+
+    D_s(N) = I + ([s]-[e]) N,
+
+where s is a simple adjacent transposition, N^2=N, and rank N=1.
+Every register has arbitrary entrance data. Equality means equality of all
+formal coefficients, including the return of all dirty spectators. Arbitrary
+scalar GL_R(K) operations may occur between paid factors.
+
+**Theorem.** The minimum paid length is inv(w). In every normalized word of
+this length, every paid coupling is exactly E and the label sequence is a
+reduced expression for w. Conversely, every reduced expression for w, with
+E at every call, attains the endpoint.
+
+This is a scoped algebraic proof, with finite corroboration. The theorem
+does not price physical scalar mixing or construct a native supplier.
+
+## What is inherited
+
+Brian's PR4765 proves tight spectator elimination over F2 for the S4
+ordered-pair module. Its Grassmann equality argument is the proof method
+used below. Ross Richardson's PR1989 supplies the ordered-pair cut for
+symmetric groups and the binary inversion tariff, retaining Adam Gall's
+cut-method credit. Nick Petalas's PR4851 already proves the length-three S3
+single-target rigidity theorem over every field, even with a larger scalar
+coupling alphabet. That special case is inherited.
+
+The new statement is the all-field, all-S_n single-target equality
+classification in the stated idempotent alphabet. We prove the finite
+ordered-pair geometry directly, rather than replaying predecessor searches.
+No literature-priority claim is made.
+
+## Normalize and choose the active line
+
+Move each scalar GL_R(K) map through its neighboring paid factor by
+conjugation. This preserves projector rank and idempotence. Augmentation,
+which sends every [g] to 1, sends the endpoint and every paid factor to I.
+It therefore forces the residual free scalar map to be I. The normalized
+word has only the displayed paid factors.
+
+Write A=im E and S=ker E, so K^R=A direct sum S. The endpoint acts by w
+on A and by identity on S. This basis choice is only for the proof. The
+conclusion in the original basis will be N=E. If R=1, S is zero and every
+rank-one idempotent is already E=I; the argument also covers this case.
+
+## Ordered-pair geometry over K
+
+Let U have basis e_(a,b) for distinct a,b in {1,...,n}. The action of g sends
+e_(a,b) to e_(g(a),g(b)); these are formal basis labels over K. Put
+
+    U+ = span{e_(a,b): a<b},    U- = span{e_(a,b): a>b},
+    V = K^R tensor U,          H = K^R tensor U+.
+
+This is a representation of the group algebra over every field. No ordering
+or positivity is imposed on K, and the geometric labels are not identified
+in characteristic two. Representation equality is used only as a necessary
+consequence of the full formal endpoint.
+
+For an invertible represented matrix P define
+
+    phi(P) = rank(pi_(K^R tensor U-) P|_H)
+           = dim H - dim(H intersect P^(-1)H).
+
+The second equality is rank-nullity. Both subspaces in the intersection
+have dimension dim H. For equal-dimensional subspaces X,Y set
+
+    d(X,Y) = dim X - dim(X intersect Y).
+
+This is an invertible-map-invariant metric. If X,Y,Z all have dimension k
+and d(X,Z)=d(X,Y)+d(Y,Z), then
+
+    X intersect Z subset Y subset X+Z.                 (1)
+
+Indeed, set a=dim(X intersect Y), b=dim(Y intersect Z),
+c=dim(X intersect Z), and t=dim(X intersect Y intersect Z). The inclusions
+(X intersect Y)+(Y intersect Z) subset Y and the inequality t<=c give
+a+b-t<=k and a+b<=k+c. This proves the triangle inequality. Equality forces
+t=c and dim((X intersect Y)+(Y intersect Z))=k, proving both inclusions in
+(1). This is the inherited Grassmann equality lemma over an arbitrary field.
+
+The crossing block of a permutation has one independent column for each
+inversion. Consequently phi(T)=inv(w), since E has one-dimensional image.
+
+For a simple s=(i,i+1), put alpha=e_(i,i+1), beta=e_(i+1,i), and let
+H_other be the span of the remaining positive ordered-pair basis vectors.
+The simple transposition permutes those remaining positive vectors.
+Write N=u v with v(u)=1. On ker v the paid factor is identity, and on
+span u it acts by s. Thus G=D_s(N) is invertible, G^2=I, and
+
+    GH = (K^R tensor H_other)
+         direct sum (ker v tensor span alpha)
+         direct sum (span u tensor span beta).          (2)
+
+It follows that d(H,GH)=phi(G)=1. These statements use idempotence and hold
+unchanged in every characteristic.
+
+## Tight peeling forces both scalar sides onto A
+
+Suppose an invertible represented P fixes S tensor U pointwise and preserves
+A tensor U, and suppose a right peel satisfies phi(PG)=phi(P)-1.
+Put X=H, Y=GH, and Z=P^(-1)H. Since G is an involution,
+
+    phi(PG)=d(H,G P^(-1)H)=d(GH,P^(-1)H)=d(Y,Z).
+
+The hypothesis is equality in the triangle inequality, so (1) applies.
+Since P is the identity on S tensor U,
+
+    S tensor U+ subset X intersect Z,
+    X+Z subset (A tensor U) direct sum (S tensor U+).    (3)
+
+By (2), u tensor beta lies in Y. The second inclusion in (1) and (3) forces
+the spectator part of u to vanish. Thus u is in A. For every x in S,
+x tensor alpha lies in X intersect Z and hence in Y. In (2) every alpha
+coefficient lies in ker v. Therefore v(x)=0 for every x in S.
+
+Both sides matter: N has image in A and annihilates S. Because A is a
+line and N is a nonzero idempotent, N acts as identity on A. Hence N=E.
+This conclusion is about the full scalar coupling, not only its image in
+the ordered-pair representation. Therefore the full formal factor fixes
+every spectator exactly.
+
+## Every peel in a shortest word is tight
+
+For invertible represented P,Q, the triangle inequality and its invariance
+give phi(PQ)<=phi(P)+phi(Q). Every paid factor has phi=1, so any m-factor
+word with endpoint T satisfies m>=inv(w).
+
+If m=inv(w), let P be the product of any initial j written factors.
+Subadditivity gives phi(P)<=j and phi(T)<=phi(P)+(m-j), forcing phi(P)=j.
+Starting at T, removing the rightmost written factor therefore drops phi
+by one. The tight-peeling argument forces that factor's coupling to be E.
+Its removal leaves a full formal endpoint acting only on A and fixing S.
+Apply the same argument to the next peel. Induction forces all couplings
+to be E. There is no bound on R in this reasoning.
+
+With common projector E, the full formal product is
+
+    I + ([s_1 ... s_m]-[e]) E.
+
+Distinct permutations are distinct group-algebra basis elements, so formal
+equality with T implies s_1 ... s_m=w. Its length m=inv(w) makes the
+expression reduced. Finally, adjacent sorting gives a reduced expression
+of length inv(w), and using E at every factor gives the displayed endpoint.
+This proves the lower bound, rigidity and converse.
+
+## Scope boundaries
+
+The theorem requires a single active line, adjacent labels, rank-one
+idempotents, the exact full endpoint and minimum unweighted length. Inserting
+a mixed factor and its inverse creates a longer valid word using spectators.
+Allowing the whole target permutation as a paid label can realize T in one
+call. The verifier checks these boundaries. Higher-rank targets, nonidempotent
+couplings and arbitrary separate generator prices are not classified here.
+
+Finite checks corroborate the written proof and do not establish its universal
+quantifiers by enumeration. Independent human and formal proof-kernel review
+are unclaimed. Native hosting, precision, tape, recursive invoices, supplier
+admission and the complete multiplication theorem remain outside scope.

research/all-field-permutation-rigidity/README.md

@@ -0,0 +1,133 @@
+# Shortest single-permutation circuits are rigid over every field
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped proof with exact finite corroboration; no new kappa.** For every
+field K, every n>=2 and every finite register count R, consider the exact
+formal endpoint
+
+    I + ([w]-[e]) E in M_R(K[S_n]),
+
+where w is a nonidentity permutation and E is a rank-one idempotent. Paid
+calls use simple adjacent transpositions and rank-one scalar idempotents.
+Arbitrary scalar GL_R(K) mixing is free, all inputs are arbitrary, and every
+dirty spectator must return exactly.
+
+The minimum is inv(w). More precisely, **every normalized minimum-length
+word uses E at every paid call**, and its labels form a reduced expression
+for w. Thus complex or odd-characteristic scalar mixing cannot move the
+active line or use dirty spectators in a shortest word of this alphabet.
+
+[PROOF.md](PROOF.md) gives the written all-parameter argument. The new step
+extends Brian's binary S4 tight-peeling geometry to all coefficient fields
+and all symmetric groups, then derives the single-line equality
+classification. Ross Richardson's binary inversion tariff and Nick Petalas's
+all-field three-call S3 special case are credited predecessor results.
+Neither is a new result of this package, and neither executable is replayed.
+
+## Evidence and reproduction
+
+The first working example is w=3412 in one-based notation, with four
+inversions. A rational three-register projector is
+
+    E = (1,2,1)^T (1,1,0) / 3.
+
+The same E at the four adjacent calls realizes the complete formal target.
+Its two-dimensional kernel is arbitrary dirty workspace and is restored.
+The faithful regular-action check includes every input column.
+
+The standard-library verifier enumerates 18,792 one-step S4 peeling cases
+over F3. The two-register domain uses all 12 rank-one idempotents as both
+endpoint and call projector. The three-register domain fixes endpoint E00
+and tests all 117 rank-one idempotent call projectors. Exactly 468 peels
+lower the cut, and each uses the endpoint projector and a right descent.
+It also checks 46 complete nonidentity S4 endpoints over Q and F3 on
+2,760 regular-action basis columns, four call omissions, four changed
+projectors and three boundary controls. These are finite corroboration of
+the written proof, not enumeration of its universal quantifiers.
+
+From the repository root with CPython 3.12 and no dependencies:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/all-field-permutation-rigidity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/all-field-permutation-rigidity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/all-field-permutation-rigidity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/all-field-permutation-rigidity --check-source-history
+```
+
+Other installations can substitute their CPython 3.12 executable. Direct
+runs are read-only and print a generated JSON receipt with the marker
+`PASS_ALL_FIELD_PERMUTATION_RIGIDITY`, enumerated counts and SHA256 hashes
+of all six package files. There is no handwritten receipt or expected
+output file. The registered ordinary and optimized runs enable warnings
+as errors. Sources are pinned as provenance, with no runtime imports.
+
+## Scope and credit
+
+The source is JoyboyBrian / Brian's
+[PR4765](https://github.com/CrocSwap/integer-mult-bounds/pull/4765), whose
+Grassmann equality and tight spectator elimination are the main predecessor
+method. Credit RossRichardson / Ross Richardson's
+[PR1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) for the
+ordered-pair cut and binary inversion tariff, retaining Adam Gall / PR1941
+and the cited cut lineage. Nick Petalas's
+[PR4851](https://github.com/CrocSwap/integer-mult-bounds/pull/4851) already
+settles the S3 length-three special case over every field, including a
+larger nonidempotent coupling alphabet. The register-model lineage retains
+eumemic / PR288, Ali Romman / PR468, Gareth Davidson / PR1333 and the
+predecessor credits. No literature-priority claim is made.
+
+Scientific base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030 with conditional kappa 0.003125804. The card's source-binding first
+example passed and was not a scientific replay. This changes
+`bit-new-register-model` to a formal equality obstruction with a changed
+coefficient-field and symmetric-group scope. Its native-supplier acceptance
+gate remains unmet. The
+[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362405)
+records that scope. Work stopped at the first verified result.
+
+The initial overlap check read current open PRs, this account's latest 200
+PRs, active Discussions and recent handoffs, merged theorem searches and
+all main READMEs for the distinctive rigidity/field/permutation terms.
+The cached card report covered 389 open PRs and 6,322 Discussion records;
+only 120 of 8,917 local notes were searched by that helper. Main-tree
+searches supplemented the sparse coverage. Arbitrary historical diffs and
+unpublished work remain outside the check. No-match searches do not prove
+novelty. [SOURCES.json](SOURCES.json) pins the credited proof sources.
+
+The theorem classifies minimum unweighted length with a single active
+line and idempotent calls. It does not classify higher-rank targets,
+nonidempotent couplings, unequal generator prices or non-simple labels.
+Native implementation, paid scalar work, compiler/hosting, precision, tape,
+stock, recursive invoices and supplier admission are outside scope. No
+selected-frontier change, complete multiplication theorem, selected cold
+replay, Lean or Docker run is claimed. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+For a rank-two endpoint projector over a nonbinary field, which normalized
+minimum-length words are possible inside its active plane? Tight peeling
+still motivates restricting attention to that plane, but the one-dimensional
+idempotence conclusion used here is unavailable. A first step is one S4
+endpoint and an exact two-dimensional coefficient calculation. No equality
+classification or physical price for that changed target is supplied here.
+
+## Verifier bounds
+
+The verifier has no recursion, subprocesses, network access or external
+mutable state. Its call graph is acyclic. All enumerations use fixed finite
+domains: S4, F3 vectors of length at most three, words of length at most
+eight and matrices of order at most 18 for crossing ranks. Each function
+fits within sixty physical lines. Explicit exception checks remain active
+under optimized Python.
+
+Python allocates tuples, dictionaries and arbitrary-size rational integers
+dynamically. This is a managed-runtime deviation from fixed allocation,
+confined to the bounded finite verifier. A formal state has at most 24
+coefficient matrices of order at most three; a regular-action vector has
+at most 72 coordinates. Exact arithmetic on this fixed fixture is bounded
+by the finite operations; no arbitrary input or real-time memory guarantee
+is claimed. Normal and optimized warning-strict replay are the available
+diagnostics. No shared diagnostic configuration changes.

research/all-field-permutation-rigidity/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/all-field-s3-shortest-rigidity/README.md",
+      "usage": "provenance",
+      "git_blob": "b486d63785f2e3e033ad6e00f4d31b5149e2ea5c",
+      "sha256": "633667ff74e2365e64fbd16826d828da29e3d205c9bb6785754cb01b8f5356a1"
+    },
+    {
+      "path": "research/s4-tight-word-spectator-elimination/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "4c3d129001e3976a64c5c58bd55bcd2a93a71781",
+      "sha256": "b2270221efb0f666225c28a8b5d16e0bc561672cf96af1263b57e32dcfe1e842"
+    },
+    {
+      "path": "research/s4-tight-word-spectator-elimination/README.md",
+      "usage": "provenance",
+      "git_blob": "8db05b993afe33649afd549f779c613a141806dc",
+      "sha256": "74f218e5cb2a28986b5db53ede7da419df5d719cd7c3bca0c955a354a24d92c4"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d",
+      "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f",
+      "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154"
+    }
+  ]
+}