Finite positive witnesses for ordinary generation

This extension uses the upstream sequence-input model without redefining it. SetDriven below refers to dependence on the input set, not set-valued output.

noncomputable def GenLimit.FiniteWitness.ofSet {α : Type u_1} (g : Finset α → α) : Generic.Generator α

Run an input-set function on an ordered finite history.

Equations

• GenLimit.FiniteWitness.ofSet g x✝ xs = g (GenLimit.Generic.sequenceSample xs)

@[simp]

theorem GenLimit.FiniteWitness.output_ofSet {α : Type u_1} (g : Finset α → α) (stream : Generic.Stream α) (t : ℕ) : Generic.output (ofSet g) stream t = g (Generic.sample stream t)

def GenLimit.FiniteWitness.Locks {α : Type u_1} (g : Finset α → α) (L : Generic.Language α) : Prop

A finite set after which every consistent finite extension is good.

Equations

• GenLimit.FiniteWitness.Locks g L = ∃ (T : Finset α), ↑T ⊆ L ∧ ∀ (S : Finset α), T ⊆ S → ↑S ⊆ L → g S ∈ L ∧ g S ∉ S

def GenLimit.FiniteWitness.SetDrivenGeneratable {α : Type u_1} (H : Generic.LanguageClass α) : Prop

Existence of one input-set generator in the original positive-text model.

Equations

• GenLimit.FiniteWitness.SetDrivenGeneratable H = ∃ (g : Finset α → α), GenLimit.Generic.IsLimitGenerator (GenLimit.FiniteWitness.ofSet g) H

def GenLimit.FiniteWitness.active {α : Type u_1} (H : Generic.LanguageClass α) (T : Generic.Language α → Finset α) (S : Finset α) : Set (Generic.Language α)

Consistent targets whose assigned positive witnesses have been observed.

Equations

• GenLimit.FiniteWitness.active H T S = {L : GenLimit.Generic.Language α | L ∈ H ∧ T L ⊆ S ∧ ↑S ⊆ L}

def GenLimit.FiniteWitness.activeCore {α : Type u_1} (H : Generic.LanguageClass α) (T : Generic.Language α → Finset α) (S : Finset α) : Set α

The simultaneous common intersection of all active targets.

Equations

• GenLimit.FiniteWitness.activeCore H T S = {x : α | ∀ L ∈ GenLimit.FiniteWitness.active H T S, x ∈ L}

def GenLimit.FiniteWitness.HasFiniteWitnesses {α : Type u_1} (H : Generic.LanguageClass α) : Prop

The paper's condition, with an assignment extended arbitrarily off H.

Equations

• One or more equations did not get rendered due to their size.

theorem GenLimit.FiniteWitness.locks_eventually_correct {α : Type u_1} {g : Finset α → α} {L : Generic.Language α} (h : Locks g L) {stream : Generic.Stream α} (hP : Generic.Presents stream L) : ∃ (t₀ : ℕ), ∀ (t : ℕ), t₀ ≤ t → Generic.CorrectAt (ofSet g) L stream t

theorem GenLimit.FiniteWitness.locks_imply_setDriven {α : Type u_1} {H : Generic.LanguageClass α} (h : ∃ (g : Finset α → α), ∀ L ∈ H, Locks g L) : SetDrivenGeneratable H

theorem GenLimit.FiniteWitness.setDriven_implies_ordinary {α : Type u_1} {H : Generic.LanguageClass α} (h : SetDrivenGeneratable H) : Generic.GeneratableInLimit H

noncomputable def GenLimit.FiniteWitness.lockingWitness {α : Type u_1} (g : Finset α → α) (L : Generic.Language α) : Finset α

Choose a finite locking witness, or the empty set when the generator does not lock.

Equations

• GenLimit.FiniteWitness.lockingWitness g L = if h : GenLimit.FiniteWitness.Locks g L then Exists.choose h else ∅

theorem GenLimit.FiniteWitness.lockingWitness_spec {α : Type u_1} {g : Finset α → α} {L : Generic.Language α} (h : Locks g L) : ↑(lockingWitness g L) ⊆ L ∧ ∀ (S : Finset α), lockingWitness g L ⊆ S → ↑S ⊆ L → g S ∈ L ∧ g S ∉ S

theorem GenLimit.FiniteWitness.locks_imply_finiteWitnesses {α : Type u_1} {H : Generic.LanguageClass α} (h : ∃ (g : Finset α → α), ∀ L ∈ H, Locks g L) : HasFiniteWitnesses H

A finite active intersection is itself a forbidden common input.

noncomputable def GenLimit.FiniteWitness.witnessGenerator {α : Type u_1} [Nonempty α] (H : Generic.LanguageClass α) (T : Generic.Language α → Finset α) (S : Finset α) : α

Choose an unseen point in the active core when one exists, with an arbitrary fallback.

Equations

• GenLimit.FiniteWitness.witnessGenerator H T S = if h : ∃ x ∈ GenLimit.FiniteWitness.activeCore H T S, x ∉ S then h.choose else Classical.choice ⋯

theorem GenLimit.FiniteWitness.finiteWitnesses_imply_locks {α : Type u_1} [Nonempty α] {H : Generic.LanguageClass α} (h : HasFiniteWitnesses H) : ∃ (g : Finset α → α), ∀ L ∈ H, Locks g L

A witness assignment gives one total function with all required locks.

theorem GenLimit.FiniteWitness.finiteWitnesses_imply_ordinary {α : Type u_1} [Nonempty α] {H : Generic.LanguageClass α} (h : HasFiniteWitnesses H) : Generic.GeneratableInLimit H