Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/MarkedInputAnnotation.marked_input_path_annotation (✓ std3). ∎
Source. Repository-derived.
Commentary.
The base path ends at a valid charge-mode goal. Its input digit stream is a lower tail followed by a nonempty repetition of [1,0,0], and at least one final zero. The two preceding input digits vanish, with the two stored source digits included when the lower tail has fewer than two entries. The initial full marker state stores the base source index and mode zero. There exists a path of the literal marker relation with exactly the same arithmetic labels, ending in mode four at the same base endpoint. The persistent output class flag is zero throughout an accepted base path, so every required marker transition is available. The first marker is selected precisely after the lower tail; all preceding modes remain zero. This statement supplies path existence; interpretation of the retained or removed lowest digit and its terminal charge correction requires further arithmetic information.