Universal normalization by finite priorities

The checkpoints here are target elements whose ambient codes are below the stage number. They replace the paper's first-k-target-element checkpoints; both exhaust each target and agree between a sufficiently confirmed sample and that target. The sample search retains the 2 * S.card length cutoff.

noncomputable def GenLimit.FiniteWitness.belowCodes (β : Type u_2) [Encodable β] (n : ℕ) : Finset β

The finite set of elements whose encoding is strictly below the given bound.

Equations

• GenLimit.FiniteWitness.belowCodes β n = (Finset.range n).preimage Encodable.encode ⋯

@[simp]

theorem GenLimit.FiniteWitness.mem_belowCodes {β : Type u_2} [Encodable β] {n : ℕ} {x : β} : x ∈ belowCodes β n ↔ Encodable.encode x < n

noncomputable def GenLimit.FiniteWitness.leastCode {β : Type u_2} [Encodable β] (P : β → Prop) (h : ∃ (x : β), P x) : β

Select the element of least encoding satisfying an inhabited predicate.

Equations

• GenLimit.FiniteWitness.leastCode P h = ⋯.min {x : β | P x} h

theorem GenLimit.FiniteWitness.leastCode_spec {β : Type u_2} [Encodable β] (P : β → Prop) (h : ∃ (x : β), P x) : P (leastCode P h)

theorem GenLimit.FiniteWitness.leastCode_le {β : Type u_2} [Encodable β] (P : β → Prop) (h : ∃ (x : β), P x) {x : β} (hx : P x) : Encodable.encode (leastCode P h) ≤ Encodable.encode x

noncomputable def GenLimit.FiniteWitness.checkpoint {α : Type u_1} [Encodable α] (L : Set α) (k : ℕ) : Finset α

The elements of a target language whose codes are below the checkpoint bound.

Equations

• GenLimit.FiniteWitness.checkpoint L k = {x ∈ GenLimit.FiniteWitness.belowCodes α k | x ∈ L}

@[simp]

theorem GenLimit.FiniteWitness.mem_checkpoint {α : Type u_1} [Encodable α] {L : Set α} {k : ℕ} {x : α} : x ∈ checkpoint L k ↔ Encodable.encode x < k ∧ x ∈ L

theorem GenLimit.FiniteWitness.checkpoint_subset {α : Type u_1} [Encodable α] (L : Set α) (k : ℕ) : ↑(checkpoint L k) ⊆ L

theorem GenLimit.FiniteWitness.checkpoint_mono {α : Type u_1} [Encodable α] {L : Set α} {j k : ℕ} (hjk : j ≤ k) : checkpoint L j ⊆ checkpoint L k

theorem GenLimit.FiniteWitness.checkpoint_agrees {α : Type u_1} [Encodable α] {L : Set α} {S : Finset α} {j k : ℕ} (hSL : ↑S ⊆ L) (hseen : checkpoint L k ⊆ S) (hjk : j ≤ k) : checkpoint (↑S) j = checkpoint L j

theorem GenLimit.FiniteWitness.content_mono {α : Type u_1} [DecidableEq α] {p q : List α} (hpq : p <+: q) : p.toFinset ⊆ q.toFinset

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

The target-dependent genuine errors used only in the proof.

Equations

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

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

The canonical sequence of least-code bad extensions for a fixed target language.

Equations

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

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

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

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

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

Exhaustiveness rules out a genuine error at every stage.