Supporting results for pointwise provable equality.

Decoding a partial-recursive index

Mathlib's Nat.Partrec.Code encoding sends the four base constructors to 0–3 and encodes a compound code as 2 * (2 * payload + b₀) + b₁ + 4, where the two bits b₀ and b₁ name the constructor: 4 pairing, 5 composition, 6 primitive recursion, 7 minimization.

codePartrecTag recovers the constructor number and codePartrecPayload the payload, whose Cantor components codePartrecPayload₁ and codePartrecPayload₂ are the two subcodes of a binary constructor. The bit extraction needs parity and halving, which are defined here from remainder and primitive recursion.

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.

The numeric view

The functions the codes below realize. The constructor numbers are 0 zero, 1 succ, 2 left, 3 right, 4 pair, 5 comp, 6 prec, 7 rfind'. For q = r + 4 the payload is r.div2.div2; a binary constructor reads its Cantor components and minimization reads the payload itself.

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodeTag (q : ℕ) : ℕ

The constructor number of a partial-recursive index.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodeTag q = if q < 4 then q else have r := q - 4; 4 + 2 * r.bodd.toNat + r.div2.bodd.toNat

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload (q : ℕ) : ℕ

The payload of a compound partial-recursive index.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload q = (q - 4).div2.div2

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₁ (q : ℕ) : ℕ

The first subcode of a binary partial-recursive constructor.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₁ q = (Nat.unpair (PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload q)).1

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₂ (q : ℕ) : ℕ

The second subcode of a binary partial-recursive constructor.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₂ q = (Nat.unpair (PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload q)).2

The realizing codes

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

The parity bit of d.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeDiv2Unary : Nat.ArithPart₁.Code 1

Halving, as a unary code, by primitive recursion on the argument.

Equations

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

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

Halving of d, rounding down.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeDiv2 d = PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeDiv2Unary.comp ![d]

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

The constructor number of the partial-recursive index d: the index itself below 4, and otherwise 4 plus the two bits of d - 4.

Equations

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

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

The payload of a compound partial-recursive index.

Equations

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

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

The first subcode of a binary partial-recursive constructor.

Equations

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

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

The second subcode of a binary partial-recursive constructor.

Equations

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

Standard computations over the natural numbers

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeBodd {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (h : Computes d g) : Computes (codeBodd d) fun (v : List.Vector ℕ n) => (g v).bodd.toNat

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeDiv2Unary : Computes codeDiv2Unary fun (v : List.Vector ℕ 1) => v.head.div2