Paired Dyadic Removals

Abstract

Two removals of the same dyadic amount from a heap deeper than the unique minimum produce exactly two minimum-depth heaps.

Theorem 1.1 (The intermediate heap and its second remainder).

$$\forall P\in \mathrm{Multiset}\left(\mathrm{Nat}\right),\forall h\in \mathrm{Nat},\forall k\in \mathrm{Nat},\left(\mathrm{Positive}\left(P\right)\wedge \left(\mathrm{HasDepth}\left(P,k+1\right)\wedge \left(\mathrm{countAt}\left(P,k+1\right)=1\wedge \left(\mathrm{mem}\left(h,P\right)\wedge k+1<\mathrm{valuation}\left(h\right)\right)\right)\right)\right)\Rightarrow \left(\mathrm{erase}\left(\mathrm{successor}\left(P,h,2^k\right),h-2^k\right)=\mathrm{erase}\left(P,h\right)\wedge \left(\left(\forall x\in \mathrm{Nat},\mathrm{mem}\left(x,\mathrm{erase}\left(\mathrm{successor}\left(P,h,2^k\right),h-2^k\right)\right)\Rightarrow k+1\le \mathrm{valuation}\left(x\right)\right)\wedge \left(\mathrm{countAt}\left(\mathrm{erase}\left(\mathrm{successor}\left(P,h,2^k\right),h-2^k\right),k+1\right)=1\wedge \left(0<h-2^k-2^k\wedge \mathrm{valuation}\left(h-2^k-2^k\right)=k+1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Games/DivisorNimBoundSmallSupport.paired_pivot_structure (✓ std3). ∎

Source. Repository-derived.

Commentary.

After the first removal, erasing the new heap recovers the unchanged heaps. They retain exactly one heap of depth k plus one. The second removal leaves a positive heap of that same depth.

References

• Truth anchor: D5/S3/Combinatorics/Games/DivisorNimBoundSmallSupport.paired_pivot_structure
• Dependency: D5/S3/Combinatorics/Games/DivisorNimBoundOutcome