Obstructions to countable tests and finite observation profiles

theorem GenLimit.FiniteWitness.no_countably_supported_dimension {α : Type u_1} [Countable α] [Infinite α] : ¬∃ (D : Set (Set α) → WithTop ℕ), (∀ (H : Generic.LanguageClass α), Generic.UUS H → (Generic.GeneratableInLimit H ↔ D H < ⊤)) ∧ ∀ (H : Generic.LanguageClass α), Generic.UUS H → D H = ⊤ → ∃ K ⊆ H, Set.Countable K ∧ D K = ⊤

The dimension is completely arbitrary: no monotonicity or computability assumption.

theorem GenLimit.FiniteWitness.finite_level_not_countably_determined (d : ℕ) : ∃ (H : Set (Set TwoCore.Point)), Generic.UUS H ∧ separationWidth H = finiteValue (d + 1) ∧ ∀ K ⊆ H, K.Countable → separationWidth K ≤ finiteValue 1

def GenLimit.FiniteWitness.finiteTraces {α : Type u_1} (H : Set (Set α)) (F : Finset α) : Set (Set α)

All restrictions of target languages to a fixed finite observation set.

Equations

• GenLimit.FiniteWitness.finiteTraces H F = {E : Set α | ∃ L ∈ H, L ∩ ↑F = E}

def GenLimit.FiniteWitness.positiveClosure {α : Type u_1} (H : Set (Set α)) (S : Finset α) : Set α

The intersection of all target languages consistent with a finite positive sample.

Equations

• GenLimit.FiniteWitness.positiveClosure H S = {x : α | ∀ L ∈ H, ↑S ⊆ L → x ∈ L}

theorem GenLimit.FiniteWitness.full_finiteTraces_of_cofinite_subset {α : Type u_1} {H : Set (Set α)} (hH : cofinite α ⊆ H) (F : Finset α) : finiteTraces H F = 𝒫 ↑F

theorem GenLimit.FiniteWitness.positiveClosure_of_cofinite_subset {α : Type u_1} {H : Set (Set α)} (hH : cofinite α ⊆ H) (S : Finset α) : positiveClosure H S = ↑S

theorem GenLimit.FiniteWitness.identical_finite_profiles {α : Type u_1} [Infinite α] : (∀ (F : Finset α), finiteTraces (cofinite α) F = finiteTraces (allInfinite α) F) ∧ ∀ (S : Finset α), positiveClosure (cofinite α) S = positiveClosure (allInfinite α) S

theorem GenLimit.FiniteWitness.profiles_do_not_determine_ordinary {α : Type u_1} [Countable α] [Infinite α] : (∀ (F : Finset α), finiteTraces (cofinite α) F = finiteTraces (allInfinite α) F) ∧ (∀ (S : Finset α), positiveClosure (cofinite α) S = positiveClosure (allInfinite α) S) ∧ Generic.GeneratableInLimit (cofinite α) ∧ ¬Generic.GeneratableInLimit (allInfinite α)