Supporting results for pointwise provable equality.

Bounded search and primitive recursion

codeBall decides a bounded universal statement by minimizing the first counterexample. The primitive-recursion constructor codePrec minimizes a Gödel-beta code of the whole computation history: codePrecPredicate states that a candidate history has the right initial entry and satisfies the step relation codePrecStep at every index below the argument, and codePrec reads the final entry out of the least such history.

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.codeBall {n : ℕ} (dφ : Nat.ArithPart₁.Code (n + 1)) (i : Fin n) : Nat.ArithPart₁.Code n

The characteristic value of ∀ j ≤ v i, dφ j, decided by minimizing the first index at which dφ fails or the bound is passed.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.precStepArgs {n : ℕ} : Fin (n + 2) → Nat.ArithPart₁.Code (n + 3)

The arguments at which the step function is applied inside a history: the history index, the entry recorded at that index, and the ambient arguments.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codePrecStep {n : ℕ} (dg : Nat.ArithPart₁.Code (n + 2)) : Nat.ArithPart₁.Code (n + 3)

The step relation between consecutive entries of a history.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeTailTail {n : ℕ} (df : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code (n + 2)

Reindex a code past the history and index arguments.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeTailTail df = df.comp fun (j : Fin n) => PointwiseComposition.Nat.ArithPart₁.Code.proj j.succ.succ

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codePrecPredicate {n : ℕ} (df : Nat.ArithPart₁.Code n) (dg : Nat.ArithPart₁.Code (n + 2)) : Nat.ArithPart₁.Code (n + 2)

A candidate history is correct: its initial entry is the base value, and every step below the argument agrees with the step function.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codePrec {n : ℕ} (df : Nat.ArithPart₁.Code n) (dg : Nat.ArithPart₁.Code (n + 2)) : Nat.ArithPart₁.Code (n + 1)

Primitive recursion with base df and step dg, read from the least correct history.

Equations

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

Standard computations over the natural numbers

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeBall {n : ℕ} {dφ : Nat.ArithPart₁.Code (n + 1)} {φ : List.Vector ℕ n → ℕ → ℕ} (hφ : Computes dφ fun (w : List.Vector ℕ (n + 1)) => φ w.tail w.head) (i : Fin n) : Computes (codeBall dφ i) fun (v : List.Vector ℕ n) => Nat.ball (v.get i) (φ v)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codePrecStep {n : ℕ} {dg : Nat.ArithPart₁.Code (n + 2)} {g : List.Vector ℕ (n + 2) → ℕ} (hg : Computes dg g) : Computes (codePrecStep dg) fun (w : List.Vector ℕ (n + 3)) => Nat.isEqNat (w.tail.head.beta (w.head + 1)) (g (w.head ::ᵥ w.tail.head.beta w.head ::ᵥ w.tail.tail.tail))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codePrecPredicate {n : ℕ} {df : Nat.ArithPart₁.Code n} {dg : Nat.ArithPart₁.Code (n + 2)} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} (hf : Computes df f) (hg : Computes dg g) : Computes (codePrecPredicate df dg) fun (w : List.Vector ℕ (n + 2)) => Nat.and (Nat.isEqNat (w.head.beta 0) (f w.tail.tail)) (Nat.ball w.tail.head fun (i : ℕ) => Nat.isEqNat (w.head.beta (i + 1)) (g (i ::ᵥ w.head.beta i ::ᵥ w.tail.tail)))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codePrec {n : ℕ} {df : Nat.ArithPart₁.Code n} {dg : Nat.ArithPart₁.Code (n + 2)} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} (hf : Computes df f) (hg : Computes dg g) : Computes (codePrec df dg) fun (v : List.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head