Initialization stages and epoch-bounded attention counting

In a priority schedule action : ℕ → Option ℕ, an action of i < e at stage s initializes e at run index s + 1 ∈ initializationStages action e = ⋃ i < e, attentionStages action i. When e acts at most once per epoch between higher-priority actions, every action of e after its first is preceded by a distinct initialization stage, giving (attentionStages action e).ncard ≤ (initializationStages action e).ncard + 1 and the inductive 2 ^ e / 2 ^ e - 1 bounds.

References

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

def TauCeti.Priority.initializationStages (action : ℕ → Option ℕ) (e : ℕ) : Set ℕ

The run indices s + 1 at which some higher-priority i < e acted at stage s.

theorem TauCeti.Priority.mem_initializationStages {action : ℕ → Option ℕ} {e t : ℕ} : t ∈ initializationStages action e ↔ ∃ (s : ℕ) (i : ℕ), t = s + 1 ∧ action s = some i ∧ i < e

Membership in initializationStages.

@[simp]

theorem TauCeti.Priority.succ_mem_initializationStages {action : ℕ → Option ℕ} {e s : ℕ} : s + 1 ∈ initializationStages action e ↔ ∃ i < e, action s = some i

s + 1 is an initialization stage of e iff some i < e acts at stage s.

@[simp]

theorem TauCeti.Priority.zero_notMem_initializationStages {action : ℕ → Option ℕ} {e : ℕ} : 0 ∉ initializationStages action e

Stage 0 is never an initialization stage.

@[simp]

theorem TauCeti.Priority.initializationStages_zero (action : ℕ → Option ℕ) : initializationStages action 0 = ∅

Priority 0 has no higher-priority requirements and is never initialized.

theorem TauCeti.Priority.initializationStages_mono (action : ℕ → Option ℕ) : Monotone (initializationStages action)

A lower-priority requirement has at least the initialization stages of a higher-priority one.

theorem TauCeti.Priority.initializationStages_succ (action : ℕ → Option ℕ) (e : ℕ) : initializationStages action (e + 1) = initializationStages action e ∪ attentionStages action e

Stepping from priority e to e + 1 adds the attention stages of e.

theorem TauCeti.Priority.initializationStages_eq_biUnion (action : ℕ → Option ℕ) (e : ℕ) : initializationStages action e = ⋃ i ∈ Finset.range e, attentionStages action i

The initialization stages of e are the union of the attention stages of i < e.

theorem TauCeti.Priority.disjoint_initializationStages_attentionStages (action : ℕ → Option ℕ) (e : ℕ) : Disjoint (initializationStages action e) (attentionStages action e)

Initialization stages and attention stages of the same requirement are disjoint.

theorem TauCeti.Priority.finite_initializationStages_of_attention {action : ℕ → Option ℕ} {e : ℕ} (h : ∀ i < e, (attentionStages action i).Finite) : (initializationStages action e).Finite

If every i < e receives attention finitely often, e is initialized finitely often.

theorem TauCeti.Priority.ncard_initializationStages_eq_sum {action : ℕ → Option ℕ} {e : ℕ} (h : ∀ i < e, (attentionStages action i).Finite) : (initializationStages action e).ncard = ∑ i ∈ Finset.range e, (attentionStages action i).ncard

The number of initializations of e sums the attention counts of i < e.

theorem TauCeti.Priority.finite_attentionStages_and_ncard_le_succ_initializationStages {action : ℕ → Option ℕ} {e : ℕ} (hfin : (initializationStages action e).Finite) (hepoch : ∀ (s₁ s₂ : ℕ), s₁ < s₂ → action s₁ = some e → action s₂ = some e → ∃ (t : ℕ), s₁ < t ∧ t < s₂ ∧ ∃ i < e, action t = some i) : (attentionStages action e).Finite ∧ (attentionStages action e).ncard ≤ (initializationStages action e).ncard + 1

At most one action per epoch. If e is initialized finitely often and some i < e acts between any two actions of e, then e acts at most (initializationStages action e).ncard + 1 times.

theorem TauCeti.Priority.finite_attentionStages_and_ncard_le_two_pow {action : ℕ → Option ℕ} (hepoch : ∀ (e s₁ s₂ : ℕ), s₁ < s₂ → action s₁ = some e → action s₂ = some e → ∃ (t : ℕ), s₁ < t ∧ t < s₂ ∧ ∃ i < e, action t = some i) (e : ℕ) : (attentionStages action e).Finite ∧ (attentionStages action e).ncard ≤ 2 ^ e

Exponential attention bound. When every requirement acts at most once per epoch, priority e receives attention at most 2 ^ e times.

theorem TauCeti.Priority.finite_initializationStages_and_ncard_le {action : ℕ → Option ℕ} (hepoch : ∀ (e s₁ s₂ : ℕ), s₁ < s₂ → action s₁ = some e → action s₂ = some e → ∃ (t : ℕ), s₁ < t ∧ t < s₂ ∧ ∃ i < e, action t = some i) (e : ℕ) : (initializationStages action e).Finite ∧ (initializationStages action e).ncard ≤ 2 ^ e - 1

Initialization bound 2 ^ e - 1. When every requirement acts at most once per epoch, priority e is initialized at most 2 ^ e - 1 times.