Target-free bounded search on the observed finite set

def GenLimit.FiniteWitness.Candidate {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) (S : Finset α) (n : ℕ) (p : List α) (k : ℕ) (q : List α) : Prop

A tentative bad extension: its output is unconfirmed by the entire sample.

Equations

• GenLimit.FiniteWitness.Candidate F S n p k q = (p <+: q ∧ p.length < q.length ∧ q.toFinset ⊆ S ∧ q.length ≤ 2 * n ∧ GenLimit.FiniteWitness.checkpoint (↑S) (k + 1) ⊆ q.toFinset ∧ F q ∉ S)

noncomputable def GenLimit.FiniteWitness.sampleRun {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) (S : Finset α) (n : ℕ) : ℕ → List α

Bounded iteration; an empty candidate set leaves the current word fixed.

Equations

• One or more equations did not get rendered due to their size.
• GenLimit.FiniteWitness.sampleRun F S n 0 = []

theorem GenLimit.FiniteWitness.sampleRun_next {α : Type u_1} [Encodable α] [DecidableEq α] {F : List α → α} {S : Finset α} {n k : ℕ} (h : ∃ (q : List α), Candidate F S n (sampleRun F S n k) k q) : Candidate F S n (sampleRun F S n k) k (sampleRun F S n (k + 1))

theorem GenLimit.FiniteWitness.sampleRun_prefix {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) (S : Finset α) (n k : ℕ) : sampleRun F S n k <+: sampleRun F S n (k + 1)

theorem GenLimit.FiniteWitness.sampleRun_content {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) (S : Finset α) (n k : ℕ) : (sampleRun F S n k).toFinset ⊆ S

theorem GenLimit.FiniteWitness.sampleRun_length {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) (S : Finset α) (n k : ℕ) : (sampleRun F S n k).length ≤ 2 * n

theorem GenLimit.FiniteWitness.sampleRun_preserves_fresh {α : Type u_1} [Encodable α] [DecidableEq α] {F : List α → α} {S : Finset α} {n k j : ℕ} (hk : F (sampleRun F S n k) ∉ S) (hkj : k ≤ j) : F (sampleRun F S n j) ∉ S

noncomputable def GenLimit.FiniteWitness.normalized {α : Type u_1} [Encodable α] [DecidableEq α] (F : List α → α) (S : Finset α) : α

The normalized output function is fixed before a target is selected.

Equations

• GenLimit.FiniteWitness.normalized F S = F (GenLimit.FiniteWitness.sampleRun F S S.card S.card)