Finite-search implementation of the bounded normalization

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

The decidable candidate test with bounded history length and observed checkpoints.

Equations

• GenLimit.FiniteWitness.finiteCandidate F S n p k q = (p <+: q ∧ p.length < q.length ∧ q.toFinset ⊆ S ∧ q.length ≤ 2 * n ∧ {x ∈ S | Encodable.encode x < k + 1} ⊆ q.toFinset ∧ F q ∉ S)

@[instance_reducible]

instance GenLimit.FiniteWitness.instDecidableFiniteCandidate {α : Type u_1} [DecidableEq α] [Encodable α] (F : List α → α) (S : Finset α) (n : ℕ) (p : List α) (k : ℕ) (q : List α) : Decidable (finiteCandidate F S n p k q)

Equations

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

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

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

The finite set of candidate histories within the fixed length bound.

Equations

• GenLimit.FiniteWitness.candidateWords F S n p k = Finset.filter (GenLimit.FiniteWitness.finiteCandidate F S n p k) (GenLimit.FiniteWitness.boundedWords S (2 * n))

theorem GenLimit.FiniteWitness.mem_candidateWords {α : Type u_1} [DecidableEq α] [Encodable α] (F : List α → α) (S : Finset α) (n : ℕ) (p : List α) (k : ℕ) (q : List α) : q ∈ candidateWords F S n p k ↔ Candidate F S n p k q

def GenLimit.FiniteWitness.pickWord {α : Type u_1} [Encodable α] (C : Finset (List α)) : List α

Decode the smallest code in a finite candidate set. This definition is executable.

Equations

• GenLimit.FiniteWitness.pickWord C = if h : C.Nonempty then (Encodable.decode ((Finset.image Encodable.encode C).min' ⋯)).getD [] else []

theorem GenLimit.FiniteWitness.pickWord_spec {α : Type u_1} [Encodable α] {C : Finset (List α)} (hC : C.Nonempty) : pickWord C ∈ C ∧ ∀ q ∈ C, Encodable.encode (pickWord C) ≤ Encodable.encode q

theorem GenLimit.FiniteWitness.pickWord_eq_leastCode {α : Type u_1} [Encodable α] {C : Finset (List α)} {P : List α → Prop} (hP : ∃ (q : List α), P q) (hC : ∀ (q : List α), q ∈ C ↔ P q) : pickWord C = leastCode P hP

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

Iterate bounded finite candidate searches, retaining the history when no candidate exists.

Equations

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

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

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

Evaluate the finite-search history at the sample-size bound.

Equations

• GenLimit.FiniteWitness.executableNormalized F S = F (GenLimit.FiniteWitness.executableRun F S S.card S.card)

theorem GenLimit.FiniteWitness.executableNormalized_eq {α : Type u_1} [DecidableEq α] [Encodable α] (F : List α → α) (S : Finset α) : executableNormalized F S = normalized F S

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

def GenLimit.FiniteWitness.maxRepair (G : Generic.Generator ℕ) (xs : List ℕ) : ℕ

A computable fresh repair on the concrete natural-number universe.

Equations

• GenLimit.FiniteWitness.maxRepair G xs = if GenLimit.FiniteWitness.listOutput G xs ∈ xs then xs.toFinset.sup id + 1 else GenLimit.FiniteWitness.listOutput G xs

theorem GenLimit.FiniteWitness.maxRepair_fresh (G : Generic.Generator ℕ) : Fresh (maxRepair G)

theorem GenLimit.FiniteWitness.maxRepair_eventuallyValid {G : Generic.Generator ℕ} {L : Set ℕ} (hG : ∀ (stream : Generic.Stream ℕ), Generic.Presents stream L → ∃ (N : ℕ), ∀ n ≥ N, Generic.CorrectAt G L stream n) : EventuallyValid (maxRepair G) L

def GenLimit.FiniteWitness.executableNormalization (G : Generic.Generator ℕ) (S : Finset ℕ) : ℕ

An executable, target-independent normalization, with the whole input set as its argument.

Equations

• GenLimit.FiniteWitness.executableNormalization G S = GenLimit.FiniteWitness.executableNormalized (GenLimit.FiniteWitness.maxRepair G) S

theorem GenLimit.FiniteWitness.executableNormalization_finite_queries {G G' : Generic.Generator ℕ} (S : Finset ℕ) (h : ∀ q ∈ boundedWords S (2 * S.card), listOutput G q = listOutput G' q) : executableNormalization G S = executableNormalization G' S

theorem GenLimit.FiniteWitness.executable_universal_normalization (G : Generic.Generator ℕ) (L : Set ℕ) : L.Infinite → (∀ (stream : Generic.Stream ℕ), Generic.Presents stream L → ∃ (N : ℕ), ∀ n ≥ N, Generic.CorrectAt G L stream n) → Locks (executableNormalization G) L