A remote record's ordinal within a shared source gap is exact

Several concurrent records can occupy the same gap in an immutable source. A coarse gap number cannot distinguish them. This question proves the exact ordinal inside that gap while retaining the complete record, including its payload. The list b contains pairs (payload, source boundary), ordered by nondecreasing boundary. Choose a valid zero-based list ordinal j. Count every record whose boundary is strictly smaller than b[j]'s boundary, and subtract that count from j. This resulting ordinal locates exactly b[j] in the stable filter of records sharing its boundary. Example: b = [(x,0),(y,0),(z,2)]. At j=1, the smaller-boundary count is0; ordinal1 of the boundary0 filter is (y,0). At j=2, the count is2; ordinal0 of the boundary2 filter is (z,2). Duplicate payloads are allowed; identity uniqueness is not a premise. Ordering within a shared gap is input list order. Sortedness matters: for [(x,2),(y,0)] at j=1, the smaller-boundary count is0, but ordinal1 of the boundary0 filter is absent. Natural subtraction is saturating, so the proof must also derive that the count never exceeds j under sortedness. This is a supporting exact lookup lemma for our source/remote layout proof, linked to numeric rank-separation question22. Locally it is used to derive an actual merged-list remote lookup. This standalone question establishes only the within-gap filter lookup. It does not establish CRDT convergence, causal projection, Rust refinement, a speedup, or novelty. Stable filtering and sorted-list order statistics are established techniques. Prepared by James Addison (jungle) with Codex. Separate adversarial AI review is recorded locally; it is not an independent human statement review on Hunchroom.

∀ (α : Type) (b : List (α × Nat)) (j : Nat),
  b.Pairwise (fun x y => x.2 ≤ y.2) →
  ∀ (hj : j < b.length),
    (b.filter fun r => r.2 == b[j].2)[j - (b.filter fun r => r.2 < b[j].2).length]? =
      some b[j]

OA_statement : Prop