Recognizing Nat.nth from counts

Nat.nth p k is the k-th natural number satisfying p, and 0 when p holds at most k times. Mathlib's Nat.nth_count identifies it whenever a witness is available: if p n holds and p has exactly k predecessors below n, then nth p k = n. What is missing is the converse bookkeeping — the only if half, including the degenerate branch — which is what a case analysis on the value of nth p k needs.

TauCeti.Nat.nth_eq_iff supplies it: nth p k = m exactly when m is a counting witness, or else m = 0 and no counting witness exists at all. The two branches are mutually exclusive, and a counting witness is unique when it exists, because Nat.count p strictly increases across a point where p holds.

The degenerate branch is not a technicality that can be assumed away: nth p k = 0 really does happen when p has at most k witnesses, and a description of the fibres of nth has to name that case. This makes the statement a usable membership criterion — for instance, it exhibits each fibre of x ↦ Nat.nth (fun i => x i = a) k as a countable Boolean combination of conditions on finitely many of the values of x.

Main results

• TauCeti.Nat.nth_eq_zero_of_forall_count_ne: with no counting witness, Nat.nth takes its junk value.
• TauCeti.Nat.nth_eq_iff: the fibres of Nat.nth p.

theorem TauCeti.Nat.nth_eq_zero_of_forall_count_ne {p : ℕ → Prop} [DecidablePred p] {k : ℕ} (h : ∀ (n : ℕ), p n → Nat.count p n ≠ k) : Nat.nth p k = 0

Without a counting witness Nat.nth is junk. If no n satisfying p has exactly k predecessors satisfying p, then p holds at most k times, so Nat.nth p k is 0.

theorem TauCeti.Nat.nth_eq_iff {p : ℕ → Prop} [DecidablePred p] {k m : ℕ} : Nat.nth p k = m ↔ p m ∧ Nat.count p m = k ∨ m = 0 ∧ ∀ (n : ℕ), ¬(p n ∧ Nat.count p n = k)

The fibres of Nat.nth p. The value Nat.nth p k is m exactly when either m is the counting witness for k — it satisfies p and has exactly k predecessors satisfying p — or there is no counting witness at all and m is the junk value 0.