Injury bookkeeping for finite-stage enumerations

A finite-injury construction enumerates a set in finite stages A s, and a requirement e protects, at each stage s, either nothing (r e s = none) or the numbers up to a restraint b (r e s = some b, an inclusive bound). A number injures e in the transition to stage s + 1 when it enters at that transition and lies at or below the active restraint.

• injuriesAt A r e s: the finite batch of numbers injuring e in that transition.
• injuryEvents A r e: the pairs (s, x) with x ∈ injuriesAt A r e s.
• injurySet A r e: the numbers that ever injure e, Soare's I_e.
• injuryStages A r e: the stages s + 1 at which some number injures e.

Finitely many injury stages are the same as an eventually injury-free tail, and give finitely many injuring numbers. When the stages are monotone, a number enters at most once (TauCeti.Enumeration.unique_entry_stage), so it injures e at most once. Then finitely many injuring numbers are equivalent to both, and there are at most as many injury stages as injuring numbers. Several numbers may injure e at one stage, so the inequality can be strict. Without monotonicity a single number can leave and re-enter, injuring e at infinitely many stages.

A restraint protecting fewer numbers at every stage has fewer injuries, and inclusions of the batches pass to the events, numbers and stages. Control of the restraint itself gives finite injury: a restraint that is eventually bounded admits only finitely many injuring numbers, with no monotonicity of the stages and no bound on its earlier values. Under monotone stages this yields an injury-free tail.

Injury concerns entries into a protected interval only. Resetting the records of lower-priority requirements, effectiveness of the injury sets, preservation of computations and satisfaction of requirements are separate matters, not treated here.

Main results

• TauCeti.Priority.mem_injuriesAt, TauCeti.Priority.injuriesAt_eq_empty_of_eq_none: membership in an injury batch; no restraint, no injury.
• TauCeti.Priority.mem_iff_mem_succ_of_injuriesAt_eq_empty: without injury, a monotone transition changes no membership at or below the restraint.
• TauCeti.Priority.injurySet_eq_image, TauCeti.Priority.injuryStages_eq_image: numbers and stages are the projections of the events.
• TauCeti.Priority.injuriesAt_mono, TauCeti.Priority.injuryEvents_mono, TauCeti.Priority.injurySet_mono, TauCeti.Priority.injuryStages_mono: a smaller restraint has fewer injuries.
• TauCeti.Priority.injOn_snd_injuryEvents: under monotone stages a number injures at most once.
• TauCeti.Priority.finite_injuryStages_iff_eventually_eq_empty: finitely many injury stages are an eventually injury-free tail, with no monotonicity.
• TauCeti.Priority.finite_injurySet_iff_finite_injuryStages, TauCeti.Priority.finite_injurySet_iff_eventually_eq_empty: under monotone stages, finitely many injuring numbers are equivalent to both.
• TauCeti.Priority.ncard_injuryStages_le: under monotone stages, there are at most as many injury stages as injuring numbers (as ncards, which are both 0 in the infinite case).
• TauCeti.Priority.finite_injurySet_of_eventually_bounded: an eventually bounded restraint admits only finitely many injuring numbers.
• TauCeti.Priority.exists_forall_injuriesAt_eq_empty_of_eventually_bounded: under monotone stages, an eventually bounded restraint gives an injury-free tail.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter VII.1.

def TauCeti.Priority.injuriesAt (A : ℕ → Finset ℕ) (r : ℕ → ℕ → Option ℕ) (e s : ℕ) : Finset ℕ

The numbers injuring requirement e in the transition to stage s + 1: the fresh entries at or below the active restraint.

def TauCeti.Priority.injuryEvents (A : ℕ → Finset ℕ) (r : ℕ → ℕ → Option ℕ) (e : ℕ) : Set (ℕ × ℕ)

The injury events of requirement e: the pairs (s, x) with x injuring e in the transition to stage s + 1.

def TauCeti.Priority.injurySet (A : ℕ → Finset ℕ) (r : ℕ → ℕ → Option ℕ) (e : ℕ) : Set ℕ

The numbers that ever injure requirement e, Soare's I_e.

def TauCeti.Priority.injuryStages (A : ℕ → Finset ℕ) (r : ℕ → ℕ → Option ℕ) (e : ℕ) : Set ℕ

The stages s + 1 at which some number injures requirement e.

@[simp]

theorem TauCeti.Priority.mem_injuriesAt {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s x : ℕ} : x ∈ injuriesAt A r e s ↔ x ∈ A (s + 1) ∧ x ∉ A s ∧ ∃ (b : ℕ), r e s = some b ∧ x ≤ b

Membership in an injury batch: a fresh entry at or below the active restraint.

theorem TauCeti.Priority.injuriesAt_subset_fresh {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : injuriesAt A r e s ⊆ Enumeration.fresh A s

Every injury is a fresh entry.

theorem TauCeti.Priority.injuriesAt_eq_empty_of_eq_none {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} (h : r e s = none) : injuriesAt A r e s = ∅

With no active restraint there is no injury.

theorem TauCeti.Priority.mem_iff_mem_succ_of_injuriesAt_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s b x : ℕ} (hA : A s ⊆ A (s + 1)) (hr : r e s = some b) (hI : injuriesAt A r e s = ∅) (hx : x ≤ b) : x ∈ A s ↔ x ∈ A (s + 1)

No injury, no change below the restraint. If nothing injures e, with active restraint b, in the transition to stage s + 1, and A s ⊆ A (s + 1), then A s and A (s + 1) have the same members at and below b.

theorem TauCeti.Priority.notMem_fresh_of_injuriesAt_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s b x : ℕ} (h : injuriesAt A r e s = ∅) (hb : r e s = some b) (hx : x ≤ b) : x ∉ Enumeration.fresh A s

If nothing injures e in the transition to stage s + 1, no number at or below the active restraint enters in that transition.

theorem TauCeti.Priority.injuriesAt_nonempty_iff {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : (injuriesAt A r e s).Nonempty ↔ ∃ x < (r e s).elim 0 fun (x : ℕ) => x + 1, x ∈ injuriesAt A r e s

A batch is nonempty exactly when it contains a number below the restraint bound, which is b + 1 for an active restraint some b and 0 for no restraint.

@[simp]

theorem TauCeti.Priority.mem_injuryEvents {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {p : ℕ × ℕ} : p ∈ injuryEvents A r e ↔ p.2 ∈ injuriesAt A r e p.1

Membership in the injury events.

@[simp]

theorem TauCeti.Priority.mem_injurySet {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e x : ℕ} : x ∈ injurySet A r e ↔ ∃ (s : ℕ), x ∈ injuriesAt A r e s

Membership in the injury set.

theorem TauCeti.Priority.mem_injuryStages {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e t : ℕ} : t ∈ injuryStages A r e ↔ ∃ (s : ℕ), t = s + 1 ∧ (injuriesAt A r e s).Nonempty

Membership in the injury stages.

@[simp]

theorem TauCeti.Priority.succ_mem_injuryStages {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : s + 1 ∈ injuryStages A r e ↔ (injuriesAt A r e s).Nonempty

s + 1 is an injury stage exactly when the batch of the transition to it is nonempty.

@[simp]

theorem TauCeti.Priority.zero_notMem_injuryStages {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : 0 ∉ injuryStages A r e

Stage 0 is never an injury stage.

theorem TauCeti.Priority.injurySet_eq_image {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : injurySet A r e = Prod.snd '' injuryEvents A r e

The injury set is the projection of the events to their numbers.

theorem TauCeti.Priority.injuryStages_eq_image {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : injuryStages A r e = (fun (p : ℕ × ℕ) => p.1 + 1) '' injuryEvents A r e

The injury stages are the projection of the events to their stages.

Comparing restraints

theorem TauCeti.Priority.injuriesAt_mono {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {r' : ℕ → ℕ → Option ℕ} {s : ℕ} (h : ∀ (c : ℕ), r' e s = some c → ∃ (b : ℕ), r e s = some b ∧ c ≤ b) : injuriesAt A r' e s ⊆ injuriesAt A r e s

A smaller restraint has fewer injuries: if every active restraint c of r' at stage s is matched by an active restraint of r at least c, every injury for r' is one for r.

theorem TauCeti.Priority.injuryEvents_mono {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {r' : ℕ → ℕ → Option ℕ} (h : ∀ (s : ℕ), injuriesAt A r' e s ⊆ injuriesAt A r e s) : injuryEvents A r' e ⊆ injuryEvents A r e

Stagewise inclusions of injury batches give an inclusion of injury events.

theorem TauCeti.Priority.injurySet_mono {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {r' : ℕ → ℕ → Option ℕ} (h : ∀ (s : ℕ), injuriesAt A r' e s ⊆ injuriesAt A r e s) : injurySet A r' e ⊆ injurySet A r e

Stagewise inclusions of injury batches give an inclusion of injury sets.

theorem TauCeti.Priority.injuryStages_mono {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {r' : ℕ → ℕ → Option ℕ} (h : ∀ (s : ℕ), injuriesAt A r' e s ⊆ injuriesAt A r e s) : injuryStages A r' e ⊆ injuryStages A r e

Stagewise inclusions of injury batches give an inclusion of injury stages.

Finiteness and monotone stages

theorem TauCeti.Priority.injOn_snd_injuryEvents {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (hA : Monotone A) : Set.InjOn Prod.snd (injuryEvents A r e)

Under monotone stages a number injures at most once: it enters the enumeration at most once.

theorem TauCeti.Priority.finite_injurySet_of_finite_injuryStages {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (h : (injuryStages A r e).Finite) : (injurySet A r e).Finite

Finitely many injury stages give finitely many injuring numbers, with no monotonicity.

theorem TauCeti.Priority.finite_injurySet_iff_finite_injuryStages {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (hA : Monotone A) : (injurySet A r e).Finite ↔ (injuryStages A r e).Finite

Finite injury numbers and finite injury stages agree under monotone stages.

theorem TauCeti.Priority.finite_injuryStages_iff_eventually_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : (injuryStages A r e).Finite ↔ ∃ (s₀ : ℕ), ∀ (s : ℕ), s₀ ≤ s → injuriesAt A r e s = ∅

Finitely many injury stages are an eventually injury-free tail, with no monotonicity.

theorem TauCeti.Priority.finite_injurySet_iff_eventually_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (hA : Monotone A) : (injurySet A r e).Finite ↔ ∃ (s₀ : ℕ), ∀ (s : ℕ), s₀ ≤ s → injuriesAt A r e s = ∅

Finitely many injuring numbers are an eventually injury-free tail, under monotone stages.

theorem TauCeti.Priority.finite_injurySet_of_eventually_bounded {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s₀ R : ℕ} (h : ∀ (s : ℕ), s₀ ≤ s → ∀ (b : ℕ), r e s = some b → b ≤ R) : (injurySet A r e).Finite

An eventually bounded restraint gives finite injury. If from stage s₀ on every active restraint of e is at most R, only finitely many numbers ever injure e. Neither monotone stages nor a bound on the restraint before s₀ is needed.

theorem TauCeti.Priority.exists_forall_injuriesAt_eq_empty_of_eventually_bounded {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (hA : Monotone A) {s₀ R : ℕ} (h : ∀ (s : ℕ), s₀ ≤ s → ∀ (b : ℕ), r e s = some b → b ≤ R) : ∃ (s₁ : ℕ), ∀ (s : ℕ), s₁ ≤ s → injuriesAt A r e s = ∅

Injury-free tail. Under monotone stages, an eventually bounded restraint is eventually never injured.

theorem TauCeti.Priority.ncard_injuryStages_le {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (hA : Monotone A) : (injuryStages A r e).ncard ≤ (injurySet A r e).ncard

At most as many injury stages as injuring numbers, when the stages are monotone. Several numbers may injure at one stage, so the inequality can be strict. When there are infinitely many injuring numbers there are infinitely many stages, and both cardinalities are 0.