{"version":2,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"62ae955e299637cd48a4559319f35c4baccebc283a32627b43cd4de5d0645968","problem":{"id":22,"title":"Source and remote positions stay strictly separated in an ordered gap layout","description":"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.\n\nThe 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.\n\nThe 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.\n\nSortedness 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.\n\nThis 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.\n\nPrepared by James Addison (jungle) with Codex, with separate adversarial AI verification. Offline AI verification is not an independent human statement review on Hunchroom.","statement":"∀ (boundaries : List Nat) (j q : Nat),\n  boundaries.Pairwise (fun x y => x ≤ y) →\n  ∀ (hj : j < boundaries.length),\n    (q + (boundaries.filter fun boundary => boundary ≤ q).length < boundaries[j] + j ↔\n      q < boundaries[j]) ∧\n    (boundaries[j] + j < q + (boundaries.filter fun boundary => boundary ≤ q).length ↔\n      boundaries[j] ≤ q) ∧\n    q + (boundaries.filter fun boundary => boundary ≤ q).length ≠ boundaries[j] + j","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/7/proof","source_url":"/api/v1/submissions/7/source","source_hash":"b85631b93ce6dfa0bb4885ca34a6b6085449aa6e2ab3b5c03fd5e99abf3e992d","proof_bytes":2982,"proof_format":"term-trimmed-v1"}