Prove exact fixed-factor dirty workspace and optimal split counts (no κ)

research/exact-factor-workspace/PROOF.md

@@ -0,0 +1,145 @@
+# Exact workspace under a single spectator basis change
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+This is a written scoped proof, with finite exact controls.
+
+## 1. Boundary and theorem
+
+Let F be any field and let R=A⊕S be a finite dimensional scalar role space.
+The original active coordinates A are fixed. Write n=dim S. Consider a fixed
+list of nonzero rank-one scalar couplings x_i y_i, with x_i∈R and y_i∈R*.
+Its paid factors may be I+λ_i x_i y_i over any unital F-algebra, with scalar
+coefficients central and λ_i nonzero. No commutativity between λ_i is needed.
+Idempotent couplings additionally satisfy y_i(x_i)=1.
+
+A permitted restriction chooses S=K⊕N, changes only the spectator basis,
+and discards the identity block N. Every original factor must be block
+diagonal on (A⊕K)⊕N, with its N block equal to identity. Thus the operation
+retains the actual couplings through a single invertible change of coordinates.
+It does not replace them by new couplings with the same contractions.
+
+Let u_i be the S component of x_i and v_i=y_i|_S. Set
+
+    U=span{u_i},  V=span{v_i},
+    u=dim U,  v=dim V,  t=rank(V×U→F),
+    d=u+v-t,  k=n-d.
+
+**Theorem.** The smallest possible dim K is exactly d. All optimal discarded
+spaces N are precisely the complements of U∩ann(V) inside ann(V). For each
+such N, all complements K to N in S containing U are optimal and permitted.
+
+If F has q elements, the numbers of distinct optimal discarded subspaces
+and ordered optimal retained/discarded decompositions are respectively
+
+    q^((u-t)k),                  q^(k(u+v-2t)).             (1)
+
+These count subspaces and ordered pairs of subspaces, not choices of bases.
+The theorem includes zero dimensional spaces, empty lists, arbitrary finite
+word lengths and dirty inputs. It requires no endpoint assumption.
+
+## 2. Factor support and the lower bound
+
+A nonzero rank-one outer product is supported on A⊕K precisely when its column
+lies in A⊕K and its functional vanishes on N. One direction follows by taking
+the outer product. For the other, any nonzero functional value exposes the
+column as the image of an input, and a nonzero column exposes every nonzero
+functional value. Multiplication by a nonzero scalar in F is injective even
+when the ambient F-algebra has zero divisors. A nonzero λ_i therefore does not
+hide a nonzero scalar coefficient of an off-diagonal block or N-block update.
+
+Consequently a split is permitted exactly when
+
+    U⊂K,                       N⊂F_0:=ann(V).             (2)
+
+Now dim F_0=n-v and W:=U∩F_0 has dimension u-t, by rank-nullity applied to
+U→V*. Since K∩N=0 and U⊂K, any permitted N is disjoint from W. Hence
+
+    dim N ≤ dim F_0-dim W = n-v-u+t = k.
+
+Since dim K=n-dim N, this proves dim K≥d. In particular d≤n once a permitted
+split is constructed. The full split K=S,N=0 also shows existence directly.
+
+## 3. Attainment and exact classification
+
+Choose any complement N of W in F_0. It has dimension k and is disjoint from
+U because N∩U=N∩W=0. Extend a basis of U together with a basis of N to a
+basis of S. Assign the added vectors to K along with U. This gives S=K⊕N,
+with dim K=n-k=d, and (2) makes every original factor legal after restriction.
+
+Conversely, an optimal split has dim N=k. Its inclusion in F_0 and trivial
+intersection with W imply F_0=W⊕N by dimensions. Thus these are all optimal
+discarded spaces. For each such N, exactly the complements K containing U
+satisfy the factor-support condition. This proves the stated classification.
+
+For F of size q, complements N to W in F_0 are graphs of arbitrary linear
+maps from one fixed k-dimensional complement to W. There are q^(k(u-t)).
+Fix N. The complements K to N in S are sections of S→S/N. The condition
+U⊂K fixes the section on the u-dimensional image of U. The remaining d-u
+directions can be lifted independently by any vector of N. There are
+q^(k(d-u))=q^(k(v-t)) choices. Multiply the two counts to obtain (1).
+The usual graph-of-a-linear-map complement count is standard linear algebra.
+
+## 4. Full words, endpoint restoration and the two contracts
+
+Choose any bases of an optimal K and N and prepend the unchanged basis of A.
+This is one scalar spectator-only basis change B. Each factor has the form
+
+    B^(-1) G_i B = G_i' ⊕ I_N.
+
+Therefore the same identity holds for every chronological partial product and
+the complete word, with the same ordered coefficient list. Self-contractions,
+nonzero rank-one status and idempotence are unchanged. If the original full
+endpoint is Q_A⊕I_S, the restricted endpoint is Q_A⊕I_K. This includes all
+dirty inputs and both off-diagonal endpoint blocks. Label-only prices and
+call counts are unchanged. B is a coordinate witness, not a priced physical
+conversion or an additional operation executed by the word.
+
+Brian's PR4783 proves that a normalized simple-label S4 word with m calls and
+ordered-pair crossing rank L admits such a restriction with dim K≤m-L.
+That theorem is a cited premise, not replayed here. The new exact answer d
+therefore satisfies d≤m-L on that domain. Computing d uses only the scalar
+couplings, and gives the exact dimension for this same restriction boundary.
+This proof itself also applies to other labels and fields. It does not
+extend Brian's inversion-slack inequality to those other alphabets.
+
+Gareth Davidson's PR2323 preserves active components and all contractions
+while replacing couplings. Its optimum is t, already proved there. It need
+not arise by a single invertible spectator basis change. The difference is
+
+    d-t=(u-t)+(v-t).
+
+Thus the new result counts the two pairing radicals that the stricter
+coordinate restriction must keep. It does not improve PR2323's resynthesis.
+
+The difference can be arbitrarily large even for restored words. For s≥1,
+take one active role e_0 and 2s dirty roles. For j=1,...,s use the idempotent
+
+    P_j=(e_0+e_j)(e_0*+e_(s+j)*).
+
+Over F2[S3], for two adjacent transpositions a,b, the formal factors
+G_a(P)=I+([a]+1)P and G_b(P)=I+([b]+1)P satisfy
+(G_a(P)G_b(P))^3=I. Concatenate these six-call relators for all P_j.
+Every dirty input is restored. Here u=v=s,t=0, so a single basis restriction
+requires 2s dirty roles, while contraction-preserving resynthesis needs zero.
+The endpoint itself is identity and has an empty word. This is a separation
+of preservation contracts, never an endpoint-workspace or paid-call lower bound.
+
+## 5. Verification and limits
+
+The finite verifier enumerates every scalar subspace pair in the declared
+small prime-field domains. A separate exhaustive oracle tries every ordered
+direct-sum decomposition and independently finds its minimum and both counts.
+It does not use the predicted minimum to prune candidates. Pairing rank is
+computed from the literal evaluation image rather than Gaussian elimination.
+
+Full-word controls use the faithful six-dimensional regular representation
+of S3, with every regular input column in every role. They check each original
+factor under an explicit invertible spectator basis, the discarded identity
+block, and both complete restored endpoints. The regular representation is
+faithful on the group algebra, so these are full formal equalities for those
+fixtures. General quantifiers follow from the proof above, not the census.
+
+Native address implementation, restricted scalar mixing, physical conversions,
+precision, tape costs, ownership, geometry, supplier admission and multiplication
+transfer remain separate obligations. No new κ or selected-frontier update is
+claimed. The result does not optimize workspace when factors can change.

research/exact-factor-workspace/README.md

@@ -0,0 +1,108 @@
+# Exact fixed-factor dirty workspace
+
+For a fixed rank-one word, one spectator-only basis change needs exactly
+
+    d = dim(U) + dim(V) - rank(V|U)
+
+retained dirty roles. Here U is the span of dirty column components and V
+the span of dirty row components. This is a scoped proof, with an exact finite
+certificate. It preserves the original active coordinates and every paid
+factor. It supplies no new κ or cheaper endpoint word.
+
+The result replaces an upper bound by the exact answer for the single-basis
+restriction used in [Brian's PR4783](https://github.com/CrocSwap/integer-mult-bounds/pull/4783).
+That predecessor gives d≤m-L for normalized simple-label S4 words. Its proof
+and executable are cited, not audited or replayed here. Our theorem works over
+any field and any unital algebra with central scalar coefficients. The S4
+inversion-slack inequality retains its predecessor's narrower hypotheses.
+
+[PROOF.md](PROOF.md) classifies every optimal retained/discarded splitting.
+Writing u=dim U, v=dim V, t=rank(V|U) and k=n-u-v+t, over a field of size q
+there are exactly q^((u-t)k) optimal discarded subspaces and
+q^(k(u+v-2t)) ordered optimal splittings. These count subspaces, not bases.
+
+[Gareth Davidson's PR2323](https://github.com/CrocSwap/integer-mult-bounds/pull/2323)
+already gives the smaller optimum t when one can replace the factors while
+preserving their contractions. Our stricter preservation boundary keeps both
+pairing radicals. The difference can be arbitrarily large even for words that
+restore every dirty input. It is not a contradiction or an improvement of
+that resynthesis theorem. No literature-priority claim is made for elementary
+subspace and complement arguments.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/exact-factor-workspace
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/exact-factor-workspace/verify.py
+```
+
+`verify.py` enumerates all subspace pairs over F2 in dimensions 0 through 4,
+F3 in dimensions 0 through 3 and F5 in dimensions 0 through 2. Its independent
+minimum oracle enumerates every ordered direct-sum decomposition without
+formula-based pruning. It checks the exact dimension and both optimal counts.
+Seven restored S3 word fixtures check all formal factors and endpoints through
+the faithful regular representation, including one-sided, paired, orthogonal
+and dense dirty couplings. All 5,669 subspace pairs agree with the minimum
+and both counts. Exact coverage and transcript hashes are generated
+in [RESULT.json](RESULT.json). Every package source file is hash-bound.
+
+Both registered commands are read-only. To regenerate the receipt, use
+`verify.py --write-result /an/unoccupied/path.json` and compare the generated
+file with RESULT.json. The direct verifier works from a Git-free package copy.
+Receipt generation refuses an occupied output path. Verification remains
+active when Python assertions are disabled.
+
+## Scope and family decision
+
+This changes the bit-new-register-model card to a formal workspace-interface
+classification. It avoids an unbounded workspace search for a supplied word,
+while retaining the exact coordinate-preservation boundary. It is a local
+module, not a new native mechanism or complete supplier. Stop after this
+classification. Physical scalar conversion, restricted gauges, native access,
+ownership, precision/tape costs and admission remain unknown, not zero.
+
+The current selected source-binding positive control passed. The card's older
+`scripts/research_baseline.py` fails with `KeyError: 'bit_lower'` on the current
+selected certificate. That unrelated script is unchanged. No historical
+construction replay, C++, Lean or Docker check is needed for this theorem.
+
+The verifier follows structured, nonrecursive control flow with fixed census
+domains. Its largest universe has 27 vectors and its largest subspace family
+has 67 members. Functions are below 60 lines. A managed-runtime allocation
+deviation applies to Python tuples, sets and arbitrary-precision integers;
+the fixed domains bound their live sizes. There is no steady service loop or
+unbounded search. The warning-strict registered normal and optimized runs
+check the complete declared domain. Reassess these bounds before widening it.
+
+## Open next questions
+
+- Can the exact coordinate restriction be computed efficiently for a large
+  supplied word with additional support constraints? Start with one actual
+  native layout and characterize the legal spectator basis changes. The full
+  GL model here does not pay or preserve those physical restrictions.
+- Which target needs less workspace after changing its factors? Specify an
+  endpoint and paid budget, then use the existing contraction-preserving
+  theorem where its alphabet is closed. This package gives no endpoint optimum.
+
+## Sources and credit
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+
+Credit Brian/JoyboyBrian PR4783 and PR4765 for the single-basis spectator
+restriction and inversion-slack context; Gareth Davidson/bitplane PR2323 for
+the exact contraction-preserving pairing compression; Cinna Davis/1337isnot1337
+PR1541 for image-span restriction; ToikY PR1662/1680 for the UT4 span and
+orientation reductions; and the register-model and cut predecessors credited
+by those packages. None of their mathematics or counts is a new deliverable
+here. [SOURCES.json](SOURCES.json) pins provenance, including the pending
+PR4783 citation, without importing predecessor executables.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133318)
+records canonical main 624de9dc66858af0945e5f8a0942488d62280d43 and priority
+revision 7. Entry overlap checked live open PRs, recent claims, merged searches
+and distinctive all-main README/proof terms. The cache covered 365 open PRs
+and 3,819 Discussion records. Sparse local notes, nested source differences
+and unpublished work are incompletely covered. No novelty certificate,
+independent human review or formal proof-kernel acceptance is claimed.