Finite positive confirmation of the canonical error priorities

theorem GenLimit.FiniteWitness.extend_inside_infinite {α : Type u_1} {L : Set α} {B : Finset α} (hL : L.Infinite) (hBL : ↑B ⊆ L) (n : ℕ) : ∃ (T : Finset α), ↑T ⊆ L ∧ B ⊆ T ∧ n ≤ T.card

theorem GenLimit.FiniteWitness.exists_confirming_witness {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) {L : Set α} (hL : L.Infinite) (m : ℕ) : ∃ (T : Finset α), ↑T ⊆ L ∧ checkpoint L (m + 1) ⊆ T ∧ (trueRun F L m).toFinset ⊆ T ∧ (trueRun F L m).length + m + 1 ≤ T.card ∧ ∀ k < m, ∀ (q : List α), Encodable.encode q < Encodable.encode (trueRun F L (k + 1)) → F q ∈ L → F q ∈ T

Finitely many earlier codes and their target-valid outputs can be confirmed.

theorem GenLimit.FiniteWitness.sampleRun_matches_true {α : Type u_1} [Encodable α] [DecidableEq α] {F : List α → α} {L : Set α} {S : Finset α} {n m : ℕ} (hSL : ↑S ⊆ L) (hseen : checkpoint L (m + 1) ⊆ S) (hcontents : (trueRun F L m).toFinset ⊆ S) (hlength : (trueRun F L m).length ≤ n) (hbefore : ∀ k < m, ∃ (q : List α), BadExtension F L (trueRun F L k) k q) (hconfirm : ∀ k < m, ∀ (q : List α), Encodable.encode q < Encodable.encode (trueRun F L (k + 1)) → F q ∈ L → F q ∈ S) (k : ℕ) : k ≤ m → sampleRun F S n k = trueRun F L k

Every sample above the confirming witness reproduces the genuine errors.