From Anagram Reachability to Combinatorial Game Values: Termination Measures and Formalization Sketches in Lean 4

Abstract

This deposit contains a self-contained Lean 4 formalization of exact multiset cover (anagram reachability) for the 32-letter multiset arising from the English phrase “one man’s slop is another man’s treasure.” The development includes:• A bounded Counts structure for decidable letter-frequency vectors• An inductive Reachable predicate for exact multiset-cover reachability• A well-founded recursive searcher with an explicit natural-number measure (Counts.sum)• A collecting enumerator sketch• A methodological working paper connecting the termination technique to Conway induction in combinatorial game theory The formalization is pedagogical and methodological. It does not claim to solve an open mathematical problem. Its value lies in exhibiting a clean, zero-sorry example of well-founded recursion that is ready for integration into larger Lean projects. All source files carry permanent authorship attribution to Benjamin Stanley Frohman (@Investor0x / GitHub BenFrohman).