Supporting results for pointwise provable equality.
Persistence of the repository's concrete evaluator at every standard program index. The induction is external on the natural-number index. The stage, input, and output range over an arbitrary model of PA, including its nonstandard elements. The constructor lemmas discharge every induction case.
theorem
PointwiseComposition.FailureOfComposition.ConcreteEvaluator.evalnCertificateFormula_natCode_persist
{M : Type u_1}
[FFL.ORingStructure M]
[M↓[ℒₒᵣ] ⊧* 𝐏𝐀]
[M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧]
(q : ℕ)
(s t u y : M)
:
Unconditional persistence for every standard Mathlib program index in every PA model. No persistence or arithmetization field is a hypothesis.