Ordered-instance allocation transfer with exact extra-copy preservation

Dev D. Goyal

Ordered-instance allocation transfer with exact extra-copy preservation

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Ordered-instance reduction for allocating indivisible goods with extra copies
Posed in: Attributed to Akrami et al., arXiv:2502.09377v3; source conventions unverified
Status: New theorem
Result: Any set-valued ordered allocation under nonnegative additive valuations transfers to named goods with every agent's utility weakly higher, the same total number of extra copies, the same per-good cap, and every good allocated.

Abstract

A set-valued ordered-instance transfer preserving utility improvement, the exact extra-copy count, per-good caps and coverage.

Details

Year: 2026
Discipline: Theoretical computer science
Area: Fair division
Subject: Fair division
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: ordered-allocation
Keywords: fair division, fair allocation, indivisible goods, ordered instances, Hall's theorem, additive valuations

Statement and scope

Formal scope. The transfer theorem is formalized. Existence of a fair allocation before transfer is outside the result; external source comparison is provisional.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 276 KB
PDF on GitHub: papers/theoretical-computer-science/ordered-allocation/manuscript.pdf
LaTeX source: papers/theoretical-computer-science/ordered-allocation/manuscript.tex
Bibliography: papers/theoretical-computer-science/ordered-allocation/references.bib

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/theoretical-computer-science/ordered-allocation/

Lean project

papers/theoretical-computer-science/ordered-allocation/formalization/ 2 Lean files

Lakefile

papers/theoretical-computer-science/ordered-allocation/formalization/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

formalization/OrderedAllocationReduction.lean

Reproduce

The commands below are quoted from papers/theoretical-computer-science/ordered-allocation/README.md, which gives their context and working directory.

Build

mkdir -p .build
latexmk -pdf -interaction=nonstopmode -halt-on-error -outdir=.build manuscript.tex
cp .build/manuscript.pdf manuscript.pdf

Formal reproduction

cd formalization
lake exe cache get
bash verify.sh

README: papers/theoretical-computer-science/ordered-allocation/README.md
Formalization notes: papers/theoretical-computer-science/ordered-allocation/FORMALIZATION.md
Source provenance: papers/theoretical-computer-science/ordered-allocation/SOURCE_PROVENANCE.md
Authorship: papers/theoretical-computer-science/ordered-allocation/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Questions and answers

What does this paper prove?

For finite goods, a nonempty finite set of agents and nonnegative additive real values, every set-valued ordered allocation can be transferred to named goods so that every utility weakly increases, the total extra-copy count is preserved exactly, the per-good cap is respected and every good is allocated. Bundle sizes and the identity of copied goods need not be preserved.

Does it prove that one extra copy suffices for exact maximin-share fairness?

No. It transfers achieved utility thresholds but does not establish existence of a fair allocation, and the comparison with the motivating question attributed to Akrami et al. (arXiv:2502.09377v3) is provisional.

Is the proof formally verified?

Lean 4 formalizes the transfer theorem and its budget and utility-threshold corollaries. The polynomial-size matching construction and its runtime are a conventional argument, not formalized.

Cite

Citation file papers/theoretical-computer-science/ordered-allocation/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{Goyal2026OrderedAllocation,
  author = {Dev D. Goyal},
  title = {Ordered-instance allocation transfer with exact extra-copy preservation},
  year = {2026},
  note = {Unpublished manuscript. Historical novelty remains provisional}
}