{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"discrete","imports":["Mathlib.Data.Finset.Card","Mathlib.Data.Finset.Powerset","Mathlib.Algebra.BigOperators.Group.Finset.Basic","Mathlib.Tactic.NormNum"],"statement_hash":"1d5fdcc48cc72fd73deb503a1d980c09b9f19af0bfd8410e197f5c0034089a3d","problem":{"id":28,"title":"State-based CRDT convergence: equal delivered sets give equal joins despite duplicates","description":"Known safety theorem for a concrete grow-only-set state CRDT. Each delivered update is a finite set of natural identities, the initial state is empty, and merge is set union. Two delivery lists containing the same set of update states produce equal merged states, even if order and multiplicities differ. Equal delivered sets is the premise; equal resulting states is the conclusion.\n\nThis is a concrete Lean restatement of the semilattice fold argument in crdt-lean Convergence.lean, with a small independent proof checked under Hunchroom's discrete profile. The cited repository is MIT licensed; its full project was not rebuilt here. This statement proves safety under equal deliveries, not network fairness or eventual delivery, application invariants, or RGA insertion semantics. Existing Isabelle and Coq CRDT developments will be supplied as additional sources. Prepared with Codex; platform checking assigns proof status.","statement":"∀ (xs ys : List (Finset Nat)), xs.toFinset = ys.toFinset →\n xs.foldr (fun update state => update ∪ state) ∅ =\n ys.foldr (fun update state => update ∪ state) ∅","profile":"discrete","module_pins":[],"module_context":[],"scope":{"obligations":["convergence"],"assumptions":["Two delivery lists contain the same set of update states."],"cost_metric":"none","model_scope":"Grow-only finite sets of natural identities; empty initial state and union merge.","implementation":"","correspondence":"abstract_model","limitations":["Safety under equal deliveries only; no eventual delivery, network fairness or RGA sequence semantics."]}},"source":"import Mathlib.Data.Finset.Card\nimport Mathlib.Data.Finset.Powerset\nimport Mathlib.Algebra.BigOperators.Group.Finset.Basic\nimport Mathlib.Tactic.NormNum\n\ndef OA_statement : Prop := (∀ (xs ys : List (Finset Nat)), xs.toFinset = ys.toFinset →\n xs.foldr (fun update state => update ∪ state) ∅ =\n ys.foldr (fun update state => update ∪ state) ∅)\n\n#check OA_statement\n","proof":null}