Recover the nearest older right neighbor from a shared-left group

For a list of distinct natural birth priorities, prove an exact neighbor identity. All queries return structural positions, not birth values. nearestLeft(i) is the closest position before i with a smaller priority. nearestRight(i) is the closest position after i with a smaller priority. Group positions by identical nearestLeft, including the group with no left neighbor. The theorem says nearestRight(i) is the next position in its group, if one exists. Otherwise it is nearestRight of its left neighbor; when there is no left neighbor, it is absent. Example: priorities [2,9,11,7,1]. Positions 1 and 3 share left neighbor 0. For position1, its right neighbor is position3, skipping position2. For position3, the group has no next member, so its right neighbor is position4, which is also the right neighbor of position0. Distinctness matters: [1,1] has two positions in the no-left group but neither has a smaller right neighbor, so the stated rule fails. The statement contains five typed lambda applications with the complete executable definitions. priorityAt uses optional lookup with default0 to make queries total; the target requires a valid position. Priorities can have holes and need not be sorted or bounded by list length. Research motivation: finite probes of a fully known linear CRDT source, retaining tombstones, match insertion origins to nearest older-born items in final structural order. This list lemma could permit a simpler source-origin index. That correspondence to all generated histories is a separate unproved obligation; this proposition does not assume or establish it. Concurrent source histories are not covered by those probes. Nearest-smaller queries, Cartesian trees and succinct navigation are established data-structure theory. We claim no new tree encoding, entire-history bit bound, runtime/memory gain, full CRDT convergence or native implementation refinement. Birth permutations, original identities, payloads, causal history and deletion metadata remain separate costs. Parent #23 supplies an abstract birth-permutation realization result, not native correspondence. Prepared by James Addison (jungle) with Codex. A separate adversarial AI fixed the local mathematical challenge before implementation and checked finite examples. A complete local proof of that challenge has passed independent fresh compilation, exact target assignment and axiom review. The exact self-contained port is undergoing separate native and pinned-runtime validation before submission; independent AI review is not a human meaning review.

(fun (priorityAt : List Nat → Nat → Nat) =>
(fun (nearestLeft : List Nat → Nat → Option Nat) =>
(fun (nearestRight : List Nat → Nat → Option Nat) =>
(fun (nextSameLeft : List Nat → Nat → Option Nat) =>
(fun (groupRight : List Nat → Nat → Option Nat) =>
∀ (a : List Nat), a.Nodup → ∀ i, i < a.length → nearestRight a i = groupRight a i
) (fun a i => match nextSameLeft a i with | some j => some j | none => (nearestLeft a i).bind (nearestRight a))
) (fun a i => (List.range a.length).find? (fun j => decide (i < j ∧ nearestLeft a j = nearestLeft a i)))
) (fun a i => (List.range a.length).find? (fun j => decide (i < j ∧ priorityAt a j < priorityAt a i)))
) (fun a i => (List.range i).reverse.find? (fun j => decide (priorityAt a j < priorityAt a i)))
) (fun a i => (a[i]?).getD 0)

OA_statement : Prop