[petalas]

Summary

This scoped written proof with exhaustive finite corroboration answers Open next question 1 of unpaidmoon's #7449: find a maximizing positive partition for the negative-slope Reading B credit, rather than only deciding whether an improving partition exists.

for each piece count k
  choose shortest free rank s
  balance the k-1 charged ranks
  locate the first nonpositive forward difference by binary search
compare these exact values and the unsplit target

For every nondecreasing discretely concave tariff with phi(0)=0, d<0 and c>=0, the reduced objective is concave in s. Its forward difference is delta(s+1) - (1-d) delta(ceil((R-s)/(k-1))). The algorithm returns an exact maximizing partition in O(R log R) arithmetic operations and comparisons in the tariff-oracle model. At zero fee, all singleton pieces attain the maximum for every tariff; for the harmonic tariff this maximizing multiset is unique at every rank.

No new kappa, supplier admission or selected-frontier change. The proof and rational optimizer are self-contained in research/negative-slope-partition-optimizer/.

Evidence

Before, #7449 provides an existence threshold and explicitly leaves the maximizer open. After, PROOF.md supplies the all-rank normal form, monotone difference test and exact optimizer. The harmonic R=12, d=-1, c=0 three-piece optimum is (2,5,5) with credit 41747/5544, strictly above both the balanced and extreme three-piece partitions.

At head 480c71bb69c305b72096f92db234bda53518ec2c, local CPython 3.12.15 warning-strict normal and optimized commands pass with zero errors: 1,000 concave integer tariff tables through rank 10, harmonic tariffs through rank 20, 3,080 tariff/slope cases, 87,703 literal partition scores, 396,388 free-piece choices, 21,784 fixed-length comparisons, 16,208 first-difference identities and 15,400 global comparisons. Six witness checks and thirteen failure controls cover interior optima, ties, invalid contracts and a nonconcave balancing failure. Literal enumeration runs at zero fee; each fixed-length maximum then receives its exact length fee for five nonnegative fee values.

Both registered checks ran locally in 2.56 and 2.43 seconds, below their 240-second limits. These are single-run timeout checks, not benchmark claims. The committed package replay passed in 5.37 seconds. Metadata/pins and the exact six committed files, modes and source-history check passed. A generated receipt binds successful counts and interpreter details to package-file SHA256 values. No receipt is hand-written.

Reproduce from the repository root:

IMB_PYTHON=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12
"$IMB_PYTHON" -I -W error -B research/negative-slope-partition-optimizer/verify.py
"$IMB_PYTHON" -I -O -W error -B research/negative-slope-partition-optimizer/verify.py
"$IMB_PYTHON" -B scripts/research_package.py --package research/negative-slope-partition-optimizer
"$IMB_PYTHON" -B scripts/check_research_commit.py --package research/negative-slope-partition-optimizer --check-source-history --check-modes

Expected markers are PASS_NEGATIVE_SLOPE_PARTITION_OPTIMIZER, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Sources, scope and limitations

Question source: unpaidmoon #7449, head 180fac9c9797fee6ec44df8d9540f71612d07e1a. unpaidmoon #7299 supplies the Reading B definition. The new proof uses that definition and elementary discrete concavity; neither predecessor theorem nor executable is replayed. Retain aliromman #5769's fee-contract lineage and Nick Petalas #6651's uniform-fee background, with #5909 as earlier unit-fee context. This contribution was produced by Nick Petalas. Classical balancing and binary search receive no literature-priority claim.

Card coverage-law-change has changed scope to this accounting question. Base is canonical main e54523517d0f03e58352e647c403a5af3e525a57; selected #7000 and priority revision 8 are unchanged. The CLAIM is #1166 (comment). Live open PRs, active Discussions, local claim locks, main's complete committed README inventory and merged searches were checked before claiming and committing. The overlap helper disclosed sparse local omissions and an account-filtered closed-PR timeout; the separate all-state own-PR list and merged searches supplement that coverage. Searches do not establish novelty.

The implementation accepts rational tariffs and ranks through 4096. The written proof covers arbitrary ranks and real parameters with exact comparisons; the finite census is corroboration. The operation bound is not a bit-complexity or physical-tape bound. A legal adapter, chronological independent delivery, dirty restoration, native implementation and a complete supplier invoice remain unproved. All five selected assumptions remain. Independent human and formal proof-kernel review are unclaimed. Lean, Docker, selected scientific replays and predecessor suites were not run.

Related open work

• Prove the Reading B existence test for a negative slope #7449 proves existence for the same negative-slope fee; this contribution determines a maximizing partition and does not re-check that proof.
• Prove rank-dependent target-fee optima and halving tests #7299 studies both fee readings and proves Reading A optima and nonnegative Reading B existence; the present maximum concerns negative Reading B.
• Name the physical adapter of selected helper 759. #7445 identifies helper 759's physical adapters and distinguishes them from the abstract fee readings; this contribution supplies no physical instantiation.
• Exclude fixed-word singleton P104 helper splits (0% κ change) #7303 bounds fixed-word singleton splits and a charged two-way moment; this contribution optimizes a declared abstract fee and makes no numerical comparison with that physical model.

Open next questions

1. Can the best piece count be located without comparing every k? First study discrete curvature of the optimized fixed-length values; maximization over s does not itself preserve concavity in k.
2. Does one actual helper adapter realize this negative-slope fee with independent delivery? First specify its producer, consumer, charge and complete restoration contract. Accounting gains alone do not supply that construction.

The completion refresh read this account's seven other open PRs created since the CLAIM: #7469, #7470, #7471, #7473, #7474, #7476 and #7477. Their titles and bodies concern different objects. None studies negative-slope Reading B partition maximization or computes a competing value, so no additional same-object line or numerical comparison is needed. No extra mathematics was run to compare them.

CI notes

CI did not certify this package. At unchanged head 480c71bb69c305b72096f92db234bda53518ec2c, run 43290173932, plan job 131434002061, failed in Onboarding helper tests. I read the completed checks once and confirmed the cause directly in the failed job log.

Exactly one of 760 tests failed, with 24 skipped: test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record. At tests/test_research_current_status.py:58, the AssertionError says that `make frontier7000-verify` was not found in the CI verification document. The replay job was skipped after plan failed; no hosted package replay ran.

I read the three relevant files at canonical main e54523517d0f03e58352e647c403a5af3e525a57 and compared them with this PR head. They are byte-identical: certificates/selected-result.json names make frontier7000-verify, while the current section of docs/ci-verification.md still describes #6030 and make frontier6030-verify. The failing test is unchanged too. This is a repository-level navigation mismatch, separate from the passing local package verification.

I independently read and checked the failed-job logs for all of these other runs. Each has that same sole failing test and missing-command assertion, with 760 tests and 24 skipped:

• rohanarun: run 42905094314, job 130140894651.
• dillona: run 42903313790, job 130134720799.
• petalas: run 43279933171, job 131398194664.
• petalas: run 43289715434, job 131432409153.
• petalas: run 43290064692, job 131433624254.

Both registered verification commands, the package replay, metadata/pins and committed-byte/mode/source-history checks passed locally at this head. No CI fix, retrigger commit, push or workflow rerun was made. Maintainers own the repair of main.

Merge Danger

Door: two-way. Blast radius: one new research directory. Shared code, frozen predecessors and the selected frontier are unchanged.