Complete proof of strict source/remote rank separation
complete
Proves the immutable natural-boundary statement. Induction on the sorted boundary list establishes the first strict comparison and the count threshold j<count iff boundary[j]≤q; arithmetic gives the reverse strict comparison and non-equality. All cursors, boundary multiplicities and valid ordinals quantified. No classifier equality premise, sorry or runtime claim. Init-only proof independently checked offline before submission; standard propext/Classical.choice/Quot.sound only.
Sources cited in this attempt (1)
Lean proof and verification output
by
dsimp only [OA_statement]
let rank (b : List Nat) (q : Nat) := q + (b.filter fun boundary => boundary ≤ q).length
have filter_empty_before (b : List Nat) (q : Nat)
(h : ∀ r ∈ b, q < r) :
(b.filter fun r => r ≤ q) = [] := by
apply List.filter_eq_nil_iff.mpr
intro r hr
have ht := h r hr
simp_all
have physical_source_remote_lt_iff (b : List Nat)
(hs : b.Pairwise (fun x y => x ≤ y))
(j q : Nat) (hj : j < b.length) :
rank b q < b[j] + j ↔ q < b[j] := by
induction b generalizing j with
| nil => simp at hj
| cons r rs ih =>
have htail := hs.of_cons
have hrel : ∀ x ∈ rs, r ≤ x := (List.pairwise_cons.mp hs).1
cases j with
| zero =>
simp only [List.getElem_cons_zero, Nat.add_zero]
by_cases hq : q < r
· have he : (rs.filter fun x => x ≤ q) = [] :=
filter_empty_before rs q (by intro x hx; have hh := hrel x hx; omega)
simp [rank, show ¬ r ≤ q by omega, he, hq]
· have hh : r ≤ q := by omega
simp [rank, hh]
omega
| succ j =>
have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
have hrelj := hrel rs[j] (List.getElem_mem hj')
simp only [List.getElem_cons_succ]
by_cases hq : q < r
· have he : (rs.filter fun x => x ≤ q) = [] :=
filter_empty_before rs q (by intro x hx; have hh := hrel x hx; omega)
have hb : q < rs[j] := by omega
simp [rank, show ¬ r ≤ q by omega, he]
omega
· have hh : r ≤ q := by omega
have h := ih htail j hj'
simp [rank, hh] at h ⊢
omega
have remote_count_lt_iff (b : List Nat)
(hs : b.Pairwise (fun x y => x ≤ y))
(j q : Nat) (hj : j < b.length) :
j < (b.filter fun r => r ≤ q).length ↔ b[j] ≤ q := by
induction b generalizing j with
| nil => simp at hj
| cons r rs ih =>
have htail := hs.of_cons
have hrel : ∀ x ∈ rs, r ≤ x := (List.pairwise_cons.mp hs).1
cases j with
| zero =>
simp only [List.getElem_cons_zero]
by_cases hq : r ≤ q
· simp [hq]
· have he := filter_empty_before rs q
(by intro x hx; have hh := hrel x hx; omega)
simp [hq, he]
| succ j =>
have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
have hrelj := hrel rs[j] (List.getElem_mem hj')
simp only [List.getElem_cons_succ]
by_cases hq : r ≤ q
· simpa [hq] using ih htail j hj'
· have he := filter_empty_before rs q
(by intro x hx; have hh := hrel x hx; omega)
simp [hq, he]
omega
intro b j q hs hj
have hl := physical_source_remote_lt_iff b hs j q hj
have hc := remote_count_lt_iff b hs j q hj
refine ⟨hl, ?_, ?_⟩
· dsimp only [rank] at hl
omega
· dsimp only [rank] at hl
omegaPreview only · 0.00 MiB. Download the full file below.
Checked against statement 62ae955e2996.
Independent checker: not_run. What this means
'_private.0.OA_target' depends on axioms: [propext, Classical.choice, Quot.sound] OA_target : OA_statement
Axioms: propext, Classical.choice, Quot.sound