Prove the all-cap formal concave tariff for repeated A2 st

research/a2-st-all-cap-tariff/PROOF.md

@@ -0,0 +1,146 @@
+# Exact capped concave tariff for repeated A2 two-letter targets
+
+This is a formal tariff theorem, not a native implementation or supplier bill.
+The generator-selective cut method is credited to Adam Gall/PR1941 and Ross
+Richardson/PR1966; the model and classical packing lemma follow Benny Zhao /
+zhaobenny's PR6817. The contribution is the complete st price for every
+remainder, not a new cut or packing principle.
+
+## Model and theorem
+
+Let K be any field, G=S3=<s,t | s²=t²=e,(st)³=e>, and d,b,r positive integers
+with finite r≥d. Work coefficientwise in M_r(K[G]). A paid factor is
+
+    F_u(A)=I+([u]−[e])A,   u∈{s,t},   0<rank_K(A)≤b.
+
+The scalar matrix A is arbitrary: it need not be idempotent, and paid factors
+are not assumed invertible. Arbitrary interleaved GL_r(K) matrices with scalar
+[e] coefficients are free. There are no free address maps, resets, discarded
+outputs or clean allocations. The complete endpoint is
+
+    T_d=diag([st],…,[st],[e],…,[e]),
+              d copies
+
+so every spectator has arbitrary input and returns exactly, with no leakage.
+The product convention is [st]=[s][t]; the rightmost factor acts first.
+
+Let f:{0,…,b}→R be nonnegative, nondecreasing, f(0)=0, with nonincreasing
+successive differences. Charge each paid factor f(rank A), identically for
+s and t. Define
+
+    P_(b,f)(d)=floor(d/b)f(b)+f(d mod b).
+
+**The exact minimum cost over finite legal words for T_d is**
+
+    2 P_(b,f)(d).                                      (1)
+
+This includes every field characteristic, every finite number of restored
+dirty spectators, nondivisible d, b=1 and b>r. It asserts neither a unique
+minimizing profile nor a classification/minimum count of calls. Flat or zero
+prices are allowed.
+
+## Two credited generator-selective cuts
+
+Use the left regular action λ of G on its six distinct basis labels over K,
+and tensor with K^r. A formal matrix word therefore induces a linear map on
+V=K[G]⊗K^r, preserving multiplication. This is a lower-bound image; attainment
+below will be checked in the full formal algebra.
+
+For a partition V=V_+⊕V_− put q(X)=rank(X_−+). For arbitrary linear X,Y,
+
+    (XY)_−+=X_−+Y_+++X_−−Y_−+,
+    q(XY)≤q(X)+q(Y).                                  (2)
+
+No factor's invertibility is needed. Choose V_+=span{e,t}⊗K^r, with the other
+four group labels in V_−. Left multiplication by t preserves {e,t}; hence
+q(F_t(A))=0. Left multiplication by s sends its two labels to s,st, both
+outside the pair. Its crossing matrix consists of two disjoint permutation
+entries, tensored with A. Therefore
+
+    q(F_s(A))=2 rank_K(A).
+
+The identity subtraction has no crossing block. Every free scalar GL_r(K)
+also has crossing rank zero: it mixes roles within each group label, not
+labels across the cut. Finally st sends e,t to st,s, both outside the pair.
+The target crosses on precisely its d active roles, giving q(T_d)=2d.
+Applying (2) to the entire word yields
+
+    sum_(s-calls) rank A ≥ d.                          (3)
+
+For the other cut take V_+=span{e,s}⊗K^r. Now s preserves the pair, while t
+sends it to t,ts and st sends it to st,sts, again outside. The same calculation
+gives
+
+    sum_(t-calls) rank A ≥ d.                          (4)
+
+These statements hold even when free maps mix productive and dirty spectator
+roles. In characteristic two, minus equals plus in the paid formula, but
+the six group labels remain distinct and the two crossing entries remain
+independent. The factor 2 is an ordinary dimension count, not a scalar whose
+inverse is used. No semisimplicity, root-sign specialization, augmentation,
+paid projector or nonsingularity hypothesis enters (2)–(4).
+
+## Classical capped packing
+
+For integers 1≤k_j≤b with sum k_j≥d, the standard concave concentration lemma
+gives
+
+    sum_j f(k_j)≥P_(b,f)(d).                           (5)
+
+For completeness, permit zero parts temporarily. If 0<a≤c<b, transfer one
+unit from a to c. The cost change is
+`[f(c+1)−f(c)]−[f(a)−f(a−1)]≤0`. Continue with this pair until one part is
+zero or b, decreasing the number of intermediate parts. Repetition leaves full b-parts and
+at most one remainder. For the original total M this gives P_(b,f)(M).
+This packed function is nondecreasing: increments within a block are those
+of f, and the step into the next full block is f(b)−f(b−1)≥0. Thus M≥d proves
+(5). For b=1 the argument is immediate. This is PR6817's cited classical
+packing argument, not a new optimization theorem.
+
+Apply (5) separately to the s ranks in (3) and t ranks in (4). Their actual
+costs add, proving the lower bound (1), even with singular/nonprojector paid
+couplings and arbitrary free scalar interleavings.
+
+## Full formal attainment and boundary
+
+Partition the first d coordinate roles into floor(d/b) disjoint blocks of
+size b and, if nonempty, one remainder block of size d mod b. Let E_B be a
+block's coordinate projector. The legal factors obey the full algebra identity
+
+    F_s(E_B)F_t(E_B)=I+([st]−[e])E_B.
+
+Indeed they act as [s][t] on that block and as identity on its complement.
+Different blocks have disjoint supports. Their products are exactly T_d,
+including every spectator column and row. No free basis operation, preparation
+or restoration is needed. Each letter's cost is P_(b,f)(d), proving attainment.
+If b>r≥d, there are no full b-blocks; the one rank-d remainder is legal, so
+the apparently unavailable rank b is never invoked. Empty remainders require
+no rank-zero paid call.
+
+PR6817 already covers divisible identical targets, every single-reflection
+remainder and d=3,b=2 for st. Formula (1) completes this particular two-letter
+target's remainder family. It does not extend to the different longest target
+sts, heterogeneous targets, other reflection alphabets or tariffs. In
+particular the combined root-orbit packing floor alone must not replace the
+two separate letter constraints. The result does not reclassify prior rank-one
+st words or claim an unrestricted circuit optimum outside this paid grammar.
+
+## Credit and limits
+
+Credit Adam Gall1941 and Ross Richardson1966 for the established separate-letter
+cut/rank-volume method; David Arias2738 and its retained root/model lineage;
+Benny Zhao/zhaobenny6817 for the all-field arbitrary-coupling model, concave
+packing and existing divisible/single-reflection/three-target st results;
+Nick Petalas5083 for the distinct longest-element batching schedule; and
+ToikY6550 for the earlier all-field rank-one st classification. Standard rank
+subadditivity and tensor-rank multiplication are elementary methods.
+
+Substantial source-aware OpenAI Codex assistance is disclosed. The coordinator
+proposed this recipe during source orientation, before expanded review identified
+the established separate-cut predecessors; this is not a blind derivation or
+literature-priority claim. Finite checks, if provided, corroborate
+the written theorem and full formal endpoints, not all possible words. No
+native rank primitive, physical price for scalar mixing, owned allocation,
+restoration/routing/precision/stock/caller bill, all-size recursion or selected
+supplier is supplied. All five framework assumptions and the frontier remain
+unchanged. No human or proof-kernel acceptance is claimed.

research/a2-st-all-cap-tariff/README.md

@@ -0,0 +1,97 @@
+# All-cap formal tariff for repeated A2 st targets
+
+This answers the repeated `st` part of [PR6817](https://github.com/CrocSwap/integer-mult-bounds/pull/6817)'s
+nondivisible-target question. It applies **established separate-letter cuts**
+to that source's common concave rank price; no new cut principle is claimed.
+
+Let K be any field, d>=1, b>=1, and r>=d any finite number of arbitrary-input
+scalar roles. The only paid address generators are the simple involutions s,t
+of S3. A paid factor is `I+([u]-[e])A`, u in {s,t}, with arbitrary scalar A
+of positive rank at most b. A may be singular or nonidempotent. Interleaved
+scalar GL_r(K) maps are free. The complete endpoint in M_r(K[S3]) is
+`diag([st],...,[st],[e],...,[e])`, with d productive roles and every spectator
+restored, including all off-diagonal group coefficients.
+
+For a common nonnegative, nondecreasing, discretely concave price f on
+0..b with f(0)=0, the exact tariff is
+
+```
+2 * (floor(d/b) * f(b) + f(d mod b)).
+```
+
+The selective regular-representation cuts `{e,t}` and `{e,s}` give separate
+rank-volume demands d. Applying the credited integer-packing lemma to each
+letter gives the lower price; disjoint coordinate blocks of size at most b
+give a matching full formal word. [PROOF.md](PROOF.md) states the argument
+over every field, including characteristic two, with arbitrary restored dirty
+workspace. [RESULT.json](RESULT.json) retains the completed finite
+corroboration. The universal statement is a written proof,
+separate from finite execution, human review and proof-kernel acceptance.
+
+The source's three-target/cap-two result and divisible cases are credited
+positive cases. The new scope is all d and b, including every nondivisible
+remainder for this specific two-letter target. Other multi-reflection or
+heterogeneous targets are outside this result.
+
+## Evidence and reproduction
+
+The new standard-library verifier authenticates the four retained source
+prose files before calculating. It checks the selective cut ranks with
+arbitrary scalar couplings over finite fields, complete signed attaining
+endpoints with dirty-role mixing, formal prices and meaningful semantic
+controls. It imports and runs no predecessor scientific checker, word,
+constructor, census or native program. The retained result covers all 722 scalar 2-by-2 matrices over F2/F3/F5
+(668 nonprojectors), 2,888 one-gate cut checks, 108 complete formal endpoints
+with 378 paid calls (297 mixing dirty roles), 144 exact price cases and seven
+controls. Arbitrary-coupling exhaustion is a one-gate cut test, not all-word
+optimality. Nonconcave/nonmonotone controls refute the packing lemma outside
+its premises; they are not completed legal-word counterexamples. The first
+run took 0.161 seconds / 21.65625 MiB; normal and optimized replays give the
+same 49,624-byte packet. The written proof supplies the universal statement.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/a2-st-all-cap-tariff
+python3.12 -B scripts/check_research_commit.py --package research/a2-st-all-cap-tariff
+```
+
+SOURCES.json binds four canonical-main provenance files. SOURCE-PINS.json
+records the exact foreign PR6817 head/path/blob/mode/hash associations and
+authenticates the byte-identical retained prose. That foreign association was
+checked during source acquisition; it is separate from the generic canonical
+Git ancestry check. Caching an open PR's commit does not make it publication
+history. Direct replay authenticates retained bytes, has no external live file
+or network dependency, and does not claim foreign ancestry. Registered normal
+and optimized commands compare the entire typed result. No new dependencies
+are required.
+
+## Open next questions
+
+Can one actual rank-capped native call be implemented with a complete price?
+Start with its native/address layout, arbitrary input and owned/restored fields,
+coupling-rank interpretation, movement and precision before assigning a new
+construction round. No such realization or map from scalar coupling rank to
+recursive child rank is supplied here. Free scalar GL maps are a formal-model
+assumption, not a physical cost waiver. Ownership, restoration, routing,
+all-size compilation, stock, precision, outer bounds and the complete supplier
+invoice remain open; all five selected assumptions and the frontier are unchanged.
+
+## Credit and scope
+
+Prepared for [ToikY](https://github.com/ToikY) with substantial source-aware
+OpenAI Codex proposal, source/overlap, proof/implementation and related-role
+review assistance. The provisional cut recipe arose during orientation before
+the claim; expanded review then identified and credited its prior method.
+Roles saw the sources and proposal; this is not blind independent acceptance.
+
+Credit Adam Gall #1941's separate cuts; Ross Richardson #1966/#1989's odd
+dihedral, separate-letter and symmetric cut work; Benny Zhao / zhaobenny
+#6817's model, concave packing lemma and three-target tariff; David Arias
+#2738's Coxeter framework; Nick Petalas #5083's distinct longest-element
+schedule; own excluded #6550's rank-two shortest-word classification; and
+their retained Adam Gall, Ross Richardson, ywz65, eumemic, Ali Romman and
+Gareth Davidson lineage. Those theorems, classifications and old finite
+replays are not claimed again. Rank subadditivity, regular representations,
+concave concentration and block batching are classical. Source notices are
+retained verbatim; new work is Apache-2.0. The `bit-new-register-model` card
+is explicitly changed to this partial formal tariff application; its native
+conversion and complete-supplier acceptance gate remain unmet.