Supporting results for pointwise provable equality.

PA-model equations for the four base program indices of the repository's arithmetized Mathlib evaluator. These equations quantify over all elements of an arbitrary PA model, including the fuel and input; they are not merely standard-natural-number equations.

theorem PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.eval_base_tag {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (d : Nat.ArithPart₁.Code r) (q : ℕ) (hq : q < 4) (v : Fin r → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (↑q :> v)) (FFL.FirstOrder.Arithmetic.code d)) : (FFL.FirstOrder.Semiformula.Evalb (↑q :> v)) (FFL.FirstOrder.Arithmetic.code (CategoricalRiceShapiro.ArithmeticCode.codePartrecTag d))

The tag decoder agrees with the index below four in every PA model.

noncomputable def PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.baseOutput {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (u : M) : M

Output of the four base programs, interpreted in an arbitrary PA model.

Equations

• PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.baseOutput q u = if q = 0 then 0 else if q = 1 then u + 1 else if q = 2 then π₁ u else π₂ u

theorem PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.base_computation_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : q < 4) (s u y : M) : (FFL.FirstOrder.Semiformula.Evalb ![s, ↑q, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ↔ u < s ∧ y = baseOutput q u

Exact graph equation for every base program and arbitrary model arguments.

theorem PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.evalnCertificateFormula_natCode_persist_of_lt_four {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : q < 4) (s t u y : M) (hst : s ≤ t) (h : (FFL.FirstOrder.Semiformula.Evalb ![s, ↑q, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula) : (FFL.FirstOrder.Semiformula.Evalb ![t, ↑q, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula

Persistence for constructor numbers zero through three needs no induction.

theorem PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.base_unbounded_computation_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : q < 4) (u y : M) : (∃ (s : M), (FFL.FirstOrder.Semiformula.Evalb ![s, ↑q, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula) ↔ y = baseOutput q u

Removing fuel yields the exact total graph for each base program.

theorem PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.identityIndex_eq : Kleene.identityIndex = 48

Mathlib's existing identity program has index 48 in its fixed numbering.

theorem PointwiseComposition.FailureOfComposition.ConcreteWitnessGraphs.identity_computation {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (s u : M) (hus : u < s) : (FFL.FirstOrder.Semiformula.Evalb ![s, ↑Kleene.identityIndex, u, u]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula

The concrete identity program computes at every fuel exceeding its input.