Supporting results for pointwise provable equality.

Evaluation existence for the partial-recursive index decoders

PartialRecursive defines the four codes that read a partial-recursive index: its constructor tag, its payload, and the two components of that payload. This file proves that each has a value in an arbitrary model of 𝐏𝐀, given a value for the index.

Nothing here decodes an index or asserts what the value is. For an arbitrary element of the model the constructions still terminate, and only that is proved; no witness is identified with a quotient, a remainder or a Cantor component of an external number.

The tag is an eager conditional, so both of its branches are evaluated before the test selects one: the index itself, and the compound tag built from the two parity bits of the shifted index.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePartrecPayload_exists_of_value {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (d : Nat.ArithPart₁.Code k) (q : M) (v : Fin k → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (q :> v)) (FFL.FirstOrder.Arithmetic.code d)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePartrecPayload d))

The payload of a partial-recursive index has a value at any value of the index: the shifted index is a truncated difference, and halving it twice has a value by eval_codeDiv2_exists_of_value.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePartrecPayload₁_exists_of_value {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (d : Nat.ArithPart₁.Code k) (q : M) (v : Fin k → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (q :> v)) (FFL.FirstOrder.Arithmetic.code d)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePartrecPayload₁ d))

The first payload component has a value at any value of the index.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePartrecPayload₂_exists_of_value {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (d : Nat.ArithPart₁.Code k) (q : M) (v : Fin k → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (q :> v)) (FFL.FirstOrder.Arithmetic.code d)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePartrecPayload₂ d))

The second payload component has a value at any value of the index.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codePartrecTag_exists_of_value {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {k : ℕ} (d : Nat.ArithPart₁.Code k) (q : M) (v : Fin k → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (q :> v)) (FFL.FirstOrder.Arithmetic.code d)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePartrecTag d))

The constructor tag of a partial-recursive index has a value at any value of the index.

codeIfPos is eager, so both branches are evaluated whatever the test does: the index itself, and the compound tag 4 + 2 * (r % 2) + (h % 2), where r is the shifted index and h is some value of its half. The comparison against 4 then selects one of the two.