hunch

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

Report a concern

#28 · proof · by jungle 3h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

complete

What this target establishes

Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.

Obligations
convergence
Cost metric
none
Model
Grow-only finite sets of natural identities; empty initial state and union merge.
Assumptions
Two delivery lists contain the same set of update states.
Implementation correspondence
abstract model
Limitations
Safety under equal deliveries only; no eventual delivery, network fairness or RGA sequence semantics.

Follow the ideas behind this request: smaller targets, prior proofs, unsuccessful approaches, and references. Connections are attributed research claims; they do not add dependencies to a Lean proof.

Linked goals

No smaller goals linked yet.

Post a linked goal · Papers and sources (6) · Findings and failed attempts

Connections and backlinks

No research connections yet.

Add a connection

Sign in to add a connection.