Counting the causes of injury

An injury budget counts distinct numbers, rather than actions or stages. If every actual injuring entry is supplied by a higher-priority contributor, and contributor i supplies at most b i distinct numbers, the total injury budget is at most the sum of these bounds. In particular, contributors supplying at most one number each give a budget of e for requirement e.

The contribution sets may overlap and the stages may enumerate several numbers at once. Neither theorem assumes monotone stages: repeated entry of the same number does not enlarge the injury-number set. Monotonicity is needed separately to bound injury stages or obtain an injury-free tail, using the results of TauCeti.Computability.Priority.Injury.Basic.

The covering hypothesis concerns every entry in injuriesAt, so a contribution ledger alone does not establish the bound. Each conclusion includes finiteness, since Set.ncard by itself does not distinguish an infinite set from an empty one.

References

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

theorem TauCeti.Priority.finite_injurySet_and_ncard_le_sum_of_causes {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (C : ℕ → Set ℕ) (b : ℕ → ℕ) (hbudget : ∀ i < e, (C i).Finite ∧ (C i).ncard ≤ b i) (hcover : ∀ (s x : ℕ), x ∈ injuriesAt A r e s → ∃ i < e, x ∈ C i) : (injurySet A r e).Finite ∧ (injurySet A r e).ncard ≤ ∑ i ∈ Finset.range e, b i

Distinct numbers injuring e are bounded by the sum of the higher-priority contribution budgets. The hypothesis hcover accounts for actual injuring entries, not just a ledger of possible contributions. Neither disjoint contributions nor monotone stages are required.

theorem TauCeti.Priority.finite_injurySet_and_ncard_le_of_subsingleton_causes {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} (C : ℕ → Set ℕ) (hunique : ∀ i < e, (C i).Subsingleton) (hcover : ∀ (s x : ℕ), x ∈ injuriesAt A r e s → ∃ i < e, x ∈ C i) : (injurySet A r e).Finite ∧ (injurySet A r e).ncard ≤ e

If every higher-priority contributor supplies at most one distinct number, there are at most e distinct numbers injuring e. Empty contribution sets are allowed. This counts numbers even when they enter together or the same number enters repeatedly.