Partial attempt: the empty-parent case
complete
This attempt proves that an event with an empty causal past has empty replay and empty reconstructed structural projection. The helper facts for filtering and any over a constantly false predicate are proved in Lean. The nonempty-parent branch is deliberately left open with skip. This is not a solution and is expected to report an unsolved goal. The missing non-prefix causal reordering/convergence argument is described in the problem. No performance or novelty claim follows. Prepared with Codex and reviewed separately by an adversarial AI evaluator. The self-contained port was source-reviewed and tested on finite kernel examples; a universal equivalence theorem between that port and the local project definitions has not been proved.
Sources cited in this attempt (2)
Lean proof and verification output
by
have hAnyFalse : ∀ (α : Type) (xs : List α), xs.any (fun _ => false) = false := by
intro α xs
induction xs with
| nil => rfl
| cons a xs ih => simp [List.any_cons, ih]
have hFilterFalse : ∀ (α : Type) (xs : List α), xs.filter (fun _ => false) = [] := by
intro α xs
induction xs with
| nil => rfl
| cons a xs ih => simp [ih]
dsimp only [OA_statement]
intro history finalState hValid hReplay event hMem
by_cases hEmpty : event.2.1 = []
· simp [hEmpty, hAnyFalse, hFilterFalse]
· skipPreview only · 0.00 MiB. Download the full file below.
This submission is not a completed checked proof.
'_private.0.OA_target' depends on axioms: [propext, sorryAx, Quot.sound]
OA_target : OA_statement
error: unsolved goals
case neg
hAnyFalse : ∀ (α : Type) (xs : List α), (xs.any fun x => false) = false
hFilterFalse : ∀ (α : Type) (xs : List α), List.filter (fun x => false) xs = []
history :
List
((Nat × Nat) ×
List (Nat × Nat) ×
(Nat × (Nat × Nat) × Nat ⊕ Nat) ×
((Nat × Nat) × (Nat × Nat) × Nat × Option (Nat × Nat) × Option (Nat × Nat) ⊕ Nat × Nat))
finalState : List (((Nat × Nat) × (Nat × Nat) × Nat × Option (Nat × Nat) × Option (Nat × Nat)) × Bool)
hValid :
List.rec (motive := fun x =>
List
((Nat × Nat) ×
List (Nat × Nat) ×
(Nat × (Nat × Nat) × Nat ⊕ Nat) ×
((Nat × Nat) × (Nat × Nat) × Nat × Option (Nat × Nat) × Option (Nat × Nat) ⊕ Nat × Nat)) →
Prop)
(fun x => True)
(fun event x rest pre =>
(¬event.fst ∈ List.map (fun event => event.fst) pre ∧
(∀ (id : Nat × Nat), id ∈ event.snd.fst → id ∈ List.map (fun event => event.fst) pre) ∧
(∀
(previous :
(Nat × Nat) ×
List (Nat × Nat) ×
(Nat × (Nat × Nat) × Nat ⊕ Nat) ×
((Nat × Nat) × (Nat × Nat) × Nat × Option (Nat × Nat) × Option (Nat × Nat) ⊕ Nat × Nat)),
previous ∈ pre →
previous.fst ∈ event.snd.fst → ∀ (id : Nat × Nat), id ∈ previous.snd.fst → id ∈ event.snd.fst) ∧
(∀
(previous :
(Nat × Nat) ×
List (Nat × Nat) ×
(Nat × (Nat × Nat) × Nat ⊕ Nat) ×
((Nat × Nat) × (Nat × Nat) × Nat × Option (Nat × Nat) × Option (Nat × Nat) ⊕ Nat × Nat)),
previous ∈ pre →
previous.fst.fst = event.fst.fst →
previous.fst.snd < event.fst.snd ∧ previous.fst ∈ event.snd.fst) ∧
∃ sourceState,
List.foldl
(fun prior op =>
prior.bind fun state =>
match op with
| Sum.inl ins =>
if
(List.rec none
(fun item x tail =>
if item.fst.fst = ins.fst then some 0 else Option.map Nat.succ tail)
state).isSome =
true then
do
throw 1
let left ←
match ins.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0 else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
let right ←
match ins.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0 else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if right < left then do
throw 2
let dest ←
Nat.rec (motive := fun x => Nat → Bool → Nat → Except Nat Nat)
(fun i scanning back =>
if right ≤ i then Except.ok (if scanning = true then back else i)
else Except.error 5)
(fun x recur i scanning back =>
if right ≤ i then pure (if scanning = true then back else i)
else
match state[i]? with
| none => do
let other ← Except.error 4
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if otherRight < right then
recur (i + 1) true (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherLeft ←
match other.fst.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
if otherLeft < left then pure (if scanning = true then back else i)
else recur (i + 1) scanning back
| some item => do
let other ← Except.ok item
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if otherRight < right then
recur (i + 1) true (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherLeft ←
match other.fst.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
if otherLeft < left then pure (if scanning = true then back else i)
else recur (i + 1) scanning back)
state.length left false left
pure (List.take dest state ++ [(ins, false)] ++ List.drop dest state)
else do
let dest ←
Nat.rec (motive := fun x => Nat → Bool → Nat → Except Nat Nat)
(fun i scanning back =>
if right ≤ i then Except.ok (if scanning = true then back else i)
else Except.error 5)
(fun x recur i scanning back =>
if right ≤ i then pure (if scanning = true then back else i)
else
match state[i]? with
| none => do
let other ← Except.error 4
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if otherRight < right then
recur (i + 1) true (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherLeft ←
match other.fst.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
if otherLeft < left then pure (if scanning = true then back else i)
else recur (i + 1) scanning back
| some item => do
let other ← Except.ok item
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if otherRight < right then
recur (i + 1) true (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherLeft ←
match other.fst.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
if otherLeft < left then pure (if scanning = true then back else i)
else recur (i + 1) scanning back)
state.length left false left
pure (List.take dest state ++ [(ins, false)] ++ List.drop dest state)
else do
let left ←
match ins.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0 else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
let right ←
match ins.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0 else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if right < left then do
throw 2
let dest ←
Nat.rec (motive := fun x => Nat → Bool → Nat → Except Nat Nat)
(fun i scanning back =>
if right ≤ i then Except.ok (if scanning = true then back else i)
else Except.error 5)
(fun x recur i scanning back =>
if right ≤ i then pure (if scanning = true then back else i)
else
match state[i]? with
| none => do
let other ← Except.error 4
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if otherRight < right then
recur (i + 1) true (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherLeft ←
match other.fst.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
if otherLeft < left then pure (if scanning = true then back else i)
else recur (i + 1) scanning back
| some item => do
let other ← Except.ok item
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok i
if otherRight < right then
recur (i + 1) true (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherLeft ←
match other.fst.snd.snd.snd.fst with
| none => Except.ok 0
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.error 0
| some i => Except.ok (i + 1)
if otherLeft < left then pure (if scanning = true then back else i)
else recur (i + 1) scanning back)
state.length left false left
pure (List.take dest state ++ [(ins, false)] ++ List.drop dest state)
else do
let dest ←
Nat.rec (motive := fun x => Nat → Bool → Nat → Except Nat Nat)
(fun i scanning back =>
if right ≤ i then Except.ok (if scanning = true then back else i)
else Except.error 5)
(fun x recur i scanning back =>
if right ≤ i then pure (if scanning = true then back else i)
else
match state[i]? with
| none => do
let other ← Except.error 4
if other.fst.snd.snd.snd.fst = ins.snd.snd.snd.fst then
if other.fst.snd.snd.snd.snd = ins.snd.snd.snd.snd then
if
(decide (ins.fst.fst < other.fst.fst.fst) ||
ins.fst.fst == other.fst.fst.fst &&
decide (ins.fst.snd < other.fst.fst.snd)) =
true then
pure (if scanning = true then back else i)
else recur (i + 1) false back
else do
let otherRight ←
match other.fst.snd.snd.snd.snd with
| none => Except.ok state.length
| some id =>
match
List.rec none
(fun item x tail =>
if item.fst.fst = id then some 0
else Option.map Nat.succ tail)
state with
| none => Except.Axioms: none