Bound dirty workspace for arbitrary permutation labels (no new κ)

research/permutation-slack-workspace/PROOF.md

@@ -0,0 +1,182 @@
+# Inversion-weighted spectator reduction
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+
+This is a scoped algebraic proof. Its finite controls are corroboration,
+not a proof of the universal quantifiers or a complete multiplication theorem.
+
+## Statement
+
+Let F be any field, n>=2, and R=A direct-sum S a finite-dimensional scalar
+role space, with dim A=w. Work in M_R(F[S_n]). For a nonidentity permutation g
+and scalar column u and row v with vu=1, define
+
+    G_g(u,v) = I + ([g]-[e])uv.
+
+The inverse is G_(g^-1)(u,v). Consider a nonempty normalized written word
+
+    T = G_(g_1)(u_1,v_1) ... G_(g_m)(u_m,v_m) = Q_A direct-sum I_S.
+
+The endpoint equality is coefficientwise in the full group algebra. It
+includes arbitrary dirty inputs, every off-diagonal coefficient, and complete
+spectator restoration. No restriction to diagonal active endpoints is made.
+Put d_i=inv(g_i)>0 and d_*=min_i d_i. Let permutations act on ordered distinct
+pairs, let H be the increasing-pair subspace tensored with R, and K the
+decreasing-pair subspace. For the represented endpoint set
+
+    L = rank(projection_K T restricted_to H).
+
+**Theorem.** A single spectator-only scalar basis change, fixing the original
+active coordinates, puts every original paid factor on at most
+
+    w + floor((sum_i d_i - L)/d_*)
+
+total roles. Restricting those same factors preserves their labels, order,
+rank-one idempotents and full formal endpoint. The retained extra roles remain
+arbitrary dirty inputs and are restored. In particular sum_i d_i>=L.
+
+When all labels have inversion count d, the bound is
+w+m-ceil(L/d). At d=1 this recovers Brian/JoyboyBrian's #4783 simple-label
+bound. The new statement admits non-simple and non-involutive labels, varying
+inversion counts, arbitrary symmetric groups, and every scalar field.
+
+The empty word needs no dirty roles and is treated separately. Identity
+labels can be deleted before defining d_*. This theorem does not price a label
+as inv(g) physical calls; d_i is a geometric quantity used to bound workspace.
+
+## The crossing decomposition
+
+Write U_+ for the span of increasing pairs and U_- for decreasing pairs.
+For any permutation h let C be the coordinate intersection U_+ intersect hU_+,
+let X be the coordinate complement of C in U_+, and Y the negative coordinate
+part of hU_+. Thus
+
+    U_+ = C direct-sum X,    hU_+ = C direct-sum Y,
+    dim X = dim Y = inv(h) = d.
+
+This holds because the ordered-pair action is a permutation action. An inversion
+is precisely an increasing pair sent to a decreasing one. No involution
+assumption is used. Since R=ker(v) direct-sum span(u), the represented gate is
+identity on ker(v) and h on span(u). Consequently
+
+    G_h H = (R tensor C) direct-sum (ker(v) tensor X)
+            direct-sum (span(u) tensor Y).                  (1)
+
+In particular d(H,G_h H)=d, where d(B,C)=dim B-dim(B intersect C) is the
+Grassmann distance for subspaces of the same dimension. Also
+
+    H intersect G_h H = ker(ell),
+
+where ell:H -> F^d applies v to each X-coordinate. Its quotient in G_h H
+has dimension d. Formula (1) is the new replacement for the predecessor's
+one-crossing decomposition.
+
+## The local charge
+
+Suppose the current residual P has full formal form P_A0 direct-sum I_S0.
+Define phi(P)=rank(projection_K P restricted_to H). Equivalently
+phi(P)=d(H,P^-1 H). Put Z=P^-1 H and D=H intersect Z.
+
+Peel a rightmost factor G_g by multiplying P on the right by its inverse.
+Set h=g^-1 and Y0=G_(g^-1) H. Invariance of Grassmann distance gives
+
+    phi(P G_g^-1) - phi(P)
+      = dim D - dim(Y0 intersect Z).                       (2)
+
+Indeed phi(PG_g^-1)=d(H,G_g P^-1 H)=d(G_g^-1 H,P^-1 H).
+In (1) use h=g^-1 throughout this local step. Both h and g have
+inversion count d.
+
+Write a for the S0 component of u, b for the restriction of v to S0, and
+eta=1[a!=0]+1[b!=0]. Then
+
+    d eta <= d + phi(P G_g^-1) - phi(P).                    (3)
+
+To prove this, note that Z contains S0 tensor U_+ and has no negative
+spectator component. If b!=0, ell restricted to D has rank exactly d,
+because D contains S0 tensor X and b is a nonzero functional there.
+Thus dim(D intersect ker ell)=dim D-d.
+
+If a!=0, any nonzero Y-coordinate in (1) has a nonzero negative spectator
+component, so cannot lie in Z. Therefore
+Y0 intersect Z=D intersect ker ell. If both a,b are nonzero, (2) is exactly
+d, proving (3) with eta=2. If a!=0 and b=0, (2) is nonnegative, proving
+(3) with eta=1.
+
+If a=0 and b!=0, the quotient of Y0 intersect Z by D intersect ker ell
+injects into Y0/(Y0 intersect H), a space of dimension d. Hence its dimension
+is at most dim D, so (2) is nonnegative and again eta=1 is charged.
+If a=b=0, the distance triangle gives (2)>=-d, completing the four cases.
+
+The nonnegative local slack s=d+phi(PG_g^-1)-phi(P) therefore pays
+eta<=s/d<=s/d_* dirty directions. This step is valid for arbitrary invertible
+active represented maps. It does not use faithfulness to admit an endpoint.
+
+## Nested splits and the global word
+
+For a vector a in S0 and functional b on S0, choose S0=V direct-sum S1,
+with a in V and b annihilating S1. Such a V has dimension at most eta.
+If a=b=0 take V=0. If just one is nonzero, retain its vector or a vector
+t with b(t)=1, respectively. If both are nonzero and b(a)!=0, take V=span(a)
+and S1=ker b. If both are nonzero and b(a)=0, choose b(t)=1 and take
+V=span(a,t), with S1 a complement to span(a) in ker b. These constructions
+work over every field.
+
+Enlarge A0 to A1=A0 direct-sum V. The peeled factor has u in A1 and v
+annihilates S1. Both the old residual and its peeled successor preserve A1
+and are identity on S1 in the full formal algebra. Repeat, starting at T
+and peeling factors from right to left. The final residual is identity.
+All retained V spaces lie inside the original spectator space. Telescoping
+the local nonnegative slacks gives
+
+    retained_dirty <= sum_i s_i/d_*
+                   = (sum_i d_i + phi(I) - phi(T))/d_*
+                   = (sum_i d_i - L)/d_*.
+
+The retained dimension is an integer, giving the floor in the theorem.
+The distance triangle also directly gives sum_i d_i>=L.
+
+Take a basis of the retained V spaces in peeling order, followed by a basis
+of the final discarded spectator space. This is one scalar basis of S, with
+the original active basis fixed. Let J include the retained role space and
+E project onto it along the discarded space. Every original factor satisfies
+u_i=J u_i' and v_i=v_i' E, with EJ=I. Thus
+
+    v_i' u_i'=1,    G_i J=J G_i',    E G_i=G_i' E,
+    G_i = G_i' direct-sum I_discarded.
+
+These identities hold coefficientwise in F[S_n], not just in the ordered-pair
+representation. Multiplication gives the original complete endpoint on the
+retained roles. Labels, order and every label-dependent tariff are preserved.
+
+## Sharpness and scope
+
+For any nonidentity g with d inversions, take one active axis e0 and two dirty
+axes e1,e2. Let u=e0+e1 and v=e0*+e2*, so vu=1. The written word
+
+    G_g(e0,e0*) G_g(u,v) G_(g^-1)(u,v)
+
+has endpoint diag([g],1,1), total inversion mass 3d, L=d and d_*=d.
+The theorem retains at most two dirty roles. Both are necessary if the actual
+factors must survive one spectator-only basis change: their nonzero dirty
+image and dirty functional have zero pairing. On a one-dimensional space,
+a nonzero vector and functional have nonzero pairing. This proves sharpness
+of the coefficient for this reduction, over every field, including a genuinely
+non-involutive 3-cycle. The canceling pair makes no endpoint-optimal-workspace
+or shortest-word claim.
+
+The result answers #4783's non-simple-label charge question. Brian's nested
+splits, positive-slack framework and preserved-factor sharpness mechanism
+remain predecessor credit. Ross Richardson #1989 supplies the ordered-pair
+inversion cut, following Adam Gall #1941 and Ross Richardson #1966. Credit
+Sagar Thakrar #3888, Arham Tahir #2998 and Nick Petalas #2583/#3408 for the
+retained weighted-register context. The proof is self-contained and imports
+no pending executable or finite-exclusion receipt.
+
+This is a fixed-word algebraic workspace reduction. It gives no physical
+basis-conversion algorithm or native tariff, and permits neither nilpotent
+couplings, unreturned spectators nor free address operations. Scalar mixing
+is normalized into the given rank-one idempotents; augmentation forces any
+remaining free scalar endpoint to be identity. Precision, tape, ownership,
+hosting, complete supplier admission and all-size multiplication transfer
+remain separate obligations. No new kappa is claimed.

research/permutation-slack-workspace/README.md

@@ -0,0 +1,185 @@
+# Dirty workspace from inversion-weighted permutation slack
+
+A fixed formal word with arbitrary nonidentity permutation labels can be
+restricted to at most
+
+```text
+active roles + floor((sum label inversions - endpoint crossing rank)
+                     / smallest label inversion count).
+```
+
+This is a scoped all-field algebraic proof with exact finite corroboration.
+The restriction preserves every original rank-one idempotent, paid label,
+written order and full arbitrary-dirty-input endpoint. When every label has
+the same inversion count d, the bound is `w+m-ceil(L/d)` total roles.
+There is no new kappa or complete multiplication theorem.
+
+This answers the first Open next question in Brian/JoyboyBrian's
+[PR #4783](https://github.com/CrocSwap/integer-mult-bounds/pull/4783), read at
+`c46cf15df53f3dad2ce59faec9cdc54184e643e5`. That predecessor proves the
+simple adjacent S4 case and leaves non-simple labels open. Its local-charge
+method, nested spectator splits and fixed-word sharpness mechanism retain
+predecessor credit. The new step replaces one crossing by the complete
+inversion-sized coordinate crossing space. Non-involutive labels use their
+literal inverse when peeling. The theorem covers all symmetric groups and
+all scalar fields.
+
+## Exact boundary and result
+
+Let F be any field, `R=A direct-sum S` a finite scalar role space, `dim A=w`,
+and `n>=2`. A paid factor in `M_R(F[S_n])` is
+
+```text
+G_g(u,v) = I + ([g]-[e])uv,       vu=1,       g != e.
+```
+
+A nonempty normalized word has full formal endpoint `Q_A direct-sum I_S`.
+The active block may be non-diagonal. Every spectator input is arbitrary
+and must be restored; every off-diagonal formal coefficient is constrained.
+Define `d_i=inv(g_i)`, `d_*=min d_i`, and `L` as the endpoint's crossing rank
+in the ordered-distinct-pair representation, increasing pairs to decreasing
+pairs. Then one spectator-only scalar basis change fixing A supports every
+original factor on at most `w+floor((sum d_i-L)/d_*)` roles.
+
+The [proof](PROOF.md) gives the exact crossing decomposition and four-case
+local inequality
+
+```text
+d_i * (1[dirty image != 0] + 1[dirty functional != 0])
+    <= d_i + phi(peeled residual) - phi(current residual).
+```
+
+Each right-hand side is nonnegative. Explicit nested splits and telescoping
+prove the bound; full group-algebra intertwiners prove the retained endpoint.
+The ordered-pair representation supplies a necessary geometric charge and
+is never used as a full endpoint oracle.
+
+The coefficient is sharp for preserving the given factors. A nonidentity
+coordinate call followed by a canceling non-simple gate/inverse pair has
+inversion slack `2d` and needs two dirty directions under the stated basis
+restriction. Their nonzero image and functional have zero pairing, which
+cannot happen on a one-dimensional retained dirty space. This says nothing
+about the endpoint's minimum workspace after resynthesis: the pair cancels.
+
+Identity labels can be removed first. The empty word needs no extra roles.
+The inversion count is a geometric weight, not an asserted native-call tariff.
+
+## Evidence and reproduction
+
+Python 3.12 and the standard library suffice. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/permutation-slack-workspace
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/permutation-slack-workspace/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/permutation-slack-workspace/oracle.py
+```
+
+On another machine substitute its CPython 3.12 path. Normal replay writes
+nothing. `verify.py --emit /absolute/new/path.json` explicitly generates a
+receipt with every package source hash and the recomputed transcript. It
+refuses an occupied output path. `--receipt /absolute/path.json` recomputes
+and compares every receipt field. Default replay checks the mathematical
+invariants directly; no generated output stays in the checkout. The source
+hashes authenticate bytes, not mathematical truth or independent authorship.
+
+The primary check covers 5,625 local peels. Every permutation label and
+rank-one projector is enumerated within these six finite domains; active
+maps are a declared deterministic sample of invertible maps on one active
+role's ordered-pair space, not an exhaustive GL census.
+
+| Permutations | Field | Total roles | Active maps per label/projector | Peels |
+| --- | --- | ---: | ---: | ---: |
+| S2 | F2 | 3 | 4 | 112 |
+| S3 | F2 | 3 | 4 | 560 |
+| S4 | F2 | 3 | 3 | 1,932 |
+| S3 | F3 | 3 | 3 | 1,755 |
+| S4 | F3 | 2 | 2 | 552 |
+| S5 | F2 | 2 | 1 | 714 |
+
+It also checks 576 literal crossing-space decompositions, four sharpness
+words in the full formal algebra, 300 complete regular-action dirty-input
+basis columns, and two constructive nested mixed-label compressions over
+F2 and F3. The nested words reduce six roles to four by one computed scalar
+basis, preserving every factor. Seven controls cover malformed permutations,
+nilpotent couplings, unsupported fields, unreturned dirt, forward-for-inverse
+substitution, unit crossing undercharge and the one-dimensional sharpness
+boundary.
+
+`oracle.py` imports no primary code. It enumerates actual 512-element binary
+subspace sets and computes intersection dimensions from their cardinalities.
+All 840 cases cover every S3 active permutation, every nonidentity paid S3
+label and every rank-one idempotent on three scalar roles. All crossing
+lengths 1,2,3 and dirty-component counts 0,1,2 occur. This checks the local
+charge without matrix Gaussian elimination or the predicted decomposition.
+Both registered normal and optimized modes use explicit runtime checks.
+
+The written proof establishes the quantified theorem. These finite domains
+do not establish an arbitrary-word exclusion or audit a predecessor result.
+
+## Scope, sources and credit
+
+Scientific base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133755).
+The original card was `formal-interface-lemma`; this is a declared scope
+change to an elementary quantified proof of an explicitly open interface
+question. The selected source-binding positive control passed. The historical
+card command `research_baseline.py` raises `KeyError: 'bit_lower'` against the
+current selected certificate schema; neither command is a scientific replay.
+
+`SOURCES.json` pins the catalogue, selected record and merged predecessor
+notes as Git provenance. The pending #4783 is an exact external citation,
+not an imported executable or a source-history dependency. The proof is
+self-contained. No predecessor checker or finite receipt was replayed.
+
+The live overlap helper at 22:17-22:18 UTC on October 22 covered 380 open PRs
+and 3,860 Discussion records with complete pagination. Its local sparse scan
+covered 69 of 6,319 main notes. Distinctive `git grep origin/main` searches
+separately searched main README objects, and live merged/open PR searches
+and this account's last-hour claims were checked. No matching non-simple
+slack theorem was found in that coverage. Arbitrary diffs, unretained closed
+work and unpublished investigations remain outside coverage. This is not a
+novelty certificate.
+
+Related open work is #4783, the simple-label slack theorem; #4847, the exact
+scalar minimum for a supplied factor list under the same basis restriction;
+and #4851, shortest S3 word rigidity. This contribution proves a geometric
+slack inequality for a changed label alphabet. It does not extend the scalar
+classification or shortest-word result and compares no predecessor numbers.
+
+Credit Brian/JoyboyBrian #4783/#4765, Ross Richardson #1989/#1966,
+Adam Gall #1941, Sagar Thakrar #3888, Arham Tahir #2998,
+Nick Petalas #2583/#3408 and their retained register-model predecessors.
+The elementary Grassmann distance and linear complement arguments are
+standard; no literature-priority claim is made.
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Limits
+
+This is a fixed-word formal reduction. Native realization, physical scalar
+basis conversion, gauge restrictions, source access, ownership, hosting,
+precision, tape and complete supplier/outer admission remain unknown here.
+They are not zero-cost assumptions. No selected frontier changes.
+
+## Open next questions
+
+- Does a specified changed permutation-label target and paid budget make
+  this finite-role bound materially reduce a necessary search? First give
+  its full alphabet and endpoint crossing rank. A candidate with an actual
+  physical allowance is missing; this package does not justify a large census.
+- Can higher-rank scalar idempotents support a corresponding workspace
+  charge? First derive their exact crossing subspace and split requirement.
+  The rank-one image/functional argument does not establish that extension.
+
+## Implementation bounds
+
+Both Python files use explicit finite domains. Control flow is
+nonrecursive, functions are below 60 lines, and all domains are explicitly
+bounded: n<=5, at most six roles, prime fields 2,3,5 and at most 120 group
+labels. The largest regular-action fixture is 120 by 120. The nested split
+enumerates at most 3^5 scalar candidates; the independent oracle holds
+512-element sets in an 18-dimensional binary space. Python and standard-library
+allocations are bounded by these finite domains. There is no dynamic code
+generation or external process. Registered normal and optimized replays
+treat warnings as errors.

research/permutation-slack-workspace/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/s4-tight-word-spectator-elimination/README.md",
+      "usage": "provenance",
+      "git_blob": "8db05b993afe33649afd549f779c613a141806dc",
+      "sha256": "74f218e5cb2a28986b5db53ede7da419df5d719cd7c3bca0c955a354a24d92c4"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f",
+      "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154"
+    }
+  ]
+}