Exact causal-parent projection for a tombstone-preserving list CRDT

No Lean proof yet. This note records evidence and a proof plan. Prepared by Claude (Anthropic model) working for James Addison. 1. Evidence. I ported the exact published model to Python and cross-checked it against the statement's own Lean lambdas, evaluated with Lean 4.34.1. indexOf's List.rec was replaced by the equivalent findIdx? only so the code generator accepts it. The port and the Lean model agree on the final replay and on every parent-context replay for 300 random concurrent histories. I then fuzzed about 60,000 random and adversarial valid histories: 2–6 actors, up to 40 events, arbitrary causally closed parent sets, hot-spot concurrent inserts, and tombstones used as anchors. Most events have non-prefix parent histories. No counterexample appeared. A stronger statement also held in 20,000 checks: replay(S) = ok(reconstruct(S, final)) for every causally down-closed subhistory S, not only parent contexts. 2. Relation to known results. The scan is Gentle's YjsMod integration: both origins, a scanning/back pointer and an id tie-break. Weidner and Kleppmann (The Art of the Fugue) state "YjsMod is equivalent to FugueMax" as a conjecture, unproven in v3, the latest version I could read. #16 implies that YjsMod's order on any causally closed set depends only on that set's origin ancestry, which is essentially the content of that conjecture for this model. So #16 is probably not a routine instance of existing convergence proofs. 3. Structural invariant. It held on all 56k reachable states checked. Write p for list position, lo/ro for origins, with bottom at the ends. (I1) p(lo y) < p(y) < p(ro y). (I2) lo-links never cross: p(lo w) < p(u) < p(w) implies p(lo w) ≤ p(lo u). Equivalently, the list is a pre-order of the left-origin tree. (I3) Among siblings (same lo), ro-links never cross: p(c) < p(d) < p(ro c) implies p(ro d) ≤ p(ro c). (I4) Siblings with equal ro appear in id order. (I5) ro(y) is a sibling of y, or lo(ro y) lies strictly before lo(y). I3 and I4 together say siblings are in a post-order of their right-origin forest, with roots ordered by decreasing right origin and ties broken by id. That is FugueMax's sibling order (their Theorem 10). 4. Closed form of scan. No invariant is needed; it matched the Lean scan on 42k insertions. Let e be the first j ≥ left such that j ≥ right, or lo(item j) lies before lo(x), or item j is a sibling with the same ro and a larger id. The result is the least q in [left, e] such that q = e, or item q is a sibling and every sibling in [q, e) has p(ro) < right. 5. Proof plan. (a) Induct over the serialization, proving the down-closed-subset statement. (b) The only nontrivial step is that inserting x commutes with restricting the state to an origin-closed item set B that contains x's context. (c) Remove the items of F\B in reverse serialization order. Each removed item is then a leaf: it is no remaining item's origin, and it is concurrent with x. (d) Using I1–I5, removing one such leaf changes the closed-form position only by the expected shift. This was checked on 23k cases. The case analysis: a leaf sibling seen during the scan is never preceded by an active LESS run unless it is itself LESS, and after a same-ro leaf with a larger id every later sibling stays LESS or same-ro. (e) I1–I5 are preserved by inserts, since the scan places x at its FugueMax slot, and by restriction to origin-closed sets. Deletions only flip flags, and reconstruct reads flags from the subhistory.