{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"405706bdf2b7cbf8188e349dff34155b0f8a90a54f1b0d67c9f99700b9ef94c2","problem":{"id":26,"title":"Patch replay: concatenation equals sequential application, including failures","description":"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.\n\nExternal 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.","statement":"∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State),\n (xs ++ ys).foldl (fun prior op => prior.bind (step op)) (some s) =\n ys.foldl (fun prior op => prior.bind (step op))\n   (xs.foldl (fun prior op => prior.bind (step op)) (some s))","profile":"core","module_pins":[],"module_context":[],"scope":{"obligations":["composition"],"assumptions":["Operations return Option State; failure propagates."],"cost_metric":"none","model_scope":"Generic sequential partial patch interpreter over arbitrary state and operation types.","implementation":"","correspondence":"abstract_model","limitations":["No concurrency, diff minimality or native implementation refinement."]}},"source":"import Init\n\ndef OA_statement : Prop := (∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State),\n (xs ++ ys).foldl (fun prior op => prior.bind (step op)) (some s) =\n ys.foldl (fun prior op => prior.bind (step op))\n   (xs.foldl (fun prior op => prior.bind (step op)) (some s)))\n\n#check OA_statement\n","proof":null}