Prove four-call optimum for all even S4 pairs with every odd label

research/s4-stable-four-call/PROOF.md

@@ -0,0 +1,123 @@
+# Exact four-call minimum with every odd S4 label
+
+## Model and theorem
+
+Let A=F2[S4] be the full formal group algebra, with [g][h]=[gh]
+and gh acting as g after h. Fix any finite register count r>=2.
+All register inputs are arbitrary. A paid call has unit cost and matrix
+
+    D_N(g) = I + ([g]+[e])N = [e](I+N) + [g]N,
+
+where g is any odd permutation and N is any rank-one idempotent in M_r(F2).
+Every scalar GL_r(F2) map is free and may occur anywhere. No address map,
+reset, clean register, erasure or additional operation is free.
+
+For any nonidentity a,b in A4, including a=b, the target is the complete
+formal matrix
+
+    T = diag([a],[b],[e],...,[e]).
+
+In particular all extra registers return individually to their arbitrary
+entrance values and every off-diagonal coupling is zero.
+
+**Theorem.** The exact paid-call minimum is four, independently of r.
+This remains a four-call lower bound if any subset of the odd labels is
+permitted; attainment below uses the full odd-label alphabet.
+
+## 1. Normalize the scalar maps
+
+For any scalar G in GL_r(F2),
+
+    G D_N(g) G^-1 = D_(G N G^-1)(g).
+
+Conjugation preserves rank one and idempotence. Move all free scalar maps
+to the right, to write an arbitrary word as a product of the same number
+of paid factors followed by one scalar map S.
+
+The augmentation homomorphism aug:A->F2 sends every group element to 1.
+It sends each paid factor to I, and sends T to I. Applying it to the word
+shows S=I. Thus it suffices to study a product of paid factors alone.
+This step counts scalar mixing at intermediate cuts and does not restrict
+which dirty roles a paid projector can couple.
+
+## 2. Every valid word has even length
+
+The sign map S4->C2 extends to an algebra homomorphism
+
+    pi:A->F2[C2],       pi([g]) = z for odd g,
+    z^2=1,             pi([g]) = 1 for even g.
+
+The ring F2[C2] is commutative. A scalar basis diagonalizes N to
+`diag(1,0,...,0)`, since an idempotent splits its image and kernel.
+Consequently pi(D_N(g)) is similar to diag(z,1,...,1), and its determinant
+is z. Determinants multiply over this commutative ring. A product of L
+paid factors therefore has determinant z^L after pi, whereas pi(T)=I
+has determinant 1. The formal basis elements 1 and z are distinct even
+in characteristic two. Hence L is even.
+
+This is the sign-determinant method already used by Cinna Davis in #1734.
+No determinant of a matrix over the noncommutative algebra A is taken.
+
+## 3. Two calls cannot deliver two active even targets
+
+Write a formal matrix as M=sum_g [g] C_g, where C_g is a binary scalar
+matrix. Define its nonidentity even coefficient rank sum by
+
+    E(M) = sum_(g even, g!=e) rank_F2(C_g).
+
+The proposed target always has E(T)=2. If a!=b, its two nonidentity
+even coefficients are the two distinct coordinate projectors, each of
+rank one. If a=b, the single coefficient at a has rank two. Restored
+spectators contribute only to the identity coefficient.
+
+For odd s,t and rank-one idempotents N,M, direct multiplication gives
+
+    D_N(s) D_M(t)
+      = [e](I+N+M+NM)
+        + [s](N+NM) + [t](M+NM) + [st]NM.       (1)
+
+Repeated group labels in (1) are combined by addition in F2. The labels
+s and t are odd. Thus the only possible nonidentity even label is st.
+If st=e there is none. Otherwise its coefficient is NM, whose rank is
+at most one. Therefore E(D_N(s)D_M(t))<=1, contradicting E(T)=2.
+
+Zero calls cannot realize T because a and b are nonidentity formal basis
+elements. Section 2 excludes one and three calls, and (1) excludes two.
+Every valid word therefore has at least four calls. This is a written
+argument for every finite r, rather than an inference from a register census.
+
+## 4. Four calls attain every target
+
+Fix the odd transposition tau=(12). For each even h, put u_h=tau h.
+It is odd, and tau u_h=h. If E_i is the i-th coordinate projector, then
+idempotence gives the formal identity
+
+    D_(E_i)(g) D_(E_i)(h) = D_(E_i)(gh).
+
+It follows that
+
+    D_(E_1)(tau) D_(E_1)(u_a)
+    D_(E_2)(tau) D_(E_2)(u_b) = T.              (2)
+
+Equation (2) uses four paid calls, requires no extra registers or scalar
+changes, and acts identically on every dirty spectator. Some u_h are
+four-cycles, so the larger paid alphabet is used. These calls are
+invertible but need not be involutions; their inverses use inverse labels.
+
+## Scope and predecessor boundary
+
+Cinna Davis's #1749 establishes a finite four-role result for eight
+noncommuting three-cycle pairs using only adjacent transpositions.
+Ross Richardson's #1989 already proves all-register exact inversion tariffs
+for that adjacent-label alphabet, including those pairs. Neither earlier
+statement is claimed as new here. The new theorem allows every odd S4
+permutation at unit price, including nonadjacent transpositions and all
+four-cycles, and covers every ordered pair of nonidentity even targets.
+The proof combines the credited sign method with the two-call coefficient
+rank sum in (1). No literature priority is claimed for determinant parity,
+group-algebra expansion, rank submultiplicativity or coordinate projectors.
+
+This is a scoped formal-alphabet proof. It supplies no native address
+implementation, physical scalar or routing price, precision bound, stock
+bound, supplier admission or complete multiplication theorem. All such
+obligations remain unproved here. The selected frontier is unchanged.

research/s4-stable-four-call/README.md

@@ -0,0 +1,118 @@
+# Four calls remain optimal with every odd S4 permutation
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. For every
+finite r>=2, every target diag([a],[b],1,...,1), with nonidentity even
+permutations a,b in S4, has exact paid-call minimum four in the following
+formal binary group-algebra model. A paid call is I+([g]+1)N, where g is
+any odd permutation at unit cost and N is any binary rank-one idempotent.
+Arbitrary scalar GL_r(F2) maps are free. Every extra register is dirty and
+must return to its individual input value. The case a=b is included.
+
+The changed hypothesis is the paid alphabet. All twelve odd permutations
+are available, including six four-cycles. Cinna Davis's [#1749](https://github.com/CrocSwap/integer-mult-bounds/pull/1749) gives the
+four-role adjacent-transposition case; Ross Richardson's [#1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) already
+settles adjacent-transposition tariffs with arbitrary dirty workspace.
+Those theorems are cited, not replayed. The new maximum-alphabet result
+covers all ordered pairs of the eleven nonidentity even S4 permutations.
+No kappa, native supplier or selected-frontier change is claimed.
+
+## Proof
+
+[PROOF.md](PROOF.md) gives the complete argument. Augmentation normalizes
+all free scalar maps away from the endpoint. The inherited sign-determinant
+method forces an even number of odd-label calls. A two-call product has at
+most one nonidentity even coefficient, of scalar rank at most one. The
+target's even coefficient rank sum is two, including when a=b. Four
+coordinate calls attain every target. The proof applies at every finite
+register count; the finite checks below only corroborate it.
+
+## Evidence and reproduction
+
+From the worktree root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/s4-stable-four-call/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/s4-stable-four-call/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/s4-stable-four-call
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/s4-stable-four-call --check-source-history
+```
+
+A reviewer can substitute any CPython 3.12 executable. The expected marker
+is PASS_S4_STABLE_FOUR_CALL. The verifier writes only stdout and prints a
+generated receipt with the SHA256 of every package file. No receipt is
+handwritten or committed. Explicit exceptions retain all checks with -O.
+
+The verifier multiplies the full formal group-algebra matrices for all
+118,080 two-call words in the larger alphabet at r=2,3. It checks (1) independently
+against convolution and checks the even coefficient rank bound. It builds
+363 four-call endpoints for all 121 target pairs at r=2,3,5 and checks
+29,040 dirty basis columns through a separate literal permutation-action
+implementation. All 484 single-call omissions are rejected.
+It also checks 650 sign determinants at r=2,3,4,5, all 432 two-role scalar
+covariances and five hypothesis controls. These
+include two-call counterexamples if even paid labels or scalar rank two
+are allowed, and a rejection of treating four-cycle calls as involutions.
+
+The card's historical first command, scripts/research_baseline.py, was
+attempted and failed with KeyError: 'bit_lower' under the selected schema.
+The current scripts/research_selected_baseline.py passed with
+PASS_RESEARCH_BASELINE_BINDINGS_ONLY. Neither is a scientific dependency
+or an operator replay, and neither was changed here.
+
+## Limits and implementation bounds
+
+Only odd paid labels and rank-one idempotents are covered. Free address
+maps, even paid labels, higher-rank paid calls, clean-only endpoints and
+changed restoration contracts can change the answer. Nothing here prices
+coefficient preparation, native implementation, scalar basis changes,
+routing, physical restoration, tape, precision or a completed consumer.
+These costs remain unknown. Independent human and formal proof-kernel
+review are unclaimed. Lean, Docker and selected cold replay were not run.
+
+The verifier has no recursion or subprocesses. Its loop domains are fixed
+at 24 group elements and at most five roles. It streams two-call words,
+retaining at most 24 scalar coefficient blocks per formal matrix. Finite
+Python tuples, dictionaries, integers and JSON serialization require
+managed allocation; this is a bounded-domain deviation from fixed
+steady-state allocation. Each hashed file is limited to 256 KiB. No
+shared code, pinned evidence or predecessor file changes.
+
+The bit-new-register-model card is changed to a formal side result with
+an enlarged paid-label set. It is not a physical construction expansion.
+Historical provenance, source pins and structured next questions are in
+[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json).
+
+## Open next questions
+
+1. Can three nonidentity even targets share fewer than six calls in the
+   maximal odd-label alphabet? Start with four calls, the only remaining
+   candidate after parity. The two-call coefficient rank proof does not
+   bound the even coefficient sum of a four-call word.
+2. Can a physical interface supply any nonadjacent odd permutation below
+   its complete adjacent-word price? Start with one four-cycle, accounting
+   for address preparation, scalar maps, restoration and routing. No such
+   implementation or complete consumer is supplied here.
+
+These follow-ups are not investigated or reserved.
+
+## Credit and overlap
+
+Cinna Davis #1749 supplies the original three-cycle/extra-register question
+and #1734 supplies the sign-determinant precedent. Ross Richardson #1989
+supplies the exact adjacent-label theorem and normalization context, with
+Adam Gall #1941 and Ross Richardson #1966 retaining the cut-method lineage.
+Retain eumemic #288, Ali Romman #468, David Govea #720 and Gareth Davidson
+#1333 for the register-model lineage. Original predecessor credit lines
+and files remain unchanged. The new result is the enlarged-alphabet
+four-call theorem and its coefficient-rank proof.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145529).
+Live open PRs, this account's recent work, the latest handoffs and local
+reservations were checked before claiming. Distinctive searches covered
+merged PRs and all main-branch README paths. The cached overlap report
+covered 314 open PRs and 4,389 Discussion records, but only 178 of 6,996
+main README paths in the sparse checkout; direct Git searches supplied
+the main-branch coverage. Arbitrary diffs and unpublished work remain
+outside that coverage. This is not a novelty certificate.

research/s4-stable-four-call/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/s4-double-transposition-seedb270/README.md",
+      "usage": "provenance",
+      "git_blob": "a15eea3cb33e00ed69e5695e3a27d0ffecbd24ec",
+      "sha256": "70098225ba21e1d2ef76600e3d4ba0f1368f4cdc2e8c9705f91eba0a1d11e4f5"
+    },
+    {
+      "path": "research/s4-noncommuting-threecycle-r4-seeda27b/README.md",
+      "usage": "provenance",
+      "git_blob": "5af621bac9e1f05e92bcb436781a781d9764eb5b",
+      "sha256": "c52c66784a662ef63854a2944ed56f8540e288e1fb1674a0d4e7fa0fd51ce430"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f",
+      "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154"
+    }
+  ]
+}

research/s4-stable-four-call/TASK.json

@@ -0,0 +1,106 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact four-call minimum for every nonidentity even S4 target pair, all finite dirty-register counts, all odd permutations available as unit-cost rank-one-idempotent calls, and free binary scalar mixing.",
+  "scope_change_reason": "The card is narrowed to a formal algebraic side result. Unlike the already-settled adjacent-label tariff, the paid alphabet includes all twelve odd permutations at unit cost.",
+  "bottleneck_link": "This rules out pair sharing even after granting every odd S4 address operation at unit price. Native implementation and the complete recursive invoice remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first original written bound with a matching exact endpoint.",
+  "outcome": "completed",
+  "evidence": "Written augmentation/parity/coefficient-rank proof plus exact full-algebra convolution and separate regular-action finite corroboration.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can three nonidentity even targets use four maximal-odd calls?",
+      "why_it_matters": "It is the next possible sharing threshold after the proved pair obstruction.",
+      "first_step": "Fix a literal triple and inspect the even coefficients of four calls.",
+      "blocked_by": "No four-call coefficient-rank bound is supplied."
+    },
+    {
+      "question": "Can one odd four-cycle be supplied below its complete adjacent-word price?",
+      "why_it_matters": "A formal enlarged alphabet gives no physical savings by itself.",
+      "first_step": "Specify and fully price one physical four-cycle caller.",
+      "blocked_by": "Native address preparation, scalar, routing and restoration costs are unknown."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145529",
+  "predecessors": [
+    {
+      "pr": 1749,
+      "author": "Cinna Davis",
+      "head": "90405b9498e4abfdd7d0eececcf11c7e83c6d13b",
+      "role": "Original finite adjacent-label question; cited only."
+    },
+    {
+      "pr": 1989,
+      "author": "Ross Richardson",
+      "head": "8b9f3ec8b1e5745c42fec68d75da5fbc82ea91ec",
+      "role": "Already-settled arbitrary-workspace adjacent tariff; cited only."
+    },
+    {
+      "pr": 1734,
+      "author": "Cinna Davis",
+      "role": "Sign-determinant precedent; cited only."
+    }
+  ],
+  "preserved_checkout": {
+    "branch": null,
+    "state": "detached HEAD, clean before work",
+    "head": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+    "prior_commits": [
+      "e0c2e09b9443f22bb9e3c76ab08d1224493040e3",
+      "e5d7e4dc31331f19fb9ee795f180e6058ccf779c",
+      "3e1645cdee74aa5efb722f7d218f7465d219e66c",
+      "1e8187bea856a358ece55fb844189078bfae48b3"
+    ]
+  },
+  "local_environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "standard library only"
+  }
+}