Labelled injury events for multi-oracle priority constructions

For an indexed family of finite-stage enumerations A : κ → ℕ → Finset ℕ and a target map target : ℕ → κ assigning the oracle monitored by requirement e, monitoredInjuryEvents A target r e : Set (κ × ℕ × ℕ) pairs target e with injuryEvents (A (target e)) r e. Retaining the label target e separates injuries across distinct oracles when combining events across priorities.

References

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

def TauCeti.Priority.monitoredInjuryEvents {κ : Type u_1} (A : κ → ℕ → Finset ℕ) (target : ℕ → κ) (r : ℕ → ℕ → Option ℕ) (e : ℕ) : Set (κ × ℕ × ℕ)

The labelled injury events (k, s, x) of requirement e, with k = target e and (s, x) ∈ injuryEvents (A (target e)) r e.

@[simp]

theorem TauCeti.Priority.mem_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {p : κ × ℕ × ℕ} : p ∈ monitoredInjuryEvents A target r e ↔ p.1 = target e ∧ p.2.2 ∈ injuriesAt (A (target e)) r e p.2.1

Membership in monitoredInjuryEvents.

theorem TauCeti.Priority.mk_mem_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {k : κ} {s x : ℕ} : (k, s, x) ∈ monitoredInjuryEvents A target r e ↔ k = target e ∧ x ∈ injuriesAt (A (target e)) r e s

Explicit triple membership in monitoredInjuryEvents.

theorem TauCeti.Priority.notMem_monitoredInjuryEvents_of_ne {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {k : κ} {s x : ℕ} (hk : k ≠ target e) : (k, s, x) ∉ monitoredInjuryEvents A target r e

Label separation. An event on k ≠ target e never belongs to monitoredInjuryEvents.

theorem TauCeti.Priority.disjoint_monitoredInjuryEvents_of_target_ne {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {A' : κ → ℕ → Finset ℕ} {target' : ℕ → κ} {r' : ℕ → ℕ → Option ℕ} {d : ℕ} (h : target d ≠ target' e) : Disjoint (monitoredInjuryEvents A target r d) (monitoredInjuryEvents A' target' r' e)

Requirements monitoring distinct oracle labels have disjoint labelled injury-event sets.

theorem TauCeti.Priority.monitoredInjuryEvents_congr_target {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {target' : ℕ → κ} (h : target e = target' e) : monitoredInjuryEvents A target r e = monitoredInjuryEvents A target' r e

Changing the target map away from e leaves monitoredInjuryEvents at e unchanged.

theorem TauCeti.Priority.monitoredInjuryEvents_eq_image {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : monitoredInjuryEvents A target r e = Prod.mk (target e) '' injuryEvents (A (target e)) r e

monitoredInjuryEvents A target r e is the target e-labelled image of injuryEvents.

@[simp]

theorem TauCeti.Priority.image_snd_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : Prod.snd '' monitoredInjuryEvents A target r e = injuryEvents (A (target e)) r e

Projecting away the oracle label recovers injuryEvents (A (target e)) r e.

theorem TauCeti.Priority.image_number_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : (fun (p : κ × ℕ × ℕ) => p.2.2) '' monitoredInjuryEvents A target r e = injurySet (A (target e)) r e

Projecting monitoredInjuryEvents to the injuring number recovers injurySet.

theorem TauCeti.Priority.image_stage_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : (fun (p : κ × ℕ × ℕ) => p.2.1 + 1) '' monitoredInjuryEvents A target r e = injuryStages (A (target e)) r e

Projecting monitoredInjuryEvents to the transition stage s + 1 recovers injuryStages.

@[simp]

theorem TauCeti.Priority.preimage_mk_monitoredInjuryEvents_self {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : Prod.mk (target e) ⁻¹' monitoredInjuryEvents A target r e = injuryEvents (A (target e)) r e

The fibre of monitoredInjuryEvents over target e is injuryEvents (A (target e)) r e.

theorem TauCeti.Priority.preimage_mk_monitoredInjuryEvents_of_ne {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {k : κ} (hk : k ≠ target e) : Prod.mk k ⁻¹' monitoredInjuryEvents A target r e = ∅

The fibre of monitoredInjuryEvents over any label k ≠ target e is empty.

theorem TauCeti.Priority.preimage_mk_biUnion_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} (k : κ) (N : ℕ) : Prod.mk k ⁻¹' ⋃ (e : ℕ), ⋃ (_ : e < N), monitoredInjuryEvents A target r e = ⋃ (e : ℕ), ⋃ (_ : e < N), ⋃ (_ : target e = k), injuryEvents (A k) r e

Restricting combined events of e < N to label k retains those e < N monitoring k.

theorem TauCeti.Priority.finite_monitoredInjuryEvents_iff_finite_injuryStages {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : (monitoredInjuryEvents A target r e).Finite ↔ (injuryStages (A (target e)) r e).Finite

Finiteness of monitoredInjuryEvents at e is equivalent to finiteness of injuryStages.

theorem TauCeti.Priority.finite_biUnion_monitoredInjuryEvents {κ : Type u_1} {A : κ → ℕ → Finset ℕ} {target : ℕ → κ} {r : ℕ → ℕ → Option ℕ} {N : ℕ} (h : ∀ e < N, (injuryStages (A (target e)) r e).Finite) : (⋃ (e : ℕ), ⋃ (_ : e < N), monitoredInjuryEvents A target r e).Finite

Combined labelled injury events on e < N are finite when each e < N has finite injuryStages.