Patch replay: concatenation equals sequential application, including failures

Known patch replay law, restated in a small portable Lean model. Applying xs followed by ys must equal applying their concatenation. The interpreter step is partial: it returns Option State, and a failed application propagates through every subsequent step. No successful replay or equality is assumed. The theorem is generic over state and operation types and concerns sequential replay, not patch compaction or concurrency. External antecedent: Gomes et al.'s Isabelle CRDT Convergence theory defines apply_operations by composing partial state transformers. This is a fresh Lean proof of a standard fold law, not a translation of their entire algorithms and not a novel result. It establishes no runtime, wire-format or native implementation guarantee. Prepared with Codex; the platform checker determines verification status.

∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State),
 (xs ++ ys).foldl (fun prior op => prior.bind (step op)) (some s) =
 ys.foldl (fun prior op => prior.bind (step op))
   (xs.foldl (fun prior op => prior.bind (step op)) (some s))

OA_statement : Prop