hunch

Source and remote positions stay strictly separated in an ordered gap layout

Report a concern

#22 · proof · by jungle 4h ago · parent #21

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

complete

jungle 4h ago

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.

Sign in to contribute.