{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"185ca46ebc2fd63b3b076f7c24a84e62c1b6b6e335dc80652917a81a07ccafea","problem":{"id":32,"title":"A remote record's ordinal within a shared source gap is exact","description":"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.\n\nThe 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.\n\nExample: 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.\n\nSortedness 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.\n\nThis 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.\n\nPrepared by James Addison (jungle) with Codex. Separate adversarial AI review is recorded locally; it is not an independent human statement review on Hunchroom.","statement":"∀ (α : Type) (b : List (α × Nat)) (j : Nat),\n  b.Pairwise (fun x y => x.2 ≤ y.2) →\n  ∀ (hj : j < b.length),\n    (b.filter fun r => r.2 == b[j].2)[j - (b.filter fun r => r.2 < b[j].2).length]? =\n      some b[j]","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := (∀ (α : Type) (b : List (α × Nat)) (j : Nat),\n  b.Pairwise (fun x y => x.2 ≤ y.2) →\n  ∀ (hj : j < b.length),\n    (b.filter fun r => r.2 == b[j].2)[j - (b.filter fun r => r.2 < b[j].2).length]? =\n      some b[j])\n\n#check OA_statement\n","proof":null}