Supporting results for pointwise provable equality.

Extending a Gödel beta code inside a model of Peano arithmetic

eval_codeBeta_of_values computes codeBeta at arbitrary elements of a model of 𝐈𝐎𝐩𝐞𝐧, but it says nothing about which value assignments are realized by some code. This file proves the one existence statement the recursion development needs: in a model of 𝐏𝐀, every beta code n and every index l admit a code n' that agrees with n at every index below l and takes a prescribed value at l.

The statement is given as a graph evaluation of codeBeta (Code.proj 0) (Code.proj 1) rather than as an equation between remainders. A value-level statement would mention %, π₁ and π₂, whose elaboration demands an 𝐈𝐎𝐩𝐞𝐧 instance that 𝐏𝐀 does not supply while the statement is being elaborated.

Pinned Foundation supplies internal finite sequences of nonstandard length, but no arbitrary-model Chinese remainder theorem and no beta encoder, so the supporting development is built here and kept private:

• a Bézout inverse, exists_mul_mod_eq_one, obtained from the least positive residue of a multiple of the argument;
• the internal factorial and the internal product of beta moduli, each defined by Foundation's 𝐈Σ₁ primitive recursion;
• coprimality of two beta moduli whose index difference divides the multiplier;
• simultaneous solution of the beta congruences prescribed by an internal sequence.

Nothing here uses Nat.beta, Computes or evaluation over standard ℕ.

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.exists_codeBeta_extension {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (n l x : M) : ∃ (n' : M), (∀ (i y : M), i < l → (FFL.FirstOrder.Semiformula.Evalb ![y, n, i]) (FFL.FirstOrder.Arithmetic.code (codeBeta (Nat.ArithPart₁.Code.proj 0) (Nat.ArithPart₁.Code.proj 1))) → (FFL.FirstOrder.Semiformula.Evalb ![y, n', i]) (FFL.FirstOrder.Arithmetic.code (codeBeta (Nat.ArithPart₁.Code.proj 0) (Nat.ArithPart₁.Code.proj 1)))) ∧ (FFL.FirstOrder.Semiformula.Evalb ![x, n', l]) (FFL.FirstOrder.Arithmetic.code (codeBeta (Nat.ArithPart₁.Code.proj 0) (Nat.ArithPart₁.Code.proj 1)))

Every Gödel beta code extends to one that keeps its values below an index and takes a prescribed value at that index.

The two evaluations are the graph of codeBeta (Code.proj 0) (Code.proj 1) at the assignments ![n, i] and ![n', i]; eval_codeBeta_of_values identifies that graph with the remainder the code computes.