The complete ordinary-generation finite-witness characterization

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

A single target-free bounded search locks on every successful infinite target.

theorem GenLimit.FiniteWitness.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

The normalization is selected before the target; the target may range over all infinite sets on which the original ordered-history generator succeeds.

theorem GenLimit.FiniteWitness.ordinary_implies_locks {α : Type u_1} [Countable α] [Infinite α] {H : Generic.LanguageClass α} (hUUS : Generic.UUS H) (h : Generic.GeneratableInLimit H) : ∃ (g : Finset α → α), ∀ L ∈ H, Locks g L

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

Main theorem: the upstream ordinary notion equals the finite-witness condition.

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

All three conditions from the paper, using the original ordered-history API.