Supporting results for pointwise provable equality.

Arithmetic operations obtained by minimization

Truncated subtraction, integer square root, the two components of Cantor unpairing, divisibility, remainder, and the Gödel beta function, each defined by minimizing an arithmetic condition.

Each construction is accompanied by the theorem that it realizes the intended function over the natural numbers. Those Computes theorems are the input of the standard-model bridge, which turns a computation over ℕ into evaluation at standard numerals in an arbitrary model.

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeSub {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

Truncated subtraction d₀ - d₁: the least x with x + d₁ = d₀, or 0 when d₀ < d₁.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeSqrt {n : ℕ} (d : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The integer square root of d: the least x with x * x ≤ d < (x+1) * (x+1).

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeUnpair₁ {n : ℕ} (d : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The first component of Cantor unpairing.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeUnpair₂ {n : ℕ} (d : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The second component of Cantor unpairing.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeDvd {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The characteristic value of d₀ ∣ d₁, decided by minimizing a quotient bounded by d₁.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeRem {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The remainder of d₀ on division by d₁.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeBeta {n : ℕ} (dn di : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The Gödel beta function: the di-th entry of the sequence coded by dn.

Equations

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

Standard computations over the natural numbers

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeSub {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeSub d₀ d₁) fun (v : List.Vector ℕ n) => g₀ v - g₁ v

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeSqrt {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codeSqrt d) fun (v : List.Vector ℕ n) => (g v).sqrt

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeUnpair₁ {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codeUnpair₁ d) fun (v : List.Vector ℕ n) => (Nat.unpair (g v)).1

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeUnpair₂ {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codeUnpair₂ d) fun (v : List.Vector ℕ n) => (Nat.unpair (g v)).2

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeDvd {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeDvd d₀ d₁) fun (v : List.Vector ℕ n) => Nat.isDvdNat (g₀ v) (g₁ v)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeRem {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeRem d₀ d₁) fun (v : List.Vector ℕ n) => g₀ v % g₁ v

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeBeta {n : ℕ} {dn di : Nat.ArithPart₁.Code n} {gn gi : List.Vector ℕ n → ℕ} (hn : Computes dn gn) (hi : Computes di gi) : Computes (codeBeta dn di) fun (v : List.Vector ℕ n) => (gn v).beta (gi v)