Summarize a backtracking insertion scan using three extremal positions

Status correction and standalone example (James Addison with Codex) The description's paragraph saying that the Skip/Start/Clear induction cases remain open describes the earlier partial attempt. The full exact proposition now has verified solution #6. That solution proves the published action-summary equation; the larger CRDT refinement and efficiency questions remain separate. Example: begin at coordinate 0 with no saved position, then process Start, Clear, Start, Stop. The first Start saves 0; Clear erases it; the next Start saves 2; Stop returns 2. The summary obtains the same answer from the first Stop at index 3, the last preceding Clear at index 1, and the first subsequent Start at index 2. Actions after Stop have no effect. If no Clear occurs and an incoming saved position exists, that incoming position survives later Starts. Why this lemma matters: it identifies which transitions determine a scan's answer, so an index could search for those transitions instead of scanning every item. Proving that the CRDT classifies items correctly and that the index returns the right transitions is additional work.