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

Can static source coordinates be compared exactly with remote coordinates using only remote gap boundaries? This is a supporting rank lemma for exact indexed list-CRDT insertion, not a claim of novelty or runtime improvement. The immutable source has positions q. Each remote item has a natural boundary: it sits before source item boundary, or at the end. Remote items are ordered by nondecreasing boundary; their list ordinal j distinguishes several remote items in the same gap. The proposed source coordinate is q plus the number of remote boundaries at most q. Remote coordinate j is boundaries[j] plus j. The exact statement proves both strict comparisons and excludes equality for every natural q and valid remote ordinal j. Source comes before remote exactly when q is less than that remote boundary. Remote comes before source exactly when its boundary is at most q. Thus a shared source gap does not identify a source record with a remote record. Equal-boundary remote items retain separate ordinals. Sortedness is an explicit and necessary premise. With boundaries [2,0], q=1 and j=0, the two formula coordinates equal2, so the unsorted variant is false. This question allows q outside any finite source length; finite-layout sentinel bounds are separate. This theorem concerns these numeric formulas. It does not prove that they equal every actual merged-list ID lookup, that the Rust range trees return the right extrema, that histories are admitted correctly, or that the CRDT converges or runs faster. The locally proved source-item merged lookup is separate; the corresponding remote lookup and full static classifier theorem remain open. Existing order statistics and range-summary methods are prior art. Prepared by James Addison (jungle) with Codex, with separate adversarial AI verification. Offline AI verification is not an independent human statement review on Hunchroom.

∀ (boundaries : List Nat) (j q : Nat),
  boundaries.Pairwise (fun x y => x ≤ y) →
  ∀ (hj : j < boundaries.length),
    (q + (boundaries.filter fun boundary => boundary ≤ q).length < boundaries[j] + j ↔
      q < boundaries[j]) ∧
    (boundaries[j] + j < q + (boundaries.filter fun boundary => boundary ≤ q).length ↔
      boundaries[j] ≤ q) ∧
    q + (boundaries.filter fun boundary => boundary ≤ q).length ≠ boundaries[j] + j

OA_statement : Prop