Canonical candidate searches and target error sequences

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

No word-length cutoff; freshness concerns the entire observed sample.

Equations

• GenLimit.FiniteWitness.Simplified.Candidate M F S p k q = (p <+: q ∧ p.length < q.length ∧ q.toFinset ⊆ S ∧ M.points (↑S) (k + 1) ⊆ q.toFinset ∧ F q ∉ S)

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

Iterate least-code candidate extensions relative to a finite observed sample.

Equations

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

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

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

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

theorem GenLimit.FiniteWitness.Simplified.append_candidate {α : Type u_1} [DecidableEq α] (M : Checkpoints α) {F : List α → α} (hF : Fresh F) {S : Finset α} (hS : S.Nonempty) {p : List α} (hp : p.toFinset ⊆ S) (k : ℕ) : Candidate M F S p k (p ++ S.toList)

Appending all observed points supplies a candidate at every round.

theorem GenLimit.FiniteWitness.Simplified.candidate_exists {α : Type u_1} [Encodable α] [DecidableEq α] (M : Checkpoints α) {F : List α → α} (hF : Fresh F) {S : Finset α} (hS : S.Nonempty) (k : ℕ) : ∃ (q : List α), Candidate M F S (sampleRun M F S k) k q

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

Evaluate the canonical history after a number of steps equal to the sample size.

Equations

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

def GenLimit.FiniteWitness.Simplified.BadExtension {α : Type u_1} [DecidableEq α] (M : Checkpoints α) (F : List α → α) (L : Set α) (p : List α) (k : ℕ) (q : List α) : Prop

A strict target-valid extension covering the next checkpoint whose output misses the target.

Equations

• GenLimit.FiniteWitness.Simplified.BadExtension M F L p k q = (p <+: q ∧ p.length < q.length ∧ ↑q.toFinset ⊆ L ∧ M.points L (k + 1) ⊆ q.toFinset ∧ F q ∉ L)

noncomputable def GenLimit.FiniteWitness.Simplified.trueRun {α : Type u_1} [Encodable α] [DecidableEq α] (M : Checkpoints α) (F : List α → α) (L : Set α) : ℕ → List α

The canonical sequence of least-code target errors using the checkpoint interface.

Equations

• One or more equations did not get rendered due to their size.
• GenLimit.FiniteWitness.Simplified.trueRun M F L 0 = []

theorem GenLimit.FiniteWitness.Simplified.trueRun_next {α : Type u_1} [Encodable α] [DecidableEq α] {M : Checkpoints α} {F : List α → α} {L : Set α} {k : ℕ} (h : ∃ (q : List α), BadExtension M F L (trueRun M F L k) k q) : BadExtension M F L (trueRun M F L k) k (trueRun M F L (k + 1))

theorem GenLimit.FiniteWitness.Simplified.trueRun_prefix {α : Type u_1} [Encodable α] [DecidableEq α] (M : Checkpoints α) (F : List α → α) (L : Set α) (k : ℕ) : trueRun M F L k <+: trueRun M F L (k + 1)

theorem GenLimit.FiniteWitness.Simplified.trueRun_legal {α : Type u_1} [Encodable α] [DecidableEq α] (M : Checkpoints α) (F : List α → α) (L : Set α) (k : ℕ) : ↑(trueRun M F L k).toFinset ⊆ L

theorem GenLimit.FiniteWitness.Simplified.trueRun_stops {α : Type u_1} [Encodable α] [DecidableEq α] (M : Checkpoints α) {F : List α → α} {L : Set α} (hvalid : EventuallyValid F L) : ∃ (m : ℕ), ¬∃ (q : List α), BadExtension M F L (trueRun M F L m) m q