Scoped proof: label saturation narrows four swaps to 10 or 12 calls

research/coordinate-cnot-label-saturation/PROOF.md

@@ -0,0 +1,166 @@
+# Saturating one coordinate-CNOT label forces the direct bill
+
+This is a written theorem for the formal register model of commdata2338's
+PR1414/1491 and Cinna Davis's PR1541. The finite checks corroborate the
+argument; they are not its all-register justification. No physical supplier
+or multiplication exponent is claimed.
+
+## Model and statement
+
+Let `G=GL_2(F2)`, with `a=[[1,1],[0,1]]`, `b=[[1,0],[1,1]]` and
+`s=aba=bab=[[0,1],[1,0]]`. For finite `r>=t>=1`, work in the **formal**
+algebra `M_r(F2[G])`. One paid unit is
+
+`D_N(g)=I+([g]+1)N`, where `g` is only `a` or `b`, `N=uv^T`, and `v^T u=1`.
+
+Free scalar `GL_r(F2)` basis changes are allowed. Every address call,
+including an undo, costs one. No other address maps, copies, erasures,
+overwrites or clean allocation are available. The complete target is
+
+`T=I+([s]+1)P`, with `P=diag(I_t,0)`.
+
+All inputs are arbitrary. Every extra register is restored and may not leak
+into active outputs. Equality is in the group algebra, not merely its
+natural two-dimensional address representation. The direct bill is `3t`:
+use `bab` or `aba` on each active coordinate projector.
+
+**Label-saturation theorem.** Write `n_a,n_b` for the paid label counts.
+Every such word has `n_a,n_b>=t`. If `n_a=t`, then `n_b>=2t`; symmetrically,
+if `n_b=t`, then `n_a>=2t`. At equality `(t,2t)` or `(2t,t)`, every normalized
+paid projector satisfies `PN=N=NP`: the paid factors do not couple the
+restored dirty complement. This last claim concerns normalized paid factors,
+not the original placement of free scalar operations.
+
+## 1. Credited reductions
+
+Move all scalar basis changes to the right, conjugating each projector.
+Augmentation `[g]->1` sends each paid factor and the target to `I`, so the
+remaining scalar factor is `I`. Rank-one idempotence is preserved. This is
+the normalization used by Gareth Davidson's PR1333 and the later CNOT work.
+
+The sign quotient `G=S3 -> C2`, over
+`F2[C2]=F2[epsilon]/(epsilon^2)`, sends each `a,b,s` to `1+epsilon`.
+The normalized formal identity therefore gives
+
+`sum_all N_i=P`, and hence `n_a+n_b = t (mod 2)`.
+
+The matrix-sum identity is stronger than its trace consequence and is needed
+below. This is the sign argument of PR1414, reused with credit.
+
+Order coordinates by the two address components in the natural
+representation. Chronological **left** multiplication gives
+
+`a: [[I,N],[0,I]]`, `b: [[I,0],[N,I]]`,
+
+and the target is `[[I+P,P],[P,I+P]]`. Only an `a` call changes the top block
+row, with image in its vector `u`; only a `b` call changes the bottom block
+row. The two final off-diagonal blocks `P` imply
+
+`im P <= span(u_a)` and `im P <= span(u_b)`.
+
+Thus each label occurs at least `t` times. This is the image-span step of
+PR1541. A formal identity implies the represented identity; the converse is
+not assumed.
+
+## 2. Exactly t a calls make the top block row rigid
+
+Suppose `n_a=t`. The `t` vectors `u_a` are a basis of `im P`. Conjugate by a
+scalar basis change on `im P`, extended by the identity on `ker P`, so that
+the image vectors, in occurrence order, are `e_1,...,e_t`. This conjugation
+commutes with `P` and does not change the target or either count.
+
+Write the running natural matrix as `[[A,B],[C,D]]`. Each active top row
+is changed by exactly one call; all other top rows are unchanged. Top row
+`i` is initially `[e_i^T,0]` and finally `[0,e_i^T]`. Before its unique call
+it equals its initial row, and after that call it equals its final row.
+Both have the same row sum. Consequently
+
+`A+B=I` at **every** chronological cut.
+
+A `b` call with projector `N_j` changes `C+D` by
+`N_j(A+B)=N_j`. Initially and finally `C+D=I`, so
+
+`sum_b N_j=0`.
+
+Combine this with the full sign identity to obtain `sum_a N_i=P`. But
+`N_i=e_i v_i^T`, so comparison of its distinct rows gives `v_i=e_i`.
+Every `a` projector is therefore precisely `E_ii` in this basis.
+
+At the unique `a` call on row `i`, the needed top-row change is
+`[e_i^T,e_i^T]`. Since its covector is `e_i`, bottom row `i` at that instant
+is exactly this row. Its two block halves sum to zero. On the other hand,
+
+`C+D=I+sum_(b before a_i) N_j`.
+
+Taking row `i` gives
+
+`e_i^T = sum_(b before a_i) e_i^T N_j`.
+
+Each summand is a scalar multiple of `v_j^T`. Thus **every active coordinate
+covector belongs to the span of the b covectors**. This chronological step,
+together with the zero sum, is the additional ingredient.
+
+## 3. A zero rank-one sum must pay for both spans
+
+Let `m=n_b`, let `U` be the `r by m` matrix with columns `u_j`, and let `V`
+be the `m by r` matrix with rows `v_j^T`, over the `b` calls. We have
+
+`UV=sum_b N_j=0`, `rank U>=t`, and `rank V>=t`.
+
+Since `im V` is contained in `ker U`, rank-nullity gives
+
+`m >= rank U + rank V >= 2t`.
+
+This proves saturation. Exchanging the two address coordinates exchanges
+`a` and `b` while fixing `s`, giving the symmetric statement.
+
+If `m=2t`, both ranks are exactly `t`. Their column and row spans contain,
+respectively, the active coordinate space and its covector space, so those
+spans equal the active spaces. Each `b` image and covector has no dirty
+component. The `a` projectors are already `E_ii`. Undoing the scalar change
+that commutes with `P` gives `PN=N=NP` for every normalized paid factor.
+
+The proof uses no upper bound on `r` or `t`, no finite search, and no
+assumption that different projectors commute.
+
+## 4. Consequences and the unresolved case
+
+* **Three swaps cost nine with arbitrary finite dirty workspace.** A word
+  below nine has odd length and at least three of each label, so only seven
+  remains, with counts `(3,4)` or `(4,3)`. Saturation rules both out. Three
+  direct `bab` words attain nine in the full formal algebra. This is an
+  analytic alternative proof of PR1541's theorem; that predecessor retains
+  priority for the arbitrary-workspace result and its checked SAT proof.
+* **Four swaps need at least ten.** Below twelve, parity and the label floor
+  leave totals eight or ten. Saturation excludes `(4,4)`, `(4,6)` and
+  `(6,4)`. Only `(5,5)` at total ten remains. The direct twelve-call word
+  attains the upper bound. This covers arbitrary finite dirty workspace and
+  strengthens the `r=4`, `{8,10,12}` boundary reported in PR1705. It does
+  **not** prove the four-swap minimum is twelve or supply a ten-call word.
+
+For completeness, PR1541's compression step reduces that remaining ten-call
+case to at most six roles: put `L=span(u_a)+span(u_b)`. Both spans contain
+`im P`, so `dim L<=n_a+n_b-t=6`. Every paid projector preserves `L`, and its
+restriction remains rank-one idempotent because its image vector lies in
+`L` and its covector evaluates to one on that vector. Restrict the full
+formal identity to `L` and choose a basis of `im P` plus `L intersect ker P`.
+This gives four active swaps and at most two dirty roles, with the same ten
+paid calls. Compression is credited to PR1541, not claimed as new here.
+
+More generally, every potential saving below `3t` must have both counts at
+least `t+1`, as well as the retained sign parity. The theorem only screens
+this fixed two-label formal model; it does not exclude other alphabets.
+
+## Credit and limits
+
+Credit commdata2338 (PR1414/1491), Gareth Davidson (PR1333), Cinna Davis
+(PR1541), and Aaron Wang (PR1705), with exact heads in TASK.json. Eumemic
+(PR288), Ali Romman (PR468), and David Govea (PR720) supply surrounding
+rational/register-model lineage. This proof does not import the rational
+three-register obstruction into the nonabelian model.
+
+Prepared for Ross Richardson with substantial OpenAI Codex assistance.
+Apache-2.0. The written proof has not been checked by a proof assistant or
+independently reviewed by a human. Physical compiler/common-label realization,
+hosting, precision/tape, full selected cold replay and analytic transfer
+remain outside this contribution. No new kappa.

research/coordinate-cnot-label-saturation/README.md

@@ -0,0 +1,171 @@
+# Coordinate-CNOT label saturation with arbitrary dirty workspace
+
+**Scoped written theorem; no new kappa.** For `t` coordinate-SWAP targets in
+the formal `F2[GL_2(F2)]` register model, exactly `t` calls of one coordinate-CNOT
+label force at least `2t` calls of the other. This holds for any finite number
+of restored dirty registers and free scalar mixing. At the saturated `3t`
+boundary, the normalized paid factors do not couple the dirty complement.
+
+The [proof](PROOF.md) gives an analytic alternative to the finite step in
+Cinna Davis's [PR1541](https://github.com/CrocSwap/integer-mult-bounds/pull/1541)
+three-swap theorem, and strengthens Aaron Wang's
+[PR1705](https://github.com/CrocSwap/integer-mult-bounds/pull/1705) four-swap
+boundary:
+
+| Target | Established consequence |
+| --- | --- |
+| Three swaps, arbitrary finite dirty workspace | Exactly nine calls; predecessor result now has a short analytic proof |
+| Four swaps, arbitrary finite dirty workspace | Minimum is **ten or twelve**; a ten-call word must use **five of each label** |
+| Remaining ten-call case | PR1541's credited compression reduces it to at most six roles: four active and two dirty |
+
+There is **no ten-call construction or exclusion** here. PR1705 excluded
+two, four and six calls at exactly four registers and left `{8,10,12}`.
+The new saturation lemma excludes eight and the unbalanced ten-call counts,
+without a larger state census. The earlier three-swap result retains its
+predecessors' priority.
+
+## Exact model and complete optimistic bill
+
+The only paid address labels are
+`a=[[1,1],[0,1]]` and `b=[[1,0],[1,1]]`; `s=aba=bab` is the swap.
+Each unit call is `I+([g]+1)uv^T`, with binary `v^T u=1`. Free scalar
+`GL_r(F2)` mixing is normalized by augmentation. The endpoint is
+`diag([s],...,[s],1,...,1)` as a **full formal group-algebra matrix**.
+Every dirty input has its prescribed output; every undo call is charged.
+No other address maps, copies, erasures or clean allocation are allowed.
+
+The direct upper bill is `3t`, with no extra roles or scalar preparation.
+Scalar work and workspace are favorably free in the lower-bound model.
+An actual supplier would still need its physical/compiler, hosting,
+precision/tape and analytic costs. This replaces the rational abelian
+starting model with a specified nonabelian binary alphabet; it does not
+reduce rational frame entries modulo two.
+
+## Why the new inequality holds
+
+If there are only `t` a-calls, their image vectors form a basis of the active
+space. In that basis, each active top block row changes exactly once, from
+its input row to its output row. Its two block halves therefore always sum
+to the same row. The b-call projectors must sum to zero.
+
+The full sign-quotient matrix equation then forces every a-projector to be
+a coordinate projector. At each a-call, its bottom row forces an active
+coordinate covector into the span of the b covectors. The b image vectors
+already span the active space. Writing their zero sum as `UV=0` gives
+`n_b >= rank(U)+rank(V) >= 2t`.
+
+The chronological covector step matters: four legal rank-one projectors
+can sum to zero with image rank three but covector rank one. This explicit
+near miss rejects a tempting one-span-only argument. The full sign equation
+also cannot be replaced by its parity consequence.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B scripts/research_package.py --package research/coordinate-cnot-label-saturation
+```
+
+Or run the three checks directly:
+
+```sh
+python3.12 -I -B research/coordinate-cnot-label-saturation/verify.py
+python3.12 -I -B research/coordinate-cnot-label-saturation/independent.py
+python3.12 -I -O -B research/coordinate-cnot-label-saturation/test_package.py
+```
+
+Expected markers are `PASS_COORDINATE_CNOT_LABEL_SATURATION`,
+`PASS_INDEPENDENT_LABEL_SATURATION`, and five passing package test groups.
+`verify.py --write` explicitly regenerates the deterministic RESULT.json;
+normal replay is read-only. There is no SAT solver, heuristic pruning,
+floating-point acceptance or dependency installation.
+
+The two implementations share the stated mathematical model and receipt
+format but no executable code. The primary engine multiplies formal
+coefficients using actual binary address matrices. The second constructs
+permutations and their faithful regular operators, enumerating scalar
+projectors separately. Both were written by one Codex agent in this session.
+
+## Finite evidence and failure controls
+
+The written argument establishes the universal statement. The following
+bounded computations corroborate it and test the implementation:
+
+* Complete exact-length, label-count-indexed formal censuses through five
+  calls on one register and six on two. The two-register layer sizes are
+  `1,12,82,496,2640,13552,58408`. These are **not** shortest-distance layer
+  sizes: the same matrix at different label counts is deliberately retained.
+  Both engines independently obtain the same canonical complete-set hashes.
+* A complete `3+3` join enumerates all **1,296 literal six-call two-swap
+  words**, with a-count histogram `{2:324,3:648,4:324}`. The primary checker
+  verifies the normalization, every relevant chronological cut, both ranks
+  and equality-case workspace restriction on all **648 saturated words**.
+  The independent engine agrees on the complete sorted-word digest.
+* Twenty-five positive words cover `t=1..5`, both saturated labels, changed
+  active bases, and zero or one dirty extra. Five deliberately touch and
+  restore that extra using two additional paid calls. Full faithful forward
+  and reverse replay covers **1,080 columns** and rejects **235 individual
+  paid-call omissions**.
+* Fifteen primary controls cover six omissions, dirty leakage, a missing
+  target, changed/expanded labels, an illegal scalar projector, Boolean
+  input, the one-span and trace-only near misses, and a natural-representation
+  alias. The last is a nonzero formal off-diagonal perturbation with zero
+  natural image; it is not asserted to be a cheaper word.
+* Five package test groups exercise optimized read-only relocation, changed
+  and missing source bytes, false theorem/cut/count receipts, both-engine
+  word/census/attainer corruption, duplicate/nonfinite JSON and missing input
+  inventory. Integer receipt fields reject Boolean and floating aliases.
+
+The independent operator engine corroborates finite evidence. It does not
+formalize the universal proof or independently derive its ten-call bound.
+
+## Provenance, overlap and scope
+
+Base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Selected record SHA256:
+`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.
+Task `bit-new-register-model`, refined to a target-specific relaxation;
+OS chooser nonce `8e7454be62cc38c3ccc7edd6bd6d2bc2`. The alternative
+helper-contract card was not chosen because its immediate interface question
+is already covered by PR1194/1311 and subsequent feedback work.
+
+[TASK.json](TASK.json) records exact predecessor heads, the scope and overlap
+coverage. [SOURCES.json](SOURCES.json) pins the original task/selection and the
+unchanged PR1414 proof text. The later PR1541/1705 heads are contextual sources;
+no pending implementation or certificate is imported. Their credited
+compression argument is restated in PROOF.md.
+
+[Discussion #1715](https://github.com/CrocSwap/integer-mult-bounds/discussions/1715)
+holds the claim and handoff. The overlap search covers open PR bodies, local
+top-level package notes and the ledger, plus Discussion bodies/comments.
+It excludes arbitrary diffs/nested code and is not a novelty certificate.
+
+Selected-source binding and package verification are separate from complete
+selected cold replay. No full supplier replay, new recursive profile,
+physical adoption, Lean proof, independent human review, measured runtime
+gain or stronger multiplication exponent is claimed. Existing frozen sources
+and the selected frontier are unchanged.
+
+## Open next questions
+
+**Does the balanced ten-call four-swap word exist?** It is the sole remaining
+potential saving below twelve in this alphabet. First encode all `5+5` label
+patterns with at most six roles, using the credited compression, a full
+formal endpoint and a proof-producing solver. The blocker is the remaining
+noncommuting projector interaction; neither this theorem nor the small
+censuses decide it. A valid word would still need all physical supplier costs.
+This question is also structured in TASK.json.
+
+## Credit and license
+
+Credit **commdata2338 / PR1414 and PR1491** for the coordinate-CNOT model,
+sign quotient and two/three-swap results; **Gareth Davidson / PR1333** for
+scalar normalization and the restricted-alphabet question; **Cinna Davis /
+PR1541** for the arbitrary-workspace three-swap theorem and role compression;
+and **Aaron Wang / PR1705** for the four-register boundary and explicit
+unfinished search. Eumemic / PR288, Ali Romman / PR468 and David Govea / PR720
+retain the surrounding rational/register-model credit.
+
+Prepared for **Ross Richardson**, with substantial **OpenAI Codex assistance**
+in reasoning, implementation, verification and writing. One agent; no
+independent human or proof-assistant review. New work is Apache-2.0.