Skip to content

Prove the exact uniform-fee target refinement optimum and halving test (no κ) - #6651

Open
petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w10-1102l-target-split-ceiling
Open

petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w10-1102l-target-split-ceiling

Conversation

@petalas

@petalas petalas commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

Result

Claim type: scoped written proof with exact finite corroboration. No κ change; the selected record stays 781451/250000000.

A productive target of rank R is refined into k independent integer-rank targets, and each piece after the first pays the same fee c. The rank tariff φ is nondecreasing and concave with φ(0)=0, which covers r^t for 0<t<1 and the comparator's cap tariffs. Under these assumptions:

  1. For each k, the balanced partition is optimal (Karamata).
  2. The balanced credit S(k) is concave in k. It equals k·ψ(R/k), the perspective of the piecewise-linear interpolant ψ of φ.
  3. The optimum is S(k*) − (k−1)c, where k is the first k with S(k+1) − S(k) ≤ c.
  4. Halving test: some refinement pays if and only if φ(⌊R/2⌋) + φ(⌈R/2⌉) − φ(R) > c.

At t = 1 − 781451/250000000, with one extra paid rank-q job per piece (c = q^t), a refinement can first pay at R = 470, 940, 1880 and 3760 for q = 1, 2, 4 and 8. These numbers use the selected value as the tariff exponent for illustration only. They make no claim about the binding supplier's normalization or about any actual helper target.

Predecessors and the new part

Evidence and reproduction

Package: research/uniform-fee-target-refinement/. The written proof is in the README. Interpreter: ~/git/integer-mult-bounds/.venv/bin/python3.12 (CPython 3.12, standard library only).

python3.12 -B research/uniform-fee-target-refinement/verify.py
python3.12 -O -B research/uniform-fee-target-refinement/verify.py
python3.12 -B scripts/research_package.py --package research/uniform-fee-target-refinement
python3.12 -B scripts/check_research_commit.py --package research/uniform-fee-target-refinement --check-source-history

Local results at 7f73f71ad336ab6b16c1f1d2e71ded7ce19444c5. The second commit changes only README credit text and re-passes every check:

  • PASS_UNIFORM_FEE_TARGET_REFINEMENT exact_checks=10392 controls=2 thresholds=q1:R>=470 q2:R>=940 q4:R>=1880 q8:R>=3760 under both flags, about 1.6 s each.
  • PASS_REGISTERED_RESEARCH_PACKAGE.
  • PASS_RESEARCH_COMMIT_BYTES.

The verifier enumerates every integer partition of R ≤ 22 under eight exact rational concave tariffs and 38 fees, and checks items 1–4 against brute force. Two controls show that the hypotheses matter: a non-concave nondecreasing tariff where halving loses but a three-way split gains, and a convex tariff where an unbalanced pair wins. The thresholds use 60-digit correctly rounded Decimal arithmetic with a certified gap of at least 1e-40. Every R up to 7520 is checked on both sides of each threshold.

Limitations

  • This is an accounting statement for a uniform per-piece fee. It does not establish independence, chronological availability, native delivery, restoration, compiler closure or caller cost for any split.
  • Rank-dependent or shared fees fall outside the theorem.
  • The finite checks corroborate the proof. The all-R statement rests on the written argument.
  • No selected replay, Lean or Docker run. Independent human and proof-kernel review are unclaimed.

Open next questions

  • Do the balanced optimum and a halving test survive rank-dependent fees, for example c + d·φ(r_i)?
  • Which selected P104 productive targets have rank above 470, and what is the cheapest legal per-piece fee for each? This is blocked because scripts/export_selected_invoice.py reports the PR6030 source as unsupported.
  • What is the joint optimum when several splits share one fixed adapter fee?

Related open work

Credit

Produced by Nick Petalas. Predecessors: Ali Romman's #5769 fee-charged target-partition contract and optimizer, and #5909's unit-fee threshold at exponent 99/100. The signed mixed-target invoice model and the concave-order comparator are by zxv. Karamata's inequality and perspective concavity are classical.

CI notes

Both hosted checks passed at head 7f73f71ad336ab6b16c1f1d2e71ded7ce19444c5 in run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/41661215990: plan (5m2s) and replay (research/uniform-fee-target-refinement) (2m12s).

Balanced splits are optimal for each piece count and their credit is
concave in the count, so any uniform-fee refinement pays only if halving
pays. Certify the selected-exponent thresholds R >= 470, 940, 1880, 3760
for one extra paid rank-1, 2, 4, 8 job per piece.
…ssors

Cite CrocSwap#5769's fee-charged partition contract and CrocSwap#5909's unit-fee
threshold at exponent 99/100 as predecessors. State the new part and how
the per-piece and per-extra-piece fee normalizations relate.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant