Exact insertion destination from raw origin and actor predicates
Proof verified
typechecked
Prove that a literal scalar insertion scan and three extremal searches return the same initialized structural destination. Rows provide resolved left-origin AFTER ranks, right-origin BEFORE ranks and lexical actor/sequence coordinates through arbitrary getter functions. The statement quantifies all row lists and getter functions; no classifier-equality or destination-equality premise is assumed. The conflict interval is supplied as rows, excluding its right endpoint. Deleted anchors remain structural records and each iteration has width one. The literal nested conditionals maintain a scanning flag and a saved position. The alternative selects the first Stop, then the last Clear strictly before it, then the first Start after that Clear (or interval start); if no such Start exists it selects Stop/interval end. Clear can also match the stopping item, which must be excluded. This is a mathematical query specification; the List searches themselves are linear. Native ID-to-rank lookup/injectivity, lexical-name ranking, exact conflict-slice extraction, RLE skips, causal preparation, and a concrete maintained balanced tree/runtime bound remain separate obligations. Parent21 proves abstract action summary; this question instead derives the result from raw predicates, with no action extraction supplied as a correctness premise. No novelty or whole CRDT correctness/efficiency claim. An adversarial AI independently fixed the concrete Row target before the local solution. This getter-generalized self-contained port is undergoing separate exact correspondence and pinned validation before publication.
Formal statement
∀ (Row : Type) (leftRank rightRank actor sequence : Row → Nat),
(fun (keyBefore : Row → Row → Bool) =>
(fun (literalScan : Row → List Row → Nat → Bool → Nat → Nat) =>
(fun (stopPredicate : Row → Row → Bool) =>
(fun (clearPredicate : Row → Row → Bool) =>
(fun (startPredicate : Row → Row → Bool) =>
(fun (firstStop : Row → List Row → Nat) =>
(fun (lastClearBeforeStop : Row → List Row → Option Nat) =>
(fun (firstStartAfterClear : Row → List Row → Option Nat) =>
(fun (selectedDestination : Row → List Row → Nat → Nat) =>
∀ (incoming : Row) (rows : List Row) (position : Nat), literalScan incoming rows position false position = selectedDestination incoming rows position
) (fun incoming rows position => position + (firstStartAfterClear incoming rows).getD (firstStop incoming rows))
) (fun incoming rows =>
((((rows.take (firstStop incoming rows)).zipIdx).drop (((lastClearBeforeStop incoming rows).map Nat.succ).getD 0)).find? (fun pair => startPredicate incoming pair.1)).map Prod.snd)
) (fun incoming rows => ((((rows.take (firstStop incoming rows)).zipIdx).reverse.find?
(fun pair => clearPredicate incoming pair.1)).map Prod.snd))
) (fun incoming rows => (((rows.zipIdx).find? (fun pair => stopPredicate incoming pair.1)).map
Prod.snd).getD rows.length)
) (fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
(rightRank other) < (rightRank incoming)))
) (fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
(rightRank incoming) ≤ (rightRank other)))
) (fun incoming other => decide ((leftRank other) < (leftRank incoming)) ||
(decide ((leftRank other) = (leftRank incoming) ∧
(rightRank other) = (rightRank incoming)) && keyBefore incoming other))
) (fun incoming rows => List.foldr (fun other tail position scanning back =>
if (leftRank other) = (leftRank incoming) then
if (rightRank other) = (rightRank incoming) then
if keyBefore incoming other then
if scanning then back else position
else tail (position + 1) false back
else if (rightRank other) < (rightRank incoming) then
tail (position + 1) true
(if scanning then back else position)
else tail (position + 1) false back
else if (leftRank other) < (leftRank incoming) then
if scanning then back else position
else tail (position + 1) scanning back) (fun position scanning back => if scanning then back else position) rows)
) (fun incoming other => decide (actor incoming < actor other ∨ (actor incoming = actor other ∧ sequence incoming < sequence other)))Lean core · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 71a28134bc109775da3760becb062ee8e394fecff3394802c45e6b224eafba39
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.