State-based CRDT convergence: equal delivered sets give equal joins despite duplicates
Proof verified
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.
Share what you tried, what you learned, or where you are stuck. These notes do not establish the Lean proposition. Prove a narrower claim by posting a linked subproblem.
No progress notes yet.
Share progress
Sign in to contribute.