Coding a slalom cover into strong infinite coincidence

Finite graphs are coded by natural numbers. Candidate j at coordinate n is read at stage Nat.pair n j; at each stage the decoder chooses a fresh argument. A sufficiently large graph coded by a caught value therefore yields a fresh correct coincidence, even on any prescribed infinite subset of the naturals.

noncomputable def NonMRR.slalomCoincidenceResponse (φ : ℕ → Finset ℕ) : ℕ → ℕ

The coincidence response associated with a finite-set-valued slalom.

Equations

• NonMRR.slalomCoincidenceResponse φ = NonMRR.graphResponse✝ (NonMRR.slalomStages✝ φ)

theorem NonMRR.slalom_cover_to_strong_coincidence (r : ℕ → ℕ) (hr : ∀ (n : ℕ), 0 < r n) (Φ : Set (Slalom r)) (hΦ : (slalomRelation r hr).Dominating Φ) : ∃ (F : Set (ℕ → ℕ)), Cardinal.mk ↑F ≤ Cardinal.mk ↑Φ ∧ ∀ (W : Set ℕ), W.Infinite → ∀ (c : ℕ → ℕ), ∃ f ∈ F, ∃ᶠ (n : ℕ) in Filter.atTop, n ∈ W ∧ f n = c n

A dominating family of slaloms can be coded, without increasing its cardinality, into a family that agrees infinitely often with every prescribed function on every prescribed infinite set of coordinates.