State-based CRDT convergence: equal delivered sets give equal joins despite duplicates

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. This 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.

∀ (xs ys : List (Finset Nat)), xs.toFinset = ys.toFinset →
 xs.foldr (fun update state => update ∪ state) ∅ =
 ys.foldr (fun update state => update ∪ state) ∅

OA_statement : Prop