Use-prefix breaches and boundary injuries

A successful oracle computation with use u reads only the oracle below u, while a restraint some b protects the numbers up to b inclusive. A restraint equal to the use thus protects one more number than the computation reads. This file separates the two conditions.

The use-prefix restraint usePrefixRestraint r protects exactly the numbers strictly below the active restraint of r: it is some c where r is some (c + 1), and inactive where r is inactive or some 0. The use-prefix breaches of requirement e are the injuries for this restraint, so the use-prefix breach batch, events, number set and stages are

• injuriesAt A (usePrefixRestraint r) e s, the fresh entries strictly below the active restraint (mem_injuriesAt_usePrefixRestraint),
• injuryEvents A (usePrefixRestraint r) e,
• injurySet A (usePrefixRestraint r) e,
• injuryStages A (usePrefixRestraint r) e,

and every result about injury objects, such as their projections and the finiteness criteria under monotone stages, applies to them verbatim. The boundary injuries boundaryInjuriesAt A r e s are the fresh entries equal to the active restraint. An injury batch is the disjoint union of its use-prefix breaches and its boundary injuries.

Finitely many injuring numbers give finitely many use-prefix breaching numbers. The converse fails: with stages [0, s) and restraint some s at stage s, every number is a boundary injury while nothing breaches the use prefix. Control of the restraint itself does give finite injury (TauCeti.Priority.finite_injurySet_of_eventually_bounded).

Main definitions

• TauCeti.Priority.usePrefixRestraint: the restraint protecting the numbers strictly below the active restraint.
• TauCeti.Priority.boundaryInjuriesAt: the fresh entries equal to the active restraint.

Main results

• TauCeti.Priority.injuriesAt_usePrefixRestraint_union_boundaryInjuriesAt, TauCeti.Priority.disjoint_injuriesAt_usePrefixRestraint_boundaryInjuriesAt: an injury batch is the disjoint union of its use-prefix breaches and its boundary injuries.
• TauCeti.Priority.finite_injurySet_usePrefixRestraint_of_finite_injurySet: finitely many injuring numbers give finitely many use-prefix breaching numbers.

References

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

The use-prefix restraint

def TauCeti.Priority.usePrefixRestraint (r : ℕ → ℕ → Option ℕ) (e s : ℕ) : Option ℕ

The restraint protecting exactly the numbers strictly below the active restraint of r: some c where r e s = some (c + 1), and inactive where r e s is none or some 0.

@[simp]

theorem TauCeti.Priority.usePrefixRestraint_eq_some_iff {r : ℕ → ℕ → Option ℕ} {e s c : ℕ} : usePrefixRestraint r e s = some c ↔ r e s = some (c + 1)

The use-prefix restraint is some c exactly where the restraint is some (c + 1).

@[simp]

theorem TauCeti.Priority.usePrefixRestraint_eq_none_iff {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : usePrefixRestraint r e s = none ↔ r e s = none ∨ r e s = some 0

The use-prefix restraint is inactive exactly where the restraint is inactive or some 0.

@[simp]

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

Membership in a use-prefix breach batch: a fresh entry strictly below the active restraint.

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

If nothing breaches the use prefix of e in the transition to stage s + 1, no number strictly below the active restraint enters in that transition.

theorem TauCeti.Priority.injuriesAt_usePrefixRestraint_subset {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : injuriesAt A (usePrefixRestraint r) e s ⊆ injuriesAt A r e s

Every use-prefix breach is an injury.

theorem TauCeti.Priority.injuryEvents_usePrefixRestraint_subset {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : injuryEvents A (usePrefixRestraint r) e ⊆ injuryEvents A r e

Every use-prefix breach event is an injury event.

theorem TauCeti.Priority.injurySet_usePrefixRestraint_subset {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : injurySet A (usePrefixRestraint r) e ⊆ injurySet A r e

Every use-prefix breaching number is an injuring number.

theorem TauCeti.Priority.injuryStages_usePrefixRestraint_subset {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} : injuryStages A (usePrefixRestraint r) e ⊆ injuryStages A r e

Every use-prefix breach stage is an injury stage.

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

Finite injury bounds the use-prefix breaches: finitely many injuring numbers give finitely many use-prefix breaching numbers. The converse fails without control of the restraint.

Boundary injuries

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

The boundary injuries of requirement e in the transition to stage s + 1: the fresh entries equal to the active restraint. Such an entry injures e but lies outside the use prefix.

@[simp]

theorem TauCeti.Priority.mem_boundaryInjuriesAt {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s x : ℕ} : x ∈ boundaryInjuriesAt A r e s ↔ x ∈ A (s + 1) ∧ x ∉ A s ∧ r e s = some x

Membership in a boundary injury batch: a fresh entry equal to the active restraint.

theorem TauCeti.Priority.boundaryInjuriesAt_subset_injuriesAt {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : boundaryInjuriesAt A r e s ⊆ injuriesAt A r e s

Every boundary injury is an injury.

theorem TauCeti.Priority.injuriesAt_usePrefixRestraint_union_boundaryInjuriesAt {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : injuriesAt A (usePrefixRestraint r) e s ∪ boundaryInjuriesAt A r e s = injuriesAt A r e s

An injury batch splits into its use-prefix breaches and its boundary injuries.

theorem TauCeti.Priority.disjoint_injuriesAt_usePrefixRestraint_boundaryInjuriesAt {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s : ℕ} : Disjoint (injuriesAt A (usePrefixRestraint r) e s) (boundaryInjuriesAt A r e s)

Use-prefix breaches and boundary injuries are disjoint.