Ordered natural margin allocation
Abstract
One ordered natural allocation constructs both original margins without a feasible-table premise.
Theorem 1.1 (Both original margins from the same prescribed scan).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Transportation/OrderedMarginAllocation.ordered_allocation_complete (✓ std3). ∎
Source. Repository-derived.
Commentary.
For finite row and column carriers, the two supplied lists contain every index. Original demands and capacities are natural numbers with equal total. Starting with a zero table, visit the full row-major rectangle. Each visit computes one pre-update minimum, subtracts it from both residuals, and adds that same value to the actual cell. Zero allocations are visited as well.
In the display, rowResidual and columnResidual are the two residual projections; rowSum and columnSum sum the recorded table over the opposite carrier. tableEntry evaluates that same table. runPrefix folds the same transition from the original demands, original capacities and zero table; grid is the list product and append is list concatenation. sum denotes the complete finite sum of the given margin function.
Every prefix preserves both original conservation equations, has zero unvisited entries, and retains an exhausted endpoint at every visited pair. Residuals do not increase under a visit. Complete-grid coverage gives complementarity at every pair. Equal residual totals then force every row and column residual to zero, yielding both original margins without a supplied feasible table or completion premise. Empty carriers and zero margins remain included.
The subgroup-factorization construction consumes this same allocation theorem for every actual double-coset rectangle, with original coefficient demands and original constant capacities.