Locking and characterization through fixed-size checkpoints

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

A sufficient finite confirming witness: markers, terminal history, and valid outputs. No enlargement to meet a word-length bound is needed.

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

theorem GenLimit.FiniteWitness.Simplified.normalized_locks {α : Type u_1} [Encodable α] [DecidableEq α] (M : Checkpoints α) (F : List α → α) (hF : Fresh F) {L : Set α} (hL : L.Infinite) (hvalid : EventuallyValid F L) : Locks (normalized M F) L

The cutoff-free search locks on every successful infinite target.

theorem GenLimit.FiniteWitness.Simplified.universal_normalization {α : Type u_1} [Countable α] [Infinite α] (G : Generic.Generator α) : ∃ (g : Finset α → α), ∀ (L : Set α), L.Infinite → (∀ (stream : Generic.Stream α), Generic.Presents stream L → ∃ (t₀ : ℕ), ∀ (t : ℕ), t₀ ≤ t → Generic.CorrectAt G L stream t) → Locks g L

Same universal quantifiers as the manuscript, for any countably infinite universe.

theorem GenLimit.FiniteWitness.Simplified.ordinary_iff_finiteWitnesses {α : Type u_1} [Countable α] [Infinite α] (H : Generic.LanguageClass α) (hUUS : Generic.UUS H) : Generic.GeneratableInLimit H ↔ HasFiniteWitnesses H

The revised proof of the characterization goes directly through locking witnesses.

theorem GenLimit.FiniteWitness.Simplified.full_characterization {α : Type u_1} [Countable α] [Infinite α] (H : Generic.LanguageClass α) (hUUS : Generic.UUS H) : (Generic.GeneratableInLimit H ↔ SetDrivenGeneratable H) ∧ (SetDrivenGeneratable H ↔ HasFiniteWitnesses H)