Prove the A4 eight-call floor with arbitrary dirty workspace (no new κ)

research/a4-dirty-workspace-minimum/PROOF.md

@@ -0,0 +1,113 @@
+# Tight radical rank removes all dirty workspace
+
+## Statement and cited premises
+
+Let `a=(123)`, `b=(124)`, `c=aba^-1b^-1`, and `d=ab` in A4.
+For every finite `r>=4`, the exact minimum number of paid factors for
+`T_r=diag([a],[b],[c],[d],1,...,1)` is eight in the following model.
+Work over `F2[A4]`. A paid factor is `D_N(g)=I+([g]+1)N`, where g is
+a or b and `N=xy^T` is a binary rank-one idempotent, so `y^T x=1`.
+Scalar `GL_r(F2)` maps are free. All r inputs are arbitrary, and the
+complete formal operator must equal `T_r`. There are no clean roles,
+COPY, ERASE, other address letters or free inverses. Restoration is paid.
+
+The new assertion is that a hypothetical six-call word on any r roles
+restricts to a legal six-call word on four roles. The eight-call conclusion
+uses two cited premises, neither audited or replayed here.
+
+* Cinna Davis #2116 excludes words of length at most six on four roles by
+  a finite exact group-algebra certificate. Sagar Thakrar #4032 retains
+  that exclusion with two further exact joins.
+* Sagar Thakrar #4032 proves `n_a,n_b>=3` and `n_a=n_b mod 3` at every
+  finite role count. Its twisted-functional decompositions below have
+  rank three for each letter. These are written all-role statements.
+
+SOURCES.json pins both packages at the base commit. The six-call exclusion
+remains a finite-certificate dependency. No wholly written replacement for
+that exclusion is claimed.
+
+## 1. Normalize scalar maps
+
+Binary scalar conjugation preserves rank-one idempotents. Collect all free
+scalar maps at one end of the word. Augmentation to F2 sends every paid
+factor and `T_r` to `I_r`, so the collected scalar map is `I_r`. We may
+therefore use a pure paid word in the original target coordinates.
+Let H be the binary span of the first four coordinate vectors.
+
+## 2. Rank saturation
+
+Over any extension K of F2, suppose `D=sum_(j=1)^q x_j v_j`, with binary
+columns `x_j`, K-rows `v_j`, and `rank_K D=q`. The column span of D is
+contained in the K-span of the q columns `x_j`. Both spaces have dimension
+q and hence are equal. Every `x_j` belongs to `col_K D`. If that space is
+a coordinate space, all entries outside it vanish in every `x_j`.
+
+## 3. Apply equality to both letters
+
+Assume a six-call word equals `T_r`. The inherited floors force
+`n_a=n_b=3`. In #4032's base-a splitting, each paid factor is `B_k E_k`.
+The semisimple factor is `B_k=D_(N_k)(a)` for an a-call and
+`B_k=D_(N_k)(a^2)` for a b-call. The latter has radical part
+`E_k=I+([d]+1)N_k` because `b=a^2 d`. Set `C_k=B_(k+1)...B_L`.
+
+The inherited twisted functional Phi to F4 gives
+
+```text
+diag(0,mu(d),mu(c),mu(d),0,...,0)
+  = sum_(b calls k) aug(C_k)^-1 mu(d) x_k y_k^T psi(C_k).
+```
+
+The three nonzero diagonal entries are nonzero because mu is injective
+on the Klein four subgroup. Every `B_k` has augmentation `I_r`, since
+`aug([a]+1)=aug([a^2]+1)=0`. Thus `aug(C_k)=I_r`, not an unspecified
+invertible map. There are exactly three summands. Section 2 places every
+b-call column in `H_b=span_F2(e_2,e_3,e_4)`.
+
+Using base b instead and putting `e=ba`, the inherited defect is
+`diag(mu(e),0,mu(c),mu(d),0,...,0)`. Its suffixes again have augmentation
+identity. Section 2 places every a-call column in
+`H_a=span_F2(e_1,e_3,e_4)`.
+
+Consequently every paid output column `x_k` belongs to H. The rows
+`y_k^T` may still read arbitrary extra dirty inputs.
+
+## 4. Restrict each factor
+
+In the split into H and its coordinate complement, write `x_k=(x'_k,0)`
+and `y_k=(y'_k,y''_k)`. The column `x'_k` is nonzero and
+`(y'_k)^T x'_k=y_k^T x_k=1`. Hence `N'_k=x'_k(y'_k)^T` is a nonzero
+binary rank-one idempotent on four roles. Each factor has block form
+
+```text
+[ D_(N'_k)(g_k)    * ]
+[       0         I ].
+```
+
+Taking the upper-left block commutes with multiplication of these block
+matrices. The six restricted factors therefore have product `T_4`, in
+contradiction to the cited four-role finite exclusion. Dependence on dirty
+inputs in the upper-right blocks cannot change this product identity.
+
+## 5. Exact minimum and limits
+
+The inherited floors exclude lengths at most five. At seven calls they
+allow only `(3,4)` and `(4,3)`, which violate `n_a=n_b mod 3`.
+Section 4 excludes six. Separate-coordinate words `a`, `b`, `abba`, `ab`
+use eight calls and extend by identity on every extra role. Eight is thus
+exact for every finite r, using the cited certificate and written identities.
+
+This is an abstract register obstruction, not a physical supplier. Other
+fields, nilpotent couplings, changed alphabets and different targets are
+outside the statement. No new kappa, selected-frontier change, full
+multiplication theorem or proof-kernel acceptance is claimed.
+
+## Credit
+
+The compression argument is produced by Nick Petalas. Sagar Thakrar #4032
+supplies the radical-rank decompositions, all-role floors and determinant
+congruence. Cinna Davis #2116 supplies the model, target, direct word and
+finite four-role exclusion. Retain Cinna Davis #2047/#2248/#2085,
+juper997 #1478, woklerx #1443, Gareth Davidson #1333, commdata2338 #1414,
+eumemic #288, Ali Romman #468 and the register-model lineage credited by
+those predecessors. Rank saturation and invariant-subspace restriction
+are classical linear algebra. Apache-2.0.

research/a4-dirty-workspace-minimum/README.md

@@ -0,0 +1,150 @@
+# The A4 eight-call floor survives arbitrary dirty workspace
+
+For every finite `r>=4`, the formal endpoint
+`diag([a],[b],[aba^-1b^-1],[ab],1,...,1)` over `F2[A4]` has exact paid-call
+minimum **eight**, with arbitrary restored dirty roles, rank-one idempotent
+couplings, positive a/b calls and free binary scalar mixing.
+
+The new result is a **scoped written workspace-compression proof** with
+finite exact corroboration. Any hypothetical six-call word compresses to
+the original four target roles. The minimum-eight corollary uses Cinna
+Davis's [#2116](https://github.com/CrocSwap/integer-mult-bounds/pull/2116)
+finite four-role exclusion and Sagar Thakrar's
+[#4032](https://github.com/CrocSwap/integer-mult-bounds/pull/4032) all-role
+radical-rank and determinant bounds as cited premises. Their searches and
+proof checks are not replayed or audited here. This does not replace the
+finite six-call exclusion with a wholly written proof.
+
+No new kappa, selected-frontier change or physical supplier is claimed.
+
+## The new step
+
+[PROOF.md](PROOF.md) gives the model and full argument. At six calls, both
+letters must attain their inherited rank-three floors. The augmentation
+of every semisimple suffix is identity, so equality forces each b-call's
+original binary output column into coordinates 2,3,4, and each a-call's
+column into coordinates 1,3,4. Every factor consequently has the form
+
+```text
+[ four-role paid factor    arbitrary dirty-input reads ]
+[          0                         I                ].
+```
+
+Restricting to the first four roles preserves the nonzero rank-one
+idempotent contract and commutes with multiplication. The restricted
+six-call word would realize the four-role target excluded by #2116/#4032.
+Their all-role lower bounds already exclude every other length below eight.
+The inherited direct eight-call word extends by identity on extra roles.
+
+This answers the restored-workspace gap in #4032's scope. A coefficient
+search on more roles cannot rescue a six-call word for this endpoint.
+The rank-saturation step is essential: the checker includes four nonzero
+rank-one summands of a rank-three target whose dirty output columns cancel.
+Thus a version of the argument with slack in the call count would fail.
+
+## Evidence and reproduction
+
+From the repository root, use standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a4-dirty-workspace-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/a4-dirty-workspace-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a4-dirty-workspace-minimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a4-dirty-workspace-minimum --check-source-history
+```
+
+Any installed CPython 3.12 may replace that interpreter path. The standalone
+verifier also works in a Git-free export. Expected markers are
+`PASS_A4_DIRTY_WORKSPACE_MINIMUM` and `PASS_REGISTERED_RESEARCH_PACKAGE`.
+Normal and optimized replay run the same explicit checks.
+
+The checker enumerates all 29,791 ordered triples of nonzero binary columns
+in five dimensions. Of these, 26,040 are independent. For each independent
+triple and both diagonal support patterns, F4 augmented-matrix elimination
+agrees with a separate oracle enumerating the binary column span. Exactly
+336 triple/support pairs are compatible, and every compatible triple lies
+in the required coordinate support. These are new rank-saturation fixtures,
+not a census of predecessor words.
+
+The literal A4 regular action checks all 3,600 admitted single factors whose
+output columns lie in the first four coordinates, across role counts 4..7.
+An additional 256 deterministic words have lengths 2..8. The resulting
+3,856 word fixtures check 287,616 complete role/address basis columns,
+including every extra-role input column. Their lower blocks are identity
+and their upper-left blocks equal the products of the restricted factors.
+Dirty inputs may feed target outputs; no clean-input assumption is made.
+The direct eight-call upper bound checks a further 264 basis columns at
+role counts 4..7. Seven malformed field/coupling inputs reject, and the
+rank-slack counterexample passes as a boundary control. A separate positive
+fixture requires an extra dirty input to contribute to a target output.
+Field arithmetic
+also checks the defining polynomial, associativity and distributivity.
+
+Each run generates a receipt binding all six package files by SHA256 and
+prints it to stdout. `--emit` prints only that generated receipt. There is
+no handwritten or frozen receipt and no default filesystem output. The
+finite tests corroborate the new linear-algebra implication; universal
+coverage comes from the written proof. Hosted replay and scientific
+acceptance are separate from these checks.
+
+## Scope, sources and costs
+
+The scientific base is canonical main
+`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7.
+[SOURCES.json](SOURCES.json) pins the predecessor READMEs and #2116's
+RESULT.json as historical mathematical premises. They are not runtime
+inputs. No predecessor executable, generated search output or numerical
+count is imported by this verifier. Frozen predecessor files stay intact.
+
+[TASK.json](TASK.json) records a changed `bit-new-register-model` scope.
+This is a formal-model side result rather than a new native alphabet.
+The card's current first-step substitute, `research_selected_baseline.py`,
+passed its source-binding orientation check. That is not evidence for this
+theorem. The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145499)
+precedes the proof and finite corroboration. Entry overlap coverage includes
+live PRs, recent handoffs, active Discussions, merged A4/workspace searches
+and all-main README terms. Sparse cached local coverage and unpublished
+work remain limitations; search absence is not a novelty certificate.
+
+Every role in this formal contract has arbitrary data and must satisfy the
+full endpoint. There are no extra preparation or restoration calls in the
+coordinate upper bound. Native implementation, frames, ownership, routing,
+hosting, precision/tape, stock, recursive child ranks, compiler and outer
+admission remain unpriced and unproved. Unknown costs are not zero.
+No physical expansion round is proposed. Nilpotent couplings, other fields,
+other targets or alphabets are outside the theorem. Lean, Docker, selected
+cold replay and independent human or proof-kernel review are unrun.
+
+## Engineering constraints
+
+Build the Lever supplies a rerunnable exact checker. Prove It Works requires
+full literal operator columns for restriction, including dirty inputs.
+Power of Ten bounds all code loops by fixed domains, at most seven roles,
+eight factors, 84 regular coordinates and matrices of shape at most 8 by 8.
+Every function is below 60 physical lines. Acceptance uses explicit
+exceptions that remain active under optimization. There is no recursion,
+subprocess, dynamic import, shared mutable state or runtime code generation.
+Managed Python allocation is a bounded rule-3 deviation; allocator internals
+are not inspected. Each local file read is capped at 128 KiB. Warning-strict
+normal and optimized registered checks provide recurring diagnostics.
+
+## Open next questions
+
+Can the original four-role six-call exclusion be replaced by a wholly written
+contradiction? This would remove the finite-certificate dependency from the
+all-workspace theorem. Start with compatibility of the two tight rank-three
+decompositions on the four target coordinates, or their second radical-layer
+coefficients. The missing compatibility argument is the blocker. This package
+does not reserve that question. Its structured form is in TASK.json.
+
+## Credit
+
+This contribution is produced by Nick Petalas. Sagar Thakrar #4032 supplies
+the radical-rank identities, all-role floors and determinant congruence.
+Cinna Davis #2116 supplies the alphabet, endpoint, coordinate word and
+finite four-role exclusion. Retain Cinna Davis #2047/#2248/#2085,
+juper997 #1478, woklerx #1443, Gareth Davidson #1333, commdata2338 #1414,
+eumemic #288, Ali Romman #468 and the retained register-model lineage.
+The new step is tight-rank workspace compression, not the predecessor
+four-role optimum. The underlying rank and restriction facts are classical.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

research/a4-dirty-workspace-minimum/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "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/a4-seven-call-radical-rank/README.md",
+      "usage": "provenance",
+      "git_blob": "ab5ea83019119dcada4b654b137d418503014cf5",
+      "sha256": "26c9a90b1e73ce90b6711417db3f023e79192acdde8b94f1e7cfa0a93fafd42b"
+    },
+    {
+      "path": "research/a4-commutator-four-role-seed-dcbf/README.md",
+      "usage": "provenance",
+      "git_blob": "4611a7e147edc288c0355207dde2174f7867e523",
+      "sha256": "07d90cc975b359e30ff4b978130c4d1893d610ff244aa29e71f3a891abdb33ba"
+    },
+    {
+      "path": "research/a4-commutator-four-role-seed-dcbf/RESULT.json",
+      "usage": "provenance",
+      "git_blob": "fa78cc9381f27efea106aac5947a465daa89b795",
+      "sha256": "2ff56618b041bbfe7d8c3c4e521cdf1b33b70d0f7299c1f56c780e76ec40a5c6"
+    }
+  ]
+}