Exact T depletion and the final complement

Abstract

Exact T depletion and the final complement.

The T extension and its exact used-set definitions belong to SourcePrefixInventory and are called directly on the M5 row-data projection. This module retains the specialized U/V0 extension and Fin(10) terminal completion; the a0<=z assumption remains essential to that tail argument.

Let keep be the source-attained retained subset of the old bank, and pay the actual selected u mask. Spend (bank minus keep) together with pay, then append T. The height immediately before T is Dcomp-ell in [0,(u-1)/2], where Dcomp=-charge(keep)-weight(pay)*u. Since 2T=N-u, T fits individually.

Before U, spend exactly keep, the complementary u mask, and the whole y row. No previously consumed label occurs again. The endpoint is -U+(z-a0)/2. The separate U gate gives height (z-a0)/2>=0. The separate V0 gate gives height (N+z-2a0)/2<=C, using a0<=z and z<=2a-3<=2a0-3.

The literal unused complement after V0 is parent D0 and the complete rows after V0 and D0. Every remaining positive is SMALL, and only D0 can be a negative LARGE occurrence. Conservation supplies its exact total. The existing TwoLargeOrdering completion theorem orders this entire complement, preserving the prefix and finishing at zero.

References

• Dependency: D5/S3/Combinatorics/Circle/M5PhysicalInventory