Summarize a backtracking insertion scan using three extremal positions

Can a four-action scan be summarized exactly by the first Stop, the last Clear before it, and the first Start after that Clear? This is a supporting lemma for an experimental index that skips immutable source runs during list-CRDT insertion. It is standard finite-state/range-summary mathematics, not a claimed new result or efficiency theorem. The proposed system still requires separate proofs of classifier predicates, origin ranks, indexed queries and causal preparation, plus complete preprocessing, memory and runtime accounting. Self-contained model: Action = Bool × Bool, with (false,false)=Skip, (false,true)=Start, (true,false)=Clear, (true,true)=Stop. Result = Sum Nat (Nat × Option Nat); inl is a stopped destination, inr is a continuing cursor and optional saved backtracking coordinate. The initial coordinate and optional saved value are arbitrary, including saved values before or after the current coordinate. Skip increments the coordinate and preserves saved. Start increments it and sets saved to the current coordinate only when no value is already saved. Clear increments it and erases saved. Stop returns the saved coordinate if present, otherwise the current coordinate. The sequential run halts at the first Stop. The summary first truncates actions strictly before the first Stop. It finds the last Clear in that active prefix, and the first Start strictly after that Clear (or the first Start anywhere if there is no Clear). A saved incoming coordinate survives exactly when no Clear occurred. If it survives, later Starts must not replace it. Otherwise the selected Start supplies its original absolute coordinate. With a Stop, return the resulting saved coordinate or Stop coordinate. Without a Stop, return the final cursor and saved coordinate. The exact proposition equates sequential run and this summary for every action list, coordinate and optional saved value. There is no action-fold equality or expected result among its premises. All definitions are included as typed lambda applications because statements cannot contain custom declarations. The Bool-pair encoding is a source-reviewed port of a local four-constructor Lean model; universal equivalence between ports is not claimed. Attempt: empty lists and any list whose first action is Stop are proved in the supplied partial attempt. The Skip/Start/Clear induction cases remain open. The local independent specification also has finite examples with a Clear before Stop and a Start after Stop, and a surviving incoming saved coordinate. Those examples are not a universal proof. Motivation: the implementation searches immutable source metadata for these extremal transitions and explicitly processes interleaved remote records. Distinct remote origins in the same source gap retain their identities and order; tombstones remain structural anchors. This question proves none of those classifier/index obligations and supplies no asymptotic or measured speedup. Generic range summaries and existing efficient CRDTs are prior art; we claim no first logarithmic CRDT result. Prepared by James Addison (jungle) with Codex, with separate adversarial AI source/finite review. AI review is not an independent human statement review on this site. The exact published expression is the challenge.

(fun (run : List (Bool × Bool) → Nat → Option Nat → Sum Nat (Nat × Option Nat)) =>
(fun (active : List (Bool × Bool) → List (Bool × Bool)) =>
(fun (lastClear : List (Bool × Bool) → Option Nat) =>
(fun (firstStart : List (Bool × Bool) → Option Nat → Option Nat) =>
(fun (summarize : List (Bool × Bool) → Nat → Option Nat → Sum Nat (Nat × Option Nat)) =>
∀ actions position saved, run actions position saved = summarize actions position saved
) (fun actions position saved =>
(fun chunk =>
(fun clear =>
(fun start =>
(fun finalSaved =>
if chunk.length < actions.length then .inl (finalSaved.getD (position + chunk.length))
else .inr (position + chunk.length, finalSaved))
((if clear.isSome then none else saved).or (start.map (position + ·))))
(firstStart chunk clear)) (lastClear chunk)) (active actions))
) (fun chunk clear =>
(((chunk.zipIdx).drop (clear.map Nat.succ |>.getD 0)).find? (fun pair => !pair.1.1 && pair.1.2)).map Prod.snd)
) (fun chunk =>
((chunk.zipIdx.reverse).find? (fun pair => pair.1.1 && !pair.1.2)).map Prod.snd)
) (fun actions => actions.takeWhile (fun action => !action.1 || !action.2))
) (fun actions =>
List.rec (fun position saved => .inr (position, saved))
(fun action _ rest position saved =>
if action.1 then
  if action.2 then .inl (saved.getD position) else rest (position + 1) none
else
  if action.2 then rest (position + 1) (some (saved.getD position))
  else rest (position + 1) saved) actions)

OA_statement : Prop