Prove the SL2(F3) five-call minimum with arbitrary dirty workspace

research/sl2f3-all-dirty-minimum/PROOF.md

@@ -0,0 +1,174 @@
+# Five calls with any finite number of restored dirty roles
+
+This proof was produced by Nick Petalas. It extends Wentao Li's #4083 beyond
+one dirty role. The endpoint, alphabet and direct word come from Cinna Davis's
+#2010. The first-order argument builds on Sagar Thakrar's #4032 twisted
+radical-rank method. The proof below supplies the new all-role lower bound.
+
+## Statement and conventions
+
+Let G = SL2(F3), with matrix multiplication as its group law, and set
+
+```
+i = [[0,1],[-1,0]],    w = [[0,-1],[1,-1]],    c = w^-1 i w.
+```
+
+For every integer r >= 3, work in M_r(F2[G]). A paid factor is
+
+```
+D_N(g) = I + ([g]+[1])N,
+g in {i,i^-1,w,w^-1},    N = x y^t,    x,y in F2^r,    y^t x = 1.
+```
+
+The target is T = diag([i],[w],[c],1,...,1). All r roles have arbitrary
+initial values; the last r-3 roles must be restored. Arbitrary free constant
+GL_r(F2) mixing is allowed. Products are written as algebraic matrix products.
+
+**Theorem.** Every word realizing T contains at least two i/i^-1 factors and
+at least three w/w^-1 factors. The exact minimum is five for every finite r.
+
+The field of role coefficients is F2. Enlarging it is a change of model.
+Formal group-algebra equality, including all dirty roles, is required.
+
+## 1. A first-order representation of the semidirect product
+
+Let P = {+/-1,+/-i,+/-c,+/-ic}. Direct multiplication of the displayed
+matrices gives the quaternion relations i^2 = c^2 = -1 and ci = -ic.
+The matrix w has order three, and conjugation by w^-1 cycles the three
+nonzero classes i,c,ic of P/{+/-1}. Thus P is normal, P intersect <w> = {1},
+and G = <w>P has a unique expression w^a p, a in {0,1,2}, p in P.
+Indeed these expressions give 24 distinct determinant-one matrices, which
+exhaust G since its first column has 8 choices and its second then has 3.
+
+Write K = F4 = F2[omega], omega^2+omega+1 = 0. Define the additive map
+
+```
+mu(+/-1)=0,    mu(+/-i)=1,    mu(+/-c)=omega,    mu(+/-ic)=omega^2.
+```
+
+It is the identification of the binary vector space P/{+/-1} with K.
+The conjugation cycle gives mu(w^-1 p w) = mu(p) omega. For g = w^a p put
+
+```
+psi(g) = omega^a,    delta(g) = mu(p).
+```
+
+For g=w^a p and h=w^b q, gh=w^(a+b)(w^-b p w^b)q. Hence
+
+```
+psi(gh) = psi(g)psi(h),
+delta(gh) = delta(h) + delta(g)psi(h).
+```
+
+Extend psi and delta linearly to F2[G], and let aug be augmentation into F2.
+Linearity gives, for all group-algebra elements A,B,
+
+```
+delta(AB) = aug(A)delta(B) + delta(A)psi(B).
+```
+
+Apply these maps entrywise to matrices. The same identity holds with matrix
+products on the right. This is a first-order representation, equivalently
+the upper-right block of the homomorphism
+g -> [[1,delta(g)],[0,psi(g)]]. It does not assume that delta is multiplicative.
+
+## 2. Two quaternion calls are necessary
+
+Every paid factor has augmentation I. For W=F_1...F_L, repeated use of the
+matrix identity gives
+
+```
+delta(W) = sum_k delta(F_k) psi(F_(k+1)...F_L).
+```
+
+For F_k=D_N(g), delta(F_k)=delta(g)N. In our alphabet,
+delta(i)=delta(i^-1)=1 and delta(w)=delta(w^-1)=0. Each nonzero summand has
+K-rank at most one, because N has rank one. Thus
+
+```
+rank_K delta(W) <= number of i/i^-1 calls.
+```
+
+But delta(T)=diag(1,0,omega,0,...,0) has rank two. This proves the first floor
+for every r. This step is the semidirect-product extension of the predecessor's
+first-order rank argument needed here. No census is involved.
+
+## 3. At most two order-three calls are rigid
+
+Put E=diag(0,1,0,...,0). The character image of the target is
+
+```
+psi(T) = I + omega^2 E.
+```
+
+Quaternion calls map to I. A w call maps to I+omega^2 N; a w^-1 call maps
+to I+omega N. By the matrix determinant lemma their determinants are omega
+and omega^-1, respectively. The target determinant is omega.
+
+If there are no w/w^-1 calls, the determinant is wrong. If there is one,
+it must be a w call, and equality of its character image with psi(T) forces
+its projector to be E.
+
+If there are two, the determinant forces both labels to be w^-1. Write
+their binary projectors N,M in product order. Their character product is
+
+```
+(I+omega N)(I+omega M)
+ = I + NM + omega(N+M+NM),
+```
+
+whereas the target is I+E+omega E. Comparing coefficients in the binary basis
+{1,omega} gives NM=E and N+M+NM=E. Therefore N=M; idempotence then gives
+N=M=E. This argument uses binary role coefficients and holds for every r.
+
+It follows that if there are at most two order-three calls, every character
+suffix psi(F_(k+1)...F_L) is diagonal and fixes every column other than
+column 2. Quaternion factors have identity character, and the only remaining
+projector is E.
+
+## 4. The conjugated output forbids those rigid cases
+
+Use the sum in Section 2. Each quaternion contribution is N times a character
+suffix. Since N is binary and that suffix fixes every column other than
+column 2, every entry of delta(W) outside column 2 lies in F2. The other
+paid calls contribute zero.
+
+The target has delta(T)_(3,3)=omega, which is not in F2. Column 3 is different
+from column 2. This contradicts W=T. Therefore there are at least three
+w/w^-1 calls. Combined with Section 2, the length is at least five.
+
+## 5. Attainment and free mixing
+
+The inherited direct word applies i on role 1, w on role 2, and the algebraic
+product w^-1 i w on role 3. These are five paid calls with coordinate
+projectors. They have the required endpoint and act identically on every
+other role, independently of its initial value. Thus the lower bound is sharp.
+
+To include interleaved constant GL_r(F2) maps, move them to one end using
+
+```
+A^-1 D_N(g) A = D_(A^-1 N A)(g).
+```
+
+Conjugation preserves binary rank-one idempotents. The resulting expression
+is H times a pure paid word of the same length, with H in GL_r(F2).
+Augmentation of every paid factor and of T is I, so H=I. The preceding
+argument therefore covers arbitrary such free mixing and every finite amount
+of restored dirty workspace.
+
+## Scope and decision
+
+This is a scoped proof in the formal alphabet of #2010/#4083. It closes the
+two-or-more-dirty-role question in #4083 without enumerating a larger alphabet.
+Searching additional restored dirty roles cannot improve this endpoint's
+five-call bill under these hypotheses. The original three-role and one-dirty-role
+results retain predecessor credit; their enumerations are not replayed here.
+
+Clean-only inputs, partially restored roles, enlarged coefficient fields,
+different paid address operations and other targets are outside this theorem.
+The first-order map also kills the nontrivial central element -1, so it supplies
+no positive lower bound for a pure central defect. No native implementation,
+physical cost, admitted supplier, multiplication theorem or new kappa follows.
+The written proof is the all-r evidence. The verifier only corroborates finite
+instances and exposes boundary failures. Independent human and formal
+proof-kernel review are unclaimed.

research/sl2f3-all-dirty-minimum/README.md

@@ -0,0 +1,123 @@
+# The SL2(F3) conjugate triple needs five calls with any dirty workspace
+
+For every finite number of restored dirty roles, the exact formal paid-call
+minimum for `diag([i],[w],[w^-1 i w],1,...,1)` remains **five**. This is a
+scoped proof with finite corroboration. It answers Open next question 1 in
+Wentao Li's [#4083](https://github.com/CrocSwap/integer-mult-bounds/pull/4083),
+which settled one dirty role and left two or more open.
+
+The alphabet is unchanged: `G=SL2(F3)`, paid labels `i,i^-1,w,w^-1`, and
+`D_N(g)=I+([g]+[1])N` for any binary rank-one idempotent `N` on all roles.
+Here `i=[[0,1],[-1,0]]`, `w=[[0,-1],[1,-1]]` over F3. Arbitrary constant
+`GL_r(F2)` mixing is free; every input is arbitrary and every extra role must
+return unchanged. [PROOF.md](PROOF.md) proves the result for every `r>=3`.
+
+## New step and consequence
+
+The first-order representation of `Q8 semidirect C3` gives a rank-two target
+defect, forcing two quaternion-label calls. In the character quotient, any
+one- or two-call realization of the required order-three output has all its
+projectors on that output alone. Its other columns cannot acquire the
+nonbinary first-order coefficient of `w^-1 i w`. Therefore three order-three
+calls are necessary, independently of the number of restored dirty roles.
+The predecessor's coordinate word attains `2+3=5`.
+
+The new contribution is this all-role proof and the order-three projector
+rigidity argument. Cinna Davis's original three-role result
+[#2010](https://github.com/CrocSwap/integer-mult-bounds/pull/2010) and Wentao
+Li's one-dirty-role result retain their credit. Their searches are not rerun.
+Sagar Thakrar's [#4032](https://github.com/CrocSwap/integer-mult-bounds/pull/4032)
+supplies the predecessor twisted radical-rank method and the question about
+extending it to a normal 2-group with an odd-order complement.
+
+Further dirty-role censuses cannot improve this endpoint under these
+hypotheses. The decision is local to this formal alphabet. A physical native
+realization, its prices, supplier admission and a new kappa remain unproved.
+Clean-only inputs, partial restoration, other targets and enlarged coefficient
+fields are outside the result. In particular the first-order map kills the
+nonidentity central element -1; it cannot certify pure central defects.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and only the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/sl2f3-all-dirty-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/sl2f3-all-dirty-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sl2f3-all-dirty-minimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sl2f3-all-dirty-minimum --check-source-history
+```
+
+The registered commands use `{python}` for portability. The expected final
+marker is `PASS_SL2F3_ALL_DIRTY_MINIMUM minimum=5 i_floor=2 w_floor=3`.
+The verifier prints a generated receipt bound to all six package file hashes;
+it does not write files. No receipt is hand-authored or stored as an expected
+answer.
+
+Finite coverage is separate from the all-role proof:
+
+- All 576 group-pair cocycle identities.
+- All 308 one-call and 60,880 two-call quotient words on 2, 3 and 4 roles.
+  Exactly one of each length reaches the quotient target at each role count.
+- 312 deterministic sampled full-group-algebra words on 3, 5 and 8 roles,
+  with lengths 0 through 12. These are samples, not an exhaustive word census.
+- The five-call endpoint on all 384 regular-action basis inputs across
+  3, 5 and 8 roles, including two and five dirty roles.
+- Eleven enumerated controls: the five single-call omissions, reversed
+  conjugation, unrestored dirty output, a changed unconjugated target,
+  nonbinary projectors, wrong cocycle orientation and the central kernel.
+
+The nonbinary control exhibits two distinct F4 rank-one idempotents with
+the same quotient endpoint; the binary rigidity proof cannot be reused in
+that enlarged field. The dirty-output control passes data-only comparison
+and fails the required full endpoint. Checks use explicit exceptions under
+both normal and optimized Python.
+
+## Verification bounds
+
+All code is package-local; no predecessor executable is imported. Loops have
+fixed finite bounds, matrices have at most eight rows, sampled words have at
+most twelve factors, and the largest materialized quotient alphabet has 240
+entries. Its two-call product is streamed. Functions are below 60 lines.
+Warning-strict normal and optimized execution are the available diagnostics;
+the checkout supplies no Python linter configuration or installed static
+checker for this package.
+
+```
+Rule: 3, fixed memory before steady operation.
+Location: verify.py exact finite computations.
+Reason: CPython allocates integers, tuples and interpreter objects dynamically.
+Scope: this bounded one-shot verifier, with no input-driven growth.
+Compensating control: eight-role/twelve-factor limits and fixed fixture counts.
+Verification: both registered warning-strict replays exercise all fixtures.
+Follow-up: use fixed buffers if this verifier becomes a long-running service.
+```
+
+Sources, exact Git blobs and SHA256 hashes are in [SOURCES.json](SOURCES.json).
+Those literature and task files are provenance, not replay dependencies.
+[TASK.json](TASK.json) records the priority-7 card and the changed scope.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Is there a fully priced native address-operation realization of this alphabet
+for a changed endpoint that could save paid work? This is the remaining
+physical-interface question from #4083, not a reason to enlarge the closed
+dirty-workspace search. Start by pinning one arbitrary-input `D_N(i)` or
+`D_N(w)` program and charging address movement, source access, hosting and
+restoration. The missing native implementation and complete producer/consumer
+bill are the blockers. No such program is supplied here.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Cinna Davis #2010 retains the endpoint, four-label alphabet and five-call
+direct word. Wentao Li / VictorLiwentao #4083 retains the one-dirty-role
+result and the explicit remaining question. Sagar Thakrar #4032 retains the
+twisted radical-rank method and its normal-2-group extension question, building
+on Cinna Davis #2116, #2047 and #2248. The retained register-model lineage
+includes Aaron Wang / navinor #1822, Ali Romman #468 and eumemic #288.
+The first-order representation and rank subadditivity are elementary tools;
+no literature-wide priority is claimed for them. The new claim is the stated
+all-role endpoint theorem and its explicit proof.

research/sl2f3-all-dirty-minimum/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/a4-seven-call-radical-rank/README.md",
+      "usage": "provenance",
+      "git_blob": "ab5ea83019119dcada4b654b137d418503014cf5",
+      "sha256": "26c9a90b1e73ce90b6711417db3f023e79192acdde8b94f1e7cfa0a93fafd42b"
+    },
+    {
+      "path": "research/sl2f3-conjugate-triple-seed592f/README.md",
+      "usage": "provenance",
+      "git_blob": "519b393c8cc7c6aba947b43d9c03bfa7591ed98a",
+      "sha256": "e3a491f3aa8b986e6047c9b41fb650e60a6c3f042223601257b0928ebd3771d6"
+    },
+    {
+      "path": "research/sl2f3-dirty-role-four/README.md",
+      "usage": "provenance",
+      "git_blob": "cb5fe755ea89535bab55b296e3bea6ef244c947a",
+      "sha256": "4e872b0915446491bdbaf661108e61d58b24ca0c2b58fecc98e72ca477db87d4"
+    }
+  ]
+}