A CRDT merge function must satisfy three properties to guarantee convergence: commutativity, associativity, and idempotency. Proving these for the G-Counter validates it as a correct CRDT.

Commutativity: merge(A, B) == merge(B, A)

• max(A[i], B[i]) == max(B[i], A[i]) for all i. This is true because max is commutative.

Associativity: merge(A, merge(B, C)) == merge(merge(A, B), C)

• max(A[i], max(B[i], C[i])) == max(max(A[i], B[i]), C[i]). True because max is associative.

Idempotency: merge(A, A) == A

• max(A[i], A[i]) == A[i]. True because max(x, x) == x.

These properties form a join semi-lattice: the set of all possible states with merge as the join operation. The system monotonically advances through this lattice, guaranteeing convergence.

Request:  {"type": "crdt_verify", "msg_id": 1, "state_a": {"n1": 3, "n2": 1}, "state_b": {"n1": 1, "n2": 5}}
Response: {"type": "crdt_verify_ok", "in_reply_to": 1, "merge_ab": {"n1": 3, "n2": 5}, "merge_ba": {"n1": 3, "n2": 5}, "commutative": true, "idempotent": true}