{"version":2,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"daa2cbedd59be36b26a221343083d9a3b05f9a48b0d88df275369df5e4524987","problem":{"id":23,"title":"Every birth permutation has a valid positional insertion replay","description":"Can every permutation of birth times be realized by a sequence of valid positional insertions, with every intermediate list equal to the final order filtered by birth time?\n\nExample: desired final order [2,0,1]. Insert identity 0 at position 0, producing [0]. Insert identity 1 at position 1, producing [0,1]. Insert identity 2 at position 0, producing [2,0,1]. Each identity is inserted once; no deletion or concurrency is needed.\n\nSelf-contained definitions: order is a list of distinct natural identities containing exactly 0 through n-1. born(order,cut) filters order to identities strictly less than cut. position(order,time) counts previously born identities before time in the final order: take the prefix before time, filter it to identities less than time, and count it. insertAt(state,pos,value) is state.take(pos) followed by value and state.drop(pos). replay begins empty and inserts identities 0,1,... using those positions.\n\nThe exact proposition requires three facts: for every cut at most n, replay equals born; each insertion position is at most the actual pre-insertion list length; and the final replay equals order. The bound matters because take/drop alone would otherwise silently clamp an invalid position. Uniqueness and complete membership are explicit premises, and no reconstruction equality is assumed.\n\nWhy this is useful: our historical source-rank problem allows arbitrary insertion positions. This lemma checks that arbitrary final-order birth permutations really occur in an abstract sequential list, rather than treating arbitrary birth arrays as unexplained inputs. It supports applying existing temporal-rank hardness reasoning. Hon, Lee, Sadakane and Tsakalidis already use a birth-only construction in their 2013 lower-bound proof; the reduction idea is prior art.\n\nThis question proves only the list construction. It does not formalize the cited cell-probe lower bound, transfer it to origin queries or whole CRDT merge latency, prove native Rust/CRDT refinement, or demonstrate a speed or memory gain. The offline construction knows the desired final order; it is not a proposed online CRDT algorithm. Prepared by James Addison (jungle) with Codex; separate adversarial AI review is recorded locally, and is not an independent human review on this site.","statement":"(fun (born : List Nat → Nat → List Nat) =>\n(fun (position : List Nat → Nat → Nat) =>\n(fun (insertAt : List Nat → Nat → Nat → List Nat) =>\n(fun (replay : List Nat → Nat → List Nat) =>\n∀ (order : List Nat) (n : Nat), order.Nodup →\n(∀ time < n, time ∈ order) → (∀ time ∈ order, time < n) →\n(∀ cut ≤ n, replay order cut = born order cut) ∧\n(∀ time < n, position order time ≤ (replay order time).length) ∧\nreplay order n = order\n) (fun order cut => Nat.rec []\n  (fun time state => insertAt state (position order time) time) cut)\n) (fun state pos value => state.take pos ++ value :: state.drop pos)\n) (fun order time => (born (order.takeWhile (fun x => x != time)) time).length)\n) (fun order cut => order.filter (fun time => time < cut))","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/8/proof","source_url":"/api/v1/submissions/8/source","source_hash":"660a68c788f18bb904771409fb89f378fcaf3d9d2159f85031549e26e30240a6","proof_bytes":3514,"proof_format":"term-trimmed-v1"}