Supporting results for pointwise provable equality.

The productiveness step in v36, for Mathlib's program numbering. The productivity function is the identity on program numbers.

def PointwiseComposition.FailureOfComposition.W (e n : ℕ) : Prop

The W construction in FailureOfComposition.

Equations

• PointwiseComposition.FailureOfComposition.W e n = ((Denumerable.ofNat Nat.Partrec.Code e).eval n).Dom

def PointwiseComposition.FailureOfComposition.diagonalHalts (n : ℕ) : Prop

The diagonal Halts construction in FailureOfComposition.

Equations

• PointwiseComposition.FailureOfComposition.diagonalHalts n = PointwiseComposition.FailureOfComposition.W n n

def PointwiseComposition.FailureOfComposition.Productive (A : ℕ → Prop) : Prop

The usual productive-set condition, including computability of the witness.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.diagonal_escape (d : ℕ) (h : ∀ (n : ℕ), W d n → ¬diagonalHalts n) : ¬diagonalHalts d ∧ ¬W d d

theorem PointwiseComposition.FailureOfComposition.complement_diagonal_productive : Productive fun (n : ℕ) => ¬diagonalHalts n

theorem PointwiseComposition.FailureOfComposition.exists_domain_index {D : ℕ → Prop} (hD : REPred D) : ∃ (d : ℕ), ∀ (n : ℕ), W d n ↔ D n

A domain presentation of an r.e. predicate, with the numbering made explicit.

theorem PointwiseComposition.FailureOfComposition.productive_escape_re {D : ℕ → Prop} (hD : REPred D) (hSound : ∀ (n : ℕ), D n → ¬diagonalHalts n) : ∃ (d : ℕ), ¬diagonalHalts d ∧ ¬D d

The diagonal index itself escapes any r.e. subset of the divergent diagonal.