Supporting results for pointwise provable equality.

The existential-stage graph of the repository's concrete evaluator.

Persistence of successful computations brings two possibly nonstandard stages to a common stage. It therefore supplies PA proofs of functionality and of the composition equation for the actual canonical composition indices.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.evaluator_persistence_provable (q : ℕ) : 𝐏𝐀 ⊢ ∀¹ ∀¹ ∀¹ ∀¹ ((“!!(FFL.FirstOrder.Semiterm.bvar 3) ≤ !!(FFL.FirstOrder.Semiterm.bvar 2)”) ⇒ₗ ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula/[FFL.FirstOrder.Semiterm.bvar 3, ↑q, FFL.FirstOrder.Semiterm.bvar 1, FFL.FirstOrder.Semiterm.bvar 0] ⇒ₗ ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula/[FFL.FirstOrder.Semiterm.bvar 2, ↑q, FFL.FirstOrder.Semiterm.bvar 1, FFL.FirstOrder.Semiterm.bvar 0])

PA proves persistence at each fixed standard index, with all stages, inputs, and outputs quantified inside the arithmetic sentence.

def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph (q : ℕ) : ProofSearch.Graph

The graph at a fixed standard program index, allowing any internal stage.

Equations

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

@[simp]

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_eval {M : Type u_1} [FFL.ORingStructure M] (q : ℕ) (v : Fin 2 → M) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(eventualGraph q) ↔ ∃ (s : M), (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral q, v 0, v 1]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_output_unique {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (q : ℕ) (x y z : M) (hy : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(eventualGraph q)) (hz : (FFL.FirstOrder.Semiformula.Evalb ![x, z]) ↑(eventualGraph q)) : y = z

Two successful computations of one standard index have the same output, even when their stages are nonstandard and different.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_functional (q : ℕ) : ProofSearch.Functional (eventualGraph q)

Functionality is proved in PA for this concrete evaluator graph.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_comp_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (fCode gCode : ℕ) (x z : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, z]) ↑(eventualGraph (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex fCode gCode)) ↔ ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(eventualGraph gCode) ∧ (FFL.FirstOrder.Semiformula.Evalb ![y, z]) ↑(eventualGraph fCode)

The composition equation holds in every PA model at all internal inputs and outputs; the two component computations need not start at the same stage.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_composition (fCode gCode : ℕ) : ProofSearch.Uniform 𝐏𝐀 (eventualGraph (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex fCode gCode)) (ProofSearch.comp (eventualGraph fCode) (eventualGraph gCode))

PA proves relational composition for the concrete program indices.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_identity : ProofSearch.Uniform 𝐏𝐀 (eventualGraph Kleene.identityIndex) ProofSearch.identity

The identity index already defined by Mathlib's program numbering realizes the equality graph in PA, at all internal inputs and outputs.

theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_empty : ProofSearch.Uniform 𝐏𝐀 (eventualGraph ConcreteEmptyGraph.concreteEmptyIndex) ProofSearch.empty

Minimization of successor supplies an explicitly encoded nowhere-defined program, whose empty graph equation is provable in PA.