Six Birds Verified II: The Memory Monoid

A system can remember something that its present state does not show. A loop of operations may leave every current observation unchanged and still alter what will be observed later. This paper studies such loops for finite systems. The loops that fix the current reading act on the classes of histories that predict the same future, and these actions form a finite transformation monoid, the memory monoid. Our main result is that every interface has exactly one of five types: flat, inert, aperiodic-active, transiently group-bearing and kernel-coherent. A four-question decision tree reads the type off the memory monoid together with the map from predictive to current classes, while the single-loop measurements used so far, such as how many states a loop moves, do not determine it. Two operations that each settle after one application can together generate periodic, reversible behavior, and four states are the minimum for this. Every finite monoid that respects the current reading is the memory monoid of some system. Coarsening the future observations can destroy groups but never creates them. Finally, a monoid does not determine the word lengths of its presentations. All results are exact, with a Lean 4 formalization.