diff --git a/research/a2-st-monotone-tariff/PROOF.md b/research/a2-st-monotone-tariff/PROOF.md new file mode 100644 index 0000000000..d4e7ae9e1b --- /dev/null +++ b/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. diff --git a/research/a2-st-monotone-tariff/README.md b/research/a2-st-monotone-tariff/README.md new file mode 100644 index 0000000000..4c3c5331f8 --- /dev/null +++ b/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. diff --git a/research/a2-st-monotone-tariff/RESULT.json b/research/a2-st-monotone-tariff/RESULT.json new file mode 100644 index 0000000000..41e97a2475 --- /dev/null +++ b/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 +} diff --git a/research/a2-st-monotone-tariff/SOURCES.json b/research/a2-st-monotone-tariff/SOURCES.json new file mode 100644 index 0000000000..131d3abdb4 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/a2-st-monotone-tariff/TASK.json b/research/a2-st-monotone-tariff/TASK.json new file mode 100644 index 0000000000..8f2773e0dd --- /dev/null +++ b/research/a2-st-monotone-tariff/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Exact repeated A2 st tariff for independent nonnegative nondecreasing rank prices and separate caps, without concavity.", + "scope_change_reason": "The card seeks native mechanism changes. This scoped formal-price side result extends the common-concave hypothesis of ToikY PR6821; no native conversion or complete supplier is supplied.", + "bottleneck_link": "A hypothetical native rank-capped interface may have nonconcave or letter-dependent complete prices. This theorem prices its repeated-st formal boundary exactly; physical realization and recursive relevance remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact monotone-price extension and package it; do not extend to new targets or decreasing tariffs.", + "outcome": "completed", + "evidence": "PROOF.md supplies the uniform argument using cited separate-letter rank floors. verify.py recomputes RESULT.json, exact partition oracles, truncation cases, full formal dirty-restored words and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physical rank-capped native interface realize a complete nonconcave or letter-dependent tariff that benefits from independent partitions?", + "why_it_matters": "A formal price gain does not itself change a recursive invoice or kappa.", + "first_step": "Specify one arbitrary-input native call, including movement, frames, ownership, scalar mixing and restoration, then price the whole boundary.", + "blocked_by": "No physical call or scalar-rank to recursive-child-rank conversion is provided." + }, + { + "question": "What exact tariff replaces the monotone theorem for one explicitly decreasing rank-price table?", + "why_it_matters": "Clipping excess rank can increase its price when monotonicity fails.", + "first_step": "Construct a full dirty-restored formal word under a chosen decreasing table and compare with the exact-mass partition relaxation.", + "blocked_by": "The present truncation inequality does not apply." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538484", + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "playbook": "Autonomous local run", + "source_question": "PR #6821 common-concave repeated-st tariff; independent monotone price extension" +} diff --git a/research/a2-st-monotone-tariff/VERIFY.json b/research/a2-st-monotone-tariff/VERIFY.json new file mode 100644 index 0000000000..8bb245fc18 --- /dev/null +++ b/research/a2-st-monotone-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact partition oracle, monotone truncation, full signed formal endpoints, paid ranks, faithful regular basis columns, omission and input controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat the same complete finite checks with optimized Python; compare the freshly generated source-bound receipt." + } + ] +} diff --git a/research/a2-st-monotone-tariff/verify.py b/research/a2-st-monotone-tariff/verify.py new file mode 100644 index 0000000000..e394ecb5a8 --- /dev/null +++ b/research/a2-st-monotone-tariff/verify.py @@ -0,0 +1,304 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the new monotone two-letter tariff.""" + +import argparse +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations_with_replacement, permutations, product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def optimum(demand, prices): + need(type(demand) is int and 0 <= demand <= 32, "demand bound") + need(2 <= len(prices) <= 33, "price capacity") + need(prices[0] == 0, "zero price") + need(all(isinstance(x, (int, Fraction)) for x in prices), "exact prices") + need(all(a <= b for a, b in zip(prices, prices[1:])), "monotone price") + costs = [Fraction(0)] * (demand + 1) + words = [()] * (demand + 1) + cap = len(prices) - 1 + for total in range(1, demand + 1): + candidates = [(prices[k] + costs[total-k], (k,) + words[total-k]) + for k in range(1, min(cap, total) + 1)] + costs[total], words[total] = min(candidates) + need(sum(words[demand]) == demand, "partition mass") + return costs[demand], words[demand] + + +def partitions(demand, cap): + """Independent count-vector oracle; no optimizer recurrence.""" + need(0 <= demand <= 8 and 1 <= cap <= 5, "oracle capacity") + result = [] + ranges = [range(demand // k + 1) for k in range(1, cap + 1)] + for counts in product(*ranges): + if sum(k*c for k, c in enumerate(counts, 1)) == demand: + result.append(tuple(k for k, c in enumerate(counts, 1) + for _ in range(c))) + need(bool(result), "oracle has a partition") + return result + + +def check_optimizer(): + cases = nonconcave = 0 + for cap in range(1, 6): + for tail in combinations_with_replacement(range(4), cap): + prices = (0,) + tail + slopes = tuple(b-a for a, b in zip(prices, prices[1:])) + for demand in range(9): + value, _ = optimum(demand, prices) + expected = min(sum(prices[k] for k in parts) + for parts in partitions(demand, cap)) + need(value == expected, "partition oracle disagreement") + cases += 1 + nonconcave += int(any(a < b for a, b in zip(slopes, slopes[1:]))) + return {"partition_optima": cases, "nonconcave_optima": nonconcave} + + +def check_truncation(): + cases = 0 + for cap in range(1, 5): + for count in range(1, 6): + for ranks in combinations_with_replacement(range(1, cap+1), count): + for demand in range(1, min(8, sum(ranks)) + 1): + remaining = demand + clipped = [] + for rank in ranks: + kept = min(rank, remaining) + clipped.append(kept) + remaining -= kept + need(remaining == 0, "unfilled truncation") + need(sum(clipped) == demand, "wrong truncation mass") + for tail in combinations_with_replacement(range(3), cap): + prices = (0,) + tail + original = sum(prices[k] for k in ranks) + reduced = sum(prices[k] for k in clipped) + best, _ = optimum(demand, prices) + need(original >= reduced >= best, "truncation tariff") + cases += 1 + return cases + + +def eye(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def add(a, b, p, sign=1): + rows = tuple(tuple(x + sign*y for x, y in zip(ar, br)) + for ar, br in zip(a, b)) + return tuple(tuple(x % p if p else x for x in row) for row in rows) + + +def mm(a, b, p): + n = len(a) + return tuple(tuple(sum(a[i][k]*b[k][j] for k in range(n)) % p + if p else sum(a[i][k]*b[k][j] for k in range(n)) + for j in range(n)) for i in range(n)) + + +def rank(a, p): + m = [[Fraction(x) if not p else x % p for x in row] for row in a] + n = len(m) + pivot = 0 + for col in range(n): + choices = [i for i in range(pivot, n) if m[i][col]] + if not choices: + continue + row = choices[0] + m[pivot], m[row] = m[row], m[pivot] + scale = pow(m[pivot][col], -1, p) if p else 1/m[pivot][col] + m[pivot] = [(x*scale) % p if p else x*scale for x in m[pivot]] + for i in range(pivot+1, n): + scale = m[i][col] + m[i] = [(x-scale*y) % p if p else x-scale*y + for x, y in zip(m[i], m[pivot])] + pivot += 1 + return pivot + + +IDENTITY = (0, 1, 2) +S = (1, 0, 2) +T = (0, 2, 1) +GROUP = tuple(permutations(range(3))) + + +def compose(a, b): + return tuple(a[b[i]] for i in range(3)) + + +def formal_multiply(a, b, p): + n = len(next(iter(a.values()))) + zero = tuple((0,) * n for _ in range(n)) + result = {} + for g, x in a.items(): + for h, y in b.items(): + label = compose(g, h) + result[label] = add(result.get(label, zero), mm(x, y, p), p) + return {g: x for g, x in result.items() if x != zero} + + +def factor(label, coupling, p): + return {IDENTITY: add(eye(len(coupling)), coupling, p, -1), label: coupling} + + +def construction(demand, left, right, p): + need(1 <= demand <= 8, "formal fixture capacity") + need(sum(left) == sum(right) == demand, "construction mass") + n = demand + 1 + factors = [] + ranks = [] + for label, parts in ((S, left), (T, right)): + start = 0 + for size in parts: + coupling = tuple(tuple(int(i == j and start <= i < start+size) + for j in range(n)) for i in range(n)) + factors.append(factor(label, coupling, p)) + ranks.append(size) + start += size + expected = {IDENTITY: tuple(tuple(int(i == j == demand) for j in range(n)) + for i in range(n)), + compose(S, T): tuple(tuple(int(i == j and i < demand) + for j in range(n)) for i in range(n))} + return factors, tuple(ranks), expected + + +def gauges(n, p): + forward, backward = eye(n), eye(n) + for i, j in ((0, n-1), (n-1, 0)): + unit = tuple(tuple(int(r == i and c == j) for c in range(n)) + for r in range(n)) + forward = mm(forward, add(eye(n), unit, p), p) + backward = mm(add(eye(n), unit, p, -1), backward, p) + need(mm(forward, backward, p) == eye(n), "gauge inverse") + return forward, backward + + +def regular_apply(formal, vector, p): + """Faithful action on labelled role vectors, separate from convolution.""" + n = len(vector[0]) + out = [[0]*n for _ in GROUP] + for h_index, h in enumerate(GROUP): + for g, matrix in formal.items(): + target = GROUP.index(compose(g, h)) + for i in range(n): + out[target][i] += sum(matrix[i][j]*vector[h_index][j] + for j in range(n)) + return tuple(tuple(x % p if p else x for x in row) for row in out) + + +def check_regular(factors, expected, p): + n = len(next(iter(expected.values()))) + for g in range(6): + for role in range(n): + vector = tuple(tuple(int(i == g and j == role) for j in range(n)) + for i in range(6)) + actual = vector + for f in reversed(factors): + actual = regular_apply(f, actual, p) + need(actual == regular_apply(expected, vector, p), "regular endpoint") + return 6*n + + +def check_constructions(): + fixtures = paid = columns = omissions = dirty_coupled = unequal_caps = 0 + missing_boundary_maps = 0 + for demand in range(1, 9): + cap_pairs = [(cap, cap) for cap in range(1, min(5, demand+2)+1)] + cap_pairs += [(2, 3), (4, 1)] + for s_cap, t_cap in cap_pairs: + s_prices = (0,) + tuple(3+k*k for k in range(1, s_cap+1)) + t_prices = tuple(Fraction(k, k+1) for k in range(t_cap+1)) + _, left = optimum(demand, s_prices) + _, right = optimum(demand, t_prices) + for p in (0, 2, 3, 5): + factors, ranks, expected = construction(demand, left, right, p) + forward, backward = gauges(demand+1, p) + changed = [{g: mm(mm(backward, x, p), forward, p) + for g, x in f.items()} for f in factors] + for f, wanted in zip(changed, ranks): + label = next(g for g in f if g != IDENTITY) + need(rank(f[label], p) == wanted, "conjugated paid rank") + dirty_coupled += int(any(f[label][demand]) or + any(row[demand] for row in f[label])) + full = [{IDENTITY: forward}] + changed + [{IDENTITY: backward}] + actual = {IDENTITY: eye(demand+1)} + for f in full: + actual = formal_multiply(actual, f, p) + need(actual == expected, "full formal endpoint") + missing_map = formal_multiply(actual, {IDENTITY: forward}, p) + need(missing_map != expected, "missing exit map accepted") + missing_boundary_maps += 1 + if demand <= 3: + columns += check_regular(full, expected, p) + for skip in range(len(changed)): + mutant = {IDENTITY: eye(demand+1)} + for j, f in enumerate(full): + if j != skip+1: + mutant = formal_multiply(mutant, f, p) + need(mutant != expected, "omitted call accepted") + omissions += 1 + fixtures += 1 + unequal_caps += int(s_cap != t_cap) + paid += len(changed) + need(dirty_coupled > 0, "dirty coupling exercised") + return {"formal_endpoints": fixtures, "paid_calls": paid, + "regular_basis_columns": columns, "rejected_omissions": omissions, + "dirty_coupled_calls": dirty_coupled, "unequal_cap_endpoints": unequal_caps, + "rejected_missing_boundary_maps": missing_boundary_maps} + + +def check_example(): + s_prices = (0,) + tuple(3+k*k for k in range(1, 5)) + t_prices = tuple(Fraction(k, k+1) for k in range(5)) + s_cost, left = optimum(7, s_prices) + t_cost, right = optimum(7, t_prices) + need((s_cost, t_cost) == (25, Fraction(31, 20)), "example optimum") + need(sorted(left) == [1, 2, 2, 2] and sorted(right) == [3, 4], "example lists") + packed = s_prices[4]+s_prices[3]+t_prices[4]+t_prices[3] + need(packed-s_cost-t_cost == 6, "example gain") + return {"demand": 7, "cap": 4, "s_ranks": list(left), "t_ranks": list(right), + "s_cost": str(s_cost), "t_cost": str(t_cost), + "optimum": str(s_cost+t_cost), "packed_comparator": str(packed)} + + +def check_rejections(): + cases = ((-1, (0, 1)), (33, (0, 1)), (1, (0,)), + (1, (1, 2)), (1, (0, -1)), (1, (0, 2, 1)), (1, (0, 1.0))) + for demand, prices in cases: + rejected = False + try: + optimum(demand, prices) + except ValueError: + rejected = True + need(rejected, "invalid input accepted") + return len(cases) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + result = {"status": "PASS_A2_ST_MONOTONE_TARIFF", + "claim_type": "scoped written proof with finite corroboration", + "optimizer": check_optimizer(), "truncation_cases": check_truncation(), + "constructions": check_constructions(), "example": check_example(), + "input_rejections": check_rejections()} + package = Path(__file__).resolve().parent + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["sha256"] = {name: sha256((package/name).read_bytes()).hexdigest() + for name in files} + if args.emit_receipt: + print(json.dumps(result, sort_keys=True, indent=2)) + else: + frozen = json.loads((package/"RESULT.json").read_text()) + need(result == frozen, "receipt disagreement") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()