Prove exact repeated-st tariffs for independent monotone prices (no κ)

research/a2-st-monotone-tariff/PROOF.md

@@ -0,0 +1,142 @@
+# Independent monotone prices for the repeated two-letter target
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Model and result
+
+Retain the model of ToikY's [#6821](https://github.com/CrocSwap/integer-mult-bounds/pull/6821).
+Let K be any field and G=S3, with simple involutions s,t. Let d>=1 and
+r>=d be finite. The complete required endpoint in M_r(K[G]) is
+
+    T_d = diag([st], ..., [st], [e], ..., [e]),
+                   d copies
+
+with arbitrary initial data on every role. Every spectator and every
+off-diagonal coefficient must be restored. A paid factor is
+
+    F_u(A) = I + ([u]-[e]) A,  u in {s,t},  0 < rank_K(A) <= b_u.
+
+The finite positive integer caps b_s,b_t may differ. A can be singular or
+nonidempotent. Interleaved scalar GL_r(K) maps are free. No free address
+maps, resets, discarded outputs or clean allocations are allowed.
+
+For each u let tau_u:{0,...,b_u}->R be nonnegative and nondecreasing, with
+tau_u(0)=0. A u-call costs tau_u(rank A). The two tables need not agree or
+be proportional, concave or convex. Set K_u=min(b_u,d) and define
+
+    H_u(0) = 0,
+    H_u(m) = min_{1 <= k <= min(K_u,m)} [tau_u(k)+H_u(m-k)],
+                                      1 <= m <= d.
+
+**Theorem.** The exact minimum bill for T_d is H_s(d)+H_t(d). Independent
+minimizing partitions for the two letters give an attaining word on the d
+productive roles, with no extra workspace. The two recurrences each have
+d+1 states and at most d K_u transitions.
+
+The universal claim is this written proof, using the cited separate-letter
+rank inequalities. The finite checker corroborates the new optimization
+and full attaining endpoints; it is not a census of all circuits.
+
+## Inherited lower bounds
+
+We cite #6821's PROOF.md, equations (3) and (4), for
+
+    sum_(s-calls) rank A >= d,
+    sum_(t-calls) rank A >= d.                         (1)
+
+Its selective regular cuts {e,t} and {e,s} apply over every field, to
+arbitrary couplings, free scalar mixing and any finite number of restored
+dirty roles. These are inherited inputs, not new cut inequalities or
+results audited here. Adam Gall #1941 and Ross Richardson #1966/#1989
+retain the separate-letter cut-method credit. ToikY applies those cuts to
+this repeated-st endpoint. Benny Zhao / zhaobenny #6817 and David Arias
+#2738 supply the retained formal model and Coxeter/packing context.
+
+## Monotone truncation and the exact price
+
+For either letter, list the positive paid ranks a_1,...,a_q of an arbitrary
+finite valid word. Equation (1) gives sum a_i>=d. There are integers
+0<=e_i<=a_i with sum e_i=d: visit the entries in order and keep the smaller
+of a_i and the remaining demand. The remaining demand reaches zero by
+the last entry. Each e_i<=min(b_u,d)=K_u. Monotonicity, including at zero,
+therefore gives
+
+    sum_i tau_u(a_i) >= sum_i tau_u(e_i) >= H_u(d).     (2)
+
+For the last inequality, drop zero entries. The recurrence is the minimum
+over all positive integer partitions of exact mass d and parts at most
+K_u. This follows by induction on the remaining mass: a first part k
+leaves the smaller instance m-k, and every partition has such a first
+part. There are finitely many candidates, so the minimum is attained.
+
+Truncation is a lower-bound argument about integer rank lists. It does
+not change the matrices of the original program or assert that truncating
+those matrices preserves their endpoint. It also handles ranks greater
+than d in a word with many dirty roles. Rank caps greater than r cause no
+problem: attaining parts are at most d<=r, and an unavailable rank is
+never requested.
+
+Apply (2) independently to s and t and add their actual costs. This proves
+the lower bound H_s(d)+H_t(d), including flat and zero prices. No bound on
+the number of spectators, beyond finiteness, is used.
+
+## Independent partitions attain the full endpoint
+
+Take a minimizing partition of d for s. Divide the first d coordinate
+roles into consecutive blocks of those sizes, and apply one s-factor with
+the coordinate projector of each block. Their product is
+
+    D_s = diag([s], ..., [s], [e], ..., [e]).
+
+Independently partition those same d roles using a minimizing partition
+for t. The blocks need not coincide with the s-blocks. Their t-factors
+multiply to D_t. In written product order the complete program is D_s D_t.
+It equals T_d coefficientwise in the full group algebra. Each spectator
+is untouched. Every call is a legal positive-rank projector with its own
+declared cap. This attaining construction requires no preparation, scalar
+maps or restoration. The price is exactly H_s(d)+H_t(d).
+
+Products act rightmost first, so a chronological implementation executes
+the t-blocks before the s-blocks. The proof and checker use written product
+order throughout. Free scalar maps are allowed in the lower bound; the
+upper word needs none. Gauged finite fixtures include them explicitly at
+both ends and restore the original full endpoint.
+
+## First strict extension
+
+At d=7 and b_s=b_t=4, use tau_s(k)=3+k^2 for positive k, tau_s(0)=0,
+and tau_t(k)=k/(k+1). Both tables are nondecreasing. The s-table has slopes
+4,3,5,7, so the common-concave theorem does not apply to it.
+
+The minimizing s-parts are 2,2,2,1, of price 25. A short lower certificate
+is tau_s(k)>=(7/2)k on 1<=k<=4, with an additional 1/2 whenever k is odd.
+Every partition of odd mass seven has at least one odd part, proving
+price at least 25. The t-parts 4,3 have price 31/20 by the credited concave
+packing lemma, or by enumerating the partitions of seven. Thus the exact
+bill is 531/20. Applying parts 4,3 to both letters would cost 651/20.
+The independent partitions save six under this declared abstract tariff.
+
+This comparison evaluates a legal coordinate word, rather than applying
+the predecessor's concave theorem outside its hypotheses. It changes no
+native or recursive invoice. The first verified extension ends this work.
+
+## Scope and credit
+
+The new result removes concavity and common pricing from #6821's exact
+repeated-st tariff, permits separate caps, and realizes independent optimal
+partitions. The rank demands, group-algebra model, partition dynamic
+programming and monotone clipping are credited or elementary inputs, not
+claimed as new general methods. Nick Petalas's older #4846 applies a
+related monotone-partition method to the different UT3 central endpoint;
+its shared degree-list issue does not occur in the consecutive two-letter
+construction here. Retain the #6821/#6817/#2738 register-model lineage,
+including ywz65, eumemic, Ali Romman and Gareth Davidson.
+
+No claim is made for decreasing prices, changed targets, other paid labels,
+free address maps or incomplete dirty restoration. Native realization,
+the price of scalar mixing, ownership, movement, frames, stock, precision,
+all-size compilation, recursive child-rank identification and the complete
+supplier/consumer invoice remain unknown. All five selected framework
+assumptions remain. No kappa or selected-frontier change, multiplication
+theorem, independent human review or formal proof-kernel acceptance is
+claimed.

research/a2-st-monotone-tariff/README.md

@@ -0,0 +1,137 @@
+# Exact repeated-st tariffs for independent monotone prices
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped written proof with exact finite corroboration; no new kappa.**
+For d repeated A2 targets st, the exact formal bill with different
+nonnegative nondecreasing rank-price tables is
+
+    H_s(d) + H_t(d),
+    H_u(0)=0,
+    H_u(m)=min_{1<=k<=min(b_u,d,m)} [tau_u(k)+H_u(m-k)].
+
+The separate finite rank caps b_s,b_t may differ. The two optimal rank
+partitions may differ. Concavity is unnecessary. The theorem holds over
+every field with arbitrary rank-capped scalar couplings, free scalar GL
+mixing and any finite number of restored dirty spectators. The complete
+endpoint is diag([st] repeated d,[e] repeated r-d) in M_r(K[S3]), including
+every off-diagonal group coefficient.
+
+[PROOF.md](PROOF.md) gives the proof and exact model. ToikY's
+[#6821](https://github.com/CrocSwap/integer-mult-bounds/pull/6821) supplies
+the separate-letter rank demands and the common-concave predecessor.
+Those results are cited inputs, not rechecked deliverables. The new step
+removes common pricing and concavity through monotone rank-list truncation
+and independent full formal constructions. The integer-partition method
+is classical; the related UT3 precedent is Nick Petalas's older #4846.
+
+At d=7 with cap four, let tau_s(k)=3+k^2 for k>0 and tau_t(k)=k/(k+1).
+The s-partition is 2,2,2,1, of price 25; the t-partition is 4,3, of price
+31/20. The exact bill is 531/20. Using parts 4,3 for both letters costs
+651/20. This six-unit improvement concerns the stated abstract tariff,
+not an admitted recursive invoice. The first verified extension ends this
+investigation.
+
+## Evidence and reproduction
+
+Use CPython 3.12 with the standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a2-st-monotone-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a2-st-monotone-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/a2-st-monotone-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a2-st-monotone-tariff --check-source-history --check-modes
+```
+
+Another installed CPython 3.12 can replace the local interpreter path.
+Expected markers are `PASS_A2_ST_MONOTONE_TARIFF`,
+`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+`--emit-receipt` prints a freshly generated source-hash-bound JSON receipt
+to stdout. Default execution recomputes and compares [RESULT.json](RESULT.json),
+writes no files and needs no Git or network. No receipt is handwritten.
+Source-provenance validation is separate from the standalone mathematics.
+
+The new checker compares the optimizer with an independently enumerated
+integer-partition oracle, including nonconcave tables and zero prices.
+It exercises monotone truncation on excess-rank lists, constructs complete
+signed group-algebra words over Q, F2, F3 and F5, checks actual paid ranks,
+and mixes an arbitrary dirty role through invertible scalar gauges with
+both endpoint maps included. A separate faithful regular-action engine
+checks every basis column of the smaller fixtures. Every omitted paid
+call must change its full endpoint. Invalid optimizer inputs must reject.
+The generated receipt records 1,125 partition optima, including 846
+nonconcave cases; 17,772 truncation cases; 212 full formal endpoints,
+including 64 with unequal caps; 1,344 regular-action basis columns;
+1,180 rejected paid-call omissions; 212 rejected missing scalar boundary
+maps; and seven invalid-input controls. There are 424 genuinely
+dirty-coupled calls among the 1,180 checked paid calls.
+
+The universal lower bound comes from the written proof and its credited
+rank-demand premise. Finite checks do not enumerate arbitrary circuits or
+establish a multiplication theorem. No predecessor scientific suite,
+selected cold replay, Lean or Docker run is part of this work. Independent
+human and formal proof-kernel review are unclaimed. Hosted CI remains
+separate from local evidence and scientific acceptance.
+
+## Scope, provenance and overlap
+
+The base is canonical main e54523517d0f03e58352e647c403a5af3e525a57,
+priority revision 8, selected #7000. The selected source-binding orientation
+passed; it was metadata orientation, not a scientific replay. The catalogue
+still describes #5599 and is treated as historical assessment context.
+TASK.json explicitly changes `bit-new-register-model` to a formal price
+side result. This does not satisfy the original native-conversion gate.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538484).
+Overlap checks covered live open PR metadata, this account's latest 200
+PRs, recent handoffs, active Discussions, the cached card search, main-tree
+README searches, and merged/all-state searches for Coxeter, repeated st,
+monotone and nonconcave tariffs. #6821's repeated-st common-concave
+restriction is the direct source. #6817 supplies the earlier common
+concave framework and different longest-element questions.
+Arbitrary code diffs, sparse local notes and unpublished work limit these
+searches. Absence of a match is not a novelty guarantee.
+
+[SOURCES.json](SOURCES.json) pins the source prose, original catalogue and
+selected record as historical provenance. The standalone verifier imports
+no predecessor code. Frozen packages, upstream and the selected frontier
+are unchanged. Retain ToikY #6821; Adam Gall #1941; Ross Richardson
+#1966/#1989; Benny Zhao / zhaobenny #6817; David Arias #2738; and their
+ywz65, eumemic, Ali Romman and Gareth Davidson register-model lineage.
+The new complete monotone-price statement and verifier were produced by
+Nick Petalas. No global literature-priority claim is made.
+
+## Open next questions
+
+Can one physically implemented rank-capped call support a complete
+nonconcave or letter-dependent price table that profits from independent
+partitions? First give its arbitrary-input entry/exit boundary and charge
+scalar mixing, movement, ownership, frames, restoration, stock, precision
+and all-size compilation. Native realization and the map from scalar rank
+to recursive child rank are unknown, so the abstract price does not admit
+a supplier. All five selected framework assumptions remain.
+
+For decreasing price tables, the monotone truncation proof fails. A next
+mathematical step would exhibit a complete formal counterexample or prove
+an exact replacement under a specific decreasing table, including dirty
+restoration. This work makes no claim for that changed hypothesis. These
+questions are structured in TASK.json; no continuation is reserved.
+
+## Verifier bounds and diagnostics
+
+The verifier has no recursion, subprocess, solver, network, dynamic import
+or shared mutable state. Optimizer demand and cap are at most 32; oracle
+demands are at most eight with cap at most five. Construction matrices
+have at most nine rows and six group labels. Every loop ranges over a
+fixed finite domain. Every function fits within sixty physical lines.
+Explicit exceptions preserve checks under optimization.
+
+Power of Ten rule 3 has a managed-Python allocation deviation confined to
+the bounded finite checker. Tuple/list/Fraction allocation and allocator
+internals are not fixed-capacity native memory. The finite domain bounds
+live collections; normal and optimized warning-strict replays check the
+same invariants. Reassess capacity and diagnostics before increasing these
+domains. File reads are restricted to the seven named package artifacts;
+no untrusted external input is read. No repository diagnostic configuration
+is changed. Full formal dirty-column checks and the separate regular
+action exercise the complete declared boundary.

research/a2-st-monotone-tariff/RESULT.json

@@ -0,0 +1,45 @@
+{
+  "claim_type": "scoped written proof with finite corroboration",
+  "constructions": {
+    "dirty_coupled_calls": 424,
+    "formal_endpoints": 212,
+    "paid_calls": 1180,
+    "regular_basis_columns": 1344,
+    "rejected_missing_boundary_maps": 212,
+    "rejected_omissions": 1180,
+    "unequal_cap_endpoints": 64
+  },
+  "example": {
+    "cap": 4,
+    "demand": 7,
+    "optimum": "531/20",
+    "packed_comparator": "651/20",
+    "s_cost": "25",
+    "s_ranks": [
+      1,
+      2,
+      2,
+      2
+    ],
+    "t_cost": "31/20",
+    "t_ranks": [
+      3,
+      4
+    ]
+  },
+  "input_rejections": 7,
+  "optimizer": {
+    "nonconcave_optima": 846,
+    "partition_optima": 1125
+  },
+  "sha256": {
+    "PROOF.md": "4008878df0ba14aa0c0443fc9086fb5188399452ef47c0c9a68d9eb92e3dc227",
+    "README.md": "f646ccbc07111f4cb45cc41774be91dd6bfb589bd8dd6553dc62fa8e140a64fd",
+    "SOURCES.json": "71e0573d2edac36c355d180462eebd0a687f51c6ff1cde7754d0c9f9e0aed398",
+    "TASK.json": "e58e8cfa8d73fb7f03cf36b8cc395b41fed1649af0cfb2274790bac71b78fb86",
+    "VERIFY.json": "6568a157c5206eb61e65b06f9ccaf02fdc52700cf9512dd5e58ca8a8f66ee9ca",
+    "verify.py": "8ee14eea640eabd8596bcf37e23d439673a65e88737c6c2c5d4ee0c770d5154d"
+  },
+  "status": "PASS_A2_ST_MONOTONE_TARIFF",
+  "truncation_cases": 17772
+}

research/a2-st-monotone-tariff/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "7f2279ec34893224361921529e7a7c9734405252",
+      "sha256": "76c25069149a699d9811c7e3dd92a9fd7271f271b5de87c9d215777b73b4999a"
+    },
+    {
+      "path": "research/a2-st-all-cap-tariff/README.md",
+      "usage": "provenance",
+      "git_blob": "65b290f04027f819b6d4295f9c6a921e2c6a1d0d",
+      "sha256": "83f19d188e3ec529ffbe5bc27013137227743b01654053a18249c8a4551c82a3"
+    }
+  ]
+}