Supporting results for pointwise provable equality.

An eager conditional and non-strict comparison

codeIfPos df dg dh is arithmetic, not lazy: it evaluates dg and dh both, and selects one of them by multiplying with the characteristic values codePos df and codeInv df. codeLe is the disjunction of strict order and equality.

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.codeIfPos {n : ℕ} (df dg dh : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

dg when df is positive and dh otherwise, selected arithmetically.

Both branches are evaluated; the construction is a sum of products, not a selected-branch semantics.

Equations

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

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

The characteristic value of d₀ ≤ d₁.

Equations

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

Standard computations over the natural numbers

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeIfPos {n : ℕ} {df dg dh : Nat.ArithPart₁.Code n} {f g h : List.Vector ℕ n → ℕ} (hf : Computes df f) (hg : Computes dg g) (hh : Computes dh h) : Computes (codeIfPos df dg dh) fun (v : List.Vector ℕ n) => if 0 < f v then g v else h v

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