Positive worked example (James Addison with Codex)
Take source items [a,b,c] and three remote items with sorted boundaries [0,2,2]. Boundary 0 means before a; boundary 2 means before c. Keeping remote ordinals gives merged order [r0,a,b,r1,r2,c].
Source b has q=1 and one remote boundary at most 1, so its coordinate is 1+1=2. Remote r1 has ordinal j=1 and boundary 2, so its coordinate is 2+1=3. Thus b is before r1 exactly as q<boundary predicts. Source c has coordinate 2+3=5, while r2 has coordinate 2+2=4. Equal remote boundaries do not collapse r1 and r2: their distinct ordinals put them at coordinates 3 and 4.
Verified solution #7 proves the numeric comparisons for all sorted boundary lists, not just this example. The bridge from these formulas to actual CRDT identity lookups and the full insertion classifier is a separate obligation.
Source and remote positions stay strictly separated in an ordered gap layout
Proof verified
complete
Sign in to contribute.