Updated: 2026-08-31
The paper’s named theoretical surface is formalized. The checked surface includes the displayed fairness and allocation definitions, Theorems 1–3, their named supporting propositions and lemmas, the general-agent insertion remark, the explicit EFX witness used in Theorem 2, and the two named Appendix A propositions. Independent reviewer annotations may be added through the packet or dashboard, but are not a prerequisite for this formalization status.
| Result | Comparison with source |
|---|---|
| Theorem 1 | Exact. |
| Theorem 2 | Exact. |
| Theorem 3 | Exact. |
| Propositions 1–6; Lemmas 1–7; Remark 3 | Exact. |
None within the selected named theoretical surface.
None.
None.
Theorem 3 provides a useful finite-allocation pattern. First partition items by their role in the instance, establish an EFX allocation for the central M2 piece, orient the remaining small-item structure in a balanced way, and then insert or compose the M34 residue while preserving the relevant inequalities. Theorem 2 illustrates the complementary obstruction pattern: derive allocation-wide lower bounds from EFX, then exhibit a Pareto improvement that the lower bounds rule out for an EFX allocation.
This closeout makes no existence claim for more than four agents beyond the results stated in the source. Theorem 1 and Theorem 2 already quantify over arbitrary (n ); Theorem 3 is deliberately reported only in its stated four-agent form.
None identified in the audited source version.
None within the reviewed named theoretical surface.
The current surface contains 24 source presentations: six definitions and 18 result claims. The result claims cover Theorems 1–3, their named propositions and lemmas, the explicit EFX witness used in Theorem 2, and the general-agent insertion claim. PaperInterface.lean contains the 18 transparent result specifications, and ProofInterface.lean supplies their checked endpoints.
No standalone paper-facing assumption is selected. Three paper-local definition prerequisites match their source connections in the prerequisite ledger. The finite chore set, nonnegative item costs, additive bundle costs, feasibility, and the tri-valued and bi-valued domains appear directly in the expanded result targets.
The statement map records exact source routes for the allocation, cost, EF, EFX, Pareto, canonical, and super-canonical definitions and for all supporting result presentations. The source-to-Spec ledger records 18 direct matching result judgments.
The three selected reusable declarations are the shared envy-free, EFX, and Pareto-optimal predicates for chores. All three match their selected source connections in the library ledger. The canonical-allocation constructions and theorem-specific decomposition remain paper-local.
DependencyDAG.tex and DependencyDAG.pdf show the six definitions and the Theorem 1, Theorem 2, and Theorem 3 result routes. The explicit Theorem 2 EFX witness and the general-agent insertion claim appear as their own nodes. The rendered DAG was visually inspected for legibility, clipping, and node-edge overlap.
The focused-build receipt records a passing paper build. The import-closure receipt and final closure receipt record the checked Lean closure and terminal obligation graph.
The checked source definitions are envy-freeness for chores, EFX for chores, Pareto optimality, canonical allocation, canonical short/long labels, and super-canonical allocation. The exact source and Lean routes are recorded in the statement map.
The 18 exact target/endpoint pairings are in PaperInterface.lean and ProofInterface.lean.
The source-to-Spec ledger contains 18 direct matches. The human review packet presents the definitions and results in dependency order.
The coverage ledger contains 20 covered named-theory items. The full 24-presentation inventory and route assignments are recorded in the statement map.