Prove the sharp rank cap for three-call A5 conjugate pairs

research/a5-rank-cap-threshold/PROOF.md

@@ -0,0 +1,134 @@
+# Sharp rank cap for the A5 conjugate-pair word
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let K be any field and V any finite-dimensional K-vector space. Work in the
+full formal matrix algebra End_K(V)[A5], with scalar operators commuting with
+group basis elements. Set x=(12)(34) and y=(135), with right-to-left permutation
+composition. Let P,Q be nonzero idempotents with PQ=QP=0, of ranks r,s.
+All of V has arbitrary initial data; the complementary space is restored.
+For each g in {x,y}, one paid call is
+
+```text
+F_g(N) = I + ([g]-[e])N,      N^2=N,      1 <= rank(N) <= h.
+T = I + ([xy]-[e])P + ([yx]-[e])Q.
+```
+
+Let h be a positive integer with h >= max(r,s). The exact minimum number
+of paid calls for T is
+
+```text
+3, if h >= r+s;
+4, if max(r,s) <= h < r+s.
+```
+
+This holds with any finite number of additional restored dirty roles and with
+arbitrary free scalar GL(V) maps. It counts paid calls only. It assigns no
+physical or recursive price to a higher-rank call or to scalar mixing.
+
+## Attribution and new step
+
+Wentao Li's #4089 proves the binary r=s=h=1 case at arbitrary role count,
+following Cinna Davis's #2246 finite-width result and question. In particular,
+the support filter and the forced middle matrix P+Q in that special case
+are predecessor ideas. We cite them without replaying their implementations.
+The new step changes the paid alphabet: higher-rank idempotents are legal.
+It gives the exact three/four-call transition for arbitrary r,s over every
+field, together with an attaining three-call construction. It does not claim
+that the rank-one lower-bound method or coordinate batching is new.
+
+## Free scalar maps
+
+Move any scalar GL(V) maps through the paid factors by conjugation.
+Conjugation preserves idempotence and rank. The group-algebra augmentation
+maps each [g] to 1, hence sends each paid factor and T to I. Therefore the
+residual scalar map is I. A normalized paid word suffices for the lower bound;
+the literal scalar maps and their physical costs are not classified.
+
+## Support lower bound
+
+Every group label in a product expansion is an ordered subsequence of its
+paid labels. No word of length at most two has both xy and yx in its support.
+Among the eight length-three words over {x,y}, only xyx and yxy do. This is a
+finite permutation statement for these particular x,y, independent of K and
+V. The verifier checks all fifteen label words of length zero through three
+by expanding every ordered subsequence. Since P and Q are nonzero and xy,yx
+are distinct group elements, T requires both coefficients. Thus at least
+three paid calls are necessary. A direct hand check of the full-length
+products is xxx=x, xxy=y, xyy=xy^2, yxx=y, yyx=y^2x and yyy=e for the six
+nonalternating words. Their proper subsequences contain at most one of xy,yx;
+direct permutation multiplication gives xy^2 != yx and y^2x != xy.
+The two alternating words contain both xy and yx as length-two subsequences.
+
+## Every three-call word pays middle rank r+s
+
+Consider F_x(A)F_y(B)F_x(C). Write each factor as (I-N)+[g]N.
+The labels xyx, xy, yx and y have the following coefficients:
+
+```text
+[xyx]  ABC
+[xy]   AB-ABC
+[yx]   BC-ABC
+[y]    B-AB-BC+ABC.
+```
+
+These four group elements are distinct; xyx and y are absent from T.
+Matching coefficients gives ABC=0, AB=P, BC=Q, and then B=P+Q.
+All identities use integer coefficients and subtraction only, so they hold
+in every characteristic. We did not assume that A,B,C are idempotent or
+that any factor is invertible in this necessity argument.
+
+For F_y(A)F_x(B)F_y(C), use the distinct labels yxy, xy, yx and x:
+
+```text
+[yxy]  ABC
+[xy]   BC-ABC
+[yx]   AB-ABC
+[x]    B-AB-BC+ABC.
+```
+
+They give ABC=0, BC=P, AB=Q and again B=P+Q.
+
+Because P,Q are orthogonal idempotents, V is the direct sum of im P,
+im Q and ker P intersect ker Q. The map P+Q is identity on the first two
+summands and zero on the third. Hence rank(B)=rank(P+Q)=r+s. A cap below r+s
+therefore excludes every three-call implementation, including arbitrary
+noncoordinate couplings and restored spectators.
+
+## Attainment
+
+The direct four-call word is
+
+```text
+F_x(P) F_y(P) F_y(Q) F_x(Q) = T.
+```
+
+Each coupling has rank r or s, so it is legal for h>=max(r,s).
+When h>=r+s, the shorter word is
+
+```text
+F_x(P) F_y(P+Q) F_x(Q) = T.
+```
+
+On im P it acts by xy; on im Q it acts by yx; on the common kernel it is
+identity. P+Q is itself idempotent. Its ranks are r,r+s,s, so every call
+is legal exactly at the stated sufficient cap. The reversed alternating
+word F_y(Q)F_x(P+Q)F_y(P) also attains T. These are full operator identities,
+not target-row observations or finite-column assumptions.
+
+Both the four-call word and the three-call word have total coupling rank
+2(r+s). Thus one paid-call overhead disappears at this rank threshold, but
+the proof makes no claim of lower total rank mass, native speed or kappa.
+Together with the lower bounds this proves the theorem. Stop here.
+
+## Limits
+
+The theorem requires full formal group-algebra equality, these two labels,
+orthogonal idempotent target blocks and h>=max(r,s). It does not determine
+the optimum when a target block itself exceeds the cap, a minimum under an
+arbitrary rank-dependent tariff, or a physical implementation cost. The
+necessity proof applies even to non-idempotent paid couplings, but the
+specified legal alphabet and the attaining constructions use idempotents.
+Independent human and formal proof-kernel review are unclaimed.

research/a5-rank-cap-threshold/README.md

@@ -0,0 +1,138 @@
+# Sharp A5 three-call rank threshold
+
+For every field and every finite dirty role space, the A5 conjugate-pair
+operator with two orthogonal target blocks of ranks r,s has exact paid-call
+minimum three when the allowed coupling rank h is at least r+s, and four
+when max(r,s)<=h<r+s. After scalar normalization, every three-call
+implementation must use middle coupling P+Q, of rank r+s. Arbitrarily many restored dirty spectators and
+free scalar mixing preserve this threshold.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+This is a scoped algebraic proof with exact finite corroboration. It changes
+the rank-one hypothesis of Wentao Li's [#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089),
+following Cinna Davis's [#2246](https://github.com/CrocSwap/integer-mult-bounds/pull/2246).
+Their rank-one theorem, support filter and special-case forced middle
+projector are cited predecessors, not new claims here. Their searches and
+verifiers are not replayed. The new result is the sharp higher-rank cap
+transition, arbitrary-rank construction and field-uniform proof.
+
+## Operator and complete invoice
+
+In End_K(V)[A5], let x=(12)(34), y=(135), and let P,Q be nonzero
+idempotents satisfying PQ=QP=0. Products act rightmost first. A paid call is
+F_g(N)=I+([g]-[e])N, with g in {x,y}, N idempotent and 1<=rank(N)<=h.
+The target is T=I+([xy]-[e])P+([yx]-[e])Q.
+
+```text
+four calls: F_x(P) F_y(P)   F_y(Q) F_x(Q)
+three calls: F_x(P) F_y(P+Q)        F_x(Q)
+```
+
+Both equal the full operator T and restore the common kernel. Their total
+coupling rank is the same, 2(r+s). The change saves one paid-call overhead
+only if the enlarged call is available under the declared cap. It is not a
+claim of native speed, a recursive-child saving or a new kappa.
+
+[PROOF.md](PROOF.md) proves the all-field threshold by matching full
+noncommutative group coefficients. The necessity argument even allows
+non-idempotent paid couplings; the legal alphabet and witnesses use
+idempotents. Scalar augmentation removes any residual free GL(V) map.
+
+## Reproduce
+
+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/a5-rank-cap-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a5-rank-cap-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/a5-rank-cap-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a5-rank-cap-threshold --check-source-history
+```
+
+Use an equivalent CPython 3.12 path on another machine. The direct marker is
+`PASS_A5_RANK_CAP_THRESHOLD`. Each direct execution is read-only and emits a
+generated receipt containing freshly computed counts and SHA256 hashes of
+all six package files. No receipt is hand-written or used as a proof input.
+The registered normal and optimized commands use explicit exception checks.
+All source pins are provenance only; the standalone verifier imports no
+predecessor implementation or external data file.
+
+The finite evidence is separate from the universal written theorem. The
+verifier expands all fifteen short label words, enumerates complete ternary
+and quinary two-role idempotent alphabets including higher-rank calls, and
+checks all attaining target pairs. It also checks exact rational and
+F2/F3/F5/F7 oblique projectors of ranks up to 3 and 4 in at most eight roles,
+complete three/four-call endpoints, every single-call omission, malformed
+inputs, and a dirty-spectator leakage control. A separate regular-action
+engine acts on every basis column of both four-role words over F3.
+
+The direct run enumerates 21,952 ternary words and 262,144 quinary words,
+with 24 and 60 three-call hits across 12 and 30 target pairs, respectively.
+Every hit has the required rank-two middle coupling. The remaining checks
+cover 60 complete endpoints from 30 oblique pairs, 480 regular-action basis
+columns, 210 omission controls, six invalid-input controls and one spectator
+leakage control. These counts are freshly enumerated, not a predecessor
+receipt or a claim of exhaustive coverage in larger dimensions.
+
+## Scope and decision
+
+The base is canonical main de5ec2e7a6074068452f45b1a191b5c72832df4a,
+priority revision 8. The selected source-binding orientation passed; it was
+metadata orientation, not a selected scientific replay. The card is
+`bit-new-register-model`, explicitly changed to the paid rank cap. This is a
+formal algebraic side result. The first improvement ends the investigation.
+
+Initial overlap checking covered live PRs, this account's recent work,
+active handoffs, all-main README searches and merged PR searches for A5,
+conjugate pairs and rank caps. The card cache reported 416 open PRs and
+5,315 Discussion records; its local scan omitted sparse packages. Direct
+Git searches covered all main READMEs for the distinctive candidate terms.
+Arbitrary code diffs and unpublished work are not fully covered. No match
+is a novelty guarantee. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214476)
+records the intended scope. Global literature priority is unclaimed.
+
+No optimum is asserted when h<max(r,s), under an arbitrary rank tariff,
+with other group labels, or for nonorthogonal targets. Native realization,
+physical scalar mixing, frames, movement, preparation, storage, restoration
+cost, precision, compiler closure and a complete recursive consumer remain
+unpriced. No selected-frontier change, supplier admission, complete
+multiplication theorem, Lean run or Docker run is supplied.
+
+## Open next questions
+
+Can an actual nonabelian native caller execute the combined middle call
+more cheaply than the two separate y calls? Start with one runtime carrier
+and a rank-two idempotent, then give a full invoice for scalar mixing,
+movement, frames and return on arbitrary dirty data. The missing native
+tariff and recursive consumer block any profitability claim. This question
+is also structured in [TASK.json](TASK.json); no follow-up is reserved.
+
+## Related work and credit
+
+- Wentao Li #4089 supplies the arbitrary-role binary rank-one theorem and
+  the support/coefficient argument. Cinna Davis #2246 supplies the original
+  A5 target, finite result and all-role question. The retained register-model
+  and PR840 construction lineage remains credited through those sources.
+- Cinna Davis's open [#3914](https://github.com/CrocSwap/integer-mult-bounds/pull/3914)
+  proves collapse into an additive caller. Our changed rank cap does not
+  remove that caller obstruction and computes no common numerical value.
+- Nick Petalas #5114 supplies an algebra-faithful address carrier;
+  JoyboyBrian #5186 supplies a distinct paid physical rank-one caller.
+  Neither is a price for the higher-rank alphabet used here.
+
+[SOURCES.json](SOURCES.json) pins exact historical provenance. Predecessor
+files and credit are unchanged. No independent acceptance is claimed.
+
+## Verifier implementation limits
+
+All loops have fixed finite domains: fields 0,2,3,5,7, role counts at most
+8, word lengths at most 4, 120 permutations and at most 32 two-role
+idempotents. Formal states have at most sixteen coefficient blocks;
+regular-action states have at most 240 scalar entries. There is no recursion,
+network access, subprocess, dynamic code generation or callback dispatch.
+Functions fit within sixty lines. Python and Fraction allocate dynamically;
+the fixed domains bound live objects but do not provide allocation-free
+execution. Warning-strict normal and optimized runs are the supported
+interpreter diagnostics. No external static analyzer is assumed installed.

research/a5-rank-cap-threshold/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/a5-conjugate-5cycle-seedd316f8/README.md",
+      "usage": "provenance",
+      "git_blob": "45411c9b33aca555b4a09fc0107edac32d59f5c1",
+      "sha256": "a45441f847baabcfb016bbd1ca44b01b5c2670ffcf9e1d6d709082c68a1dc402"
+    },
+    {
+      "path": "research/a5-conjugate-any-registers/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "a72b89bdd2428b78c6424d2d2299bdb1ac2981d3",
+      "sha256": "921a84d24148d27932aad24a9a5d74bd235de0c1b2f27c2b9bfc5d37fcf51dcf"
+    },
+    {
+      "path": "research/a5-conjugate-any-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "92fa82d936248c7e3485e4ea3aecac88f42988f9",
+      "sha256": "26246a1b0448048f59d2a80e09addcf80950d728f2c768e56d32f145c59fd773"
+    }
+  ]
+}

research/a5-rank-cap-threshold/TASK.json

@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "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": "Sharp three/four-call paid-rank threshold for arbitrary orthogonal A5 conjugate target blocks over every field and every finite dirty role space.",
+  "scope_change_reason": "Change the fixed rank-one binary alphabet to rank-at-most-h idempotents over any field. This is a scoped algebraic side result; no native implementation or admission is supplied.",
+  "bottleneck_link": "A higher-rank call merges two same-label jobs across opposite word orders. The new cap threshold states exactly when one call overhead can disappear. Total coupling rank remains unchanged, and physical costs are unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after proving and exactly corroborating the sharp cap threshold; do not expand into a new caller or longer-word search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-field theorem; verify.py computes complete endpoints, finite higher-rank alphabets and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual nonabelian native caller execute the rank-(r+s) middle call more cheaply than the two separate y calls?",
+      "why_it_matters": "The formal word saves one call overhead but no total coupling rank; physical profitability needs a complete invoice.",
+      "first_step": "Specify one runtime carrier and its rank-two idempotent action, including scalar mixing, movement, frame conversion, arbitrary dirty input and complete return.",
+      "blocked_by": "No native tariff or complete recursive consumer for the enlarged alphabet is supplied."
+    }
+  ],
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214476",
+    "base_checked_utc": "2026-10-27T10:00:00Z",
+    "priority_revision": 8,
+    "overlap": "All-main README searches plus live PR bodies and handoffs; card cache covers 416 open PRs and 5315 Discussion records with sparse local omissions. No-match searches do not establish novelty. No PR opened by this account during the preceding 24 hours is targeted."
+  },
+  "environment": {
+    "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+    "dependencies": "standard library only",
+    "playbook": "autonomous-run",
+    "platform": "macOS-27.0.1-arm64-arm-64bit"
+  },
+  "claim_type": "scoped algebraic proof"
+}