Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/BasePositionMemory.base_path_position_memory (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a path starting in an initial state, slot one is the parity of the next signed-digit position. The first emitted digit is the dummy digit at position minus one, so the parity is the path length plus one modulo two. Slots two and three retain the endpoint parities. For either stream the current and previous digit slots are entries zero and one of the reversed emitted list, with zero used when an entry is absent. The last-sign slot is the last nonzero emitted digit, also with default zero. These identities apply at intermediate states as well as accepting states. The last-option expression is none for an empty list and some(List.getLast(…)) otherwise; the nonempty proof argument is implicit.