Prove five A2 targets need five rank-three calls (no κ)

research/a2-five-target-cap-three/PROOF.md

@@ -0,0 +1,111 @@
+# Five rank-three calls for five A2 longest-element targets
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and model
+
+Let K be any field and W=S3 have simple involutions s,t with sts=tst.
+Write w0=sts. Fix any finite r>=5. Work coefficientwise in M_r(K[W]);
+every role has arbitrary initial data. The required complete endpoint is
+
+    T = diag([w0],[w0],[w0],[w0],[w0],1,...,1).
+
+A paid call is F_u(A)=I+([u]-[e])A, where u is s or t and
+1<=rank_K(A)<=3. Scalar GL_r(K) maps may be interleaved for free.
+Couplings A need not be projectors or invertible. There are no other free
+address operations, clean allocations, resets or discarded outputs.
+Every spectator and every off-diagonal formal coefficient must be restored.
+
+Let f on {0,1,2,3} be nonnegative, nondecreasing and discretely concave,
+with f(0)=0. The cost of a paid call is f(rank A), the same for both labels.
+Then the exact formal tariff is
+
+    optimum = 5 f(3).
+
+In particular, the minimum number of paid invocations is five, by taking
+f(k)=1 for k>0. This is a formal call price, not a native or recursive bill.
+
+## Attaining support schedule
+
+Number productive roles 0 through 4, and let E_B be the diagonal projector
+on B. Execute the following calls chronologically:
+
+| Call | Label | Support B | Rank |
+| --- | --- | --- | ---: |
+| 1 | s | {0,1,2} | 3 |
+| 2 | t | {0,1,4} | 3 |
+| 3 | s | {0,3,4} | 3 |
+| 4 | t | {2,3,4} | 3 |
+| 5 | s | {1,2,3} | 3 |
+
+On roles 0,1,2,3 the chronological subsequence is s,t,s. On role 4 it is
+t,s,t. Both are palindromes equal to w0, so the rightmost-first convention
+for multiplying column-vector operators gives the same endpoint. A call
+acts as its group label on its support and as identity everywhere else.
+All role matrices are diagonal. Thus the full group-algebra product is T,
+including every zero off-diagonal and the identity on every spectator.
+This is valid over every field, including characteristic two. It uses no
+scalar mixing, dirty helper, preparation, restoration or extra call.
+All five calls have rank three and cost 5 f(3).
+
+## Matching lower bound
+
+Use the all-field root-cut rank bound in zhaobenny's
+[PR6817, proof section 2](../coxeter-capped-concave-tariff/PROOF.md),
+building on David Arias's [PR2738](../coxeter-root-tariff/PROOF.md).
+Its hypotheses are exactly the formal factors, scalar maps and complete
+dirty endpoint above. The A2 simple roots form one root orbit, and w0
+has three inversions. Five targets therefore force
+
+    sum_j rank_K(A_j) >= 15.
+
+This inequality is an inherited theorem, not re-proved or replayed here.
+Its allowance of arbitrary scalar couplings and arbitrarily many restored
+dirty spectators is needed for the lower bound, even though the attaining
+word uses diagonal projectors and no spectators.
+
+Concavity and f(0)=0 give f(k)>=k f(3)/3 for k=1,2,3. Consequently every
+legal finite circuit has cost at least
+
+    sum_j f(rank A_j) >= f(3)/3 sum_j rank A_j >= 5 f(3).
+
+The support schedule attains this bound. No classification of circuits,
+finite-field extrapolation or numerical root calculation is required.
+For unit invocation prices, the same rank bound rules out four calls,
+since four rank-three calls supply at most twelve rank units.
+
+## Improvement and relation to prior work
+
+The direct fixed partition into a three-role block and a two-role block
+applies the three-letter word separately, costing 3 f(3)+3 f(2).
+The displayed schedule saves exactly 3 f(2)-2 f(3), which is nonnegative
+by concavity and positive for every strictly concave f. At f(k)=k/(k+1),
+the exact price is 15/4 instead of 17/4, saving 1/2. This comparator is an
+explicit construction, not a claimed optimum of any enlarged model.
+
+Nick Petalas's [PR5083](../rank2-swap-batching/README.md) already gives
+three longest-element targets at rank cap two using changing supports.
+That idea and schedule are credited, not claimed again. The present new
+instance has five targets, cap three and five full-rank calls. PR6817's
+divisible theorem does not cover 3 not dividing 5, and its cap-two st
+correction has a different target. ToikY's
+[PR6821](../a2-st-all-cap-tariff/README.md) settles repeated st at every
+cap; it does not settle repeated w0. We answer one instance of PR6817's
+explicit nondivisible-target question. No claim of literature priority
+for support scheduling, concavity or the root-cut method is made.
+
+## Evidence and limits
+
+The standalone verifier multiplies full signed coefficients in K[S3].
+It also checks the full left regular action using a separate GL2(F2)
+address representation. Finite gauges mix productive and dirty roles,
+with explicit entrance and exit scalar maps. These are corroborating
+examples; the displayed word and cited lower bound give the universal proof.
+The verifier does not run any predecessor's scientific program.
+
+Scalar coupling rank is not recursive child rank. Native realization,
+the price of scalar maps, routing, storage, ownership, precision, stock,
+hosting, compilation and the complete supplier invoice remain unknown.
+No new kappa, supplier admission, selected-frontier change, independent
+human review, formal-kernel acceptance or complete multiplication theorem
+is claimed. The five selected framework assumptions remain.

research/a2-five-target-cap-three/README.md

@@ -0,0 +1,151 @@
+# Five A2 longest-element targets need five rank-three calls
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped written proof with exact finite corroboration. Five identical
+longest-element targets w0=sts=tst in S3 have exact formal tariff **5 f(3)**
+when paid scalar rank is capped at three and the common rank price f is
+nonnegative, nondecreasing and discretely concave, with f(0)=0. The result
+holds over every field, with free scalar GL mixing and any finite number
+of restored dirty spectators. In particular, five unit-priced invocations
+are necessary and sufficient.
+
+The new diagonal support schedule has five rank-three calls, compared with
+six calls of ranks (3,3,3,2,2,2) from fixed disjoint batching. It costs
+5 f(3) instead of 3 f(3)+3 f(2), saving 3 f(2)-2 f(3). At f(k)=k/(k+1),
+the exact bill is 15/4 instead of 17/4. The matching 15-unit rank lower
+bound is a cited predecessor theorem, not a new result here.
+
+[PROOF.md](PROOF.md) gives the complete endpoint, five support sets and
+all-field argument. This answers one nondivisible-target instance explicitly
+left open by zhaobenny's [PR6817](https://github.com/CrocSwap/integer-mult-bounds/pull/6817).
+Its divisible theorem does not cover five targets at cap three. Nick Petalas's
+[PR5083](https://github.com/CrocSwap/integer-mult-bounds/pull/5083) already
+supplies the changing-support idea and the distinct three-target/cap-two
+word; those are credited. ToikY's
+[PR6821](https://github.com/CrocSwap/integer-mult-bounds/pull/6821) treats
+repeated st, a different endpoint. The new contribution is this five-target
+support schedule and its sharp cap-three tariff, not a new root-cut or
+concavity principle.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a2-five-target-cap-three/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/a2-five-target-cap-three/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a2-five-target-cap-three
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a2-five-target-cap-three --check-source-history --check-modes
+```
+
+Other installations can substitute their CPython 3.12 path. The direct
+commands print `PASS_A2_FIVE_TARGET_CAP_THREE` in a newly computed JSON
+receipt bound to the SHA256 of all six package files. They write no files,
+import no predecessor program and require no Git, network or external input.
+`SOURCES.json` pins cited prose and the historical task context as provenance;
+the package validator authenticates those Git pins separately.
+
+The finite checks cover exactly:
+
+- 24 complete signed group-algebra endpoints over Q, F2, F3 and F5, using
+  five, six and eight roles and two scalar gauges. All 120 paid couplings
+  have rank three and are idempotent; 78 genuinely couple productive and
+  dirty roles. Entrance and exit scalar maps restore the target endpoint.
+- 912 basis columns of the complete left regular action, using a separate
+  GL2(F2) address representation rather than the S3 permutation product.
+- 120 omitted-call and 120 label-flip mutants, each rejected by its complete
+  formal endpoint. These controls concern the new word only.
+- 36 exact rational price schedules, including all 35 nonincreasing
+  nonnegative integer slope triples with slopes at most four, plus
+  f(k)=k/(k+1). Each is compared against all 90 nonnegative rank-count
+  profiles with total rank 15 through 17, for 3,240 comparisons.
+  Exactly 31 of the 36 schedules give strict savings over fixed batching.
+
+The price-profile enumeration suffices for this finite relaxation: from
+any list of ranks 1..3 with total at least 15, retain a prefix through its
+first crossing of 15. Its total lies in 15..17 and its cost cannot increase.
+The universal circuit lower bound is the written cited theorem, not an
+extrapolation from this finite price test or from the tested fields.
+
+Local validation uses CPython 3.12.15 on macOS arm64. Normal, optimized
+and registered replay are the required checks; exact timings and the
+publication commit are recorded in the PR body. Hosted CI status is separate.
+No local mathematical check is deferred solely to CI. Independent human
+and formal proof-kernel review are unclaimed.
+
+## Scope and overlap
+
+The formal paid operation is I+([u]-[e])A, u in {s,t}, with arbitrary
+scalar A of positive rank at most three. The endpoint is diagonal with
+five [w0] entries and identity on every other role. Arbitrary couplings,
+free scalar maps and restored dirty spectators are allowed for the lower
+bound. The attaining schedule needs only coordinate projectors and no
+spectators. It does not classify other target counts, caps or prices.
+
+This is a changed-scope side result for `bit-new-register-model`. It does
+not fulfill that card's native-conversion or complete-supplier gate.
+Scalar coupling rank is not recursive child rank. The actual physical
+price, ownership, routing, storage, precision, stock, compilation, hosting
+and complete supplier invoice remain unknown. No new kappa, supplier
+admission or selected-frontier change is claimed; all five selected
+framework assumptions remain. Lean, Docker, the selected cold replay
+and predecessor scientific suites were not run.
+
+The scientific base is canonical main
+`e54523517d0f03e58352e647c403a5af3e525a57`, with the selected #7000 record
+and priority revision 8 pinned separately in `SOURCES.json`. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538441)
+states the same five-target/cap-three scope.
+
+Entry overlap included live open PRs, account PR history, recent handoffs,
+active discussions, relevant PR bodies, and distinctive whole-main README
+searches for the specific and general batching formulas. The cached scan
+covered 477 open PRs and 7,121 Discussion records with complete remote
+pagination, but only 169 materialized notes against 10,178 HEAD note paths.
+Whole-main Git searches supplemented that sparse coverage. A separate
+source-reference scan covered 477 open and 6,175 closed PR bodies and found
+no account PR created since November 4 citing #6817. These snapshots are
+non-atomic; arbitrary diffs, unmaterialized nested code and unpublished
+work are outside coverage. A lack of matches is not a novelty certificate.
+
+## Credit
+
+zhaobenny / Benny Zhao's #6817 supplies the all-field rank-cap model,
+nondivisible-target question and root-cut/concave-price lower bound.
+David Arias's #2738 supplies its Coxeter predecessor. Nick Petalas's
+#5083 supplies the older cap-two changing-support construction. ToikY's
+#6821 settles the distinct repeated-st question. Credit also Adam Gall,
+Ross Richardson, ywz65, eumemic, Ali Romman and Gareth Davidson for the
+retained cut and register-model lineage. All predecessor notices remain
+unchanged. No literature-priority claim is made for support scheduling,
+concavity, matrix rank or regular representations.
+
+## Open next questions
+
+Can a native implementation supply a rank-three call with a complete
+subadditive price? First specify the actual data/address layout and
+arbitrary-input entry/exit contract, then charge scalar maps, movement,
+ownership, precision and restoration. No such physical contract or map
+from scalar rank to recursive child rank is supplied here.
+
+Which other nondivisible longest-element batches attain the packed floor?
+Start with a support-incidence feasibility problem at one declared target
+count and cap. This result gives no general scheduling theorem or chronology
+obstruction. No broader construction or follow-on scope is reserved.
+
+## Verifier bounds
+
+The verifier has no recursion, subprocess, solver, external mutable state
+or unbounded CLI input. Dimensions are at most eight, each formal matrix
+has at most 6*8*8=384 coefficient positions, and words have five calls.
+Price loops use 36 schedules and 972 candidate rank-count tuples before
+filtering. All functions are shorter than sixty physical lines. Explicit
+exceptions preserve invariants under optimized Python.
+
+Python's managed tuples, dictionaries and arbitrary-size integers allocate
+during calculation. This is a deviation from fixed allocation, confined to
+the bounded finite verifier. Fixed dimensions, domains and support-capacity
+checks bound live collections. Warning-strict normal and optimized replay
+check the same result. A future larger or native verifier must reassess
+allocation rather than inherit a real-time or native-memory guarantee.

research/a2-five-target-cap-three/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/a2-st-all-cap-tariff/README.md",
+      "usage": "provenance",
+      "git_blob": "65b290f04027f819b6d4295f9c6a921e2c6a1d0d",
+      "sha256": "83f19d188e3ec529ffbe5bc27013137227743b01654053a18249c8a4551c82a3"
+    },
+    {
+      "path": "research/coxeter-capped-concave-tariff/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "00c633badd2f1848ec34b9893553161012e7a8f3",
+      "sha256": "1ef4cb87aee9ca82b9fe42a114b152e1241b7454d68dd49ea8d260fb91e28353"
+    },
+    {
+      "path": "research/coxeter-capped-concave-tariff/README.md",
+      "usage": "provenance",
+      "git_blob": "a9098b3da041be510c0853c5330f74d9e3521219",
+      "sha256": "75fec6903abe17ebeee06627b5cbf7b38d9b00ef5f233774d64539755c339120"
+    },
+    {
+      "path": "research/rank2-swap-batching/README.md",
+      "usage": "provenance",
+      "git_blob": "431363d53d9d5b6f1832698cc7332244e0e4efd0",
+      "sha256": "2eded51bc7d80e360ff3937f3cc9feddb79e35b3f3d5ee3d69ac5b232b0d8054"
+    }
+  ]
+}